THEOREM

*******

a^b^c=a^(b*c) (for non-zero base (a) OR both non-zero exponents (b and c)

ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => [~a=0 | ~b=0 & ~c=0 => a^b^c=a^(b*c)]]

This machine-verified, formal proof was written with the aid of the author's DC Proof 2.0 freeware available at http://www.dcproof.com

Dan Christensen

2019-11-10

OUTLINE

*******

Lines Content

***** *******

1-16 Axioms/Definitions

17-19 Lemmas (links to proofs)

25-212 Case 1: Prove that ~x=0 => x^y^z=x^(y*z) (by induction)

213-243 Case 2: Prove that ~y=0 & ~z=0 => x^y^z=x^(y*z)

AXIOMS/DEFINTITIONS

*******************

Define: n, 0, 1

1 Set(n)

Axiom

2 0 e n

Axiom

3 1 e n

Axiom

Properties of +

***************

Closed on n

4 ALL(a):ALL(b):[a e n & b e n => a+b e n]

Axiom

5 ALL(a):[a e n => a+0=a & 0+a=a]

Axiom

Properties of *

***************

Closed on n

6 ALL(a):ALL(b):[a e n & b e n => a*b e n]

Axiom

Multiplying by 0

7 ALL(a):[a e n => a*0=0]

Axiom

Multiplying by 1

8 ALL(a):[a e n => a*1=a & 1*a=a]

Axiom

Multiplying both sides

9 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => [a=b => a*c=b*c]]

Axiom

* Distributive over +

10 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => a*(b+c)=a*b+a*c]

Axiom

Product of non-zeroes

11 ALL(a):ALL(b):[a e n & b e n => [~a=0 & ~b=0 => ~a*b=0]]

Axiom

Induction principle

12 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

Define: ^ on n

**************

13 ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => a^b e n]]

Axiom

14 0^1=0

Axiom

15 ALL(a):[a e n => [~a=0 => a^0=1]]

Axiom

16 ALL(a):ALL(b):[a e n & b e n

=> [~[a=0 & b=0] => a^(b+1)=a^b*a]]

Axiom

LEMMAS

******

Non-zero powers of zero are zero Proof

17 ALL(a):[a e n => [~a=0 => 0^a=0]]

Axiom

Powers of non-zero bases are non-zero Proof

18 ALL(a):ALL(b):[a e n & b e n => [~a=0 => ~a^b=0]]

Axiom

Product of Powers Proof

19 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n

=> [~a=0 | ~b=0 & ~c=0 => a^b*a^c=a^(b+c)]]

Axiom

PROOF

*****

Prove: ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n

=> [~a=0 | ~b=0 & ~c=0 => a^b^c=a^(b*c)]]

Suppose...

20 x e n & y e n & z e n

Premise

21 x e n

Split, 20

22 y e n

Split, 20

23 z e n

Split, 20

Prove: ~x=0 | ~y=0 & ~z=0 => x^y^z=x^(y*z)

Suppose... (two cases to consider)

24 ~x=0 | ~y=0 & ~z=0

Premise

Case 1

Prove: ~x=0 => x^y^z=x^(y*z) (by induction)

Suppose...

25 ~x=0

Premise

Construct set p for proof by induction

26 EXIST(sub):[Set(sub) & ALL(c):[c e sub <=> c e n & x^y^c=x^(y*c)]]

Subset, 1

27 Set(p) & ALL(c):[c e p <=> c e n & x^y^c=x^(y*c)]

E Spec, 26

Define: p

28 Set(p)

Split, 27

29 ALL(c):[c e p <=> c e n & x^y^c=x^(y*c)]

Split, 27

Apply principle of induction

30 Set(p) & ALL(b):[b e p => b e n]

=> [0 e p & ALL(b):[b e p => b+1 e p]

=> ALL(b):[b e n => b e p]]

U Spec, 12

Prove: ALL(b):[b e p => b e n]

Suppose...

31 t e p

Premise

Apply definition of p

32 t e p <=> t e n & x^y^t=x^(y*t)

U Spec, 29

33 [t e p => t e n & x^y^t=x^(y*t)]

& [t e n & x^y^t=x^(y*t) => t e p]

Iff-And, 32

34 t e p => t e n & x^y^t=x^(y*t)

Split, 33

35 t e n & x^y^t=x^(y*t) => t e p

Split, 33

36 t e n & x^y^t=x^(y*t)

Detach, 34, 31

37 t e n

Split, 36

As Required:

38 ALL(b):[b e p => b e n]

