THEOREM
*******
Here, given some of the common
rules of basic arithmetic (line 1-14) and the standard definitions of the even
numbers (lines 15-17) and odd numbers (line 19-20) we formally prove that, for all
even numbers, the next number will be an odd number.
ALL(a):[a e n => [a e even => a+1 e odd ]] where n = the set of natural numbers
COROLLARY
*********
ALL(a):[a e n => 2*a e even & 2*a+1 e odd ]
By Dan Christensen
2023-02-16
PROOF
*****
Basic Rules of Arithmetic Required (derivable
from Peano's Axioms)
Define: 0, 1, 2
1 0 e n
Axiom
2 1 e n
Axiom
3 ~1=0
Axiom
4 2 e n
Axiom
5 ~2=0
Axiom
From Definition of + (addition)
6 ALL(a):ALL(b):[a e n & b e n => a+b e n]
Axiom
Properties of +
7 ALL(a):ALL(b):[a e n & b e n => a+b=b+a]
Axiom
From Definition of * (multiplication)
8 ALL(a):ALL(b):[a e n & b e n => a*b e n]
Axiom
9 ~EXIST(a):[a e n & 2*a=1]
Axiom
From Definition of -
(subtraction)
10 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => [a=c+b => a-b=c]]
Axiom
11 ALL(a):ALL(b):[a e n & b e n => [b<a => a-b e n]]
Axiom
Define: <
12 ALL(a):ALL(b):[a e n & b e n => [a<b <=> EXIST(c):[c e n & ~c=0 & a+c=b]]]
Axiom
Properties of <
13 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n & ~a=0 =>
[a*b<a*c => b<c]]
Axiom
14 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => [c<b
=> a*(b-c)=a*b-a*c]]
Axiom
Define: even (Formal proof of existence here)
15 Set(even)
Axiom
even is a subset
of n
16 ALL(a):[a e even => a e n]
Axiom
17 ALL(a):[a e n => [a e even <=> EXIST(b):[b e n & a=2*b]]]
Axiom
Define: odd
18 Set(odd)
Axiom
odd is a subset
of n
19 ALL(a):[a e odd => a e n]
Axiom
20 ALL(a):[a e n => [a e odd <=> ~a e even]]
Axiom
LEMMA
Prove: ALL(a):[a e n => ~EXIST(b):[b e n &
2*a+1=2*b]]
Suppose...
21 x e n
Premise
Prove: ~EXIST(b):[b e n & 2*x+1=2*b]
Suppose to the contrary...
22 y e n & 2*x+1=2*y
Premise
23 y e n
Split, 22
24 2*x+1=2*y
Split, 22
Prove: 2*y=2*x+1 by commutativity
Apply definition of *
25 ALL(b):[2 e n & b e n => 2*b e n]
U Spec, 8
26 2 e n & x e n => 2*x e n
U Spec, 25
27 2 e n & x e n
Join, 4, 21
28 2*x e n
Detach, 26, 27
29 2 e n & y e n => 2*y e n
U Spec, 25
30 2 e n & y e n
Join, 4, 23
31 2*y e n
Detach, 29, 30
32 ALL(b):ALL(c):[2*y e n & b e n & c e n => [2*y=c+b => 2*y-b=c]]
U Spec, 10, 31
33 ALL(c):[2*y e n & 2*x e n & c e n => [2*y=c+2*x => 2*y-2*x=c]]
U Spec, 32, 28
34 2*y e n & 2*x e n & 1 e n => [2*y=1+2*x => 2*y-2*x=1]
U Spec, 33
35 2*y e n & 2*x e n
Join, 31, 28
36 2*y e n & 2*x e n & 1 e n
Join, 35, 2
37 2*y=1+2*x => 2*y-2*x=1
Detach, 34, 36
As Required:
38 2*y=2*x+1
Sym, 24
Apply commutativity of +
39 ALL(b):[2*x e n & b e n => 2*x+b=b+2*x]
U Spec, 7, 28
40 2*x e n & 1 e n => 2*x+1=1+2*x
U Spec, 39
41 2*x e n & 1 e n
Join, 28, 2
42 2*x+1=1+2*x
Detach, 40, 41
As Required:
43 2*y=1+2*x
Substitute, 42,
38
44 2*y-2*x=1
Detach, 37, 43
Apply property of <
45 ALL(b):ALL(c):[2 e n & b e n & c e n => [c<b
=> 2*(b-c)=2*b-2*c]]
U Spec, 14
46 ALL(c):[2 e n & y e n & c e n => [c<y => 2*(y-c)=2*y-2*c]]
U Spec, 45
47 2 e n & y e n & x e n => [x<y => 2*(y-x)=2*y-2*x]
U Spec, 46
48 2 e n & y e n
Join, 4, 23
49 2 e n & y e n & x e n
Join, 48, 21
50 x<y => 2*(y-x)=2*y-2*x
Detach, 47, 49
Prove: x<y
Apply definition of <
51 ALL(b):[2*x e n & b e n => [2*x<b <=> EXIST(c):[c e n & ~c=0 & 2*x+c=b]]]
U Spec, 12, 28
52 2*x e n & 2*y e n => [2*x<2*y <=>
EXIST(c):[c e n & ~c=0 & 2*x+c=2*y]]
U Spec, 51, 31
53 2*x e n & 2*y e n
Join, 28, 31
54 2*x<2*y <=> EXIST(c):[c e n & ~c=0 & 2*x+c=2*y]
Detach, 52, 53
55 [2*x<2*y => EXIST(c):[c e n & ~c=0 & 2*x+c=2*y]]
&
[EXIST(c):[c e n & ~c=0 & 2*x+c=2*y] => 2*x<2*y]
Iff-And, 54
56 EXIST(c):[c e n & ~c=0 & 2*x+c=2*y] => 2*x<2*y
Split, 55
57 1 e n & ~1=0
Join, 2, 3
58 1 e n & ~1=0 & 2*x+1=2*y
Join, 57, 24
59 EXIST(c):[c e n & ~c=0 & 2*x+c=2*y]
E Gen, 58
60 2*x<2*y
Detach, 56, 59
Apply property of <
61 ALL(b):ALL(c):[2 e n & b e n & c e n & ~2=0 => [2*b<2*c =>
b<c]]
U Spec, 13
62 ALL(c):[2 e n & x e n & c e n & ~2=0 => [2*x<2*c => x<c]]
U Spec, 61
63 2 e n & x e n & y e n & ~2=0 => [2*x<2*y => x<y]
U Spec, 62
64 2 e n & x e n
Join, 4, 21
65 2 e n & x e n & y e n
Join, 64, 23
66 2 e n & x e n & y e n & ~2=0
Join, 65, 5
67 2*x<2*y => x<y
Detach, 63, 66
As Required:
68 x<y
Detach, 67, 60
69 2*(y-x)=2*y-2*x
Detach, 50, 68
70 2*(y-x)=1
Substitute, 69,
44
Apply property of -
71 ALL(b):[y e n & b e n => [b<y => y-b e n]]
U Spec, 11
72 y e n & x e n => [x<y => y-x e n]
U Spec, 71
73 y e n & x e n
Join, 23, 21
74 x<y => y-x e n
Detach, 72, 73
75 y-x e n
Detach, 74, 68
76 y-x e n & 2*(y-x)=1
Join, 75, 70
77 EXIST(a):[a e n & 2*a=1]
E Gen, 76
78 EXIST(a):[a e n & 2*a=1]
&
~EXIST(a):[a e n & 2*a=1]
Join, 77, 9
As Required:
79 ~EXIST(b):[b e n & 2*x+1=2*b]
4 Conclusion, 22
LEMMA
*****
80 ALL(a):[a e n =>
~EXIST(b):[b e n & 2*a+1=2*b]]
4 Conclusion, 21
Prove: ALL(a):[a e n => [a e even => a+1 e odd]]
Suppose...
81 x e n
Premise
Prove: x e even =>
x+1 e odd
Suppose...
82 x e even
Premise
83 x e n => [x e even <=> EXIST(b):[b e n & x=2*b]]
U Spec, 17
84 x e even <=> EXIST(b):[b e n & x=2*b]
Detach, 83, 81
85 [x e even => EXIST(b):[b e n & x=2*b]]
&
[EXIST(b):[b e n & x=2*b] => x e even]
Iff-And, 84
86 x e even => EXIST(b):[b e n & x=2*b]
Split, 85
87 EXIST(b):[b e n & x=2*b]
Detach, 86, 82
88 y e n & x=2*y
E Spec, 87
89 y e n
Split, 88
90 x=2*y
Split, 88
91 ALL(b):[x e n & b e n => x+b e n]
U Spec, 6
92 x e n & 1 e n => x+1 e n
U Spec, 91
93 x e n & 1 e n
Join, 81, 2
94 x+1 e n
Detach, 92, 93
95 x+1 e n => [x+1 e odd <=> ~x+1 e even]
U Spec, 20, 94
96 x+1 e odd <=> ~x+1 e even
Detach, 95, 94
97 [x+1 e odd => ~x+1 e even] & [~x+1 e even => x+1 e odd]
Iff-And, 96
Sufficient: For x+1 e odd
98 ~x+1 e even => x+1 e odd
Split, 97
Prove: ~x+1 e even
Suppose to the contrary...
99 x+1 e even
Premise
100 x+1 e n => [x+1 e even <=> EXIST(b):[b e n & x+1=2*b]]
U Spec, 17, 99
101 x+1 e even <=> EXIST(b):[b e n & x+1=2*b]
Detach, 100, 94
102 [x+1 e even => EXIST(b):[b e n & x+1=2*b]]
&
[EXIST(b):[b e n & x+1=2*b] => x+1 e even]
Iff-And, 101
103 x+1 e even => EXIST(b):[b e n & x+1=2*b]
Split, 102
104 EXIST(b):[b e n & x+1=2*b]
Detach, 103, 99
Apply lemma
105 y e n => ~EXIST(b):[b e n & 2*y+1=2*b]
U Spec, 80
106 ~EXIST(b):[b e n & 2*y+1=2*b]
Detach, 105, 89
107 EXIST(b):[b e n & 2*y+1=2*b]
Substitute, 90,
104
108 ~EXIST(b):[b e n & 2*y+1=2*b]
&
EXIST(b):[b e n & 2*y+1=2*b]
Join, 106, 107
As Required:
109 ~x+1 e even
4 Conclusion, 99
110 x+1 e odd
Detach, 98, 109
As Required:
111 x e even => x+1 e odd
4 Conclusion, 82
THEOREM
*******
112 ALL(a):[a e n => [a e even => a+1 e odd]]
4 Conclusion, 81
Prove: ALL(a):[a e n => 2*a e even &
2*a+1 e odd]
Suppose...
113 x e n
Premise
114 ALL(b):[2 e n & b e n => 2*b e n]
U Spec, 8
115 2 e n & x e n => 2*x e n
U Spec, 114
116 2 e n & x e n
Join, 4, 113
117 2*x e n
Detach, 115, 116
118 2*x e n => [2*x e even <=> EXIST(b):[b e n & 2*x=2*b]]
U Spec, 17, 117
119 2*x e even <=> EXIST(b):[b e n & 2*x=2*b]
Detach, 118, 117
120 [2*x e even => EXIST(b):[b e n & 2*x=2*b]]
&
[EXIST(b):[b e n & 2*x=2*b] => 2*x e even]
Iff-And, 119
Sufficient: For 2*x e even
121 EXIST(b):[b e n & 2*x=2*b] => 2*x e even
Split, 120
122 2*x=2*x
Reflex, 117
123 x e n & 2*x=2*x
Join, 113, 122
124 EXIST(b):[b e n & 2*x=2*b]
E Gen, 123
125 2*x e even
Detach, 121, 124
126 2*x e n => [2*x e even => 2*x+1 e odd]
U Spec, 112, 125
127 2*x e even => 2*x+1 e odd
Detach, 126, 117
128 2*x+1 e odd
Detach, 127, 125
129 2*x e even & 2*x+1 e odd
Join, 125, 128
COROLLARY
*********
130 ALL(a):[a e n => 2*a e even & 2*a+1 e odd]
4 Conclusion, 113