THEOREM
*******
ALL(a):[a e n => [~a=0 => a^0=1]] <=> ALL(a):[a e n => a^2=a*a]
Given: ALL(a):ALL(b):[a e n & b e n => a^b e n]
ALL(a):ALL(b):[a e n & b e n => a^(b+1)=a^b*a]
By Dan Christensen
November 2013
(This proof was written with the aid of the author's DC Proof 2.0 software at http://www.dcproof.com )
BASIC PRINCIPLES OF ARITHMETIC USED
***********************************
n is a set (the set of natural numbers)
1 Set(n)
Axiom
+ is a binary function on n
2 ALL(a):ALL(b):[a e n & b e n => a+b e n]
Axiom
* is a binary function on n
3 ALL(a):ALL(b):[a e n & b e n => a*b e n]
Axiom
4 0 e n
Axiom
5 1 e n
Axiom
6 2 e n
Axiom
7 2=1+1
Axiom
8 ALL(a):[a e n => a+0=a]
Axiom
9 ALL(a):[a e n => a*0=0]
Axiom
10 ALL(a):[a e n => a*1=a]
Axiom
Commutativity of +
11 ALL(a):ALL(b):[a e n & b e n => a+b=b+a]
Axiom
Commutativity of *
12 ALL(a):ALL(b):[a e n & b e n => a*b=b*a]
Axiom
Right cancelability of *
13 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => [~b=0 => [a*b=c*b => a=c]]]
Axiom
Define: ^
*********
^ is a binary function on n
14 ALL(a):ALL(b):[a e n & b e n => a^b e n]
Axiom
^ is repeated multiplication
15 ALL(a):ALL(b):[a e n & b e n => a^(b+1)=a^b*a]
Axiom
PROOF
*****
'=>'
Prove: ALL(a):[a e n => [~a=0 => a^0=1]]
=> ALL(a):[a e n => a^2=a*a]
Suppose...
16 ALL(a):[a e n => [~a=0 => a^0=1]]
Premise
Prove: ALL(a):[a e n => a^2=a*a]
Suppose...
17 x e n
Premise
Two cases:
18 x=0 | ~x=0
Or Not
Case 1
Prove: x=0 => x^2=x*x
Suppose...
19 x=0
Premise
Apply definition of ^
20 ALL(b):[0 e n & b e n => 0^b e n]
U Spec, 14
21 0 e n & 0 e n => 0^0 e n
U Spec, 20
22 0 e n & 0 e n
Join, 4, 4
23 0^0 e n
Detach, 21, 22
Apply definition of ^
24 ALL(b):[0 e n & b e n => 0^(b+1)=0^b*0]
U Spec, 15
25 0 e n & 0 e n => 0^(0+1)=0^0*0
U Spec, 24
26 0^(0+1)=0^0*0
Detach, 25, 22
Apply zero product rule
27 0^0 e n => 0^0*0=0
U Spec, 9
28 0^0*0=0
Detach, 27, 23
29 0^(0+1)=0
Substitute, 28, 26
30 1 e n => 1+0=1
U Spec, 8
31 1+0=1
Detach, 30, 5
Apply commutativity of +
32 ALL(b):[1 e n & b e n => 1+b=b+1]
U Spec, 11
33 1 e n & 0 e n => 1+0=0+1
U Spec, 32
34 1 e n & 0 e n
Join, 5, 4
35 1+0=0+1
Detach, 33, 34
36 0+1=1
Substitute, 35, 31
37 0^1=0
Substitute, 36, 29
Apply definition of ^
38 ALL(b):[0 e n & b e n => 0^(b+1)=0^b*0]
U Spec, 15
39 0 e n & 1 e n => 0^(1+1)=0^1*0
U Spec, 38
40 0 e n & 1 e n
Join, 4, 5
41 0^(1+1)=0^1*0
Detach, 39, 40
42 0^2=0^1*0
Substitute, 7, 41
43 0^2=0*0
Substitute, 37, 42
44 x^2=x*x
Substitute, 19, 43
As Required:
45 x=0 => x^2=x*x
4 Conclusion, 19
Case 2
Prove: ALL(a):[a e n => a^2=a*a]
Suppose...
46 ~x=0
Premise
Apply premise
47 x e n => [~x=0 => x^0=1]
U Spec, 16
48 ~x=0 => x^0=1
Detach, 47, 17
49 x^0=1
Detach, 48, 46
Apply definition of ^
50 ALL(b):[x e n & b e n => x^(b+1)=x^b*x]
U Spec, 15
51 x e n & 0 e n => x^(0+1)=x^0*x
U Spec, 50
52 x e n & 0 e n
Join, 17, 4
53 x^(0+1)=x^0*x
Detach, 51, 52
Apply 0 sum rule
54 1 e n => 1+0=1
U Spec, 8
55 1+0=1
Detach, 54, 5
Apply commutativity of +
56 ALL(b):[1 e n & b e n => 1+b=b+1]
U Spec, 11
57 1 e n & 0 e n => 1+0=0+1
U Spec, 56
58 1 e n & 0 e n
Join, 5, 4
59 1+0=0+1
Detach, 57, 58
60 0+1=1
Substitute, 59, 55
61 x^1=x^0*x
Substitute, 60, 53
62 x^1=1*x
Substitute, 49, 61
Apply communtativity of *
63 ALL(b):[1 e n & b e n => 1*b=b*1]
U Spec, 12
64 1 e n & x e n => 1*x=x*1
U Spec, 63
65 1 e n & x e n
Join, 5, 17
66 1*x=x*1
Detach, 64, 65
67 x^1=x*1
Substitute, 66, 62
68 x e n => x*1=x
U Spec, 10
69 x*1=x
Detach, 68, 17
70 x^1=x
Substitute, 69, 67
Apply definition of ^
71 ALL(b):[x e n & b e n => x^(b+1)=x^b*x]
U Spec, 15
72 x e n & 1 e n => x^(1+1)=x^1*x
U Spec, 71
73 x e n & 1 e n
Join, 17, 5
74 x^(1+1)=x^1*x
Detach, 72, 73
75 x^2=x^1*x
Substitute, 7, 74
76 x^2=x*x
Substitute, 70, 75
As Required:
77 ~x=0 => x^2=x*x
4 Conclusion, 46
78 [x=0 => x^2=x*x] & [~x=0 => x^2=x*x]
Join, 45, 77
79 x^2=x*x
Cases, 18, 78
As Required:
80 ALL(a):[a e n => a^2=a*a]
4 Conclusion, 17
As Required:
81 ALL(a):[a e n => [~a=0 => a^0=1]]
=> ALL(a):[a e n => a^2=a*a]
4 Conclusion, 16
'<='
Prove: ALL(a):[a e n => a^2=a*a] => ALL(a):[a e n => [~a=0 => a^0=1]]
Suppose...
82 ALL(a):[a e n => a^2=a*a]
Premise
Prove: ALL(a):[a e n => [~a=0 => a^0=1]]
Suppose...
83 x e n
Premise
Prove: ~x=0 => x^0=1
Suppose...
84 ~x=0
Premise
Apply premise
85 x e n => x^2=x*x
U Spec, 82
86 x^2=x*x
Detach, 85, 83
87 x^(1+1)=x*x
Substitute, 7, 86
Apply definition of ^
88 ALL(b):[x e n & b e n => x^(b+1)=x^b*x]
U Spec, 15
89 x e n & 1 e n => x^(1+1)=x^1*x
U Spec, 88
90 x e n & 1 e n
Join, 83, 5
91 x^(1+1)=x^1*x
Detach, 89, 90
92 x^1*x=x*x
Substitute, 91, 87
Apply right cancelability of *
93 ALL(b):ALL(c):[x^1 e n & b e n & c e n => [~b=0 => [x^1*b=c*b => x^1=c]]]
U Spec, 13
94 ALL(c):[x^1 e n & x e n & c e n => [~x=0 => [x^1*x=c*x => x^1=c]]]
U Spec, 93
95 x^1 e n & x e n & x e n => [~x=0 => [x^1*x=x*x => x^1=x]]
U Spec, 94
Apply definition of ^
96 ALL(b):[x e n & b e n => x^b e n]
U Spec, 14
97 x e n & 1 e n => x^1 e n
U Spec, 96
98 x e n & 1 e n
Join, 83, 5
99 x^1 e n
Detach, 97, 98
100 x^1 e n & x e n
Join, 99, 83
101 x^1 e n & x e n & x e n
Join, 100, 83
102 ~x=0 => [x^1*x=x*x => x^1=x]
Detach, 95, 101
103 x^1*x=x*x => x^1=x
Detach, 102, 84
104 x^1=x
Detach, 103, 92
Apply definition of ^
105 ALL(b):[x e n & b e n => x^(b+1)=x^b*x]
U Spec, 15
106 x e n & 0 e n => x^(0+1)=x^0*x
U Spec, 105
107 x e n & 0 e n
Join, 83, 4
108 x^(0+1)=x^0*x
Detach, 106, 107
109 1 e n => 1+0=1
U Spec, 8
110 1+0=1
Detach, 109, 5
Apply commutativity of +
111 ALL(b):[1 e n & b e n => 1+b=b+1]
U Spec, 11
112 1 e n & 0 e n => 1+0=0+1
U Spec, 111
113 1 e n & 0 e n
Join, 5, 4
114 1+0=0+1
Detach, 112, 113
115 0+1=1
Substitute, 114, 110
116 x^1=x^0*x
Substitute, 115, 108
117 x=x^0*x
Substitute, 104, 116
Apply product of 1 rule
118 x e n => x*1=x
U Spec, 10
119 x*1=x
Detach, 118, 83
Apply commutativity of *
120 ALL(b):[x e n & b e n => x*b=b*x]
U Spec, 12
121 x e n & 1 e n => x*1=1*x
U Spec, 120
122 x e n & 1 e n
Join, 83, 5
123 x*1=1*x
Detach, 121, 122
124 1*x=x
Substitute, 123, 119
125 1*x=x^0*x
Substitute, 124, 117
Apply right cancelablity of *
126 ALL(b):ALL(c):[1 e n & b e n & c e n => [~b=0 => [1*b=c*b => 1=c]]]
U Spec, 13
127 ALL(c):[1 e n & x e n & c e n => [~x=0 => [1*x=c*x => 1=c]]]
U Spec, 126
128 1 e n & x e n & x^0 e n => [~x=0 => [1*x=x^0*x => 1=x^0]]
U Spec, 127
Apply definition of ^
129 ALL(b):[x e n & b e n => x^b e n]
U Spec, 14
130 x e n & 0 e n => x^0 e n
U Spec, 129
131 x e n & 0 e n
Join, 83, 4
132 x^0 e n
Detach, 130, 131
133 1 e n & x e n
Join, 5, 83
134 1 e n & x e n & x^0 e n
Join, 133, 132
135 ~x=0 => [1*x=x^0*x => 1=x^0]
Detach, 128, 134
136 1*x=x^0*x => 1=x^0
Detach, 135, 84
137 1=x^0
Detach, 136, 125
138 x^0=1
Sym, 137
As Required:
139 ~x=0 => x^0=1
4 Conclusion, 84
As Required:
140 ALL(a):[a e n => [~a=0 => a^0=1]]
4 Conclusion, 83
As Required:
141 ALL(a):[a e n => a^2=a*a]
=> ALL(a):[a e n => [~a=0 => a^0=1]]
4 Conclusion, 82
142 [ALL(a):[a e n => [~a=0 => a^0=1]]
=> ALL(a):[a e n => a^2=a*a]]
& [ALL(a):[a e n => a^2=a*a]
=> ALL(a):[a e n => [~a=0 => a^0=1]]]
Join, 81, 141
As Required:
143 ALL(a):[a e n => [~a=0 => a^0=1]]
<=> ALL(a):[a e n => a^2=a*a]
Iff-And, 142