4 Conclusion, 31

39 Set(p) & ALL(b):[b e p => b e n]

Join, 28, 38

Sufficient: For ALL(b):[b e n => b e p]

40 0 e p & ALL(b):[b e p => b+1 e p]

=> ALL(b):[b e n => b e p]

Detach, 30, 39

BASE CASE

*********

Apply definition of p

41 0 e p <=> 0 e n & x^y^0=x^(y*0)

U Spec, 29

42 [0 e p => 0 e n & x^y^0=x^(y*0)]

& [0 e n & x^y^0=x^(y*0) => 0 e p]

Iff-And, 41

43 0 e p => 0 e n & x^y^0=x^(y*0)

Split, 42

Sufficient: For 0 e p

44 0 e n & x^y^0=x^(y*0) => 0 e p

Split, 42

45 ALL(b):[x e n & b e n => [~[x=0 & b=0] => x^b e n]]

U Spec, 13

46 x e n & y e n => [~[x=0 & y=0] => x^y e n]

U Spec, 45

47 x e n & y e n

Join, 21, 22

48 ~[x=0 & y=0] => x^y e n

Detach, 46, 47

Prove: ~[x=0 & y=0]

Suppose to the contrary...

49 x=0 & y=0

Premise

50 x=0

Split, 49

51 y=0

Split, 49

52 x=0 & ~x=0

Join, 50, 25

As Required:

53 ~[x=0 & y=0]

4 Conclusion, 49

54 x^y e n

Detach, 48, 53

Apply axiom

55 x^y e n => [~x^y=0 => x^y^0=1]

U Spec, 15, 54

56 ~x^y=0 => x^y^0=1

Detach, 55, 54

Apply lemma

57 ALL(b):[x e n & b e n => [~x=0 => ~x^b=0]]

U Spec, 18

58 x e n & y e n => [~x=0 => ~x^y=0]

U Spec, 57

59 x e n & y e n

Join, 21, 22

60 ~x=0 => ~x^y=0

Detach, 58, 59

61 ~x^y=0

Detach, 60, 25

62 x^y^0=1

Detach, 56, 61

Apply axiom

63 y e n => y*0=0

U Spec, 7

64 y*0=0

Detach, 63, 22

65 0 e n & x^y^0=x^0 => 0 e p

Substitute, 64, 44

66 0 e n & 1=x^0 => 0 e p

Substitute, 62, 65

Apply axiom

67 x e n => [~x=0 => x^0=1]

U Spec, 15

68 ~x=0 => x^0=1

Detach, 67, 21

69 x^0=1

Detach, 68, 25

70 0 e n & 1=1 => 0 e p

Substitute, 69, 66

71 1=1

Reflex

72 0 e n & 1=1

Join, 2, 71

As Required:

73 0 e p

Detach, 70, 72

INDUCTIVE STEP

**************

Prove: ALL(b):[b e p => b+1 e p]

Suppose...

74 t e p

Premise

Apply definition of p

75 t e p <=> t e n & x^y^t=x^(y*t)

U Spec, 29

76 [t e p => t e n & x^y^t=x^(y*t)]

& [t e n & x^y^t=x^(y*t) => t e p]

Iff-And, 75

77 t e p => t e n & x^y^t=x^(y*t)

Split, 76

78 t e n & x^y^t=x^(y*t) => t e p

Split, 76

79 t e n & x^y^t=x^(y*t)

Detach, 77, 74

80 t e n

Split, 79

Multiply both sides by x^y

81 x^y^t=x^(y*t)

Split, 79

Apply axiom

82 ALL(b):[t e n & b e n => t+b e n]

U Spec, 4

83 t e n & 1 e n => t+1 e n

U Spec, 82

84 t e n & 1 e n

Join, 80, 3

85 t+1 e n

Detach, 83, 84

Apply definition of p

86 t+1 e p <=> t+1 e n & x^y^(t+1)=x^(y*(t+1))

U Spec, 29, 85

87 [t+1 e p => t+1 e n & x^y^(t+1)=x^(y*(t+1))]

& [t+1 e n & x^y^(t+1)=x^(y*(t+1)) => t+1 e p]

Iff-And, 86

88 t+1 e p => t+1 e n & x^y^(t+1)=x^(y*(t+1))

Split, 87

Sufficient: For t+1 e p

89 t+1 e n & x^y^(t+1)=x^(y*(t+1)) => t+1 e p

Split, 87

Apply axiom

90 ALL(b):[x e n & b e n => [~[x=0 & b=0] => x^b e n]]

