THEOREM
*******
ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => a^b*a^c=a^(b+c)] <=> 0^0=0 | 0^0=1
(This proof was written with the aid of the author's DC Proof 2.0 software available at http://www.dcproof.com )
BASIC PROPERTIES OF ARITHMETIC USED
***********************************
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
0 is additive identity element
6 ALL(a):[a e n => a+0=a]
Axiom
7 ALL(a):[a e n => a*0=0]
Axiom
1 is the multiplicative identity element
8 ALL(a):[a e n => a*1=a]
Axiom
The principle of mathematical induction (starting at 0)
9 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
Associativity of +
10 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => a+b+c=a+(b+c)]
Axiom
Commutativity of +
11 ALL(a):ALL(b):[a e n & b e n => a+b=b+a]
Axiom
Associativity of *
12 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => a*b*c=a*(b*c)]
Axiom
Commutativity of *
13 ALL(a):ALL(b):[a e n & b e n => a*b=b*a]
Axiom
14 ALL(a):[a e n => [a=a*a => a=0 | a=1]]
Axiom
Define: ^
*********
15 ALL(a):ALL(b):[a e n & b e n => a^b e n]
Axiom
16 ALL(a):[a e n => [~a=0 => a^0=1]]
Axiom
17 ALL(a):ALL(b):[a e n & b e n => a^(b+1)=a^b*a]
Axiom
PROOF
*****
'=>'
Prove: ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => a^b * a^c = a^(b+c)]
=> 0^0=0 | 0^0=1
Suppose...
18 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => a^b*a^c=a^(b+c)]
Premise
Apply premise
19 ALL(b):ALL(c):[0 e n & b e n & c e n => 0^b*0^c=0^(b+c)]
U Spec, 18
20 ALL(c):[0 e n & 0 e n & c e n => 0^0*0^c=0^(0+c)]
U Spec, 19
21 0 e n & 0 e n & 0 e n => 0^0*0^0=0^(0+0)
U Spec, 20
22 0 e n & 0 e n
Join, 4, 4
23 0 e n & 0 e n & 0 e n
Join, 22, 4
24 0^0*0^0=0^(0+0)
Detach, 21, 23
25 0 e n => 0+0=0
U Spec, 6
26 0+0=0
Detach, 25, 4
27 0^0*0^0=0^0
Substitute, 26, 24
28 0^0 e n => [0^0=0^0*0^0 => 0^0=0 | 0^0=1]
U Spec, 14
29 ALL(b):[0 e n & b e n => 0^b e n]
U Spec, 15
30 0 e n & 0 e n => 0^0 e n
U Spec, 29
31 0 e n & 0 e n
Join, 4, 4
32 0^0 e n
Detach, 30, 31
33 0^0=0^0*0^0 => 0^0=0 | 0^0=1
Detach, 28, 32
34 0^0=0^0*0^0
Sym, 27
35 0^0=0 | 0^0=1
Detach, 33, 34
As Required:
36 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => a^b*a^c=a^(b+c)]
=> 0^0=0 | 0^0=1
4 Conclusion, 18
'<='
Prove: 0^0=0 | 0^0=1
=> ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => a^b*a^c=a^(b+c)]
Suppose...
37 0^0=0 | 0^0=1
Premise
Case 1
Prove: f(0,0)=0
=> ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => a^b * a^c = a^(b+c)]
Suppose...
38 0^0=0
Premise
Prove: ALL(a):[a e n => ALL(b):[b e n => a^b*a^0=a^(b+0)]]
Suppose...
39 x e n
Premise
Construct subset of n for induction
Apply Subset Axiom
40 EXIST(sub):[Set(sub) & ALL(b):[b e sub <=> b e n & x^b*x^0=x^(b+0)]]
Subset, 1
41 Set(p1) & ALL(b):[b e p1 <=> b e n & x^b*x^0=x^(b+0)]
E Spec, 40
Define: p1
**********
42 Set(p1)
Split, 41
43 ALL(b):[b e p1 <=> b e n & x^b*x^0=x^(b+0)]
Split, 41
Apply PMI for p1
44 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, 9
Prove: p1 is a subset of n
Suppose...
45 q e p1
Premise
Apply defintion of p1
46 q e p1 <=> q e n & x^q*x^0=x^(q+0)
U Spec, 43
47 [q e p1 => q e n & x^q*x^0=x^(q+0)]
& [q e n & x^q*x^0=x^(q+0) => q e p1]
Iff-And, 46
48 q e p1 => q e n & x^q*x^0=x^(q+0)
Split, 47
49 q e n & x^q*x^0=x^(q+0) => q e p1
Split, 47
50 q e n & x^q*x^0=x^(q+0)
Detach, 48, 45
51 q e n
Split, 50
p1 is a subset of n
As Required:
52 ALL(b):[b e p1 => b e n]
4 Conclusion, 45
53 Set(p1) & ALL(b):[b e p1 => b e n]
Join, 42, 52
Sufficient: For ALL(b):[b e n => b e p1]
54 0 e p1 & ALL(b):[b e p1 => b+1 e p1]
=> ALL(b):[b e n => b e p1]
Detach, 44, 53
Base case
Prove: 0 e p1
Apply definition of p1
55 0 e p1 <=> 0 e n & x^0*x^0=x^(0+0)
U Spec, 43
56 [0 e p1 => 0 e n & x^0*x^0=x^(0+0)]
& [0 e n & x^0*x^0=x^(0+0) => 0 e p1]
Iff-And, 55
57 0 e p1 => 0 e n & x^0*x^0=x^(0+0)
Split, 56
Sufficient: For 0 e p1
58 0 e n & x^0*x^0=x^(0+0) => 0 e p1
Split, 56
Two cases:
59 x=0 | ~x=0
Or Not
Case 1
Prove: x=0 => 0 e p1
Suppose...
60 x=0
Premise
61 x^0=0
Substitute, 60, 38
62 0 e n => 0+0=0
U Spec, 6
63 0+0=0
Detach, 62, 4
64 x^(0+0)=0
Substitute, 63, 61
65 0 e n => 0*0=0
U Spec, 7
66 0*0=0
Detach, 65, 4
67 x^0*x^0=0
Substitute, 61, 66
68 x^0*x^0=x^(0+0)
Substitute, 64, 67
69 0 e n & x^0*x^0=x^(0+0)
Join, 4, 68
70 0 e p1
Detach, 58, 69
As Required:
71 x=0 => 0 e p1
4 Conclusion, 60
Case 2
Prove:
Suppose...
72 ~x=0
Premise
Apply definiton of ^
73 x e n => [~x=0 => x^0=1]
U Spec, 16
74 ~x=0 => x^0=1
Detach, 73, 39
75 x^0=1
Detach, 74, 72
76 0 e n => 0+0=0
U Spec, 6
77 0+0=0
Detach, 76, 4
78 x^(0+0)=1
Substitute, 77, 75
79 1 e n => 1*1=1
U Spec, 8
80 1*1=1
Detach, 79, 5
81 x^0*x^0=1
Substitute, 75, 80
82 x^0*x^0=x^(0+0)
Substitute, 78, 81
83 0 e n & x^0*x^0=x^(0+0)
Join, 4, 82
84 0 e p1
Detach, 58, 83
As Required:
85 ~x=0 => 0 e p1
4 Conclusion, 72
86 [x=0 => 0 e p1] & [~x=0 => 0 e p1]
Join, 71, 85
As Required:
87 0 e p1
Cases, 59, 86
Prove: ALL(b):[b e p1 => b+1 e p1]
Suppose...
88 y e p1
Premise
Apply definition of p1
89 y e p1 <=> y e n & x^y*x^0=x^(y+0)
U Spec, 43
90 [y e p1 => y e n & x^y*x^0=x^(y+0)]
& [y e n & x^y*x^0=x^(y+0) => y e p1]
Iff-And, 89
91 y e p1 => y e n & x^y*x^0=x^(y+0)
Split, 90
92 y e n & x^y*x^0=x^(y+0) => y e p1
Split, 90
93 y e n & x^y*x^0=x^(y+0)
Detach, 91, 88
94 y e n
Split, 93
95 x^y*x^0=x^(y+0)
Split, 93
Apply definition of p1
96 y+1 e p1 <=> y+1 e n & x^(y+1)*x^0=x^(y+1+0)
U Spec, 43
97 [y+1 e p1 => y+1 e n & x^(y+1)*x^0=x^(y+1+0)]
& [y+1 e n & x^(y+1)*x^0=x^(y+1+0) => y+1 e p1]
Iff-And, 96
98 y+1 e p1 => y+1 e n & x^(y+1)*x^0=x^(y+1+0)
Split, 97
Sufficient: For y+1 e p1
99 y+1 e n & x^(y+1)*x^0=x^(y+1+0) => y+1 e p1
Split, 97
100 ALL(b):[y e n & b e n => y+b e n]
U Spec, 2
101 y e n & 1 e n => y+1 e n
U Spec, 100
102 y e n & 1 e n
Join, 94, 5
103 y+1 e n
Detach, 101, 102
104 x^(y+1)*x^0=x^(y+1)*x^0
Reflex
Apply definition of ^
105 ALL(b):[x e n & b e n => x^(b+1)=x^b*x]
U Spec, 17
106 x e n & y e n => x^(y+1)=x^y*x
U Spec, 105
107 x e n & y e n
Join, 39, 94
108 x^(y+1)=x^y*x
Detach, 106, 107
109 x^(y+1)*x^0=x^y*x*x^0
Substitute, 108, 104
Apply associativity of *
110 ALL(b):ALL(c):[x^y e n & b e n & c e n => x^y*b*c=x^y*(b*c)]
U Spec, 12
111 ALL(c):[x^y e n & x e n & c e n => x^y*x*c=x^y*(x*c)]
U Spec, 110
112 x^y e n & x e n & x^0 e n => x^y*x*x^0=x^y*(x*x^0)
U Spec, 111
Apply definition of ^
113 ALL(b):[x e n & b e n => x^b e n]
U Spec, 15
114 x e n & y e n => x^y e n
U Spec, 113
115 x e n & y e n
Join, 39, 94
116 x^y e n
Detach, 114, 115
117 ALL(b):[x e n & b e n => x^b e n]
U Spec, 15
118 x e n & 0 e n => x^0 e n
U Spec, 117
119 x e n & 0 e n
Join, 39, 4
120 x^0 e n
Detach, 118, 119
121 x^y e n & x e n
Join, 116, 39
122 x^y e n & x e n & x^0 e n
Join, 121, 120
123 x^y*x*x^0=x^y*(x*x^0)
Detach, 112, 122
124 x^(y+1)*x^0=x^y*(x*x^0)
Substitute, 123, 109
Appy commutativity of *
125 ALL(b):[x e n & b e n => x*b=b*x]
U Spec, 13
126 x e n & x^0 e n => x*x^0=x^0*x
U Spec, 125
127 x e n & x^0 e n
Join, 39, 120
128 x*x^0=x^0*x
Detach, 126, 127
129 x^(y+1)*x^0=x^y*(x^0*x)
Substitute, 128, 124
Apply associativity of *
130 ALL(b):ALL(c):[x^y e n & b e n & c e n => x^y*b*c=x^y*(b*c)]
U Spec, 12
131 ALL(c):[x^y e n & x^0 e n & c e n => x^y*x^0*c=x^y*(x^0*c)]
U Spec, 130
132 x^y e n & x^0 e n & x e n => x^y*x^0*x=x^y*(x^0*x)
U Spec, 131
133 x^y e n & x^0 e n
Join, 116, 120
134 x^y e n & x^0 e n & x e n
Join, 133, 39
135 x^y*x^0*x=x^y*(x^0*x)
Detach, 132, 134
136 x^(y+1)*x^0=x^y*x^0*x
Substitute, 135, 129
LHS
137 x^(y+1)*x^0=x^(y+0)*x
Substitute, 95, 136
138 x^(y+1+0)=x^(y+1+0)
Reflex
Apply associativity of +
139 ALL(b):ALL(c):[y e n & b e n & c e n => y+b+c=y+(b+c)]
U Spec, 10
140 ALL(c):[y e n & 1 e n & c e n => y+1+c=y+(1+c)]
U Spec, 139
141 y e n & 1 e n & 0 e n => y+1+0=y+(1+0)
U Spec, 140
142 y e n & 1 e n
Join, 94, 5
143 y e n & 1 e n & 0 e n
Join, 142, 4
144 y+1+0=y+(1+0)
Detach, 141, 143
145 x^(y+1+0)=x^(y+(1+0))
Substitute, 144, 138
Apply commutativity of +
146 ALL(b):[1 e n & b e n => 1+b=b+1]
U Spec, 11
147 1 e n & 0 e n => 1+0=0+1
U Spec, 146
148 1 e n & 0 e n
Join, 5, 4
149 1+0=0+1
Detach, 147, 148
150 x^(y+1+0)=x^(y+(0+1))
Substitute, 149, 145
Apply associativity of +
151 ALL(b):ALL(c):[y e n & b e n & c e n => y+b+c=y+(b+c)]
U Spec, 10
152 ALL(c):[y e n & 0 e n & c e n => y+0+c=y+(0+c)]
U Spec, 151
153 y e n & 0 e n & 1 e n => y+0+1=y+(0+1)
U Spec, 152
154 y e n & 0 e n
Join, 94, 4
155 y e n & 0 e n & 1 e n
Join, 154, 5
156 y+0+1=y+(0+1)
Detach, 153, 155
157 x^(y+1+0)=x^(y+0+1)
Substitute, 156, 150
Apply definition of ^
158 ALL(b):[x e n & b e n => x^(b+1)=x^b*x]
U Spec, 17
159 x e n & y+0 e n => x^(y+0+1)=x^(y+0)*x
U Spec, 158
160 ALL(b):[y e n & b e n => y+b e n]
U Spec, 2
161 y e n & 0 e n => y+0 e n
U Spec, 160
162 y e n & 0 e n
Join, 94, 4
163 y+0 e n
Detach, 161, 162
164 x e n & y+0 e n
Join, 39, 163
165 x^(y+0+1)=x^(y+0)*x
Detach, 159, 164
RHS
166 x^(y+1+0)=x^(y+0)*x
Substitute, 165, 157
167 x^(y+1)*x^0=x^(y+1+0)
Substitute, 166, 137
168 y+1 e n & x^(y+1)*x^0=x^(y+1+0)
Join, 103, 167
169 y+1 e p1
Detach, 99, 168
As Required:
170 ALL(b):[b e p1 => b+1 e p1]
4 Conclusion, 88
171 0 e p1 & ALL(b):[b e p1 => b+1 e p1]
Join, 87, 170
By induction...
As Required:
172 ALL(b):[b e n => b e p1]
Detach, 54, 171
Prove: ALL(b):[b e n => x^b*x^0=x^(b+0)]
Suppose...
173 y e n
Premise
174 y e n => y e p1
U Spec, 172
175 y e p1
Detach, 174, 173
Apply definition of p1
176 y e p1 <=> y e n & x^y*x^0=x^(y+0)
U Spec, 43
177 [y e p1 => y e n & x^y*x^0=x^(y+0)]
& [y e n & x^y*x^0=x^(y+0) => y e p1]
Iff-And, 176
178 y e p1 => y e n & x^y*x^0=x^(y+0)
Split, 177
179 y e n & x^y*x^0=x^(y+0) => y e p1
Split, 177
180 y e n & x^y*x^0=x^(y+0)
Detach, 178, 175
181 y e n
Split, 180
182 x^y*x^0=x^(y+0)
Split, 180
As Required:
183 ALL(b):[b e n => x^b*x^0=x^(b+0)]
4 Conclusion, 173
As Required:
184 ALL(a):[a e n => ALL(b):[b e n => a^b*a^0=a^(b+0)]]
4 Conclusion, 39
Prove: ALL(a):ALL(b):[a e n & b e n => a^b*a^0=a^(b+0)]
Suppose...
185 x e n & y e n
Premise
186 x e n
Split, 185
187 y e n
Split, 185
Apply definition of ^
188 x e n => ALL(b):[b e n => x^b*x^0=x^(b+0)]
U Spec, 184
189 ALL(b):[b e n => x^b*x^0=x^(b+0)]
Detach, 188, 186
190 y e n => x^y*x^0=x^(y+0)
U Spec, 189
191 x^y*x^0=x^(y+0)
Detach, 190, 187
As Required:
192 ALL(a):ALL(b):[a e n & b e n => a^b*a^0=a^(b+0)]
4 Conclusion, 185
Prove: ALL(a):ALL(b):[a e n & b e n => ALL(c):[c e n => a^b*a^c=a^(b+c)]]
Suppose...
193 x e n & y e n
Premise
194 x e n
Split, 193
195 y e n
Split, 193
196 EXIST(sub):[Set(sub) & ALL(c):[c e sub <=> c e n & x^y*x^c=x^(y+c)]]
Subset, 1
197 Set(p2) & ALL(c):[c e p2 <=> c e n & x^y*x^c=x^(y+c)]
E Spec, 196
Define: p2
**********
198 Set(p2)
Split, 197
199 ALL(c):[c e p2 <=> c e n & x^y*x^c=x^(y+c)]
Split, 197
200 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, 9
Prove: ALL(b):[b e p2 => b e n]
Suppose...
201 q e p2
Premise
202 q e p2 <=> q e n & x^y*x^q=x^(y+q)
U Spec, 199
203 [q e p2 => q e n & x^y*x^q=x^(y+q)]
& [q e n & x^y*x^q=x^(y+q) => q e p2]
Iff-And, 202
204 q e p2 => q e n & x^y*x^q=x^(y+q)
Split, 203
205 q e n & x^y*x^q=x^(y+q) => q e p2
Split, 203
206 q e n & x^y*x^q=x^(y+q)
Detach, 204, 201
207 q e n
Split, 206
As Required:
208 ALL(b):[b e p2 => b e n]
4 Conclusion, 201
209 Set(p2) & ALL(b):[b e p2 => b e n]
Join, 198, 208
Sufficient: For ALL(b):[b e n => b e p2]
210 0 e p2 & ALL(b):[b e p2 => b+1 e p2]
=> ALL(b):[b e n => b e p2]
Detach, 200, 209
211 0 e p2 <=> 0 e n & x^y*x^0=x^(y+0)
U Spec, 199
212 [0 e p2 => 0 e n & x^y*x^0=x^(y+0)]
& [0 e n & x^y*x^0=x^(y+0) => 0 e p2]
Iff-And, 211
213 0 e p2 => 0 e n & x^y*x^0=x^(y+0)
Split, 212
Sufficient: For 0 e p2
214 0 e n & x^y*x^0=x^(y+0) => 0 e p2
Split, 212
215 ALL(b):[x e n & b e n => x^b*x^0=x^(b+0)]
U Spec, 192
216 x e n & y e n => x^y*x^0=x^(y+0)
U Spec, 215
217 x^y*x^0=x^(y+0)
Detach, 216, 193
218 0 e n & x^y*x^0=x^(y+0)
Join, 4, 217
As Required:
219 0 e p2
Detach, 214, 218
Prove: ALL(b):[b e p2 => b+1 e p2]
Suppose...
220 z e p2
Premise
221 z e p2 <=> z e n & x^y*x^z=x^(y+z)
U Spec, 199
222 [z e p2 => z e n & x^y*x^z=x^(y+z)]
& [z e n & x^y*x^z=x^(y+z) => z e p2]
Iff-And, 221
223 z e p2 => z e n & x^y*x^z=x^(y+z)
Split, 222
224 z e n & x^y*x^z=x^(y+z) => z e p2
Split, 222
225 z e n & x^y*x^z=x^(y+z)
Detach, 223, 220
226 z e n
Split, 225
227 x^y*x^z=x^(y+z)
Split, 225
228 z+1 e p2 <=> z+1 e n & x^y*x^(z+1)=x^(y+(z+1))
U Spec, 199
229 [z+1 e p2 => z+1 e n & x^y*x^(z+1)=x^(y+(z+1))]
& [z+1 e n & x^y*x^(z+1)=x^(y+(z+1)) => z+1 e p2]
Iff-And, 228
230 z+1 e p2 => z+1 e n & x^y*x^(z+1)=x^(y+(z+1))
Split, 229
Sufficient: For z+1 e p2
231 z+1 e n & x^y*x^(z+1)=x^(y+(z+1)) => z+1 e p2
Split, 229
232 ALL(b):[z e n & b e n => z+b e n]
U Spec, 2
233 z e n & 1 e n => z+1 e n
U Spec, 232
234 z e n & 1 e n
Join, 226, 5
235 z+1 e n
Detach, 233, 234
236 x^y*x^(z+1)=x^y*x^(z+1)
Reflex
237 ALL(b):[x e n & b e n => x^(b+1)=x^b*x]
U Spec, 17
238 x e n & z e n => x^(z+1)=x^z*x
U Spec, 237
239 x e n & z e n
Join, 194, 226
240 x^(z+1)=x^z*x
Detach, 238, 239
241 x^y*x^(z+1)=x^y*(x^z*x)
Substitute, 240, 236
242 ALL(b):ALL(c):[x^y e n & b e n & c e n => x^y*b*c=x^y*(b*c)]
U Spec, 12
243 ALL(c):[x^y e n & x^z e n & c e n => x^y*x^z*c=x^y*(x^z*c)]
U Spec, 242
244 x^y e n & x^z e n & x e n => x^y*x^z*x=x^y*(x^z*x)
U Spec, 243
245 ALL(b):[x e n & b e n => x^b e n]
U Spec, 15
246 x e n & y e n => x^y e n
U Spec, 245
247 x^y e n
Detach, 246, 193
248 x e n & z e n => x^z e n
U Spec, 245
249 x e n & z e n
Join, 194, 226
250 x^z e n
Detach, 248, 249
251 x^y e n & x^z e n
Join, 247, 250
252 x^y e n & x^z e n & x e n
Join, 251, 194
253 x^y*x^z*x=x^y*(x^z*x)
Detach, 244, 252
254 x^y*x^(z+1)=x^y*x^z*x
Substitute, 253, 241
LHS
255 x^y*x^(z+1)=x^(y+z)*x
Substitute, 227, 254
256 x^(y+(z+1))=x^(y+(z+1))
Reflex
257 ALL(b):ALL(c):[y e n & b e n & c e n => y+b+c=y+(b+c)]
U Spec, 10
258 ALL(c):[y e n & z e n & c e n => y+z+c=y+(z+c)]
U Spec, 257
259 y e n & z e n & 1 e n => y+z+1=y+(z+1)
U Spec, 258
260 y e n & z e n
Join, 195, 226
261 y e n & z e n & 1 e n
Join, 260, 5
262 y+z+1=y+(z+1)
Detach, 259, 261
263 x^(y+(z+1))=x^(y+z+1)
Substitute, 262, 256
264 ALL(b):[x e n & b e n => x^(b+1)=x^b*x]
U Spec, 17
265 x e n & y+z e n => x^(y+z+1)=x^(y+z)*x
U Spec, 264
266 ALL(b):[y e n & b e n => y+b e n]
U Spec, 2
267 y e n & z e n => y+z e n
U Spec, 266
268 y e n & z e n
Join, 195, 226
269 y+z e n
Detach, 267, 268
270 x e n & y+z e n
Join, 194, 269
271 x^(y+z+1)=x^(y+z)*x
Detach, 265, 270
RHS
272 x^(y+(z+1))=x^(y+z)*x
Substitute, 271, 263
273 x^y*x^(z+1)=x^(y+(z+1))
Substitute, 272, 255
274 z+1 e n & x^y*x^(z+1)=x^(y+(z+1))
Join, 235, 273
275 z+1 e p2
Detach, 231, 274
As Required:
276 ALL(b):[b e p2 => b+1 e p2]
4 Conclusion, 220
277 0 e p2 & ALL(b):[b e p2 => b+1 e p2]
Join, 219, 276
278 ALL(b):[b e n => b e p2]
Detach, 210, 277
Prove: ALL(c):[c e n => x^y*x^c=x^(y+c)]
Suppose...
279 z e n
Premise
280 z e n => z e p2
U Spec, 278
281 z e p2
Detach, 280, 279
282 z e p2 <=> z e n & x^y*x^z=x^(y+z)
U Spec, 199
283 [z e p2 => z e n & x^y*x^z=x^(y+z)]
& [z e n & x^y*x^z=x^(y+z) => z e p2]
Iff-And, 282
284 z e p2 => z e n & x^y*x^z=x^(y+z)
Split, 283
285 z e n & x^y*x^z=x^(y+z) => z e p2
Split, 283
286 z e n & x^y*x^z=x^(y+z)
Detach, 284, 281
287 z e n
Split, 286
288 x^y*x^z=x^(y+z)
Split, 286
As Required:
289 ALL(c):[c e n => x^y*x^c=x^(y+c)]
4 Conclusion, 279
As Required:
290 ALL(a):ALL(b):[a e n & b e n => ALL(c):[c e n => a^b*a^c=a^(b+c)]]
4 Conclusion, 193
Prove: ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => a^b*a^c=a^(b+c)]
Suppose...
291 x e n & y e n & z e n
Premise
292 x e n
Split, 291
293 y e n
Split, 291
294 z e n
Split, 291
295 ALL(b):[x e n & b e n => ALL(c):[c e n => x^b*x^c=x^(b+c)]]
U Spec, 290
296 x e n & y e n => ALL(c):[c e n => x^y*x^c=x^(y+c)]
U Spec, 295
297 x e n & y e n
Join, 292, 293
298 ALL(c):[c e n => x^y*x^c=x^(y+c)]
Detach, 296, 297
299 z e n => x^y*x^z=x^(y+z)
U Spec, 298
300 x^y*x^z=x^(y+z)
Detach, 299, 294
As Required:
301 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => a^b*a^c=a^(b+c)]
4 Conclusion, 291
As Required:
302 0^0=0
=> ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => a^b*a^c=a^(b+c)]
4 Conclusion, 38
Case 2
Prove: 0^0=1
=> ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => a^b*a^c=a^(b+c)]
Suppose...
303 0^0=1
Premise
Prove: ALL(a):[a e n => ALL(b):[b e n => a^b*a^0=a^(b+0)]]
Suppose...
304 x e n
Premise
305 EXIST(sub):[Set(sub) & ALL(b):[b e sub <=> b e n & x^b*x^0=x^(b+0)]]
Subset, 1
306 Set(p3) & ALL(b):[b e p3 <=> b e n & x^b*x^0=x^(b+0)]
E Spec, 305
Define: p3
**********
307 Set(p3)
Split, 306
308 ALL(b):[b e p3 <=> b e n & x^b*x^0=x^(b+0)]
Split, 306
Apply PMI for p3
309 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, 9
Prove: p3 is a subset of n
Suppose...
310 q e p3
Premise
311 q e p3 <=> q e n & x^q*x^0=x^(q+0)
U Spec, 308
312 [q e p3 => q e n & x^q*x^0=x^(q+0)]
& [q e n & x^q*x^0=x^(q+0) => q e p3]
Iff-And, 311
313 q e p3 => q e n & x^q*x^0=x^(q+0)
Split, 312
314 q e n & x^q*x^0=x^(q+0) => q e p3
Split, 312
315 q e n & x^q*x^0=x^(q+0)
Detach, 313, 310
316 q e n
Split, 315
As Required:
317 ALL(b):[b e p3 => b e n]
4 Conclusion, 310
318 Set(p3) & ALL(b):[b e p3 => b e n]
Join, 307, 317
Sufficient: For ALL(b):[b e n => b e p3]
319 0 e p3 & ALL(b):[b e p3 => b+1 e p3]
=> ALL(b):[b e n => b e p3]
Detach, 309, 318
320 0 e p3 <=> 0 e n & x^0*x^0=x^(0+0)
U Spec, 308
321 [0 e p3 => 0 e n & x^0*x^0=x^(0+0)]
& [0 e n & x^0*x^0=x^(0+0) => 0 e p3]
Iff-And, 320
322 0 e p3 => 0 e n & x^0*x^0=x^(0+0)
Split, 321
Sufficient: For 0 e p3
323 0 e n & x^0*x^0=x^(0+0) => 0 e p3
Split, 321
Two cases:
324 x=0 | ~x=0
Or Not
Case 1
Prove: x=0 => 0 e p3
Suppose...
325 x=0
Premise
326 x^0=1
Substitute, 325, 303
327 1 e n => 1*1=1
U Spec, 8
328 1*1=1
Detach, 327, 5
LHS
329 x^0*x^0=1
Substitute, 326, 328
330 0 e n => 0+0=0
U Spec, 6
331 0+0=0
Detach, 330, 4
RHS
332 x^(0+0)=1
Substitute, 331, 326
333 x^0*x^0=x^(0+0)
Substitute, 332, 329
334 0 e n & x^0*x^0=x^(0+0)
Join, 4, 333
335 0 e p3
Detach, 323, 334
As Required:
336 x=0 => 0 e p3
4 Conclusion, 325
Case 2
Prove: ~x=0 => 0 e p3
Suppose...
337 ~x=0
Premise
338 x e n => [~x=0 => x^0=1]
U Spec, 16
339 ~x=0 => x^0=1
Detach, 338, 304
340 x^0=1
Detach, 339, 337
341 1 e n => 1*1=1
U Spec, 8
342 1*1=1
Detach, 341, 5
LHS
343 x^0*x^0=1
Substitute, 340, 342
344 0 e n => 0+0=0
U Spec, 6
345 0+0=0
Detach, 344, 4
RHS
346 x^(0+0)=1
Substitute, 345, 340
347 x^0*x^0=x^(0+0)
Substitute, 346, 343
348 0 e n & x^0*x^0=x^(0+0)
Join, 4, 347
349 0 e p3
Detach, 323, 348
As Required:
350 ~x=0 => 0 e p3
4 Conclusion, 337
351 [x=0 => 0 e p3] & [~x=0 => 0 e p3]
Join, 336, 350
As Required:
352 0 e p3
Cases, 324, 351
Prove: ALL(b):[b e p3 => b+1 e p3]
Suppose...
353 y e p3
Premise
354 y e p3 <=> y e n & x^y*x^0=x^(y+0)
U Spec, 308
355 [y e p3 => y e n & x^y*x^0=x^(y+0)]
& [y e n & x^y*x^0=x^(y+0) => y e p3]
Iff-And, 354
356 y e p3 => y e n & x^y*x^0=x^(y+0)
Split, 355
357 y e n & x^y*x^0=x^(y+0) => y e p3
Split, 355
358 y e n & x^y*x^0=x^(y+0)
Detach, 356, 353
359 y e n
Split, 358
360 x^y*x^0=x^(y+0)
Split, 358
361 y+1 e p3 <=> y+1 e n & x^(y+1)*x^0=x^(y+1+0)
U Spec, 308
362 [y+1 e p3 => y+1 e n & x^(y+1)*x^0=x^(y+1+0)]
& [y+1 e n & x^(y+1)*x^0=x^(y+1+0) => y+1 e p3]
Iff-And, 361
363 y+1 e p3 => y+1 e n & x^(y+1)*x^0=x^(y+1+0)
Split, 362
Sufficient: For y+1 e p3 (as above)
364 y+1 e n & x^(y+1)*x^0=x^(y+1+0) => y+1 e p3
Split, 362
365 ALL(b):[y e n & b e n => y+b e n]
U Spec, 2
366 y e n & 1 e n => y+1 e n
U Spec, 365
367 y e n & 1 e n
Join, 359, 5
368 y+1 e n
Detach, 366, 367
369 x^(y+1)*x^0=x^(y+1)*x^0
Reflex
370 ALL(b):[x e n & b e n => x^(b+1)=x^b*x]
U Spec, 17
371 x e n & y e n => x^(y+1)=x^y*x
U Spec, 370
372 x e n & y e n
Join, 304, 359
373 x^(y+1)=x^y*x
Detach, 371, 372
374 x^(y+1)*x^0=x^y*x*x^0
Substitute, 373, 369
375 ALL(b):ALL(c):[x^y e n & b e n & c e n => x^y*b*c=x^y*(b*c)]
U Spec, 12
376 ALL(c):[x^y e n & x e n & c e n => x^y*x*c=x^y*(x*c)]
U Spec, 375
377 x^y e n & x e n & x^0 e n => x^y*x*x^0=x^y*(x*x^0)
U Spec, 376
378 ALL(b):[x e n & b e n => x^b e n]
U Spec, 15
379 x e n & y e n => x^y e n
U Spec, 378
380 x^y e n
Detach, 379, 372
381 x e n & 0 e n => x^0 e n
U Spec, 378
382 x e n & 0 e n
Join, 304, 4
383 x^0 e n
Detach, 381, 382
384 x^y e n & x e n
Join, 380, 304
385 x^y e n & x e n & x^0 e n
Join, 384, 383
386 x^y*x*x^0=x^y*(x*x^0)
Detach, 377, 385
387 x^(y+1)*x^0=x^y*(x*x^0)
Substitute, 386, 374
388 ALL(b):[x e n & b e n => x*b=b*x]
U Spec, 13
389 x e n & x^0 e n => x*x^0=x^0*x
U Spec, 388
390 x e n & x^0 e n
Join, 304, 383
391 x*x^0=x^0*x
Detach, 389, 390
392 x^(y+1)*x^0=x^y*(x^0*x)
Substitute, 391, 387
393 ALL(b):ALL(c):[x^y e n & b e n & c e n => x^y*b*c=x^y*(b*c)]
U Spec, 12
394 ALL(c):[x^y e n & x^0 e n & c e n => x^y*x^0*c=x^y*(x^0*c)]
U Spec, 393
395 x^y e n & x^0 e n & x e n => x^y*x^0*x=x^y*(x^0*x)
U Spec, 394
396 x^y e n & x^0 e n
Join, 380, 383
397 x^y e n & x^0 e n & x e n
Join, 396, 304
398 x^y*x^0*x=x^y*(x^0*x)
Detach, 395, 397
399 x^(y+1)*x^0=x^y*x^0*x
Substitute, 398, 392
LHS
400 x^(y+1)*x^0=x^(y+0)*x
Substitute, 360, 399
401 x^(y+1+0)=x^(y+1+0)
Reflex
402 ALL(b):ALL(c):[y e n & b e n & c e n => y+b+c=y+(b+c)]
U Spec, 10
403 ALL(c):[y e n & 1 e n & c e n => y+1+c=y+(1+c)]
U Spec, 402
404 y e n & 1 e n & 0 e n => y+1+0=y+(1+0)
U Spec, 403
405 y e n & 1 e n
Join, 359, 5
406 y e n & 1 e n & 0 e n
Join, 405, 4
407 y+1+0=y+(1+0)
Detach, 404, 406
408 x^(y+1+0)=x^(y+(1+0))
Substitute, 407, 401
409 ALL(b):[1 e n & b e n => 1+b=b+1]
U Spec, 11
410 1 e n & 0 e n => 1+0=0+1
U Spec, 409
411 1 e n & 0 e n
Join, 5, 4
412 1+0=0+1
Detach, 410, 411
413 x^(y+1+0)=x^(y+(0+1))
Substitute, 412, 408
414 ALL(b):ALL(c):[y e n & b e n & c e n => y+b+c=y+(b+c)]
U Spec, 10
415 ALL(c):[y e n & 0 e n & c e n => y+0+c=y+(0+c)]
U Spec, 414
416 y e n & 0 e n & 1 e n => y+0+1=y+(0+1)
U Spec, 415
417 y e n & 0 e n
Join, 359, 4
418 y e n & 0 e n & 1 e n
Join, 417, 5
419 y+0+1=y+(0+1)
Detach, 416, 418
420 x^(y+1+0)=x^(y+0+1)
Substitute, 419, 413
421 ALL(b):[x e n & b e n => x^(b+1)=x^b*x]
U Spec, 17
422 x e n & y+0 e n => x^(y+0+1)=x^(y+0)*x
U Spec, 421
423 ALL(b):[y e n & b e n => y+b e n]
U Spec, 2
424 y e n & 0 e n => y+0 e n
U Spec, 423
425 y e n & 0 e n
Join, 359, 4
426 y+0 e n
Detach, 424, 425
427 x e n & y+0 e n
Join, 304, 426
428 x^(y+0+1)=x^(y+0)*x
Detach, 422, 427
RHS
429 x^(y+1+0)=x^(y+0)*x
Substitute, 428, 420
430 x^(y+1)*x^0=x^(y+1+0)
Substitute, 429, 400
431 y+1 e n & x^(y+1)*x^0=x^(y+1+0)
Join, 368, 430
432 y+1 e p3
Detach, 364, 431
As Required:
433 ALL(b):[b e p3 => b+1 e p3]
4 Conclusion, 353
434 0 e p3 & ALL(b):[b e p3 => b+1 e p3]
Join, 352, 433
435 ALL(b):[b e n => b e p3]
Detach, 319, 434
Prove: ALL(b):[b e n => x^b*x^0=x^(b+0)]
Suppose...
436 y e n
Premise
437 y e n => y e p3
U Spec, 435
438 y e p3
Detach, 437, 436
439 y e p3 <=> y e n & x^y*x^0=x^(y+0)
U Spec, 308
440 [y e p3 => y e n & x^y*x^0=x^(y+0)]
& [y e n & x^y*x^0=x^(y+0) => y e p3]
Iff-And, 439
441 y e p3 => y e n & x^y*x^0=x^(y+0)
Split, 440
442 y e n & x^y*x^0=x^(y+0) => y e p3
Split, 440
443 y e n & x^y*x^0=x^(y+0)
Detach, 441, 438
444 y e n
Split, 443
445 x^y*x^0=x^(y+0)
Split, 443
As Required:
446 ALL(b):[b e n => x^b*x^0=x^(b+0)]
4 Conclusion, 436
As Required:
447 ALL(a):[a e n => ALL(b):[b e n => a^b*a^0=a^(b+0)]]
4 Conclusion, 304
Prove: ALL(a):ALL(b):[a e n & b e n => a^b*a^0=a^(b+0)]
Suppose...
448 x e n & y e n
Premise
449 x e n
Split, 448
450 y e n
Split, 448
451 x e n => ALL(b):[b e n => x^b*x^0=x^(b+0)]
U Spec, 447
452 ALL(b):[b e n => x^b*x^0=x^(b+0)]
Detach, 451, 449
453 y e n => x^y*x^0=x^(y+0)
U Spec, 452
454 x^y*x^0=x^(y+0)
Detach, 453, 450
As Required:
455 ALL(a):ALL(b):[a e n & b e n => a^b*a^0=a^(b+0)]
4 Conclusion, 448
456 x e n & y e n
Premise
457 x e n
Split, 456
458 y e n
Split, 456
459 EXIST(sub):[Set(sub) & ALL(c):[c e sub <=> c e n & x^y*x^c=x^(y+c)]]
Subset, 1
460 Set(p4) & ALL(c):[c e p4 <=> c e n & x^y*x^c=x^(y+c)]
E Spec, 459
Define: p4
**********
461 Set(p4)
Split, 460
462 ALL(c):[c e p4 <=> c e n & x^y*x^c=x^(y+c)]
Split, 460
463 Set(p4) & ALL(b):[b e p4 => b e n]
=> [0 e p4 & ALL(b):[b e p4 => b+1 e p4]
=> ALL(b):[b e n => b e p4]]
U Spec, 9
Prove: p4 is a subset of n
Suppose...
464 q e p4
Premise
465 q e p4 <=> q e n & x^y*x^q=x^(y+q)
U Spec, 462
466 [q e p4 => q e n & x^y*x^q=x^(y+q)]
& [q e n & x^y*x^q=x^(y+q) => q e p4]
Iff-And, 465
467 q e p4 => q e n & x^y*x^q=x^(y+q)
Split, 466
468 q e n & x^y*x^q=x^(y+q) => q e p4
Split, 466
469 q e n & x^y*x^q=x^(y+q)
Detach, 467, 464
470 q e n
Split, 469
As Required:
471 ALL(b):[b e p4 => b e n]
4 Conclusion, 464
472 Set(p4) & ALL(b):[b e p4 => b e n]
Join, 461, 471
Sufficient: For ALL(b):[b e n => b e p4]
473 0 e p4 & ALL(b):[b e p4 => b+1 e p4]
=> ALL(b):[b e n => b e p4]
Detach, 463, 472
474 0 e p4 <=> 0 e n & x^y*x^0=x^(y+0)
U Spec, 462
475 [0 e p4 => 0 e n & x^y*x^0=x^(y+0)]
& [0 e n & x^y*x^0=x^(y+0) => 0 e p4]
Iff-And, 474
476 0 e p4 => 0 e n & x^y*x^0=x^(y+0)
Split, 475
Sufficient: For 0 e p4 x^0*x^0=x^(0+0)???
477 0 e n & x^y*x^0=x^(y+0) => 0 e p4
Split, 475
478 ALL(b):[x e n & b e n => x^b*x^0=x^(b+0)]
U Spec, 455
479 x e n & y e n => x^y*x^0=x^(y+0)
U Spec, 478
480 x^y*x^0=x^(y+0)
Detach, 479, 456
481 0 e n & x^y*x^0=x^(y+0)
Join, 4, 480
As Required:
482 0 e p4
Detach, 477, 481
Prove: ALL(b):[b e p4 => b+1 e p4]
Suppose...
483 z e p4
Premise
484 z e p4 <=> z e n & x^y*x^z=x^(y+z)
U Spec, 462
485 [z e p4 => z e n & x^y*x^z=x^(y+z)]
& [z e n & x^y*x^z=x^(y+z) => z e p4]
Iff-And, 484
486 z e p4 => z e n & x^y*x^z=x^(y+z)
Split, 485
487 z e n & x^y*x^z=x^(y+z) => z e p4
Split, 485
488 z e n & x^y*x^z=x^(y+z)
Detach, 486, 483
489 z e n
Split, 488
490 x^y*x^z=x^(y+z)
Split, 488
491 z+1 e p4 <=> z+1 e n & x^y*x^(z+1)=x^(y+(z+1))
U Spec, 462
492 [z+1 e p4 => z+1 e n & x^y*x^(z+1)=x^(y+(z+1))]
& [z+1 e n & x^y*x^(z+1)=x^(y+(z+1)) => z+1 e p4]
Iff-And, 491
493 z+1 e p4 => z+1 e n & x^y*x^(z+1)=x^(y+(z+1))
Split, 492
Sufficient: For z+1 e p4
494 z+1 e n & x^y*x^(z+1)=x^(y+(z+1)) => z+1 e p4
Split, 492
495 ALL(b):[z e n & b e n => z+b e n]
U Spec, 2
496 z e n & 1 e n => z+1 e n
U Spec, 495
497 z e n & 1 e n
Join, 489, 5
498 z+1 e n
Detach, 496, 497
499 x^y*x^(z+1)=x^y*x^(z+1)
Reflex
500 ALL(b):[x e n & b e n => x^(b+1)=x^b*x]
U Spec, 17
501 x e n & z e n => x^(z+1)=x^z*x
U Spec, 500
502 x e n & z e n
Join, 457, 489
503 x^(z+1)=x^z*x
Detach, 501, 502
504 x^y*x^(z+1)=x^y*(x^z*x)
Substitute, 503, 499
505 ALL(b):ALL(c):[x^y e n & b e n & c e n => x^y*b*c=x^y*(b*c)]
U Spec, 12
506 ALL(c):[x^y e n & x^z e n & c e n => x^y*x^z*c=x^y*(x^z*c)]
U Spec, 505
507 x^y e n & x^z e n & x e n => x^y*x^z*x=x^y*(x^z*x)
U Spec, 506
508 ALL(b):[x e n & b e n => x^b e n]
U Spec, 15
509 x e n & y e n => x^y e n
U Spec, 508
510 x^y e n
Detach, 509, 456
511 x e n & z e n => x^z e n
U Spec, 508
512 x e n & z e n
Join, 457, 489
513 x^z e n
Detach, 511, 512
514 x^y e n & x^z e n
Join, 510, 513
515 x^y e n & x^z e n & x e n
Join, 514, 457
516 x^y*x^z*x=x^y*(x^z*x)
Detach, 507, 515
517 x^y*x^(z+1)=x^y*x^z*x
Substitute, 516, 504
LHS
518 x^y*x^(z+1)=x^(y+z)*x
Substitute, 490, 517
519 x^(y+(z+1))=x^(y+(z+1))
Reflex
520 ALL(b):ALL(c):[y e n & b e n & c e n => y+b+c=y+(b+c)]
U Spec, 10
521 ALL(c):[y e n & z e n & c e n => y+z+c=y+(z+c)]
U Spec, 520
522 y e n & z e n & 1 e n => y+z+1=y+(z+1)
U Spec, 521
523 y e n & z e n
Join, 458, 489
524 y e n & z e n & 1 e n
Join, 523, 5
525 y+z+1=y+(z+1)
Detach, 522, 524
526 x^(y+(z+1))=x^(y+z+1)
Substitute, 525, 519
527 ALL(b):[x e n & b e n => x^(b+1)=x^b*x]
U Spec, 17
528 x e n & y+z e n => x^(y+z+1)=x^(y+z)*x
U Spec, 527
529 ALL(b):[y e n & b e n => y+b e n]
U Spec, 2
530 y e n & z e n => y+z e n
U Spec, 529
531 y e n & z e n
Join, 458, 489
532 y+z e n
Detach, 530, 531
533 x e n & y+z e n
Join, 457, 532
534 x^(y+z+1)=x^(y+z)*x
Detach, 528, 533
RHS
535 x^(y+(z+1))=x^(y+z)*x
Substitute, 534, 526
536 x^y*x^(z+1)=x^(y+(z+1))
Substitute, 535, 518
537 z+1 e n & x^y*x^(z+1)=x^(y+(z+1))
Join, 498, 536
538 z+1 e p4
Detach, 494, 537
As Required:
539 ALL(b):[b e p4 => b+1 e p4]
4 Conclusion, 483
540 0 e p4 & ALL(b):[b e p4 => b+1 e p4]
Join, 482, 539
As Required:
541 ALL(b):[b e n => b e p4]
Detach, 473, 540
Prove: ALL(c):[c e n => x^y*x^c=x^(y+c)]
Suppose...
542 z e n
Premise
543 z e n => z e p4
U Spec, 541
544 z e p4
Detach, 543, 542
545 z e p4 <=> z e n & x^y*x^z=x^(y+z)
U Spec, 462
546 [z e p4 => z e n & x^y*x^z=x^(y+z)]
& [z e n & x^y*x^z=x^(y+z) => z e p4]
Iff-And, 545
547 z e p4 => z e n & x^y*x^z=x^(y+z)
Split, 546
548 z e n & x^y*x^z=x^(y+z) => z e p4
Split, 546
549 z e n & x^y*x^z=x^(y+z)
Detach, 547, 544
550 z e n
Split, 549
551 x^y*x^z=x^(y+z)
Split, 549
As Required:
552 ALL(c):[c e n => x^y*x^c=x^(y+c)]
4 Conclusion, 542
As Required:
553 ALL(a):ALL(b):[a e n & b e n => ALL(c):[c e n => a^b*a^c=a^(b+c)]]
4 Conclusion, 456
Prove: ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => a^b*a^c=a^(b+c)]
Suppose...
554 x e n & y e n & z e n
Premise
555 x e n
Split, 554
556 y e n
Split, 554
557 z e n
Split, 554
558 ALL(b):[x e n & b e n => ALL(c):[c e n => x^b*x^c=x^(b+c)]]
U Spec, 553
559 x e n & y e n => ALL(c):[c e n => x^y*x^c=x^(y+c)]
U Spec, 558
560 x e n & y e n
Join, 555, 556
561 ALL(c):[c e n => x^y*x^c=x^(y+c)]
Detach, 559, 560
562 z e n => x^y*x^z=x^(y+z)
U Spec, 561
563 x^y*x^z=x^(y+z)
Detach, 562, 557
As Required:
564 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => a^b*a^c=a^(b+c)]
4 Conclusion, 554
As Required:
565 0^0=1
=> ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => a^b*a^c=a^(b+c)]
4 Conclusion, 303
566 [0^0=0
=> ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => a^b*a^c=a^(b+c)]]
& [0^0=1
=> ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => a^b*a^c=a^(b+c)]]
Join, 302, 565
567 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => a^b*a^c=a^(b+c)]
Cases, 37, 566
As Required:
568 0^0=0 | 0^0=1
=> ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => a^b*a^c=a^(b+c)]
4 Conclusion, 37
569 [ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => a^b*a^c=a^(b+c)]
=> 0^0=0 | 0^0=1]
& [0^0=0 | 0^0=1
=> ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => a^b*a^c=a^(b+c)]]
Join, 36, 568
As Required:
570 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => a^b*a^c=a^(b+c)]
<=> 0^0=0 | 0^0=1
Iff-And, 569