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

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

Axiom

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