U Spec, 13

91 x e n & y e n => [~[x=0 & y=0] => x^y e n]

U Spec, 90

92 x e n & y e n

Join, 21, 22

93 ~[x=0 & y=0] => x^y e n

Detach, 91, 92

94 x^y e n

Detach, 93, 53

Apply axiom

95 ALL(b):[x^y e n & b e n => [~[x^y=0 & b=0] => x^y^b e n]]

U Spec, 13, 94

96 x^y e n & t e n => [~[x^y=0 & t=0] => x^y^t e n]

U Spec, 95

97 x^y e n & t e n

Join, 94, 80

98 ~[x^y=0 & t=0] => x^y^t e n

Detach, 96, 97

Prove: ~[x^y=0 & t=0]

Suppose to the contrary...

99 x^y=0 & t=0

Premise

100 x^y=0

Split, 99

101 t=0

Split, 99

Apply lemma

102 ALL(b):[x e n & b e n => [~x=0 => ~x^b=0]]

U Spec, 18

103 x e n & y e n => [~x=0 => ~x^y=0]

U Spec, 102

104 x e n & y e n

Join, 21, 22

105 ~x=0 => ~x^y=0

Detach, 103, 104

106 ~x^y=0

Detach, 105, 25

107 x^y=0 & ~x^y=0

Join, 100, 106

As Required:

108 ~[x^y=0 & t=0]

4 Conclusion, 99

109 x^y^t e n

Detach, 98, 108

Apply axiom

110 ALL(b):[y e n & b e n => y*b e n]

U Spec, 6

111 y e n & t e n => y*t e n

U Spec, 110

112 y e n & t e n

Join, 22, 80

113 y*t e n

Detach, 111, 112

Apply axiom

114 ALL(b):[x e n & b e n => [~[x=0 & b=0] => x^b e n]]

U Spec, 13

115 x e n & y*t e n => [~[x=0 & y*t=0] => x^(y*t) e n]

U Spec, 114, 113

116 x e n & y*t e n

Join, 21, 113

117 ~[x=0 & y*t=0] => x^(y*t) e n

Detach, 115, 116

Prove: ~[x=0 & y*t=0]

Suppose to the contrary...

118 x=0 & y*t=0

Premise

119 x=0

Split, 118

120 y*t=0

Split, 118

121 x=0 & ~x=0

Join, 119, 25

As Required:

122 ~[x=0 & y*t=0]

4 Conclusion, 118

123 x^(y*t) e n

Detach, 117, 122

Apply axiom

124 ALL(b):ALL(c):[x^y^t e n & b e n & c e n => [x^y^t=b => x^y^t*c=b*c]]

U Spec, 9, 109

125 ALL(c):[x^y^t e n & x^(y*t) e n & c e n => [x^y^t=x^(y*t) => x^y^t*c=x^(y*t)*c]]

U Spec, 124, 123

126 x^y^t e n & x^(y*t) e n & x^y e n => [x^y^t=x^(y*t) => x^y^t*x^y=x^(y*t)*x^y]

U Spec, 125, 94

127 x^y^t e n & x^(y*t) e n

Join, 109, 123

128 x^y^t e n & x^(y*t) e n & x^y e n

Join, 127, 94

129 x^y^t=x^(y*t) => x^y^t*x^y=x^(y*t)*x^y

Detach, 126, 128

130 x^y^t*x^y=x^(y*t)*x^y

Detach, 129, 81

131 x^y e n => [~x^y=0 => x^y^0=1]

U Spec, 15, 94

132 ~x^y=0 => x^y^0=1

Detach, 131, 94

Apply lemma

133 ALL(b):[x e n & b e n => [~x=0 => ~x^b=0]]

U Spec, 18

134 x e n & y e n => [~x=0 => ~x^y=0]

U Spec, 133

135 x e n & y e n

Join, 21, 22

136 ~x=0 => ~x^y=0

Detach, 134, 135

137 ~x^y=0

Detach, 136, 25

138 x^y^0=1

Detach, 132, 137

Apply axiom

139 ALL(b):[x^y e n & b e n

=> [~[x^y=0 & b=0] => x^y^(b+1)=x^y^b*x^y]]

U Spec, 16, 94

140 x^y e n & 0 e n

=> [~[x^y=0 & 0=0] => x^y^(0+1)=x^y^0*x^y]

U Spec, 139

141 x^y e n & 0 e n

Join, 94, 2

142 ~[x^y=0 & 0=0] => x^y^(0+1)=x^y^0*x^y

