THEOREM

*******

(a*b)^c = a^c * b^c  (for non-zero exponent (c) OR both non-zero bases (a and b))

ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => [~c=0 | ~a=0 & ~b=0 => (a*b)^c = a^c * 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-15     Axioms/Definitions for n, 0, 1, +, *, ^

16       Lemma for non-zero exponents of zero  (link to proof)

17-201   Prove that if ~a=0 and ~b=0, then (a*b)^c=a^c*b^c for all c e n (by induction).

202-297  Prove that if ~c=0, then (a*b)^c=a^c*b^c for all a, b e n.

298-319  Combine results to obtain theorem as required.

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

Properties of *

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

Closed on n

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

Axiom

Multiplying by 0

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

Axiom

Multiplying by 1

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

Axiom

* Associative

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

Axiom

* Commutative

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

Axiom

Product on non-zero numbers

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

Axiom

Principle of Mathematical Induction (used for proof by induction)

11   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

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

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

Axiom

13   0^1=0

Axiom

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

Axiom

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

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

Axiom

LEMMA

*****

Non-zero exponents of zero                   Proof

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

Axiom

PROOF

*****

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

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

Suppose...

17   x e n & y e n

Premise

18   x e n

Split, 17

19   y e n

Split, 17

Prove: ~x=0 & ~y=0 => ALL(c):[c e n => (x*y)^c=x^c*y^c]

Suppose...

20   ~x=0 & ~y=0

Premise

21   ~x=0

Split, 20

22   ~y=0

Split, 20

Prove: ALL(c):[c e n => (x*y)^c=x^c*y^c]  (by induction)

Construct set p

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

Subset, 1

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

E Spec, 23

Define: p

25   Set(p)

Split, 24

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

Split, 24

Apply Principle of Induction

27   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, 11

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

Suppose...

28   t e p

Premise

Apply definition of p

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

U Spec, 26

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

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

Iff-And, 29

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

Split, 30

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

Split, 30

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

Detach, 31, 28

34   t e n

Split, 33

As Required:

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

4 Conclusion, 28

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

Join, 25, 35

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

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

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

Detach, 27, 36

BASE CASE

*********

Apply definition of p

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

U Spec, 26

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

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

Iff-And, 38

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

Split, 39

Sufficient: For 0 e p

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

Split, 39

Apply axiom

42   ALL(b):[x e n & b e n => [~x=0 & ~b=0 => ~x*b=0]]

U Spec, 10

43   x e n & y e n => [~x=0 & ~y=0 => ~x*y=0]

U Spec, 42

44   ~x=0 & ~y=0 => ~x*y=0

Detach, 43, 17

45   ~x*y=0

Detach, 44, 20

Apply axiom

46   ALL(b):[x e n & b e n => x*b e n]

U Spec, 5

47   x e n & y e n => x*y e n

U Spec, 46

48   x*y e n

Detach, 47, 17

Apply axiom

49   x*y e n => [~x*y=0 => (x*y)^0=1]

U Spec, 14, 48

50   ~x*y=0 => (x*y)^0=1

Detach, 49, 48

LHS

51   (x*y)^0=1

Detach, 50, 45

Apply axiom

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

U Spec, 14

53   ~x=0 => x^0=1

Detach, 52, 18

54   x^0=1

Detach, 53, 21

Apply axiom

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

U Spec, 14

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

Detach, 55, 19

57   y^0=1

Detach, 56, 22

Apply axiom

58   1 e n => 1*1=1 & 1*1=1

U Spec, 7

59   1*1=1 & 1*1=1

Detach, 58, 3

60   1*1=1

Split, 59

61   1*1=1

Split, 59

62   x^0*1=1

Substitute, 54, 61

RHS

63   x^0*y^0=1

Substitute, 57, 62

64   (x*y)^0=x^0*y^0

Substitute, 63, 51

65   0 e n & (x*y)^0=x^0*y^0

Join, 2, 64

As Required:

66   0 e p

Detach, 41, 65

INDUCTIVE STEP

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

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

Suppose...

67   t e p

Premise

Apply definition of p

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

U Spec, 26

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

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

Iff-And, 68

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

Split, 69

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

Split, 69

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

Detach, 70, 67

73   t e n

Split, 72

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

Split, 72

Apply axiom

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

U Spec, 4

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

U Spec, 75

77   t e n & 1 e n

Join, 73, 3

78   t+1 e n

Detach, 76, 77

Apply definition of p

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

U Spec, 26, 78

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

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

Iff-And, 79

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

Split, 80

Sufficient: For t+1 e p

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

Split, 80

Apply axiom

83   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, 15, 48

84   x*y e n & t e n

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

U Spec, 83

85   x*y e n & t e n

Join, 48, 73

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

Detach, 84, 85

87   x*y=0 & t=0

Premise

88   x*y=0

Split, 87

89   t=0

Split, 87

90   x*y=0 & ~x*y=0

Join, 88, 45

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

4 Conclusion, 87

LHS

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

Detach, 86, 91

Rearrange terms using associativity and commutativity

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

Substitute, 74, 92

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

U Spec, 12

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

U Spec, 94

96   x e n & t e n

Join, 18, 73

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

Detach, 95, 96

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

Suppose to the contrary...

98   x=0 & t=0

Premise

99   x=0

Split, 98

100  t=0

Split, 98

101  x=0 & ~x=0

Join, 99, 21

As Required:

102  ~[x=0 & t=0]

4 Conclusion, 98

103  x^t e n

Detach, 97, 102

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

U Spec, 12

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

U Spec, 104

106  y e n & t e n

Join, 19, 73

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

Detach, 105, 106

108  y=0 & t=0

Premise

109  y=0

Split, 108

110  t=0

Split, 108

111  y=0 & ~y=0

Join, 109, 22

112  ~[y=0 & t=0]

4 Conclusion, 108

113  y^t e n

Detach, 107, 112

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

U Spec, 8, 103

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

U Spec, 114, 113

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

U Spec, 115, 48

117  x^t e n & y^t e n

Join, 103, 113

118  x^t e n & y^t e n & x*y e n

Join, 117, 48

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

Detach, 116, 118

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

Substitute, 119, 93

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

U Spec, 9, 113

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

U Spec, 121, 48

123  y^t e n & x*y e n

Join, 113, 48

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

Detach, 122, 123

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

Substitute, 124, 120

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

U Spec, 8, 103

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

U Spec, 126, 48

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

U Spec, 127, 113

129  x^t e n & x*y e n

Join, 103, 48

130  x^t e n & x*y e n & y^t e n

Join, 129, 113

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

Detach, 128, 130

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

Substitute, 131, 125

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

U Spec, 8, 103

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

U Spec, 133

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

U Spec, 134

136  x^t e n & x e n

Join, 103, 18

137  x^t e n & x e n & y e n

Join, 136, 19

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

Detach, 135, 137

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

Substitute, 138, 132

140  ALL(b):[x e n & b e n

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

U Spec, 15

141  x e n & t e n

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

U Spec, 140

142  x e n & t e n

Join, 18, 73

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

Detach, 141, 142

144  x=0 & t=0

Premise

145  x=0

Split, 144

146  t=0

Split, 144

147  x=0 & ~x=0

Join, 145, 21

148  ~[x=0 & t=0]

4 Conclusion, 144

149  x^(t+1)=x^t*x

Detach, 143, 148

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

Substitute, 149, 139

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

U Spec, 12

152  x e n & t+1 e n => [~[x=0 & t+1=0] => x^(t+1) e n]

U Spec, 151, 78

153  x e n & t+1 e n

Join, 18, 78

154  ~[x=0 & t+1=0] => x^(t+1) e n

Detach, 152, 153

155  x=0 & t+1=0

Premise

156  x=0

Split, 155

157  t+1=0

Split, 155

158  x=0 & ~x=0

Join, 156, 21

159  ~[x=0 & t+1=0]

4 Conclusion, 155

160  x^(t+1) e n

Detach, 154, 159

161  ALL(b):ALL(c):[x^(t+1) e n & b e n & c e n => x^(t+1)*b*c=x^(t+1)*(b*c)]

U Spec, 8, 160

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

U Spec, 161

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

U Spec, 162, 113

164  x^(t+1) e n & y e n

Join, 160, 19

165  x^(t+1) e n & y e n & y^t e n

Join, 164, 113

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

Detach, 163, 165

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

Substitute, 166, 150

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

U Spec, 9

169  y e n & y^t e n => y*y^t=y^t*y

U Spec, 168, 113

170  y e n & y^t e n

Join, 19, 113

171  y*y^t=y^t*y

Detach, 169, 170

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

Substitute, 171, 167

173  ALL(b):[y e n & b e n

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

U Spec, 15

174  y e n & t e n

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

U Spec, 173

175  y e n & t e n

Join, 19, 73

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

Detach, 174, 175

177  y=0 & t=0

Premise

178  y=0

Split, 177

179  t=0

Split, 177

180  y=0 & ~y=0

Join, 178, 22

181  ~[y=0 & t=0]

4 Conclusion, 177

182  y^(t+1)=y^t*y

Detach, 176, 181

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

Substitute, 182, 172

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

Join, 78, 183

185  t+1 e p

Detach, 82, 184

As Required:

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

4 Conclusion, 67

Joining results...

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

Join, 66, 186

As Required:

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

Detach, 37, 187

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

Suppose...

189  z e n

Premise

190  z e n => z e p

U Spec, 188

191  z e p

Detach, 190, 189

Apply definition of p

192  z e p <=> z e n & (x*y)^z=x^z*y^z

U Spec, 26

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

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

Iff-And, 192

194  z e p => z e n & (x*y)^z=x^z*y^z

Split, 193

195  z e n & (x*y)^z=x^z*y^z => z e p

Split, 193

196  z e n & (x*y)^z=x^z*y^z

Detach, 194, 191

197  z e n

Split, 196

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

Split, 196

As Required:

199  ALL(c):[c e n => (x*y)^c=x^c*y^c]

4 Conclusion, 189

As Required:

200  ~x=0 & ~y=0 => ALL(c):[c e n => (x*y)^c=x^c*y^c]

4 Conclusion, 20

As Required:

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

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

4 Conclusion, 17

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

Suppose...

202  x e n & y e n & z e n

Premise

203  x e n

Split, 202

204  y e n

Split, 202

205  z e n

Split, 202

Two cases:

206  x=0 | ~x=0

Or Not

Two sub-cases

207  y=0 | ~y=0

Or Not

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

Suppose...

208  ~z=0

Premise

Apply lemma

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

U Spec, 16

210  ~z=0 => 0^z=0

Detach, 209, 205

211  0^z=0

Detach, 210, 208

Case 1

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

Suppose...

212  x=0

Premise

Sub-case 1

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

Suppose...

213  y=0

Premise

Apply axiom

214  0 e n => 0*0=0 & 0*0=0

U Spec, 6

215  0*0=0 & 0*0=0

Detach, 214, 2

216  0*0=0

Split, 215

217  0*0=0

Split, 215

218  x*0=0

Substitute, 212, 217

219  x*y=0

Substitute, 213, 218

LHS

220  (x*y)^z=0

Substitute, 219, 211

221  x^z=0

Substitute, 212, 211

222  y^z=0

Substitute, 213, 211

223  x^z*0=0

Substitute, 221, 217

RHS

224  x^z*y^z=0

Substitute, 222, 223

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

Substitute, 224, 220

Sub-case 1

As Required:

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

4 Conclusion, 213

Sub-case 2

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

Suppose...

227  ~y=0

Premise

228  y e n => y*0=0 & 0*y=0

U Spec, 6

229  y*0=0 & 0*y=0

Detach, 228, 204

230  y*0=0

Split, 229

231  0*y=0

Split, 229

232  x*y=0

Substitute, 212, 231

LHS

233  (x*y)^z=0

Substitute, 232, 211

234  x^z=0

Substitute, 212, 211

Apply axiom

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

U Spec, 12

236  y e n & z e n => [~[y=0 & z=0] => y^z e n]

U Spec, 235

237  y e n & z e n

Join, 204, 205

238  ~[y=0 & z=0] => y^z e n

Detach, 236, 237

239  y=0 & z=0

Premise

240  y=0

Split, 239

241  z=0

Split, 239

242  y=0 & ~y=0

Join, 240, 227

243  ~[y=0 & z=0]

4 Conclusion, 239

244  y^z e n

Detach, 238, 243

245  y^z e n => y^z*0=0 & 0*y^z=0

U Spec, 6, 244

246  y^z*0=0 & 0*y^z=0

Detach, 245, 244

247  y^z*0=0

Split, 246

248  0*y^z=0

Split, 246

RHS

249  x^z*y^z=0

Substitute, 234, 248

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

Substitute, 249, 233

Sub-case 2

As Required:

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

4 Conclusion, 227

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

Join, 226, 251

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

Cases, 207, 252

Case 1

As Required:

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

4 Conclusion, 212

Case 2

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

Suppose...

255  ~x=0

Premise

Sub-case 1

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

Suppose...

256  y=0

Premise

Apply axiom

257  x e n => x*0=0 & 0*x=0

U Spec, 6

258  x*0=0 & 0*x=0

Detach, 257, 203

259  x*0=0

Split, 258

260  0*x=0

Split, 258

261  x*y=0

Substitute, 256, 259

LHS

262  (x*y)^z=0

Substitute, 261, 211

263  y^z=0

Substitute, 256, 211

Apply axiom

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

U Spec, 12

265  x e n & z e n => [~[x=0 & z=0] => x^z e n]

U Spec, 264

266  x e n & z e n

Join, 203, 205

267  ~[x=0 & z=0] => x^z e n

Detach, 265, 266

268  x=0 & z=0

Premise

269  x=0

Split, 268

270  z=0

Split, 268

271  x=0 & ~x=0

Join, 269, 255

272  ~[x=0 & z=0]

4 Conclusion, 268

273  x^z e n

Detach, 267, 272

Apply axiom

274  x^z e n => x^z*0=0 & 0*x^z=0

U Spec, 6, 273

275  x^z*0=0 & 0*x^z=0

Detach, 274, 273

276  x^z*0=0

Split, 275

277  0*x^z=0

Split, 275

RHS

278  x^z*y^z=0

Substitute, 263, 276

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

Substitute, 278, 262

Sub-case 1

As Required:

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

4 Conclusion, 256

Sub-case 2

281  ~y=0

Premise

Apply previous result

282  ALL(b):[x e n & b e n

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

U Spec, 201

283  x e n & y e n

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

U Spec, 282

284  x e n & y e n

Join, 203, 204

285  ~x=0 & ~y=0 => ALL(c):[c e n => (x*y)^c=x^c*y^c]

Detach, 283, 284

286  ~x=0 & ~y=0

Join, 255, 281

287  ALL(c):[c e n => (x*y)^c=x^c*y^c]

Detach, 285, 286

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

U Spec, 287

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

Detach, 288, 205

Sub-case 2

As Required:

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

4 Conclusion, 281

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

Join, 280, 290

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

Cases, 207, 291

Case 2

As Required:

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

4 Conclusion, 255

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

Join, 254, 293

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

Cases, 206, 294

As Required:

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

4 Conclusion, 208

As Required:

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

4 Conclusion, 202

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

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

Suppose...

298  x e n & y e n & z e n

Premise

299  x e n

Split, 298

300  y e n

Split, 298

301  z e n

Split, 298

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

Two cases to consider:

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

Premise

Apply previous result

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

U Spec, 297

304  ALL(c):[x e n & y e n & c e n => [~c=0 => (x*y)^c=x^c*y^c]]

U Spec, 303

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

U Spec, 304

Case 1

As Required:

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

Detach, 305, 298

Case 2

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

Suppose...

307  ~x=0 & ~y=0

Premise

Apply previous result

308  ALL(b):[x e n & b e n

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

U Spec, 201

309  x e n & y e n

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

U Spec, 308

310  x e n & y e n

Join, 299, 300

311  ~x=0 & ~y=0 => ALL(c):[c e n => (x*y)^c=x^c*y^c]

Detach, 309, 310

312  ALL(c):[c e n => (x*y)^c=x^c*y^c]

Detach, 311, 307

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

U Spec, 312

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

Detach, 313, 301

Case 2

As Required:

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

4 Conclusion, 307

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

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

Join, 306, 315

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

Cases, 302, 316

As Required:

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

4 Conclusion, 302

As Required:

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

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

4 Conclusion, 298