THEOREM

*******

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

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-10-26

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

Adding 0

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

Axiom

+ Commutative

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

Axiom

+ Associative

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

Axiom

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

Axiom

Properties of *

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

Closed on n

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

Axiom

Multiplying by 0

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

Axiom

Multiplying by 1

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

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

* Commutative

13 ALL(a):ALL(b):[a e n & b e n => a*b=b*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

Principle of Mathematical Induction

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

18 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

PROOF

*****

Suppose...

19 x e n & y e n & ~x=0

Premise

20 x e n

Split, 19

21 y e n

Split, 19

22 ~x=0

Split, 19

Construct p

Apply Subset Axiom

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

Subset, 1

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

E Spec, 23

Define: p

25 Set(p)

Split, 24

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

Split, 24

Apply Principle of Mathematical Induction of set p

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, 18

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^y*x^t

U Spec, 26

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

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

Iff-And, 29

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

Split, 30

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

Split, 30

33 t e n & x^(y+t)=x^y*x^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

*********

Prove: 0 e p

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

U Spec, 26

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

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

Iff-And, 38

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

Split, 39

Sufficient: For 0 e p

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

Split, 39

Apply definition of ^ on n

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

U Spec, 14

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

U Spec, 42

44 x e n & y e n

Join, 20, 21

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

Detach, 43, 44

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

Suppose to the contrary...

46 x=0 & y=0

Premise

47 x=0

Split, 46

48 y=0

Split, 46

49 x=0 & ~x=0

Join, 47, 22

As Required:

50 ~[x=0 & y=0]

4 Conclusion, 46

51 x^y e n

Detach, 45, 50

52 x^y=x^y

Reflex, 51

53 y e n => y+0=y

U Spec, 5

54 y+0=y

Detach, 53, 21

55 x^(y+0)=x^y

Substitute, 54, 52

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

U Spec, 11, 51

57 x^y*1=x^y

Detach, 56, 51

58 x^(y+0)=x^y*1

Substitute, 57, 55

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

U Spec, 16

60 ~x=0 => x^0=1

Detach, 59, 20

61 x^0=1

Detach, 60, 22

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

Substitute, 61, 58

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

Join, 2, 62

As Required:

64 0 e p

Detach, 41, 63

INDUCTIVE STEP

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

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

Suppose...

65 t e p

Premise

Apply definition of p

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

U Spec, 26

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

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

Iff-And, 66

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

Split, 67

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

Split, 67

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

Detach, 68, 65

71 t e n

Split, 70

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

Split, 70

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

U Spec, 4

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

U Spec, 73

75 t e n & 1 e n

Join, 71, 3

76 t+1 e n

Detach, 74, 75

Apply definition of p

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

U Spec, 26, 76

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

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

Iff-And, 77

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

Split, 78

Sufficient: For t+1 e p

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

Split, 78

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

U Spec, 4

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

U Spec, 81, 76

83 y e n & t+1 e n

Join, 21, 76

84 y+(t+1) e n

Detach, 82, 83

Apply definition of p

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

U Spec, 14

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

U Spec, 85, 84

87 x e n & y+(t+1) e n

Join, 20, 84

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

Detach, 86, 87

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

Suppose to the contrary...

89 x=0 & y+(t+1)=0

Premise

90 x=0

Split, 89

91 y+(t+1)=0

Split, 89

92 x=0 & ~x=0

Join, 90, 22

As Required:

93 ~[x=0 & y+(t+1)=0]

4 Conclusion, 89

94 x^(y+(t+1)) e n

Detach, 88, 93

95 x^(y+(t+1))=x^(y+(t+1))

Reflex, 94

Apply associativity of +

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

U Spec, 7

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

U Spec, 96

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

U Spec, 97

99 y e n & t e n

Join, 21, 71

100 y e n & t e n & 1 e n

Join, 99, 3

101 y+t+1=y+(t+1)

Detach, 98, 100

102 x^(y+(t+1))=x^(y+t+1)

Substitute, 101, 95

Apply definition of ^

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

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

U Spec, 17

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

U Spec, 4

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

U Spec, 104

106 y+t e n

Detach, 105, 99

Apply definition of p

107 x e n & y+t e n

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

U Spec, 103, 106

108 x e n & y+t e n

Join, 20, 106

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

Detach, 107, 108

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

Suppose to the contrary...

110 x=0 & y+t=0

Premise

111 x=0

Split, 110

112 y+t=0

Split, 110

113 x=0 & ~x=0

Join, 111, 22

As Required:

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

4 Conclusion, 110

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

Detach, 109, 114

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

Substitute, 115, 102

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

Substitute, 72, 116

Apply definition of ^

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

U Spec, 14

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

U Spec, 118

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

Detach, 119, 44

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

Suppose to the contrary...

121 x=0 & y=0

Premise

122 x=0

Split, 121

123 y=0

Split, 121

124 x=0 & ~x=0

Join, 122, 22

As Required:

125 ~[x=0 & y=0]

4 Conclusion, 121

126 x^y e n

Detach, 120, 125

Apply definition of ^

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

U Spec, 118, 76

128 x e n & t+1 e n

Join, 20, 76

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

Detach, 127, 128

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

Suppose to the contrary...

130 x=0 & t+1=0

Premise

131 x=0

Split, 130

132 t+1=0

Split, 130

133 x=0 & ~x=0

Join, 131, 22

As Required:

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

4 Conclusion, 130

135 x^(t+1) e n

Detach, 129, 134

Apply definition of *

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

U Spec, 9, 126

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

U Spec, 136, 135

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

Join, 126, 135

139 x^y*x^(t+1) e n

Detach, 137, 138

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

Reflex, 139

Apply definition of ^

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

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

U Spec, 17

142 x e n & t e n

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

U Spec, 141

143 x e n & t e n

Join, 20, 71

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

Detach, 142, 143

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

Suppose to the contrary...

145 x=0 & t=0

Premise

146 x=0

Split, 145

147 t=0

Split, 145

148 x=0 & ~x=0

Join, 146, 22

As Required:

149 ~[x=0 & t=0]

4 Conclusion, 145

113

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

Detach, 144, 149

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

Substitute, 150, 140

Apply associativity of * on n

152 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, 126

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

U Spec, 14

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

U Spec, 153

155 x e n & t e n

Join, 20, 71

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

Detach, 154, 155

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

Suppose to the contrary...

157 x=0 & t=0

Premise

158 x=0

Split, 157

159 t=0

Split, 157

160 x=0 & ~x=0

Join, 158, 22

As Required:

161 ~[x=0 & t=0]

4 Conclusion, 157

162 x^t e n

Detach, 156, 161

Apply associativity of *

163 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, 152, 162

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

U Spec, 163

165 x^y e n & x^t e n

Join, 126, 162

166 x^y e n & x^t e n & x e n

Join, 165, 20

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

Detach, 164, 166

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

Substitute, 167, 151

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

Substitute, 168, 117

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

Join, 76, 169

171 t+1 e p

Detach, 80, 170

As Required:

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

4 Conclusion, 65

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

Join, 64, 172

As Required:

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

Detach, 37, 173

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

Suppose...

175 t e n

Premise

176 t e n => t e p

U Spec, 174

177 t e p

Detach, 176, 175

Apply definition of p

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

U Spec, 26

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

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

Iff-And, 178

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

Split, 179

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

Split, 179

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

Detach, 180, 177

183 t e n

Split, 182

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

Split, 182

As Required:

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

4 Conclusion, 175

As Required:

186 ALL(a):ALL(b):[a e n & b e n & ~a=0

=> ALL(c):[c e n => a^(b+c)=a^b*a^c]]

4 Conclusion, 19

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

Suppose...

187 x e n & y e n & z e n

Premise

188 x e n

Split, 187

189 y e n

Split, 187

190 z e n

Split, 187

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

Suppose...

191 ~x=0

Premise

Apply previous result

192 ALL(b):[x e n & b e n & ~x=0

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

U Spec, 186

193 x e n & y e n & ~x=0

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

U Spec, 192

194 x e n & y e n

Join, 188, 189

195 x e n & y e n & ~x=0

Join, 194, 191

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

Detach, 193, 195

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

U Spec, 196

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

Detach, 197, 190

As Required:

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

4 Conclusion, 191

As Required:

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

4 Conclusion, 187