Detach, 140, 141

Prove: ~[x^y=0 & 0=0]

Suppose to the contrary...

143 x^y=0 & 0=0

Premise

144 x^y=0

Split, 143

145 0=0

Split, 143

146 x^y=0 & ~x^y=0

Join, 144, 137

As Required:

147 ~[x^y=0 & 0=0]

4 Conclusion, 143

148 x^y^(0+1)=x^y^0*x^y

Detach, 142, 147

Apply axiom

149 1 e n => 1+0=1 & 0+1=1

U Spec, 5

150 1+0=1 & 0+1=1

Detach, 149, 3

151 1+0=1

Split, 150

152 0+1=1

Split, 150

153 x^y^1=x^y^0*x^y

Substitute, 152, 148

154 x^y e n => [~x^y=0 => x^y^0=1]

U Spec, 15, 94

155 ~x^y=0 => x^y^0=1

Detach, 154, 54

156 x^y^0=1

Detach, 155, 137

157 x^y^1=1*x^y

Substitute, 156, 153

158 x^y e n => x^y*1=x^y & 1*x^y=x^y

U Spec, 8, 94

159 x^y*1=x^y & 1*x^y=x^y

Detach, 158, 94

160 x^y*1=x^y

Split, 159

161 1*x^y=x^y

Split, 159

162 x^y^1=x^y

Substitute, 161, 157

163 x^y^t*x^y^1=x^(y*t)*x^y

Substitute, 162, 130

164 ALL(b):ALL(c):[x^y e n & b e n & c e n

=> [~x^y=0 | ~b=0 & ~c=0 => x^y^b*x^y^c=x^y^(b+c)]]

U Spec, 19, 94

165 ALL(c):[x^y e n & t e n & c e n

=> [~x^y=0 | ~t=0 & ~c=0 => x^y^t*x^y^c=x^y^(t+c)]]

U Spec, 164

166 x^y e n & t e n & 1 e n

=> [~x^y=0 | ~t=0 & ~1=0 => x^y^t*x^y^1=x^y^(t+1)]

U Spec, 165

167 x^y e n & t e n

Join, 94, 80

168 x^y e n & t e n & 1 e n

Join, 167, 3

169 ~x^y=0 | ~t=0 & ~1=0 => x^y^t*x^y^1=x^y^(t+1)

Detach, 166, 168

170 ~x^y=0 | ~t=0 & ~1=0

Arb Or, 137

171 x^y^t*x^y^1=x^y^(t+1)

Detach, 169, 170

172 x^y^(t+1)=x^(y*t)*x^y

Substitute, 171, 163

173 ALL(b):ALL(c):[x e n & b e n & c e n

=> [~x=0 | ~b=0 & ~c=0 => x^b*x^c=x^(b+c)]]

U Spec, 19

174 ALL(c):[x e n & y*t e n & c e n

=> [~x=0 | ~y*t=0 & ~c=0 => x^(y*t)*x^c=x^(y*t+c)]]

U Spec, 173, 113

175 x e n & y*t e n & y e n

=> [~x=0 | ~y*t=0 & ~y=0 => x^(y*t)*x^y=x^(y*t+y)]

U Spec, 174

176 x e n & y*t e n

Join, 21, 113

177 x e n & y*t e n & y e n

Join, 176, 22

178 ~x=0 | ~y*t=0 & ~y=0 => x^(y*t)*x^y=x^(y*t+y)

Detach, 175, 177

179 ~x=0 | ~y*t=0 & ~y=0

Arb Or, 25

180 x^(y*t)*x^y=x^(y*t+y)

Detach, 178, 179

181 x^y^(t+1)=x^(y*t+y)

Substitute, 180, 172

182 ALL(b):ALL(c):[y e n & b e n & c e n => y*(b+c)=y*b+y*c]

U Spec, 10

183 ALL(c):[y e n & t e n & c e n => y*(t+c)=y*t+y*c]

U Spec, 182

184 y e n & t e n & 1 e n => y*(t+1)=y*t+y*1

U Spec, 183

185 y e n & t e n

Join, 22, 80

186 y e n & t e n & 1 e n

Join, 185, 3

187 y*(t+1)=y*t+y*1

Detach, 184, 186

188 y e n => y*1=y & 1*y=y

U Spec, 8

189 y*1=y & 1*y=y

Detach, 188, 22

190 y*1=y

Split, 189

191 1*y=y

Split, 189

192 y*(t+1)=y*t+y

Substitute, 190, 187

