THEOREM
*******
ALL(pow):ALL(pow'):[ALL(a):ALL(b):[a e n & b e n => pow(a,b) e n]
& ALL(a):[a e n => pow(a,2)=a*a]
& ALL(a):ALL(b):[a e n & b e n => pow(a,b+1)=pow(a,b)*a]
& ALL(a):ALL(b):[a e n & b e n => pow'(a,b) e n]
& ALL(a):[a e n => pow'(a,2)=a*a]
& ALL(a):ALL(b):[a e n & b e n => pow'(a,b+1)=pow'(a,b)*a]
=> ALL(a):ALL(b):[a e n & b e n & ~[a=0 & b=0] => pow(a,b)=pow'(a,b)]]
This machine-verified formal proof was written with the aid of
the author's DC Proof 2.0 software available at http://www.dcproof.com
AXIOMS / DEFINITIONS 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
3 0 e n
Axiom
4 1 e n
Axiom
5 ~1=0
Axiom
6 2 e n
Axiom
7 2=1+1
Axiom
Adding 0
8 ALL(a):[a e n => a+0=a]
Axiom
+ is commutative
9 ALL(a):ALL(b):[a e n & b e n => a+b=b+a]
Axiom
Multiplication by 0
10 ALL(a):[a e n => a*0=0]
Axiom
Multiplication by 1
11 ALL(a):[a e n => a*1=a]
Axiom
Commutativity of *
12 ALL(a):ALL(b):[a e n & b e n => a*b=b*a]
Axiom
Right cancelablity 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
The principle of mathematical induction (PMI)
14 ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [0 e a & ALL(b):[b e a => b+1 e a]
=> ALL(b):[b e n => b e a]]]
Axiom
PROOF
*****
Suppose...
15 ALL(a):ALL(b):[a e n & b e n => pow(a,b) e n]
& ALL(a):[a e n => pow(a,2)=a*a]
& ALL(a):ALL(b):[a e n & b e n => pow(a,b+1)=pow(a,b)*a]
& ALL(a):ALL(b):[a e n & b e n => pow'(a,b) e n]
& ALL(a):[a e n => pow'(a,2)=a*a]
& ALL(a):ALL(b):[a e n & b e n => pow'(a,b+1)=pow'(a,b)*a]
Premise
Define: pow
***********
16 ALL(a):ALL(b):[a e n & b e n => pow(a,b) e n]
Split, 15
17 ALL(a):[a e n => pow(a,2)=a*a]
Split, 15
18 ALL(a):ALL(b):[a e n & b e n => pow(a,b+1)=pow(a,b)*a]
Split, 15
Define: pow'
************
19 ALL(a):ALL(b):[a e n & b e n => pow'(a,b) e n]
Split, 15
20 ALL(a):[a e n => pow'(a,2)=a*a]
Split, 15
21 ALL(a):ALL(b):[a e n & b e n => pow'(a,b+1)=pow'(a,b)*a]
Split, 15
22 ALL(b):[0 e n & b e n => pow(0,b) e n]
U Spec, 16
23 0 e n & 0 e n => pow(0,0) e n
U Spec, 22
24 0 e n & 0 e n
Join, 3, 3
25 pow(0,0) e n
Detach, 23, 24
26 ALL(b):[0 e n & b e n => pow'(0,b) e n]
U Spec, 19
27 0 e n & 0 e n => pow'(0,0) e n
U Spec, 26
28 pow'(0,0) e n
Detach, 27, 24
Prove: ALL(a):ALL(b):[a e n & b e n & ~[a=0 & b=0] => pow(a,b)=pow'(a,b)]]
Suppose...
29 x e n & y e n & ~[x=0 & y=0]
Premise
30 x e n
Split, 29
31 y e n
Split, 29
32 ~[x=0 & y=0]
Split, 29
33 ~~[x=0 => ~y=0]
Imply-And, 32
34 x=0 => ~y=0
Rem DNeg, 33
Two cases:
35 x=0 | ~x=0
Or Not
Case One: (Base x = 0, Exponent y =/= 0)
Prove: x=0 => pow(x,y)=pow'(x,y)
Suppose...
36 x=0
Premise
37 ~y=0
Detach, 34, 36
38 EXIST(sub):[Set(sub) & ALL(b):[b e sub <=> b e n & [~b=0 => pow(x,b)=0]]]
Subset, 1
39 Set(p1) & ALL(b):[b e p1 <=> b e n & [~b=0 => pow(x,b)=0]]
E Spec, 38
Define: p1
40 Set(p1)
Split, 39
41 ALL(b):[b e p1 <=> b e n & [~b=0 => pow(x,b)=0]]
Split, 39
Apply Principle of Mathematical Induction
42 Set(p1) & ALL(b):[b e p1 => b e n]
=> [0 e p1 & ALL(b):[b e p1 => b+1 e p1]
=> ALL(b):[b e n => b e p1]]
U Spec, 14
Prove: ALL(b):[b e p1 => b e n]
Suppose...
43 t e p1
Premise
44 t e p1 <=> t e n & [~t=0 => pow(x,t)=0]
U Spec, 41
45 [t e p1 => t e n & [~t=0 => pow(x,t)=0]]
& [t e n & [~t=0 => pow(x,t)=0] => t e p1]
Iff-And, 44
46 t e p1 => t e n & [~t=0 => pow(x,t)=0]
Split, 45
47 t e n & [~t=0 => pow(x,t)=0] => t e p1
Split, 45
48 t e n & [~t=0 => pow(x,t)=0]
Detach, 46, 43
49 t e n
Split, 48
As Required:
50 ALL(b):[b e p1 => b e n]
4 Conclusion, 43
51 Set(p1) & ALL(b):[b e p1 => b e n]
Join, 40, 50
Sufficient: ALL(b):[b e n => b e p1]
52 0 e p1 & ALL(b):[b e p1 => b+1 e p1]
=> ALL(b):[b e n => b e p1]
Detach, 42, 51
53 0 e p1 <=> 0 e n & [~0=0 => pow(x,0)=0]
U Spec, 41
54 [0 e p1 => 0 e n & [~0=0 => pow(x,0)=0]]
& [0 e n & [~0=0 => pow(x,0)=0] => 0 e p1]
Iff-And, 53
55 0 e p1 => 0 e n & [~0=0 => pow(x,0)=0]
Split, 54
56 0 e n & [~0=0 => pow(x,0)=0] => 0 e p1
Split, 54
57 0=0
Reflex
58 ~0=0 => pow(x,0)=0
Arb Cons, 57
59 0 e n & [~0=0 => pow(x,0)=0]
Join, 3, 58
As Required:
60 0 e p1
Detach, 56, 59
Prove: ALL(b):[b e p1 => b+1 e p1]
Suppose...
61 t e p1
Premise
62 t e p1 <=> t e n & [~t=0 => pow(x,t)=0]
U Spec, 41
63 [t e p1 => t e n & [~t=0 => pow(x,t)=0]]
& [t e n & [~t=0 => pow(x,t)=0] => t e p1]
Iff-And, 62
64 t e p1 => t e n & [~t=0 => pow(x,t)=0]
Split, 63
65 t e n & [~t=0 => pow(x,t)=0] => t e p1
Split, 63
66 t e n & [~t=0 => pow(x,t)=0]
Detach, 64, 61
67 t e n
Split, 66
68 ~t=0 => pow(x,t)=0
Split, 66
69 ~~t=0 | pow(x,t)=0
Imply-Or, 68
Two sub-cases:
70 t=0 | pow(x,t)=0
Rem DNeg, 69
71 t+1 e p1 <=> t+1 e n & [~t+1=0 => pow(x,t+1)=0]
U Spec, 41
72 [t+1 e p1 => t+1 e n & [~t+1=0 => pow(x,t+1)=0]]
& [t+1 e n & [~t+1=0 => pow(x,t+1)=0] => t+1 e p1]
Iff-And, 71
73 t+1 e p1 => t+1 e n & [~t+1=0 => pow(x,t+1)=0]
Split, 72
74 t+1 e n & [~t+1=0 => pow(x,t+1)=0] => t+1 e p1
Split, 72
75 t+1 e n & [~~t+1=0 | pow(x,t+1)=0] => t+1 e p1
Imply-Or, 74
Sufficient: t+1 e p1
76 t+1 e n & [t+1=0 | pow(x,t+1)=0] => t+1 e p1
Rem DNeg, 75
77 ALL(b):[t e n & b e n => t+b e n]
U Spec, 2
78 t e n & 1 e n => t+1 e n
U Spec, 77
79 t e n & 1 e n
Join, 67, 4
80 t+1 e n
Detach, 78, 79
Sub-case One
Prove: t=0 => t+1 e p1
Suppose...
81 t=0
Premise
82 ALL(b):[x e n & b e n => pow(x,b+1)=pow(x,b)*x]
U Spec, 18
83 x e n & t e n => pow(x,t+1)=pow(x,t)*x
U Spec, 82
84 x e n & t e n
Join, 30, 67
85 pow(x,t+1)=pow(x,t)*x
Detach, 83, 84
86 pow(x,t+1)=pow(x,0)*x
Substitute, 81, 85
87 pow(x,t+1)=pow(0,0)*0
Substitute, 36, 86
88 pow(0,0) e n => pow(0,0)*0=0
U Spec, 10
89 pow(0,0)*0=0
Detach, 88, 25
90 pow(x,t+1)=0
Substitute, 89, 87
91 t+1=0 | pow(x,t+1)=0
Arb Or, 90
92 t+1 e n & [t+1=0 | pow(x,t+1)=0]
Join, 80, 91
93 t+1 e p1
Detach, 76, 92
As Required:
94 t=0 => t+1 e p1
4 Conclusion, 81
Sub-case two
Prove: pow(x,t)=0 => t+1 e p1
Suppose...
95 pow(x,t)=0
Premise
96 ALL(b):[x e n & b e n => pow(x,b+1)=pow(x,b)*x]
U Spec, 18
97 x e n & t e n => pow(x,t+1)=pow(x,t)*x
U Spec, 96
98 x e n & t e n
Join, 30, 67
99 pow(x,t+1)=pow(x,t)*x
Detach, 97, 98
100 pow(x,t+1)=0*x
Substitute, 95, 99
101 pow(x,t+1)=0*0
Substitute, 36, 100
102 0 e n => 0*0=0
U Spec, 10
103 0*0=0
Detach, 102, 3
104 pow(x,t+1)=0
Substitute, 103, 101
105 t+1=0 | pow(x,t+1)=0
Arb Or, 104
106 t+1 e n & [t+1=0 | pow(x,t+1)=0]
Join, 80, 105
107 t+1 e p1
Detach, 76, 106
As Required:
108 pow(x,t)=0 => t+1 e p1
4 Conclusion, 95
109 [t=0 => t+1 e p1] & [pow(x,t)=0 => t+1 e p1]
Join, 94, 108
110 t+1 e p1
Cases, 70, 109
As Required:
111 ALL(b):[b e p1 => b+1 e p1]
4 Conclusion, 61
112 0 e p1 & ALL(b):[b e p1 => b+1 e p1]
Join, 60, 111
113 ALL(b):[b e n => b e p1]
Detach, 52, 112
114 t e n
Premise
115 t e n => t e p1
U Spec, 113
116 t e p1
Detach, 115, 114
117 t e p1 <=> t e n & [~t=0 => pow(x,t)=0]
U Spec, 41
118 [t e p1 => t e n & [~t=0 => pow(x,t)=0]]
& [t e n & [~t=0 => pow(x,t)=0] => t e p1]
Iff-And, 117
119 t e p1 => t e n & [~t=0 => pow(x,t)=0]
Split, 118
120 t e n & [~t=0 => pow(x,t)=0] => t e p1
Split, 118
121 t e n & [~t=0 => pow(x,t)=0]
Detach, 119, 116
122 t e n
Split, 121
123 ~t=0 => pow(x,t)=0
Split, 121
As Required:
124 ALL(a):[a e n => [~a=0 => pow(x,a)=0]]
4 Conclusion, 114
125 EXIST(sub):[Set(sub) & ALL(b):[b e sub <=> b e n & [~b=0 => pow'(x,b)=0]]]
Subset, 1
126 Set(p2) & ALL(b):[b e p2 <=> b e n & [~b=0 => pow'(x,b)=0]]
E Spec, 125
Define: p2
127 Set(p2)
Split, 126
128 ALL(b):[b e p2 <=> b e n & [~b=0 => pow'(x,b)=0]]
Split, 126
Apply the Principle of Mathematical Induction
129 Set(p2) & ALL(b):[b e p2 => b e n]
=> [0 e p2 & ALL(b):[b e p2 => b+1 e p2]
=> ALL(b):[b e n => b e p2]]
U Spec, 14
130 0 e p2 <=> 0 e n & [~0=0 => pow'(x,0)=0]
U Spec, 128
131 [0 e p2 => 0 e n & [~0=0 => pow'(x,0)=0]]
& [0 e n & [~0=0 => pow'(x,0)=0] => 0 e p2]
Iff-And, 130
132 0 e p2 => 0 e n & [~0=0 => pow'(x,0)=0]
Split, 131
133 0 e n & [~0=0 => pow'(x,0)=0] => 0 e p2
Split, 131
134 0=0
Reflex
135 ~0=0 => pow'(x,0)=0
Arb Cons, 134
136 0=0
Reflex
137 ~0=0 => pow'(x,0)=0
Arb Cons, 136
138 0 e n & [~0=0 => pow'(x,0)=0]
Join, 3, 137
139 0 e p2
Detach, 133, 138
Prove: ALL(b):[b e p2 => b+1 e p2]
Suppose...
140 t e p2
Premise
141 t e p2 <=> t e n & [~t=0 => pow'(x,t)=0]
U Spec, 128
142 [t e p2 => t e n & [~t=0 => pow'(x,t)=0]]
& [t e n & [~t=0 => pow'(x,t)=0] => t e p2]
Iff-And, 141
143 t e p2 => t e n & [~t=0 => pow'(x,t)=0]
Split, 142
144 t e n & [~t=0 => pow'(x,t)=0] => t e p2
Split, 142
145 t e n & [~t=0 => pow'(x,t)=0]
Detach, 143, 140
146 t e n
Split, 145
147 ~t=0 => pow'(x,t)=0
Split, 145
148 ~~t=0 | pow'(x,t)=0
Imply-Or, 147
Two sub-cases
149 t=0 | pow'(x,t)=0
Rem DNeg, 148
150 t+1 e p2 <=> t+1 e n & [~t+1=0 => pow'(x,t+1)=0]
U Spec, 128
151 [t+1 e p2 => t+1 e n & [~t+1=0 => pow'(x,t+1)=0]]
& [t+1 e n & [~t+1=0 => pow'(x,t+1)=0] => t+1 e p2]
Iff-And, 150
152 t+1 e p2 => t+1 e n & [~t+1=0 => pow'(x,t+1)=0]
Split, 151
153 t+1 e n & [~t+1=0 => pow'(x,t+1)=0] => t+1 e p2
Split, 151
154 t+1 e n & [~~t+1=0 | pow'(x,t+1)=0] => t+1 e p2
Imply-Or, 153
155 t+1 e n & [t+1=0 | pow'(x,t+1)=0] => t+1 e p2
Rem DNeg, 154
156 ALL(b):[t e n & b e n => t+b e n]
U Spec, 2
157 t e n & 1 e n => t+1 e n
U Spec, 156
158 t e n & 1 e n
Join, 146, 4
159 t+1 e n
Detach, 157, 158
Sub-case one
Prove: t=0 => t+1 e p2
Suppose...
160 t=0
Premise
161 ALL(b):[x e n & b e n => pow'(x,b+1)=pow'(x,b)*x]
U Spec, 21
162 x e n & 0 e n => pow'(x,0+1)=pow'(x,0)*x
U Spec, 161
163 x e n & 0 e n
Join, 30, 3
164 pow'(x,0+1)=pow'(x,0)*x
Detach, 162, 163
165 pow'(x,t+1)=pow'(x,0)*x
Substitute, 160, 164
166 pow'(x,t+1)=pow'(0,0)*0
Substitute, 36, 165
167 pow'(0,0) e n => pow'(0,0)*0=0
U Spec, 10
168 pow'(0,0)*0=0
Detach, 167, 28
169 pow'(x,t+1)=0
Substitute, 168, 166
170 t+1=0 | pow'(x,t+1)=0
Arb Or, 169
171 t+1 e n & [t+1=0 | pow'(x,t+1)=0]
Join, 159, 170
172 t+1 e p2
Detach, 155, 171
As Required:
173 t=0 => t+1 e p2
4 Conclusion, 160
Sub-case two
Prove: pow'(x,t)=0 => t+1 e p2
Suppose...
174 pow'(x,t)=0
Premise
175 ALL(b):[x e n & b e n => pow'(x,b+1)=pow'(x,b)*x]
U Spec, 21
176 x e n & t e n => pow'(x,t+1)=pow'(x,t)*x
U Spec, 175
177 x e n & t e n
Join, 30, 146
178 pow'(x,t+1)=pow'(x,t)*x
Detach, 176, 177
179 pow'(x,t+1)=0*x
Substitute, 174, 178
180 pow'(x,t+1)=0*0
Substitute, 36, 179
181 0 e n => 0*0=0
U Spec, 10
182 0*0=0
Detach, 181, 3
183 pow'(x,t+1)=0
Substitute, 182, 180
184 t+1=0 | pow'(x,t+1)=0
Arb Or, 183
185 t+1 e n & [t+1=0 | pow'(x,t+1)=0]
Join, 159, 184
186 t+1 e p2
Detach, 155, 185
As Required:
187 pow'(x,t)=0 => t+1 e p2
4 Conclusion, 174
188 [t=0 => t+1 e p2] & [pow'(x,t)=0 => t+1 e p2]
Join, 173, 187
189 t+1 e p2
Cases, 149, 188
As Required:
190 ALL(b):[b e p2 => b+1 e p2]
4 Conclusion, 140
191 0 e p2 & ALL(b):[b e p2 => b+1 e p2]
Join, 139, 190
Prove: ALL(b):[b e p2 => b e n]
Suppose...
192 t e p2
Premise
193 t e p2 <=> t e n & [~t=0 => pow'(x,t)=0]
U Spec, 128
194 [t e p2 => t e n & [~t=0 => pow'(x,t)=0]]
& [t e n & [~t=0 => pow'(x,t)=0] => t e p2]
Iff-And, 193
195 t e p2 => t e n & [~t=0 => pow'(x,t)=0]
Split, 194
196 t e n & [~t=0 => pow'(x,t)=0] => t e p2
Split, 194
197 t e n & [~t=0 => pow'(x,t)=0]
Detach, 195, 192
198 t e n
Split, 197
As Required:
199 ALL(b):[b e p2 => b e n]
4 Conclusion, 192
200 Set(p2) & ALL(b):[b e p2 => b e n]
Join, 127, 199
201 0 e p2 & ALL(b):[b e p2 => b+1 e p2]
=> ALL(b):[b e n => b e p2]
Detach, 129, 200
202 0 e p2 & ALL(b):[b e p2 => b+1 e p2]
Join, 139, 190
As Required:
203 ALL(b):[b e n => b e p2]
Detach, 201, 202
Prove: ALL(a):[a e n => [~a=0 => pow'(x,a)=0]]
Suppose...
204 t e n
Premise
205 t e n => t e p2
U Spec, 203
206 t e p2
Detach, 205, 204
207 t e p2 <=> t e n & [~t=0 => pow'(x,t)=0]
U Spec, 128
208 [t e p2 => t e n & [~t=0 => pow'(x,t)=0]]
& [t e n & [~t=0 => pow'(x,t)=0] => t e p2]
Iff-And, 207
209 t e p2 => t e n & [~t=0 => pow'(x,t)=0]
Split, 208
210 t e n & [~t=0 => pow'(x,t)=0] => t e p2
Split, 208
211 t e n & [~t=0 => pow'(x,t)=0]
Detach, 209, 206
212 t e n
Split, 211
213 ~t=0 => pow'(x,t)=0
Split, 211
As Required:
214 ALL(a):[a e n => [~a=0 => pow'(x,a)=0]]
4 Conclusion, 204
215 y e n => [~y=0 => pow(x,y)=0]
U Spec, 124
216 ~y=0 => pow(x,y)=0
Detach, 215, 31
217 pow(x,y)=0
Detach, 216, 37
218 y e n => [~y=0 => pow'(x,y)=0]
U Spec, 214
219 ~y=0 => pow'(x,y)=0
Detach, 218, 31
220 pow'(x,y)=0
Detach, 219, 37
221 pow(x,y)=pow'(x,y)
Substitute, 220, 217
As Required:
222 x=0 => pow(x,y)=pow'(x,y)
4 Conclusion, 36
Case two
Prove: ~x=0 => pow(x,y)=pow'(x,y)
Suppose...
223 ~x=0
Premise
224 x e n => pow(x,2)=x*x
U Spec, 17
225 pow(x,2)=x*x
Detach, 224, 30
226 ALL(b):[x e n & b e n => pow(x,b+1)=pow(x,b)*x]
U Spec, 18
227 x e n & 1 e n => pow(x,1+1)=pow(x,1)*x
U Spec, 226
228 x e n & 1 e n
Join, 30, 4
229 pow(x,1+1)=pow(x,1)*x
Detach, 227, 228
230 pow(x,2)=pow(x,1)*x
Substitute, 7, 229
231 x*x=pow(x,1)*x
Substitute, 225, 230
232 pow(x,1)*x=x*x
Sym, 231
233 ALL(b):ALL(c):[pow(x,1) e n & b e n & c e n & ~b=0 => [pow(x,1)*b=c*b => pow(x,1)=c]]
U Spec, 13
234 ALL(c):[pow(x,1) e n & x e n & c e n & ~x=0 => [pow(x,1)*x=c*x => pow(x,1)=c]]
U Spec, 233
235 pow(x,1) e n & x e n & x e n & ~x=0 => [pow(x,1)*x=x*x => pow(x,1)=x]
U Spec, 234
236 ALL(b):[x e n & b e n => pow(x,b) e n]
U Spec, 16
237 x e n & 1 e n => pow(x,1) e n
U Spec, 236
238 pow(x,1) e n
Detach, 237, 228
239 pow(x,1) e n & x e n
Join, 238, 30
240 pow(x,1) e n & x e n & x e n
Join, 239, 30
241 pow(x,1) e n & x e n & x e n & ~x=0
Join, 240, 223
242 pow(x,1)*x=x*x => pow(x,1)=x
Detach, 235, 241
243 pow(x,1)=x
Detach, 242, 232
244 ALL(b):[x e n & b e n => pow(x,b+1)=pow(x,b)*x]
U Spec, 18
245 x e n & 0 e n => pow(x,0+1)=pow(x,0)*x
U Spec, 244
246 x e n & 0 e n
Join, 30, 3
247 pow(x,0+1)=pow(x,0)*x
Detach, 245, 246
248 1 e n => 1+0=1
U Spec, 8
249 1+0=1
Detach, 248, 4
250 ALL(b):[0 e n & b e n => 0+b=b+0]
U Spec, 9
251 0 e n & 1 e n => 0+1=1+0
U Spec, 250
252 0 e n & 1 e n
Join, 3, 4
253 0+1=1+0
Detach, 251, 252
254 0+1=1
Substitute, 253, 249
255 pow(x,1)=pow(x,0)*x
Substitute, 254, 247
256 x=pow(x,0)*x
Substitute, 243, 255
257 x e n => x*1=x
U Spec, 11
258 x*1=x
Detach, 257, 30
259 ALL(b):[x e n & b e n => x*b=b*x]
U Spec, 12
260 x e n & 1 e n => x*1=1*x
U Spec, 259
261 x e n & 1 e n
Join, 30, 4
262 x*1=1*x
Detach, 260, 261
263 1*x=x
Substitute, 262, 258
264 1*x=pow(x,0)*x
Substitute, 263, 256
265 pow(x,0)*x=1*x
Sym, 264
266 ALL(b):ALL(c):[pow(x,0) e n & b e n & c e n & ~b=0 => [pow(x,0)*b=c*b => pow(x,0)=c]]
U Spec, 13
267 ALL(c):[pow(x,0) e n & x e n & c e n & ~x=0 => [pow(x,0)*x=c*x => pow(x,0)=c]]
U Spec, 266
268 pow(x,0) e n & x e n & 1 e n & ~x=0 => [pow(x,0)*x=1*x => pow(x,0)=1]
U Spec, 267
269 ALL(b):[x e n & b e n => pow(x,b) e n]
U Spec, 16
270 x e n & 0 e n => pow(x,0) e n
U Spec, 269
271 x e n & 0 e n
Join, 30, 3
272 pow(x,0) e n
Detach, 270, 271
273 pow(x,0) e n & x e n
Join, 272, 30
274 pow(x,0) e n & x e n & 1 e n
Join, 273, 4
275 pow(x,0) e n & x e n & 1 e n & ~x=0
Join, 274, 223
276 pow(x,0)*x=1*x => pow(x,0)=1
Detach, 268, 275
277 pow(x,0)=1
Detach, 276, 265
278 x e n => pow'(x,2)=x*x
U Spec, 20
279 pow'(x,2)=x*x
Detach, 278, 30
280 ALL(b):[x e n & b e n => pow'(x,b+1)=pow'(x,b)*x]
U Spec, 21
281 x e n & 1 e n => pow'(x,1+1)=pow'(x,1)*x
U Spec, 280
282 x e n & 1 e n
Join, 30, 4
283 pow'(x,1+1)=pow'(x,1)*x
Detach, 281, 282
284 pow'(x,2)=pow'(x,1)*x
Substitute, 7, 283
285 x*x=pow'(x,1)*x
Substitute, 279, 284
286 pow'(x,1)*x=x*x
Sym, 285
287 ALL(b):ALL(c):[pow'(x,1) e n & b e n & c e n & ~b=0 => [pow'(x,1)*b=c*b => pow'(x,1)=c]]
U Spec, 13
288 ALL(c):[pow'(x,1) e n & x e n & c e n & ~x=0 => [pow'(x,1)*x=c*x => pow'(x,1)=c]]
U Spec, 287
289 pow'(x,1) e n & x e n & x e n & ~x=0 => [pow'(x,1)*x=x*x => pow'(x,1)=x]
U Spec, 288
290 ALL(b):[x e n & b e n => pow'(x,b) e n]
U Spec, 19
291 x e n & 1 e n => pow'(x,1) e n
U Spec, 290
292 pow'(x,1) e n
Detach, 291, 228
293 pow'(x,1) e n & x e n
Join, 292, 30
294 pow'(x,1) e n & x e n & x e n
Join, 293, 30
295 pow'(x,1) e n & x e n & x e n & ~x=0
Join, 294, 223
296 pow'(x,1)*x=x*x => pow'(x,1)=x
Detach, 289, 295
297 pow'(x,1)=x
Detach, 296, 286
298 ALL(b):[x e n & b e n => pow'(x,b+1)=pow'(x,b)*x]
U Spec, 21
299 x e n & 0 e n => pow'(x,0+1)=pow'(x,0)*x
U Spec, 298
300 pow'(x,0+1)=pow'(x,0)*x
Detach, 299, 246
301 pow'(x,1)=pow'(x,0)*x
Substitute, 254, 300
302 x=pow'(x,0)*x
Substitute, 297, 301
303 pow'(x,0)*x=x
Sym, 302
304 pow'(x,0)*x=1*x
Substitute, 263, 303
305 ALL(b):ALL(c):[pow'(x,0) e n & b e n & c e n & ~b=0 => [pow'(x,0)*b=c*b => pow'(x,0)=c]]
U Spec, 13
306 ALL(c):[pow'(x,0) e n & x e n & c e n & ~x=0 => [pow'(x,0)*x=c*x => pow'(x,0)=c]]
U Spec, 305
307 pow'(x,0) e n & x e n & 1 e n & ~x=0 => [pow'(x,0)*x=1*x => pow'(x,0)=1]
U Spec, 306
308 ALL(b):[x e n & b e n => pow'(x,b) e n]
U Spec, 19
309 x e n & 0 e n => pow'(x,0) e n
U Spec, 308
310 x e n & 0 e n
Join, 30, 3
311 pow'(x,0) e n
Detach, 309, 310
312 pow'(x,0) e n & x e n
Join, 311, 30
313 pow'(x,0) e n & x e n & 1 e n
Join, 312, 4
314 pow'(x,0) e n & x e n & 1 e n & ~x=0
Join, 313, 223
315 pow'(x,0)*x=1*x => pow'(x,0)=1
Detach, 307, 314
316 pow'(x,0)=1
Detach, 315, 304
317 pow(x,0)=pow'(x,0)
Substitute, 316, 277
318 EXIST(sub):[Set(sub) & ALL(b):[b e sub <=> b e n & pow(x,b)=pow'(x,b)]]
Subset, 1
319 Set(p3) & ALL(b):[b e p3 <=> b e n & pow(x,b)=pow'(x,b)]
E Spec, 318
Define: p3
320 Set(p3)
Split, 319
321 ALL(b):[b e p3 <=> b e n & pow(x,b)=pow'(x,b)]
Split, 319
322 Set(p3) & ALL(b):[b e p3 => b e n]
=> [0 e p3 & ALL(b):[b e p3 => b+1 e p3]
=> ALL(b):[b e n => b e p3]]
U Spec, 14
Prove: ALL(b):[b e p3 => b e n]
Suppose...
323 t e p3
Premise
324 t e p3 <=> t e n & pow(x,t)=pow'(x,t)
U Spec, 321
325 [t e p3 => t e n & pow(x,t)=pow'(x,t)]
& [t e n & pow(x,t)=pow'(x,t) => t e p3]
Iff-And, 324
326 t e p3 => t e n & pow(x,t)=pow'(x,t)
Split, 325
327 t e n & pow(x,t)=pow'(x,t) => t e p3
Split, 325
328 t e n & pow(x,t)=pow'(x,t)
Detach, 326, 323
329 t e n
Split, 328
As Required:
330 ALL(b):[b e p3 => b e n]
4 Conclusion, 323
331 Set(p3) & ALL(b):[b e p3 => b e n]
Join, 320, 330
Sufficient: ALL(b):[b e n => b e p3]
332 0 e p3 & ALL(b):[b e p3 => b+1 e p3]
=> ALL(b):[b e n => b e p3]
Detach, 322, 331
333 0 e p3 <=> 0 e n & pow(x,0)=pow'(x,0)
U Spec, 321
334 [0 e p3 => 0 e n & pow(x,0)=pow'(x,0)]
& [0 e n & pow(x,0)=pow'(x,0) => 0 e p3]
Iff-And, 333
335 0 e p3 => 0 e n & pow(x,0)=pow'(x,0)
Split, 334
Sufficient: 0 e p3
336 0 e n & pow(x,0)=pow'(x,0) => 0 e p3
Split, 334
337 0 e n & pow(x,0)=pow'(x,0)
Join, 3, 317
338 0 e p3
Detach, 336, 337
Prove: ALL(b):[b e p3 => b+1 e p3]
Suppose...
339 t e p3
Premise
340 t e p3 <=> t e n & pow(x,t)=pow'(x,t)
U Spec, 321
341 [t e p3 => t e n & pow(x,t)=pow'(x,t)]
& [t e n & pow(x,t)=pow'(x,t) => t e p3]
Iff-And, 340
342 t e p3 => t e n & pow(x,t)=pow'(x,t)
Split, 341
343 t e n & pow(x,t)=pow'(x,t) => t e p3
Split, 341
344 t e n & pow(x,t)=pow'(x,t)
Detach, 342, 339
345 t e n
Split, 344
346 pow(x,t)=pow'(x,t)
Split, 344
347 t+1 e p3 <=> t+1 e n & pow(x,t+1)=pow'(x,t+1)
U Spec, 321
348 [t+1 e p3 => t+1 e n & pow(x,t+1)=pow'(x,t+1)]
& [t+1 e n & pow(x,t+1)=pow'(x,t+1) => t+1 e p3]
Iff-And, 347
349 t+1 e p3 => t+1 e n & pow(x,t+1)=pow'(x,t+1)
Split, 348
Sufficient: t+1 e p3
350 t+1 e n & pow(x,t+1)=pow'(x,t+1) => t+1 e p3
Split, 348
351 ALL(b):[t e n & b e n => t+b e n]
U Spec, 2
352 t e n & 1 e n => t+1 e n
U Spec, 351
353 t e n & 1 e n
Join, 345, 4
354 t+1 e n
Detach, 352, 353
355 ALL(b):[x e n & b e n => pow(x,b+1)=pow(x,b)*x]
U Spec, 18
356 x e n & t e n => pow(x,t+1)=pow(x,t)*x
U Spec, 355
357 x e n & t e n
Join, 30, 345
358 pow(x,t+1)=pow(x,t)*x
Detach, 356, 357
359 ALL(b):[x e n & b e n => pow'(x,b+1)=pow'(x,b)*x]
U Spec, 21
360 x e n & t e n => pow'(x,t+1)=pow'(x,t)*x
U Spec, 359
361 pow'(x,t+1)=pow'(x,t)*x
Detach, 360, 357
362 pow'(x,t+1)=pow(x,t)*x
Substitute, 346, 361
363 pow(x,t+1)=pow'(x,t+1)
Substitute, 362, 358
364 t+1 e n & pow(x,t+1)=pow'(x,t+1)
Join, 354, 363
365 t+1 e p3
Detach, 350, 364
As Required:
366 ALL(b):[b e p3 => b+1 e p3]
4 Conclusion, 339
367 0 e p3 & ALL(b):[b e p3 => b+1 e p3]
Join, 338, 366
As Required:
368 ALL(b):[b e n => b e p3]
Detach, 332, 367
Prove: ALL(b):[b e n => pow(x,b)=pow'(x,b)]
Suppose...
369 t e n
Premise
370 t e n => t e p3
U Spec, 368
371 t e p3
Detach, 370, 369
372 t e p3 <=> t e n & pow(x,t)=pow'(x,t)
U Spec, 321
373 [t e p3 => t e n & pow(x,t)=pow'(x,t)]
& [t e n & pow(x,t)=pow'(x,t) => t e p3]
Iff-And, 372
374 t e p3 => t e n & pow(x,t)=pow'(x,t)
Split, 373
375 t e n & pow(x,t)=pow'(x,t) => t e p3
Split, 373
376 t e n & pow(x,t)=pow'(x,t)
Detach, 374, 371
377 t e n
Split, 376
378 pow(x,t)=pow'(x,t)
Split, 376
379 ALL(b):[b e n => pow(x,b)=pow'(x,b)]
4 Conclusion, 369
380 y e n => pow(x,y)=pow'(x,y)
U Spec, 379
381 pow(x,y)=pow'(x,y)
Detach, 380, 31
As Required:
382 ~x=0 => pow(x,y)=pow'(x,y)
4 Conclusion, 223
383 [x=0 => pow(x,y)=pow'(x,y)]
& [~x=0 => pow(x,y)=pow'(x,y)]
Join, 222, 382
384 pow(x,y)=pow'(x,y)
Cases, 35, 383
As Required:
385 ALL(a):ALL(b):[a e n & b e n & ~[a=0 & b=0] => pow(a,b)=pow'(a,b)]
4 Conclusion, 29
As Required:
386 ALL(pow):ALL(pow'):[ALL(a):ALL(b):[a e n & b e n => pow(a,b) e n]
& ALL(a):[a e n => pow(a,2)=a*a]
& ALL(a):ALL(b):[a e n & b e n => pow(a,b+1)=pow(a,b)*a]
& ALL(a):ALL(b):[a e n & b e n => pow'(a,b) e n]
& ALL(a):[a e n => pow'(a,2)=a*a]
& ALL(a):ALL(b):[a e n & b e n => pow'(a,b+1)=pow'(a,b)*a]
=> ALL(a):ALL(b):[a e n & b e n & ~[a=0 & b=0] => pow(a,b)=pow'(a,b)]]
4 Conclusion, 15