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