THEOREM

*******

a^b * a^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*a^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

Dan Christensen

2019-11-10

OUTLINE

*******

Lines Content

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

1-17 Axioms/Definitions for n, 0, 1, +, *, ^

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

24-167 Case 1: ~b=0 and ~c=0 => a^b * a^c = a^(b+c) (by induction)

168-203 Case 2: ~a=0 => a^b * a^c = a^(b+c)

204-207 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

+ Associative

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

Axiom

Adding 0

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

Axiom

Adding non-zeroes

7 ALL(a):ALL(b):[a e n & b e n => [~a=0 | ~b=0 => ~a+b=0]]

Axiom

Properties of *

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

Closed on n

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

Axiom

Multiplying by 0

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

Axiom

Multiplying by 1

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

Axiom

Multiplying both sides

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

Axiom

* Associative

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

Axiom

Induction priniciple

13 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

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

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

Axiom

15 0^1=0

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=0 & b=0] => a^(b+1)=a^b*a]]

Axiom

LEMMA

*****

Non-zero powers of zero equal zero Proof

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

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*a^c=a^(b+c)]]

Suppose...

19 x e n & y e n & z e n

Premise

20 x e n

Split, 19

21 y e n

Split, 19

22 z e n

Split, 19

Suppose... (two cases to consider)

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

Premise

Case 1

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

Suppose...

24 ~x=0

Premise

Construct set p for proof by induction

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

Subset, 1

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

E Spec, 25

Define: p

27 Set(p)

Split, 26

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

Split, 26

Apply induction principle

29 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, 13

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

Suppose...

30 t e p

Premise

Apply definition of p

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

U Spec, 28

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

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

Iff-And, 31

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

Split, 32

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

Split, 32

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

Detach, 33, 30

36 t e n

Split, 35

As Required:

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

4 Conclusion, 30

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

Join, 27, 37

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

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

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

Detach, 29, 38

BASE CASE

*********

Apply definition of p

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

U Spec, 28

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

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

Iff-And, 40

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

Split, 41

Sufficient: For 0 e p

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

Split, 41

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

U Spec, 16

45 ~x=0 => x^0=1

Detach, 44, 20

46 x^0=1

Detach, 45, 24

Apply axiom

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

U Spec, 14

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

U Spec, 47

49 x e n & y e n

Join, 20, 21

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

Detach, 48, 49

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

Suppose to the contrary...

51 x=0 & y=0

Premise

52 x=0

Split, 51

53 y=0

Split, 51

54 x=0 & ~x=0

Join, 52, 24

As Required:

55 ~[x=0 & y=0]

4 Conclusion, 51

56 x^y e n

Detach, 50, 55

57 x^y e n => x^y*1=x^y

U Spec, 10, 56

58 x^y*1=x^y

Detach, 57, 56

59 x^y*x^0=x^y

Substitute, 46, 58

Apply axiom

60 y e n => y+0=y & 0+y=y

U Spec, 6

61 y+0=y & 0+y=y

Detach, 60, 21

62 y+0=y

Split, 61

63 0+y=y

Split, 61

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

Substitute, 62, 59

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

Join, 2, 64

As Required:

66 0 e p

Detach, 43, 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*x^t=x^(y+t)

U Spec, 28

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

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

Iff-And, 68

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

Split, 69

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

Split, 69

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

Detach, 70, 67

73 t e n

Split, 72

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

Split, 72

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*x^(t+1)=x^(y+(t+1))

U Spec, 28, 78

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

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

Iff-And, 79

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

Split, 80

Sufficient: For t+1 e p

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

Split, 80

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

U Spec, 14

Apply axiom

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

U Spec, 83

85 x e n & t e n

Join, 20, 73

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

Detach, 84, 85

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

Suppose to the contrary...

87 x=0 & t=0

Premise

88 x=0

Split, 87

89 t=0

Split, 87

90 x=0 & ~x=0

Join, 88, 24

As Required:

91 ~[x=0 & t=0]

4 Conclusion, 87

92 x^t e n

Detach, 86, 91

Apply axiom

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

U Spec, 8, 56

94 x^y e n & x^t e n => x^y*x^t e n

U Spec, 93, 92

95 x^y e n & x^t e n

Join, 56, 92

96 x^y*x^t e n

Detach, 94, 95

Apply axiom

97 ALL(b):[y e n & b e n => y+b e n]

U Spec, 4

98 y e n & t e n => y+t e n

U Spec, 97

99 y e n & t e n

Join, 21, 73

100 y+t e n

Detach, 98, 99

Apply axiom

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

U Spec, 14

102 x e n & y+t e n => [~[x=0 & y+t=0] => x^(y+t) e n]

U Spec, 101, 100

103 x e n & y+t e n

Join, 20, 100

104 ~[x=0 & y+t=0] => x^(y+t) e n

Detach, 102, 103

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

Suppose to the contrary...

105 x=0 & y+t=0

Premise

106 x=0

Split, 105

107 y+t=0

Split, 105

108 x=0 & ~x=0

Join, 106, 24

As Required:

109 ~[x=0 & y+t=0]

4 Conclusion, 105

110 x^(y+t) e n

Detach, 104, 109

