THEOREM
*******
EXIST(pow):[ALL(a):ALL(b):[a e n & b e n & ~[a=0 & b=0] => pow(a,b) e n]
& pow(0,1)=0
& ALL(a):[a e n => pow(a,2)=a*a]
& ALL(a):ALL(b):[a e n & b e n & ~[a=0 & b=0] => pow(a,b+1)=pow(a,b)*a]]
Equivalently...
EXIST(pow):[ALL(a):ALL(b):[a e n & b e n & ~[a=0 & b=0] => pow(a,b) e n]
& ALL(a):[a e n & ~a=0 => pow(a,0)=1]
& pow(0,1)=0
& ALL(a):ALL(b):[a e n & b e n & ~[a=0 & b=0] => pow(a,b+1)=pow(a,b)*a]]
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
Alternative function axiom used here:
1 ALL(f):ALL(a):ALL(b):[ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e f => (c1,c2) e a & d e b]
& ALL(c1):ALL(c2):[(c1,c2) e a => EXIST(d):[d e b & (c1,c2,d) e f]]
& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e f & (c1,c2,d2) e f => d1=d2]
=> ALL(c1):ALL(c2):ALL(d):[d=f(c1,c2) <=> (c1,c2,d) e f]]
Axiom
AXIOMS / DEFINITIONS USED
*************************
n is a set (the set of natural numbers)
2 Set(n)
Axiom
3 0 e n
Axiom
4 ALL(a):[a e n => ~a+1=0]
Axiom
5 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
+ is a binary function on n
6 ALL(a):ALL(b):[a e n & b e n => a+b e n]
Axiom
* is a binary function on n
7 ALL(a):ALL(b):[a e n & b e n => a*b e n]
Axiom
8 1 e n
Axiom
9 ~1=0
Axiom
10 2 e n
Axiom
11 2=1+1
Axiom
12 ~2=0
Axiom
Adding 0
13 ALL(a):[a e n => a+0=a]
Axiom
Multiplying by 0
14 ALL(a):[a e n => a*0=0]
Axiom
Multiplying by 1
15 ALL(a):[a e n => a*1=a]
Axiom
+ is commutative
16 ALL(a):ALL(b):[a e n & b e n => a+b=b+a]
Axiom
* is commutative
17 ALL(a):ALL(b):[a e n & b e n => a*b=b*a]
Axiom
Right-cancelability of *
18 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n & ~b=0 => [a*b=c*b => a=c]]
Axiom
PREVIOUS RESULT
***************
Infinitely many pow functions PROOF
19 ALL(x0):[x0 e n
=> EXIST(pow):[ALL(a):ALL(b):[a e n & b e n => pow(a,b) e n]
& pow(0,0)=x0
& 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]]]
Axiom
PROOF
*****
Apply previous result
20 0 e n
=> EXIST(pow):[ALL(a):ALL(b):[a e n & b e n => pow(a,b) e n]
& pow(0,0)=0
& 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]]
U Spec, 19
21 EXIST(pow):[ALL(a):ALL(b):[a e n & b e n => pow(a,b) e n]
& pow(0,0)=0
& 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]]
Detach, 20, 3
Define: pow (with pow(0,0)=0)
***********
22 ALL(a):ALL(b):[a e n & b e n => pow(a,b) e n]
& pow(0,0)=0
& 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]
E Spec, 21
Define: pow (with pow(0,0)=0)
***********
23 ALL(a):ALL(b):[a e n & b e n => pow(a,b) e n]
Split, 22
24 pow(0,0)=0
Split, 22
25 ALL(a):[a e n => pow(a,2)=a*a]
Split, 22
26 ALL(a):ALL(b):[a e n & b e n => pow(a,b+1)=pow(a,b)*a]
Split, 22
27 ALL(a1):ALL(a2):[Set(a1) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e a1 & c2 e a2]]]
Cart Prod
28 ALL(a2):[Set(n) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e n & c2 e a2]]]
U Spec, 27
29 Set(n) & Set(n) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e n & c2 e n]]
U Spec, 28
30 Set(n) & Set(n)
Join, 2, 2
31 EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e n & c2 e n]]
Detach, 29, 30
32 Set'(n2) & ALL(c1):ALL(c2):[(c1,c2) e n2 <=> c1 e n & c2 e n]
E Spec, 31
Define: n2
**********
33 Set'(n2)
Split, 32
34 ALL(c1):ALL(c2):[(c1,c2) e n2 <=> c1 e n & c2 e n]
Split, 32
35 ALL(a1):ALL(a2):ALL(a3):[Set(a1) & Set(a2) & Set(a3) => EXIST(b):[Set''(b) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e b <=> c1 e a1 & c2 e a2 & c3 e a3]]]
Cart Prod
36 ALL(a2):ALL(a3):[Set(n) & Set(a2) & Set(a3) => EXIST(b):[Set''(b) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e b <=> c1 e n & c2 e a2 & c3 e a3]]]
U Spec, 35
37 ALL(a3):[Set(n) & Set(n) & Set(a3) => EXIST(b):[Set''(b) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e b <=> c1 e n & c2 e n & c3 e a3]]]
U Spec, 36
38 Set(n) & Set(n) & Set(n) => EXIST(b):[Set''(b) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e b <=> c1 e n & c2 e n & c3 e n]]
U Spec, 37
39 Set(n) & Set(n)
Join, 2, 2
40 Set(n) & Set(n) & Set(n)
Join, 39, 2
41 EXIST(b):[Set''(b) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e b <=> c1 e n & c2 e n & c3 e n]]
Detach, 38, 40
42 Set''(n3) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e n3 <=> c1 e n & c2 e n & c3 e n]
E Spec, 41
Define: n3
**********
43 Set''(n3)
Split, 42
44 ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e n3 <=> c1 e n & c2 e n & c3 e n]
Split, 42
45 EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) e sub <=> (a,b) e n2 & ~[a=0 & b=0]]]
Subset, 33
46 Set'(n2') & ALL(a):ALL(b):[(a,b) e n2' <=> (a,b) e n2 & ~[a=0 & b=0]]
E Spec, 45
Define: n2'
***********
47 Set'(n2')
Split, 46
48 ALL(a):ALL(b):[(a,b) e n2' <=> (a,b) e n2 & ~[a=0 & b=0]]
Split, 46
49 EXIST(sub):[Set''(sub) & ALL(a):ALL(b):ALL(c):[(a,b,c) e sub
<=> (a,b,c) e n3 & [(a,b) e n2' & c=pow(a,b)]]]
Subset, 43
50 Set''(pow') & ALL(a):ALL(b):ALL(c):[(a,b,c) e pow'
<=> (a,b,c) e n3 & [(a,b) e n2' & c=pow(a,b)]]
E Spec, 49
Define: pow'
************
51 Set''(pow')
Split, 50
52 ALL(a):ALL(b):ALL(c):[(a,b,c) e pow'
<=> (a,b,c) e n3 & [(a,b) e n2' & c=pow(a,b)]]
Split, 50
53 ALL(a):ALL(b):[ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e pow' => (c1,c2) e a & d e b]
& ALL(c1):ALL(c2):[(c1,c2) e a => EXIST(d):[d e b & (c1,c2,d) e pow']]
& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e pow' & (c1,c2,d2) e pow' => d1=d2]
=> ALL(c1):ALL(c2):ALL(d):[d=pow'(c1,c2) <=> (c1,c2,d) e pow']]
U Spec, 1
54 ALL(b):[ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e pow' => (c1,c2) e n2' & d e b]
& ALL(c1):ALL(c2):[(c1,c2) e n2' => EXIST(d):[d e b & (c1,c2,d) e pow']]
& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e pow' & (c1,c2,d2) e pow' => d1=d2]
=> ALL(c1):ALL(c2):ALL(d):[d=pow'(c1,c2) <=> (c1,c2,d) e pow']]
U Spec, 53
Sufficient: For functionality of pow'
55 ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e pow' => (c1,c2) e n2' & d e n]
& ALL(c1):ALL(c2):[(c1,c2) e n2' => EXIST(d):[d e n & (c1,c2,d) e pow']]
& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e pow' & (c1,c2,d2) e pow' => d1=d2]
=> ALL(c1):ALL(c2):ALL(d):[d=pow'(c1,c2) <=> (c1,c2,d) e pow']
U Spec, 54
Prove: ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e f => (c1,c2) e a & d e b]
Suppose...
56 (x,y,z) e pow'
Premise
57 ALL(b):ALL(c):[(x,b,c) e pow'
<=> (x,b,c) e n3 & [(x,b) e n2' & c=pow(x,b)]]
U Spec, 52
58 ALL(c):[(x,y,c) e pow'
<=> (x,y,c) e n3 & [(x,y) e n2' & c=pow(x,y)]]
U Spec, 57
59 (x,y,z) e pow'
<=> (x,y,z) e n3 & [(x,y) e n2' & z=pow(x,y)]
U Spec, 58
60 [(x,y,z) e pow' => (x,y,z) e n3 & [(x,y) e n2' & z=pow(x,y)]]
& [(x,y,z) e n3 & [(x,y) e n2' & z=pow(x,y)] => (x,y,z) e pow']
Iff-And, 59
61 (x,y,z) e pow' => (x,y,z) e n3 & [(x,y) e n2' & z=pow(x,y)]
Split, 60
62 (x,y,z) e n3 & [(x,y) e n2' & z=pow(x,y)] => (x,y,z) e pow'
Split, 60
63 (x,y,z) e n3 & [(x,y) e n2' & z=pow(x,y)]
Detach, 61, 56
64 (x,y,z) e n3
Split, 63
65 (x,y) e n2' & z=pow(x,y)
Split, 63
66 (x,y) e n2'
Split, 65
67 z=pow(x,y)
Split, 65
68 ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]
U Spec, 44
69 ALL(c3):[(x,y,c3) e n3 <=> x e n & y e n & c3 e n]
U Spec, 68
70 (x,y,z) e n3 <=> x e n & y e n & z e n
U Spec, 69
71 [(x,y,z) e n3 => x e n & y e n & z e n]
& [x e n & y e n & z e n => (x,y,z) e n3]
Iff-And, 70
72 (x,y,z) e n3 => x e n & y e n & z e n
Split, 71
73 x e n & y e n & z e n => (x,y,z) e n3
Split, 71
74 x e n & y e n & z e n
Detach, 72, 64
75 x e n
Split, 74
76 y e n
Split, 74
77 z e n
Split, 74
78 (x,y) e n2' & z e n
Join, 66, 77
Functionality: Part 1
79 ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e pow' => (c1,c2) e n2' & d e n]
4 Conclusion, 56
Suppose...
80 (x,y) e n2'
Premise
81 ALL(b):ALL(c):[(x,b,c) e pow'
<=> (x,b,c) e n3 & [(x,b) e n2' & c=pow(x,b)]]
U Spec, 52
82 ALL(c):[(x,y,c) e pow'
<=> (x,y,c) e n3 & [(x,y) e n2' & c=pow(x,y)]]
U Spec, 81
83 (x,y,pow(x,y)) e pow'
<=> (x,y,pow(x,y)) e n3 & [(x,y) e n2' & pow(x,y)=pow(x,y)]
U Spec, 82
84 [(x,y,pow(x,y)) e pow' => (x,y,pow(x,y)) e n3 & [(x,y) e n2' & pow(x,y)=pow(x,y)]]
& [(x,y,pow(x,y)) e n3 & [(x,y) e n2' & pow(x,y)=pow(x,y)] => (x,y,pow(x,y)) e pow']
Iff-And, 83
85 (x,y,pow(x,y)) e pow' => (x,y,pow(x,y)) e n3 & [(x,y) e n2' & pow(x,y)=pow(x,y)]
Split, 84
Sufficient: (x,y,pow(x,y)) e pow'
86 (x,y,pow(x,y)) e n3 & [(x,y) e n2' & pow(x,y)=pow(x,y)] => (x,y,pow(x,y)) e pow'
Split, 84
87 ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]
U Spec, 44
88 ALL(c3):[(x,y,c3) e n3 <=> x e n & y e n & c3 e n]
U Spec, 87
89 (x,y,pow(x,y)) e n3 <=> x e n & y e n & pow(x,y) e n
U Spec, 88
90 [(x,y,pow(x,y)) e n3 => x e n & y e n & pow(x,y) e n]
& [x e n & y e n & pow(x,y) e n => (x,y,pow(x,y)) e n3]
Iff-And, 89
91 (x,y,pow(x,y)) e n3 => x e n & y e n & pow(x,y) e n
Split, 90
92 x e n & y e n & pow(x,y) e n => (x,y,pow(x,y)) e n3
Split, 90
93 ALL(b):[x e n & b e n => pow(x,b) e n]
U Spec, 23
94 x e n & y e n => pow(x,y) e n
U Spec, 93
95 ALL(b):[(x,b) e n2' <=> (x,b) e n2 & ~[x=0 & b=0]]
U Spec, 48
96 (x,y) e n2' <=> (x,y) e n2 & ~[x=0 & y=0]
U Spec, 95
97 [(x,y) e n2' => (x,y) e n2 & ~[x=0 & y=0]]
& [(x,y) e n2 & ~[x=0 & y=0] => (x,y) e n2']
Iff-And, 96
98 (x,y) e n2' => (x,y) e n2 & ~[x=0 & y=0]
Split, 97
99 (x,y) e n2 & ~[x=0 & y=0] => (x,y) e n2'
Split, 97
100 (x,y) e n2 & ~[x=0 & y=0]
Detach, 98, 80
101 (x,y) e n2
Split, 100
102 ~[x=0 & y=0]
Split, 100
103 ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]
U Spec, 34
104 (x,y) e n2 <=> x e n & y e n
U Spec, 103
105 [(x,y) e n2 => x e n & y e n]
& [x e n & y e n => (x,y) e n2]
Iff-And, 104
106 (x,y) e n2 => x e n & y e n
Split, 105
107 x e n & y e n => (x,y) e n2
Split, 105
108 x e n & y e n
Detach, 106, 101
109 x e n
Split, 108
110 y e n
Split, 108
111 pow(x,y) e n
Detach, 94, 108
112 x e n & y e n & pow(x,y) e n
Join, 108, 111
113 (x,y,pow(x,y)) e n3
Detach, 92, 112
114 pow(x,y)=pow(x,y)
Reflex
115 (x,y) e n2' & pow(x,y)=pow(x,y)
Join, 80, 114
116 (x,y,pow(x,y)) e n3
& [(x,y) e n2' & pow(x,y)=pow(x,y)]
Join, 113, 115
117 (x,y,pow(x,y)) e pow'
Detach, 86, 116
118 (x,y) e n2' & pow(x,y)=pow(x,y)
Join, 80, 114
119 (x,y,pow(x,y)) e n3
& [(x,y) e n2' & pow(x,y)=pow(x,y)]
Join, 113, 118
120 (x,y,pow(x,y)) e pow'
Detach, 86, 119
121 pow(x,y) e n & (x,y,pow(x,y)) e pow'
Join, 111, 120
122 EXIST(d):[d e n & (x,y,d) e pow']
E Gen, 121
Functionality: Part 2
123 ALL(c1):ALL(c2):[(c1,c2) e n2' => EXIST(d):[d e n & (c1,c2,d) e pow']]
4 Conclusion, 80
124 (x,y,z1) e pow' & (x,y,z2) e pow'
Premise
125 (x,y,z1) e pow'
Split, 124
126 (x,y,z2) e pow'
Split, 124
127 ALL(b):ALL(c):[(x,b,c) e pow'
<=> (x,b,c) e n3 & [(x,b) e n2' & c=pow(x,b)]]
U Spec, 52
128 ALL(c):[(x,y,c) e pow'
<=> (x,y,c) e n3 & [(x,y) e n2' & c=pow(x,y)]]
U Spec, 127
129 (x,y,z1) e pow'
<=> (x,y,z1) e n3 & [(x,y) e n2' & z1=pow(x,y)]
U Spec, 128
130 [(x,y,z1) e pow' => (x,y,z1) e n3 & [(x,y) e n2' & z1=pow(x,y)]]
& [(x,y,z1) e n3 & [(x,y) e n2' & z1=pow(x,y)] => (x,y,z1) e pow']
Iff-And, 129
131 (x,y,z1) e pow' => (x,y,z1) e n3 & [(x,y) e n2' & z1=pow(x,y)]
Split, 130
132 (x,y,z1) e n3 & [(x,y) e n2' & z1=pow(x,y)] => (x,y,z1) e pow'
Split, 130
133 (x,y,z1) e n3 & [(x,y) e n2' & z1=pow(x,y)]
Detach, 131, 125
134 (x,y,z1) e n3
Split, 133
135 (x,y) e n2' & z1=pow(x,y)
Split, 133
136 (x,y) e n2'
Split, 135
137 z1=pow(x,y)
Split, 135
138 (x,y,z2) e pow'
<=> (x,y,z2) e n3 & [(x,y) e n2' & z2=pow(x,y)]
U Spec, 128
139 [(x,y,z2) e pow' => (x,y,z2) e n3 & [(x,y) e n2' & z2=pow(x,y)]]
& [(x,y,z2) e n3 & [(x,y) e n2' & z2=pow(x,y)] => (x,y,z2) e pow']
Iff-And, 138
140 (x,y,z2) e pow' => (x,y,z2) e n3 & [(x,y) e n2' & z2=pow(x,y)]
Split, 139
141 (x,y,z2) e n3 & [(x,y) e n2' & z2=pow(x,y)] => (x,y,z2) e pow'
Split, 139
142 (x,y,z2) e n3 & [(x,y) e n2' & z2=pow(x,y)]
Detach, 140, 126
143 (x,y,z2) e n3
Split, 142
144 (x,y) e n2' & z2=pow(x,y)
Split, 142
145 (x,y) e n2'
Split, 144
146 z2=pow(x,y)
Split, 144
147 z1=z2
Substitute, 146, 137
Functionality: Part 3
148 ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e pow' & (c1,c2,d2) e pow' => d1=d2]
4 Conclusion, 124
149 ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e pow' => (c1,c2) e n2' & d e n]
& ALL(c1):ALL(c2):[(c1,c2) e n2' => EXIST(d):[d e n & (c1,c2,d) e pow']]
Join, 79, 123
150 ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e pow' => (c1,c2) e n2' & d e n]
& ALL(c1):ALL(c2):[(c1,c2) e n2' => EXIST(d):[d e n & (c1,c2,d) e pow']]
& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e pow' & (c1,c2,d2) e pow' => d1=d2]
Join, 149, 148
As Required: pow' is a function
151 ALL(c1):ALL(c2):ALL(d):[d=pow'(c1,c2) <=> (c1,c2,d) e pow']
Detach, 55, 150
152 (x,y) e n2'
Premise
153 ALL(c2):[(x,c2) e n2' => EXIST(d):[d e n & (x,c2,d) e pow']]
U Spec, 123
154 (x,y) e n2' => EXIST(d):[d e n & (x,y,d) e pow']
U Spec, 153
155 EXIST(d):[d e n & (x,y,d) e pow']
Detach, 154, 152
156 z e n & (x,y,z) e pow'
E Spec, 155
157 z e n
Split, 156
158 (x,y,z) e pow'
Split, 156
159 ALL(c2):ALL(d):[d=pow'(x,c2) <=> (x,c2,d) e pow']
U Spec, 151
160 ALL(d):[d=pow'(x,y) <=> (x,y,d) e pow']
U Spec, 159
161 z=pow'(x,y) <=> (x,y,z) e pow'
U Spec, 160
162 [z=pow'(x,y) => (x,y,z) e pow']
& [(x,y,z) e pow' => z=pow'(x,y)]
Iff-And, 161
163 z=pow'(x,y) => (x,y,z) e pow'
Split, 162
164 (x,y,z) e pow' => z=pow'(x,y)
Split, 162
165 z=pow'(x,y)
Detach, 164, 158
166 pow'(x,y) e n
Substitute, 165, 157
As Required:
167 ALL(a):ALL(b):[(a,b) e n2' => pow'(a,b) e n]
4 Conclusion, 152
168 (x,y) e n2'
Premise
169 ALL(b):ALL(c):[(x,b,c) e pow'
<=> (x,b,c) e n3 & [(x,b) e n2' & c=pow(x,b)]]
U Spec, 52
170 ALL(c):[(x,y,c) e pow'
<=> (x,y,c) e n3 & [(x,y) e n2' & c=pow(x,y)]]
U Spec, 169
171 (x,y,pow(x,y)) e pow'
<=> (x,y,pow(x,y)) e n3 & [(x,y) e n2' & pow(x,y)=pow(x,y)]
U Spec, 170
172 [(x,y,pow(x,y)) e pow' => (x,y,pow(x,y)) e n3 & [(x,y) e n2' & pow(x,y)=pow(x,y)]]
& [(x,y,pow(x,y)) e n3 & [(x,y) e n2' & pow(x,y)=pow(x,y)] => (x,y,pow(x,y)) e pow']
Iff-And, 171
173 (x,y,pow(x,y)) e pow' => (x,y,pow(x,y)) e n3 & [(x,y) e n2' & pow(x,y)=pow(x,y)]
Split, 172
Sufficient: (x,y,pow(x,y)) e pow'
174 (x,y,pow(x,y)) e n3 & [(x,y) e n2' & pow(x,y)=pow(x,y)] => (x,y,pow(x,y)) e pow'
Split, 172
175 ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]
U Spec, 44
176 ALL(c3):[(x,y,c3) e n3 <=> x e n & y e n & c3 e n]
U Spec, 175
177 (x,y,pow(x,y)) e n3 <=> x e n & y e n & pow(x,y) e n
U Spec, 176
178 [(x,y,pow(x,y)) e n3 => x e n & y e n & pow(x,y) e n]
& [x e n & y e n & pow(x,y) e n => (x,y,pow(x,y)) e n3]
Iff-And, 177
179 (x,y,pow(x,y)) e n3 => x e n & y e n & pow(x,y) e n
Split, 178
180 x e n & y e n & pow(x,y) e n => (x,y,pow(x,y)) e n3
Split, 178
181 ALL(b):[x e n & b e n => pow(x,b) e n]
U Spec, 23
182 x e n & y e n => pow(x,y) e n
U Spec, 181
183 ALL(b):[(x,b) e n2' <=> (x,b) e n2 & ~[x=0 & b=0]]
U Spec, 48
184 (x,y) e n2' <=> (x,y) e n2 & ~[x=0 & y=0]
U Spec, 183
185 [(x,y) e n2' => (x,y) e n2 & ~[x=0 & y=0]]
& [(x,y) e n2 & ~[x=0 & y=0] => (x,y) e n2']
Iff-And, 184
186 (x,y) e n2' => (x,y) e n2 & ~[x=0 & y=0]
Split, 185
187 (x,y) e n2 & ~[x=0 & y=0] => (x,y) e n2'
Split, 185
188 (x,y) e n2 & ~[x=0 & y=0]
Detach, 186, 168
189 (x,y) e n2
Split, 188
190 ~[x=0 & y=0]
Split, 188
191 ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]
U Spec, 34
192 (x,y) e n2 <=> x e n & y e n
U Spec, 191
193 [(x,y) e n2 => x e n & y e n]
& [x e n & y e n => (x,y) e n2]
Iff-And, 192
194 (x,y) e n2 => x e n & y e n
Split, 193
195 x e n & y e n => (x,y) e n2
Split, 193
196 x e n & y e n
Detach, 194, 189
197 pow(x,y) e n
Detach, 182, 196
198 x e n & y e n & pow(x,y) e n
Join, 196, 197
199 (x,y,pow(x,y)) e n3
Detach, 180, 198
200 pow(x,y)=pow(x,y)
Reflex
201 (x,y) e n2' & pow(x,y)=pow(x,y)
Join, 168, 200
202 (x,y,pow(x,y)) e n3
& [(x,y) e n2' & pow(x,y)=pow(x,y)]
Join, 199, 201
203 (x,y,pow(x,y)) e pow'
Detach, 174, 202
204 ALL(c2):ALL(d):[d=pow'(x,c2) <=> (x,c2,d) e pow']
U Spec, 151
205 ALL(d):[d=pow'(x,y) <=> (x,y,d) e pow']
U Spec, 204
206 pow(x,y)=pow'(x,y) <=> (x,y,pow(x,y)) e pow'
U Spec, 205
207 [pow(x,y)=pow'(x,y) => (x,y,pow(x,y)) e pow']
& [(x,y,pow(x,y)) e pow' => pow(x,y)=pow'(x,y)]
Iff-And, 206
208 pow(x,y)=pow'(x,y) => (x,y,pow(x,y)) e pow'
Split, 207
209 (x,y,pow(x,y)) e pow' => pow(x,y)=pow'(x,y)
Split, 207
210 pow(x,y)=pow'(x,y)
Detach, 209, 203
211 pow'(x,y)=pow(x,y)
Sym, 210
As Required:
212 ALL(a):ALL(b):[(a,b) e n2' => pow'(a,b)=pow(a,b)]
4 Conclusion, 168
213 x e n
Premise
214 x e n => pow(x,2)=x*x
U Spec, 25
215 pow(x,2)=x*x
Detach, 214, 213
216 ALL(b):[(x,b) e n2' => pow'(x,b)=pow(x,b)]
U Spec, 212
217 (x,2) e n2' => pow'(x,2)=pow(x,2)
U Spec, 216
218 ALL(b):[(x,b) e n2' <=> (x,b) e n2 & ~[x=0 & b=0]]
U Spec, 48
219 (x,2) e n2' <=> (x,2) e n2 & ~[x=0 & 2=0]
U Spec, 218
220 [(x,2) e n2' => (x,2) e n2 & ~[x=0 & 2=0]]
& [(x,2) e n2 & ~[x=0 & 2=0] => (x,2) e n2']
Iff-And, 219
221 (x,2) e n2' => (x,2) e n2 & ~[x=0 & 2=0]
Split, 220
222 (x,2) e n2 & ~[x=0 & 2=0] => (x,2) e n2'
Split, 220
223 ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]
U Spec, 34
224 (x,2) e n2 <=> x e n & 2 e n
U Spec, 223
225 [(x,2) e n2 => x e n & 2 e n]
& [x e n & 2 e n => (x,2) e n2]
Iff-And, 224
226 (x,2) e n2 => x e n & 2 e n
Split, 225
227 x e n & 2 e n => (x,2) e n2
Split, 225
228 x e n & 2 e n
Join, 213, 10
229 (x,2) e n2
Detach, 227, 228
230 x=0 & 2=0
Premise
231 x=0
Split, 230
232 2=0
Split, 230
233 2=0 & ~2=0
Join, 232, 12
234 ~[x=0 & 2=0]
4 Conclusion, 230
235 (x,2) e n2 & ~[x=0 & 2=0]
Join, 229, 234
236 (x,2) e n2'
Detach, 222, 235
237 pow'(x,2)=pow(x,2)
Detach, 217, 236
238 pow'(x,2)=x*x
Substitute, 215, 237
As Required:
239 ALL(a):[a e n => pow'(a,2)=a*a]
4 Conclusion, 213
240 (x,y) e n2'
Premise
241 ALL(b):[(x,b) e n2' <=> (x,b) e n2 & ~[x=0 & b=0]]
U Spec, 48
242 (x,y) e n2' <=> (x,y) e n2 & ~[x=0 & y=0]
U Spec, 241
243 [(x,y) e n2' => (x,y) e n2 & ~[x=0 & y=0]]
& [(x,y) e n2 & ~[x=0 & y=0] => (x,y) e n2']
Iff-And, 242
244 (x,y) e n2' => (x,y) e n2 & ~[x=0 & y=0]
Split, 243
245 (x,y) e n2 & ~[x=0 & y=0] => (x,y) e n2'
Split, 243
246 (x,y) e n2 & ~[x=0 & y=0]
Detach, 244, 240
247 (x,y) e n2
Split, 246
248 ~[x=0 & y=0]
Split, 246
249 ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]
U Spec, 34
250 (x,y) e n2 <=> x e n & y e n
U Spec, 249
251 [(x,y) e n2 => x e n & y e n]
& [x e n & y e n => (x,y) e n2]
Iff-And, 250
252 (x,y) e n2 => x e n & y e n
Split, 251
253 x e n & y e n => (x,y) e n2
Split, 251
254 x e n & y e n
Detach, 252, 247
255 ALL(b):[x e n & b e n => pow(x,b+1)=pow(x,b)*x]
U Spec, 26
256 x e n
Split, 254
257 y e n
Split, 254
258 x e n & y e n => pow(x,y+1)=pow(x,y)*x
U Spec, 255
259 pow(x,y+1)=pow(x,y)*x
Detach, 258, 254
260 ALL(b):[(x,b) e n2' => pow'(x,b)=pow(x,b)]
U Spec, 212
261 (x,y+1) e n2' => pow'(x,y+1)=pow(x,y+1)
U Spec, 260
262 ALL(b):[(x,b) e n2' <=> (x,b) e n2 & ~[x=0 & b=0]]
U Spec, 48
263 (x,y+1) e n2' <=> (x,y+1) e n2 & ~[x=0 & y+1=0]
U Spec, 262
264 [(x,y+1) e n2' => (x,y+1) e n2 & ~[x=0 & y+1=0]]
& [(x,y+1) e n2 & ~[x=0 & y+1=0] => (x,y+1) e n2']
Iff-And, 263
265 (x,y+1) e n2' => (x,y+1) e n2 & ~[x=0 & y+1=0]
Split, 264
266 (x,y+1) e n2 & ~[x=0 & y+1=0] => (x,y+1) e n2'
Split, 264
267 ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]
U Spec, 34
268 (x,y+1) e n2 <=> x e n & y+1 e n
U Spec, 267
269 [(x,y+1) e n2 => x e n & y+1 e n]
& [x e n & y+1 e n => (x,y+1) e n2]
Iff-And, 268
270 (x,y+1) e n2 => x e n & y+1 e n
Split, 269
271 x e n & y+1 e n => (x,y+1) e n2
Split, 269
272 ALL(b):[y e n & b e n => y+b e n]
U Spec, 6
273 y e n & 1 e n => y+1 e n
U Spec, 272
274 y e n & 1 e n
Join, 257, 8
275 y+1 e n
Detach, 273, 274
276 x e n & y+1 e n
Join, 256, 275
277 (x,y+1) e n2
Detach, 271, 276
278 x=0 & y+1=0
Premise
279 x=0
Split, 278
280 y+1=0
Split, 278
281 y e n => ~y+1=0
U Spec, 4
282 ~y+1=0
Detach, 281, 257
283 y+1=0 & ~y+1=0
Join, 280, 282
284 ~[x=0 & y+1=0]
4 Conclusion, 278
285 (x,y+1) e n2 & ~[x=0 & y+1=0]
Join, 277, 284
286 (x,y+1) e n2'
Detach, 266, 285
287 pow'(x,y+1)=pow(x,y+1)
Detach, 261, 286
288 ALL(b):[(x,b) e n2' => pow'(x,b)=pow(x,b)]
U Spec, 212
289 (x,y) e n2' => pow'(x,y)=pow(x,y)
U Spec, 288
290 pow'(x,y)=pow(x,y)
Detach, 289, 240
291 pow'(x,y+1)=pow(x,y)*x
Substitute, 287, 259
292 pow'(x,y+1)=pow'(x,y)*x
Substitute, 290, 291
As Required:
293 ALL(a):ALL(b):[(a,b) e n2' => pow'(a,b+1)=pow'(a,b)*a]
4 Conclusion, 240
294 x e n & y e n & ~[x=0 & y=0]
Premise
295 x e n
Split, 294
296 y e n
Split, 294
297 ~[x=0 & y=0]
Split, 294
298 ALL(b):[(x,b) e n2' => pow'(x,b) e n]
U Spec, 167
299 (x,y) e n2' => pow'(x,y) e n
U Spec, 298
300 ALL(b):[(x,b) e n2' <=> (x,b) e n2 & ~[x=0 & b=0]]
U Spec, 48
301 (x,y) e n2' <=> (x,y) e n2 & ~[x=0 & y=0]
U Spec, 300
302 [(x,y) e n2' => (x,y) e n2 & ~[x=0 & y=0]]
& [(x,y) e n2 & ~[x=0 & y=0] => (x,y) e n2']
Iff-And, 301
303 (x,y) e n2' => (x,y) e n2 & ~[x=0 & y=0]
Split, 302
304 (x,y) e n2 & ~[x=0 & y=0] => (x,y) e n2'
Split, 302
305 ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]
U Spec, 34
306 (x,y) e n2 <=> x e n & y e n
U Spec, 305
307 [(x,y) e n2 => x e n & y e n]
& [x e n & y e n => (x,y) e n2]
Iff-And, 306
308 (x,y) e n2 => x e n & y e n
Split, 307
309 x e n & y e n => (x,y) e n2
Split, 307
310 x e n & y e n
Join, 295, 296
311 (x,y) e n2
Detach, 309, 310
312 (x,y) e n2 & ~[x=0 & y=0]
Join, 311, 297
313 (x,y) e n2'
Detach, 304, 312
314 pow'(x,y) e n
Detach, 299, 313
As Required:
315 ALL(a):ALL(b):[a e n & b e n & ~[a=0 & b=0] => pow'(a,b) e n]
4 Conclusion, 294
Suppose...
316 x e n & y e n & ~[x=0 & y=0]
Premise
317 x e n
Split, 316
318 y e n
Split, 316
319 ~[x=0 & y=0]
Split, 316
320 ALL(b):[(x,b) e n2' => pow'(x,b+1)=pow'(x,b)*x]
U Spec, 293
321 (x,y) e n2' => pow'(x,y+1)=pow'(x,y)*x
U Spec, 320
322 ALL(b):[(x,b) e n2' <=> (x,b) e n2 & ~[x=0 & b=0]]
U Spec, 48
323 (x,y) e n2' <=> (x,y) e n2 & ~[x=0 & y=0]
U Spec, 322
324 [(x,y) e n2' => (x,y) e n2 & ~[x=0 & y=0]]
& [(x,y) e n2 & ~[x=0 & y=0] => (x,y) e n2']
Iff-And, 323
325 (x,y) e n2' => (x,y) e n2 & ~[x=0 & y=0]
Split, 324
326 (x,y) e n2 & ~[x=0 & y=0] => (x,y) e n2'
Split, 324
327 ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]
U Spec, 34
328 (x,y) e n2 <=> x e n & y e n
U Spec, 327
329 [(x,y) e n2 => x e n & y e n]
& [x e n & y e n => (x,y) e n2]
Iff-And, 328
330 (x,y) e n2 => x e n & y e n
Split, 329
331 x e n & y e n => (x,y) e n2
Split, 329
332 x e n & y e n
Join, 317, 318
333 (x,y) e n2
Detach, 331, 332
334 (x,y) e n2 & ~[x=0 & y=0]
Join, 333, 319
335 (x,y) e n2'
Detach, 326, 334
336 pow'(x,y+1)=pow'(x,y)*x
Detach, 321, 335
As Required:
337 ALL(a):ALL(b):[a e n & b e n & ~[a=0 & b=0]
=> pow'(a,b+1)=pow'(a,b)*a]
4 Conclusion, 316
Prove: pow'(0,1)=0
Apply definition of pow
338 ALL(b):[0 e n & b e n => pow(0,b+1)=pow(0,b)*0]
U Spec, 26
339 0 e n & 0 e n => pow(0,0+1)=pow(0,0)*0
U Spec, 338
340 0 e n & 0 e n
Join, 3, 3
341 pow(0,0+1)=pow(0,0)*0
Detach, 339, 340
342 1 e n => 1+0=1
U Spec, 13
343 1+0=1
Detach, 342, 8
344 ALL(b):[0 e n & b e n => 0+b=b+0]
U Spec, 16
345 0 e n & 1 e n => 0+1=1+0
U Spec, 344
346 0 e n & 1 e n
Join, 3, 8
347 0+1=1+0
Detach, 345, 346
348 0+1=1
Substitute, 347, 343
349 pow(0,1)=pow(0,0)*0
Substitute, 348, 341
350 pow(0,1)=0*0
Substitute, 24, 349
351 0 e n => 0*0=0
U Spec, 14
352 0*0=0
Detach, 351, 3
353 pow(0,1)=0
Substitute, 352, 350
354 ALL(b):[(0,b) e n2' => pow'(0,b)=pow(0,b)]
U Spec, 212
355 (0,1) e n2' => pow'(0,1)=pow(0,1)
U Spec, 354
356 ALL(b):[(0,b) e n2' <=> (0,b) e n2 & ~[0=0 & b=0]]
U Spec, 48
357 (0,1) e n2' <=> (0,1) e n2 & ~[0=0 & 1=0]
U Spec, 356
358 [(0,1) e n2' => (0,1) e n2 & ~[0=0 & 1=0]]
& [(0,1) e n2 & ~[0=0 & 1=0] => (0,1) e n2']
Iff-And, 357
359 (0,1) e n2' => (0,1) e n2 & ~[0=0 & 1=0]
Split, 358
360 (0,1) e n2 & ~[0=0 & 1=0] => (0,1) e n2'
Split, 358
361 ALL(c2):[(0,c2) e n2 <=> 0 e n & c2 e n]
U Spec, 34
362 (0,1) e n2 <=> 0 e n & 1 e n
U Spec, 361
363 [(0,1) e n2 => 0 e n & 1 e n]
& [0 e n & 1 e n => (0,1) e n2]
Iff-And, 362
364 (0,1) e n2 => 0 e n & 1 e n
Split, 363
365 0 e n & 1 e n => (0,1) e n2
Split, 363
366 0 e n & 1 e n
Join, 3, 8
367 (0,1) e n2
Detach, 365, 366
368 0=0 & 1=0
Premise
369 0=0
Split, 368
370 1=0
Split, 368
371 1=0 & ~1=0
Join, 370, 9
372 ~[0=0 & 1=0]
4 Conclusion, 368
373 (0,1) e n2 & ~[0=0 & 1=0]
Join, 367, 372
374 (0,1) e n2'
Detach, 360, 373
375 pow'(0,1)=pow(0,1)
Detach, 355, 374
As Required:
376 pow'(0,1)=0
Substitute, 375, 353
377 x e n & ~x=0
Premise
378 x e n
Split, 377
379 ~x=0
Split, 377
380 x e n => pow'(x,2)=x*x
U Spec, 239
381 pow'(x,2)=x*x
Detach, 380, 378
382 ALL(b):[x e n & b e n & ~[x=0 & b=0]
=> pow'(x,b+1)=pow'(x,b)*x]
U Spec, 337
383 x e n & 1 e n & ~[x=0 & 1=0]
=> pow'(x,1+1)=pow'(x,1)*x
U Spec, 382
384 x=0 & 1=0
Premise
385 x=0
Split, 384
386 1=0
Split, 384
387 1=0 & ~1=0
Join, 386, 9
388 ~[x=0 & 1=0]
4 Conclusion, 384
389 x e n & 1 e n
Join, 378, 8
390 x e n & 1 e n & ~[x=0 & 1=0]
Join, 389, 388
391 pow'(x,1+1)=pow'(x,1)*x
Detach, 383, 390
392 pow'(x,2)=pow'(x,1)*x
Substitute, 11, 391
393 x*x=pow'(x,1)*x
Substitute, 381, 392
394 pow'(x,1)*x=x*x
Sym, 393
395 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, 18
396 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, 395
397 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, 396
398 ALL(b):[(x,b) e n2' => pow'(x,b) e n]
U Spec, 167
399 (x,1) e n2' => pow'(x,1) e n
U Spec, 398
400 ALL(b):[(x,b) e n2' <=> (x,b) e n2 & ~[x=0 & b=0]]
U Spec, 48
401 (x,1) e n2' <=> (x,1) e n2 & ~[x=0 & 1=0]
U Spec, 400
402 [(x,1) e n2' => (x,1) e n2 & ~[x=0 & 1=0]]
& [(x,1) e n2 & ~[x=0 & 1=0] => (x,1) e n2']
Iff-And, 401
403 (x,1) e n2' => (x,1) e n2 & ~[x=0 & 1=0]
Split, 402
404 (x,1) e n2 & ~[x=0 & 1=0] => (x,1) e n2'
Split, 402
405 ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]
U Spec, 34
406 (x,1) e n2 <=> x e n & 1 e n
U Spec, 405
407 [(x,1) e n2 => x e n & 1 e n]
& [x e n & 1 e n => (x,1) e n2]
Iff-And, 406
408 (x,1) e n2 => x e n & 1 e n
Split, 407
409 x e n & 1 e n => (x,1) e n2
Split, 407
410 x e n & 1 e n
Join, 378, 8
411 (x,1) e n2
Detach, 409, 410
412 x=0 & 1=0
Premise
413 x=0
Split, 412
414 1=0
Split, 412
415 1=0 & ~1=0
Join, 414, 9
416 ~[x=0 & 1=0]
4 Conclusion, 412
417 (x,1) e n2 & ~[x=0 & 1=0]
Join, 411, 416
418 (x,1) e n2'
Detach, 404, 417
419 pow'(x,1) e n
Detach, 399, 418
420 pow'(x,1) e n & x e n
Join, 419, 378
421 pow'(x,1) e n & x e n & x e n
Join, 420, 378
422 pow'(x,1) e n & x e n & x e n & ~x=0
Join, 421, 379
423 pow'(x,1)*x=x*x => pow'(x,1)=x
Detach, 397, 422
424 pow'(x,1)=x
Detach, 423, 394
425 ALL(b):[x e n & b e n & ~[x=0 & b=0]
=> pow'(x,b+1)=pow'(x,b)*x]
U Spec, 337
426 x e n & 0 e n & ~[x=0 & 0=0]
=> pow'(x,0+1)=pow'(x,0)*x
U Spec, 425
427 x=0 & 0=0
Premise
428 x=0
Split, 427
429 0=0
Split, 427
430 x=0 & ~x=0
Join, 428, 379
431 ~[x=0 & 0=0]
4 Conclusion, 427
432 x e n & 0 e n
Join, 378, 3
433 x e n & 0 e n & ~[x=0 & 0=0]
Join, 432, 431
434 pow'(x,0+1)=pow'(x,0)*x
Detach, 426, 433
435 pow'(x,1)=pow'(x,0)*x
Substitute, 348, 434
436 x=pow'(x,0)*x
Substitute, 424, 435
437 pow'(x,0)*x=x
Sym, 436
438 x e n => x*1=x
U Spec, 15
439 x*1=x
Detach, 438, 378
440 ALL(b):[x e n & b e n => x*b=b*x]
U Spec, 17
441 x e n & 1 e n => x*1=1*x
U Spec, 440
442 x e n & 1 e n
Join, 378, 8
443 x*1=1*x
Detach, 441, 442
444 1*x=x
Substitute, 443, 439
445 pow'(x,0)*x=1*x
Substitute, 444, 437
446 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, 18
447 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, 446
448 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, 447
449 ALL(b):[(x,b) e n2' => pow'(x,b) e n]
U Spec, 167
450 (x,0) e n2' => pow'(x,0) e n
U Spec, 449
451 ALL(b):[(x,b) e n2' <=> (x,b) e n2 & ~[x=0 & b=0]]
U Spec, 48
452 (x,0) e n2' <=> (x,0) e n2 & ~[x=0 & 0=0]
U Spec, 451
453 [(x,0) e n2' => (x,0) e n2 & ~[x=0 & 0=0]]
& [(x,0) e n2 & ~[x=0 & 0=0] => (x,0) e n2']
Iff-And, 452
454 (x,0) e n2' => (x,0) e n2 & ~[x=0 & 0=0]
Split, 453
455 (x,0) e n2 & ~[x=0 & 0=0] => (x,0) e n2'
Split, 453
456 ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]
U Spec, 34
457 (x,0) e n2 <=> x e n & 0 e n
U Spec, 456
458 [(x,0) e n2 => x e n & 0 e n]
& [x e n & 0 e n => (x,0) e n2]
Iff-And, 457
459 (x,0) e n2 => x e n & 0 e n
Split, 458
460 x e n & 0 e n => (x,0) e n2
Split, 458
461 x e n & 0 e n
Join, 378, 3
462 (x,0) e n2
Detach, 460, 461
463 (x,0) e n2 & ~[x=0 & 0=0]
Join, 462, 431
464 (x,0) e n2'
Detach, 455, 463
465 pow'(x,0) e n
Detach, 450, 464
466 pow'(x,0) e n & x e n
Join, 465, 378
467 pow'(x,0) e n & x e n & 1 e n
Join, 466, 8
468 pow'(x,0) e n & x e n & 1 e n & ~x=0
Join, 467, 379
469 pow'(x,0)*x=1*x => pow'(x,0)=1
Detach, 448, 468
470 pow'(x,0)=1
Detach, 469, 445
As Required:
471 ALL(a):[a e n & ~a=0 => pow'(a,0)=1]
4 Conclusion, 377
472 ALL(a):ALL(b):[a e n & b e n & ~[a=0 & b=0] => pow'(a,b) e n]
& pow'(0,1)=0
Join, 315, 376
473 ALL(a):ALL(b):[a e n & b e n & ~[a=0 & b=0] => pow'(a,b) e n]
& pow'(0,1)=0
& ALL(a):[a e n => pow'(a,2)=a*a]
Join, 472, 239
474 ALL(a):ALL(b):[a e n & b e n & ~[a=0 & b=0] => pow'(a,b) e n]
& pow'(0,1)=0
& ALL(a):[a e n => pow'(a,2)=a*a]
& ALL(a):ALL(b):[a e n & b e n & ~[a=0 & b=0]
=> pow'(a,b+1)=pow'(a,b)*a]
Join, 473, 337
As Required: (with pow(a,2))
475 EXIST(pow):[ALL(a):ALL(b):[a e n & b e n & ~[a=0 & b=0] => pow(a,b) e n]
& pow(0,1)=0
& ALL(a):[a e n => pow(a,2)=a*a]
& ALL(a):ALL(b):[a e n & b e n & ~[a=0 & b=0]
=> pow(a,b+1)=pow(a,b)*a]]
E Gen, 474
476 ALL(a):ALL(b):[a e n & b e n & ~[a=0 & b=0] => pow'(a,b) e n]
& ALL(a):[a e n & ~a=0 => pow'(a,0)=1]
Join, 315, 471
477 ALL(a):ALL(b):[a e n & b e n & ~[a=0 & b=0] => pow'(a,b) e n]
& ALL(a):[a e n & ~a=0 => pow'(a,0)=1]
& pow'(0,1)=0
Join, 476, 376
478 ALL(a):ALL(b):[a e n & b e n & ~[a=0 & b=0] => pow'(a,b) e n]
& ALL(a):[a e n & ~a=0 => pow'(a,0)=1]
& pow'(0,1)=0
& ALL(a):ALL(b):[a e n & b e n & ~[a=0 & b=0]
=> pow'(a,b+1)=pow'(a,b)*a]
Join, 477, 337
Equivalently and much easier to work with...
As Required: (with pow(a,0))
479 EXIST(pow):[ALL(a):ALL(b):[a e n & b e n & ~[a=0 & b=0] => pow(a,b) e n]
& ALL(a):[a e n & ~a=0 => pow(a,0)=1]
& pow(0,1)=0
& ALL(a):ALL(b):[a e n & b e n & ~[a=0 & b=0]
=> pow(a,b+1)=pow(a,b)*a]]
E Gen, 478