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