Apply associativity and commutativity to rearrange terms

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

U Spec, 11, 96

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

U Spec, 111, 110

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

U Spec, 112

114 x^y*x^t e n & x^(y+t) e n

Join, 96, 110

115 x^y*x^t e n & x^(y+t) e n & x e n

Join, 114, 20

116 x^y*x^t=x^(y+t) => x^y*x^t*x=x^(y+t)*x

Detach, 113, 115

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

Detach, 116, 74

118 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, 56

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

U Spec, 118, 92

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

U Spec, 119

121 x^y e n & x^t e n

Join, 56, 92

122 x^y e n & x^t e n & x e n

Join, 121, 20

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

Detach, 120, 122

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

Substitute, 123, 117

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

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

U Spec, 17

126 x e n & t e n

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

U Spec, 125

127 x e n & t e n

Join, 20, 73

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

Detach, 126, 127

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

Detach, 128, 91

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

Substitute, 129, 124

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

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

U Spec, 17

132 x e n & y+t e n

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

U Spec, 131, 100

133 x e n & y+t e n

Join, 20, 100

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

Detach, 132, 133

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

Suppose to the contrary...

135 x=0 & y+t=0

Premise

136 x=0

Split, 135

137 y+t=0

Split, 135

138 x=0 & ~x=0

Join, 136, 24

As Required:

139 ~[x=0 & y+t=0]

4 Conclusion, 135

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

Detach, 134, 139

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

Substitute, 140, 130

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

U Spec, 5

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

U Spec, 142

144 y e n & t e n & 1 e n => y+t+1=y+(t+1)

U Spec, 143

145 y e n & t e n

Join, 21, 73

146 y e n & t e n & 1 e n

Join, 145, 3

147 y+t+1=y+(t+1)

Detach, 144, 146

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

Substitute, 147, 141

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

Join, 78, 148

150 t+1 e p

Detach, 82, 149

As Required:

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

4 Conclusion, 67

Joining results...

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

Join, 66, 151

As Required:

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

Detach, 39, 152

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

Suppose...

154 t e n

Premise

155 t e n => t e p

U Spec, 153

156 t e p

Detach, 155, 154

Apply definition of p

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

U Spec, 28

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

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

Iff-And, 157

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

Split, 158

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

Split, 158

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

Detach, 159, 156

162 t e n

Split, 161

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

Split, 161

As Required:

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

4 Conclusion, 154

165 z e n => x^y*x^z=x^(y+z)

U Spec, 164

166 x^y*x^z=x^(y+z)

Detach, 165, 22

Case 1

As Required:

167 ~x=0 => x^y*x^z=x^(y+z)

4 Conclusion, 24

Case 2

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

Suppose...

168 ~y=0 & ~z=0

Premise

169 ~y=0

Split, 168

170 ~z=0

Split, 168

Two sub-cases:

171 x=0 | ~x=0

Or Not

Sub-case 1

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

Suppose...

172 x=0

Premise

Apply lemma

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

U Spec, 18

174 ~y=0 => 0^y=0

Detach, 173, 21

175 0^y=0

Detach, 174, 169

176 x^y=0

Substitute, 172, 175

Apply lemma

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

U Spec, 18

178 ~z=0 => 0^z=0

Detach, 177, 22

179 0^z=0

Detach, 178, 170

180 x^z=0

Substitute, 172, 179

181 0 e n => 0*0=0

U Spec, 9

182 0*0=0

Detach, 181, 2

183 x^y*0=0

Substitute, 176, 182

LHS

184 x^y*x^z=0

Substitute, 180, 183

Apply axiom

185 ALL(b):[y e n & b e n => y+b e n]

U Spec, 4

186 y e n & z e n => y+z e n

U Spec, 185

187 y e n & z e n

Join, 21, 22

188 y+z e n

Detach, 186, 187

Apply lemma

189 y+z e n => [~y+z=0 => 0^(y+z)=0]

U Spec, 18, 188

190 ~y+z=0 => 0^(y+z)=0

Detach, 189, 188

Apply axiom

191 ALL(b):[y e n & b e n => [~y=0 | ~b=0 => ~y+b=0]]

U Spec, 7

192 y e n & z e n => [~y=0 | ~z=0 => ~y+z=0]

U Spec, 191

193 y e n & z e n

Join, 21, 22

194 ~y=0 | ~z=0 => ~y+z=0

Detach, 192, 193

195 ~y=0 | ~z=0

Arb Or, 169

196 ~y+z=0

Detach, 194, 195

197 0^(y+z)=0

Detach, 190, 196

198 x^(y+z)=0

Substitute, 172, 197

199 x^y*x^z=x^(y+z)

Substitute, 198, 184

Sub-case 1

As Required:

200 x=0 => x^y*x^z=x^(y+z)

4 Conclusion, 172

Combining results...

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

Join, 200, 167

202 x^y*x^z=x^(y+z)

Cases, 171, 201

Case 2

As Required:

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

4 Conclusion, 168

Combining results...

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

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

Join, 167, 203

205 x^y*x^z=x^(y+z)

Cases, 23, 204

As Required:

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

4 Conclusion, 23

As Required:

207 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)]]

4 Conclusion, 19