193 x^y^(t+1)=x^(y*(t+1))

Substitute, 192, 181

194 t+1 e n & x^y^(t+1)=x^(y*(t+1))

Join, 85, 193

195 t+1 e p

Detach, 89, 194

As Required:

196 ALL(b):[b e p => b+1 e p]

4 Conclusion, 74

Joining results

197 0 e p & ALL(b):[b e p => b+1 e p]

Join, 73, 196

As Required:

198 ALL(b):[b e n => b e p]

Detach, 40, 197

Prove: ALL(b):[b e n => x^y^b=x^(y*b)]

Suppose...

199 t e n

Premise

200 t e n => t e p

U Spec, 198

201 t e p

Detach, 200, 199

Apply definition of p

202 t e p <=> t e n & x^y^t=x^(y*t)

U Spec, 29

203 [t e p => t e n & x^y^t=x^(y*t)]

& [t e n & x^y^t=x^(y*t) => t e p]

Iff-And, 202

204 t e p => t e n & x^y^t=x^(y*t)

Split, 203

205 t e n & x^y^t=x^(y*t) => t e p

Split, 203

206 t e n & x^y^t=x^(y*t)

Detach, 204, 201

207 t e n

Split, 206

208 x^y^t=x^(y*t)

Split, 206

As Required:

209 ALL(b):[b e n => x^y^b=x^(y*b)]

4 Conclusion, 199

210 z e n => x^y^z=x^(y*z)

U Spec, 209

211 x^y^z=x^(y*z)

Detach, 210, 23

Case 1

As Required:

212 ~x=0 => x^y^z=x^(y*z)

4 Conclusion, 25

Case 2

Prove: ~y=0 & ~z=0 => x^y^z=x^(y*z)

Suppose...

213 ~y=0 & ~z=0

Premise

214 ~y=0

Split, 213

215 ~z=0

Split, 213

Two sub-cases

216 x=0 | ~x=0

Or Not

Sub-case 1

Prove: x=0 => x^y^z=x^(y*z)

Suppose...

217 x=0

Premise

218 y e n => [~y=0 => 0^y=0]

U Spec, 17

219 ~y=0 => 0^y=0

Detach, 218, 22

220 0^y=0

Detach, 219, 214

221 x^y=0

Substitute, 217, 220

222 z e n => [~z=0 => 0^z=0]

U Spec, 17

223 ~z=0 => 0^z=0

Detach, 222, 23

224 0^z=0

Detach, 223, 215

LHS

225 x^y^z=0

Substitute, 221, 224

226 ALL(b):[y e n & b e n => y*b e n]

U Spec, 6

227 y e n & z e n => y*z e n

U Spec, 226

228 y e n & z e n

Join, 22, 23

229 y*z e n

Detach, 227, 228

230 y*z e n => [~y*z=0 => 0^(y*z)=0]

U Spec, 17, 229

231 ~y*z=0 => 0^(y*z)=0

Detach, 230, 229

232 ALL(b):[y e n & b e n => [~y=0 & ~b=0 => ~y*b=0]]

U Spec, 11

233 y e n & z e n => [~y=0 & ~z=0 => ~y*z=0]

U Spec, 232

234 y e n & z e n

Join, 22, 23

235 ~y=0 & ~z=0 => ~y*z=0

Detach, 233, 234

236 ~y*z=0

Detach, 235, 213

237 0^(y*z)=0

Detach, 231, 236

238 x^(y*z)=0

Substitute, 217, 237

239 x^y^z=x^(y*z)

Substitute, 238, 225

Sub-case 1

As Required:

240 x=0 => x^y^z=x^(y*z)

4 Conclusion, 217

Joining results...

Latter is sub-case 2

241 [x=0 => x^y^z=x^(y*z)] & [~x=0 => x^y^z=x^(y*z)]

Join, 240, 212

242 x^y^z=x^(y*z)

Cases, 216, 241

Case 2

As Required:

243 ~y=0 & ~z=0 => x^y^z=x^(y*z)

4 Conclusion, 213

244 [~x=0 => x^y^z=x^(y*z)]

& [~y=0 & ~z=0 => x^y^z=x^(y*z)]

Join, 212, 243

245 x^y^z=x^(y*z)

Cases, 24, 244

As Required:

246 ~x=0 | ~y=0 & ~z=0 => x^y^z=x^(y*z)

4 Conclusion, 24

As Required:

247 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n

=> [~a=0 | ~b=0 & ~c=0 => a^b^c=a^(b*c)]]

4 Conclusion, 20