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