THEOREM
*******
The Product of Powers Rule: x^y * x^z = x^(y+z) for ~x=0
ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n & ~a=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 software available at http://www.dcproof.com
AXIOMS / DEFINITIONS USED
*************************
Define: ^ (partial function on n, infix version of pow function)
1 ALL(a):ALL(b):[a e n & b e n & ~[a=0 & b=0] => a^b e n]
Axiom
2 ALL(a):[a e n & ~a=0 => a^0=1]
Axiom
3 0^1=0
Axiom
4 ALL(a):ALL(b):[a e n & b e n & ~[a=0 & b=0] => a^(b+1)=a^b*a]
Axiom
n is a set (the set of natural numbers)
5 Set(n)
Axiom
6 0 e n
Axiom
Define: +
7 ALL(a):ALL(b):[a e n & b e n => a+b e n]
Axiom
Define: *
8 ALL(a):ALL(b):[a e n & b e n => a*b e n]
Axiom
Define: 1
9 1 e n
Axiom
Adding 0
10 ALL(a):[a e n => a+0=a]
Axiom
Multiplying by 0
11 ALL(a):[a e n => a*0=0]
Axiom
Multiplying by 1
12 ALL(a):[a e n => a*1=a]
Axiom
+ is associative
13 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => a+b+c=a+(b+c)]
Axiom
+ is commutative
14 ALL(a):ALL(b):[a e n & b e n => a+b=b+a]
Axiom
* is associative
15 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => a*b*c=a*(b*c)]
Axiom
The principle of mathematical induction (starting at 0)
16 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
Prove: ALL(a):ALL(b):[a e n & b e n & ~a=0
=> ALL(c):[c e n => a^(b+c)=a^b*a^c]]
Suppose...
17 x e n & y e n & ~x=0
Premise
18 x e n
Split, 17
19 y e n
Split, 17
20 ~x=0
Split, 17
21 EXIST(sub):[Set(sub) & ALL(c):[c e sub <=> c e n & x^(y+c)=x^y*x^c]]
Subset, 5
22 Set(p) & ALL(c):[c e p <=> c e n & x^(y+c)=x^y*x^c]
E Spec, 21
Define: p
23 Set(p)
Split, 22
24 ALL(c):[c e p <=> c e n & x^(y+c)=x^y*x^c]
Split, 22
Apply Principle of Mathematical Induction
25 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, 16
Prove: ALL(b):[b e p => b e n]
Suppose...
26 t e p
Premise
27 t e p <=> t e n & x^(y+t)=x^y*x^t
U Spec, 24
28 [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, 27
29 t e p => t e n & x^(y+t)=x^y*x^t
Split, 28
30 t e n & x^(y+t)=x^y*x^t => t e p
Split, 28
31 t e n & x^(y+t)=x^y*x^t
Detach, 29, 26
32 t e n
Split, 31
As Required:
33 ALL(b):[b e p => b e n]
4 Conclusion, 26
34 Set(p) & ALL(b):[b e p => b e n]
Join, 23, 33
Sufficient: ALL(b):[b e n => b e p]
35 0 e p & ALL(b):[b e p => b+1 e p]
=> ALL(b):[b e n => b e p]
Detach, 25, 34
36 0 e p <=> 0 e n & x^(y+0)=x^y*x^0
U Spec, 24
37 [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, 36
38 0 e p => 0 e n & x^(y+0)=x^y*x^0
Split, 37
Sufficient: 0 e p
39 0 e n & x^(y+0)=x^y*x^0 => 0 e p
Split, 37
40 x^y=x^y
Reflex
41 y e n => y+0=y
U Spec, 10
42 y+0=y
Detach, 41, 19
43 x^(y+0)=x^y
Substitute, 42, 40
44 x^y e n => x^y*1=x^y
U Spec, 12
45 ALL(b):[x e n & b e n & ~[x=0 & b=0] => x^b e n]
U Spec, 1
46 x e n & y e n & ~[x=0 & y=0] => x^y e n
U Spec, 45
47 x=0 & y=0
Premise
48 x=0
Split, 47
49 y=0
Split, 47
50 x=0 & ~x=0
Join, 48, 20
51 ~[x=0 & y=0]
4 Conclusion, 47
52 x e n & y e n
Join, 18, 19
53 x e n & y e n & ~[x=0 & y=0]
Join, 52, 51
54 x^y e n
Detach, 46, 53
55 x^y*1=x^y
Detach, 44, 54
56 x^(y+0)=x^y*1
Substitute, 55, 43
57 x e n & ~x=0 => x^0=1
U Spec, 2
58 x e n & ~x=0
Join, 18, 20
59 x^0=1
Detach, 57, 58
60 x^(y+0)=x^y*x^0
Substitute, 59, 56
61 0 e n & x^(y+0)=x^y*x^0
Join, 6, 60
As Required:
62 0 e p
Detach, 39, 61
Prove: ALL(b):[b e p => b+1 e p]
Suppose...
63 t e p
Premise
64 t e p <=> t e n & x^(y+t)=x^y*x^t
U Spec, 24
65 [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, 64
66 t e p => t e n & x^(y+t)=x^y*x^t
Split, 65
67 t e n & x^(y+t)=x^y*x^t => t e p
Split, 65
68 t e n & x^(y+t)=x^y*x^t
Detach, 66, 63
69 t e n
Split, 68
70 x^(y+t)=x^y*x^t
Split, 68
71 t+1 e p <=> t+1 e n & x^(y+(t+1))=x^y*x^(t+1)
U Spec, 24
72 [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, 71
73 t+1 e p => t+1 e n & x^(y+(t+1))=x^y*x^(t+1)
Split, 72
Sufficient: t+1 e p
74 t+1 e n & x^(y+(t+1))=x^y*x^(t+1) => t+1 e p
Split, 72
75 ALL(b):[t e n & b e n => t+b e n]
U Spec, 7
76 t e n & 1 e n => t+1 e n
U Spec, 75
77 t e n & 1 e n
Join, 69, 9
78 t+1 e n
Detach, 76, 77
79 x^(y+(t+1))=x^(y+(t+1))
Reflex
80 ALL(b):ALL(c):[y e n & b e n & c e n => y+b+c=y+(b+c)]
U Spec, 13
81 ALL(c):[y e n & t e n & c e n => y+t+c=y+(t+c)]
U Spec, 80
82 y e n & t e n & 1 e n => y+t+1=y+(t+1)
U Spec, 81
83 y e n & t e n
Join, 19, 69
84 y e n & t e n & 1 e n
Join, 83, 9
85 y+t+1=y+(t+1)
Detach, 82, 84
86 x^(y+(t+1))=x^(y+t+1)
Substitute, 85, 79
87 ALL(b):[x e n & b e n & ~[x=0 & b=0] => x^(b+1)=x^b*x]
U Spec, 4
88 x e n & y+t e n & ~[x=0 & y+t=0] => x^(y+t+1)=x^(y+t)*x
U Spec, 87
89 ALL(b):[y e n & b e n => y+b e n]
U Spec, 7
90 y e n & t e n => y+t e n
U Spec, 89
91 y e n & t e n
Join, 19, 69
92 y+t e n
Detach, 90, 91
Prove: ~[x=0 & y+t=0]
Suppose to the contrary...
93 x=0 & y+t=0
Premise
94 x=0
Split, 93
95 y+t=0
Split, 93
96 x=0 & ~x=0
Join, 94, 20
As Required:
97 ~[x=0 & y+t=0]
4 Conclusion, 93
98 x e n & y+t e n
Join, 18, 92
99 x e n & y+t e n & ~[x=0 & y+t=0]
Join, 98, 97
100 x^(y+t+1)=x^(y+t)*x
Detach, 88, 99
101 x^(y+(t+1))=x^(y+t)*x
Substitute, 100, 86
102 x^(y+(t+1))=x^y*x^t*x
Substitute, 70, 101
103 x^y*x^(t+1)=x^y*x^(t+1)
Reflex
104 ALL(b):[x e n & b e n & ~[x=0 & b=0] => x^(b+1)=x^b*x]
U Spec, 4
105 x e n & t e n & ~[x=0 & t=0] => x^(t+1)=x^t*x
U Spec, 104
Prove: ~[x=0 & t=0]
Suppose to the contrary...
106 x=0 & t=0
Premise
107 x=0
Split, 106
108 t=0
Split, 106
109 x=0 & ~x=0
Join, 107, 20
As Required:
110 ~[x=0 & t=0]
4 Conclusion, 106
111 x e n & t e n
Join, 18, 69
112 x e n & t e n & ~[x=0 & t=0]
Join, 111, 110
113 x^(t+1)=x^t*x
Detach, 105, 112
114 x^y*x^(t+1)=x^y*(x^t*x)
Substitute, 113, 103
115 ALL(b):ALL(c):[x^y e n & b e n & c e n => x^y*b*c=x^y*(b*c)]
U Spec, 15
116 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, 115
117 x^y e n & x^t e n & x e n => x^y*x^t*x=x^y*(x^t*x)
U Spec, 116
118 ALL(b):[x e n & b e n & ~[x=0 & b=0] => x^b e n]
U Spec, 1
119 x e n & y e n & ~[x=0 & y=0] => x^y e n
U Spec, 118
120 x^y e n
Detach, 119, 53
121 ALL(b):[x e n & b e n & ~[x=0 & b=0] => x^b e n]
U Spec, 1
122 x e n & t e n & ~[x=0 & t=0] => x^t e n
U Spec, 121
123 x^t e n
Detach, 122, 112
124 x^y e n & x^t e n
Join, 120, 123
125 x^y e n & x^t e n & x e n
Join, 124, 18
126 x^y*x^t*x=x^y*(x^t*x)
Detach, 117, 125
127 x^y*x^(t+1)=x^y*x^t*x
Substitute, 126, 114
128 x^(y+(t+1))=x^y*x^(t+1)
Substitute, 127, 102
129 t+1 e n & x^(y+(t+1))=x^y*x^(t+1)
Join, 78, 128
130 t+1 e p
Detach, 74, 129
As Required:
131 ALL(b):[b e p => b+1 e p]
4 Conclusion, 63
132 0 e p & ALL(b):[b e p => b+1 e p]
Join, 62, 131
As Required:
133 ALL(b):[b e n => b e p]
Detach, 35, 132
Prove: ALL(c):[c e n => x^(y+c)=x^y*x^c]
Suppose...
134 t e n
Premise
135 t e n => t e p
U Spec, 133
136 t e p
Detach, 135, 134
137 t e p <=> t e n & x^(y+t)=x^y*x^t
U Spec, 24
138 [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, 137
139 t e p => t e n & x^(y+t)=x^y*x^t
Split, 138
140 t e n & x^(y+t)=x^y*x^t => t e p
Split, 138
141 t e n & x^(y+t)=x^y*x^t
Detach, 139, 136
142 t e n
Split, 141
143 x^(y+t)=x^y*x^t
Split, 141
As Required:
144 ALL(c):[c e n => x^(y+c)=x^y*x^c]
4 Conclusion, 134
As Required:
145 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, 17
Prove: ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n & ~a=0 => a^b*a^c=a^(b+c)]
Suppose...
146 x e n & y e n & z e n & ~x=0
Premise
147 x e n
Split, 146
148 y e n
Split, 146
149 z e n
Split, 146
150 ~x=0
Split, 146
151 ALL(b):[x e n & b e n & ~x=0
=> ALL(c):[c e n => x^(b+c)=x^b*x^c]]
U Spec, 145
152 x e n & y e n & ~x=0
=> ALL(c):[c e n => x^(y+c)=x^y*x^c]
U Spec, 151
153 x e n & y e n
Join, 147, 148
154 x e n & y e n & ~x=0
Join, 153, 150
155 ALL(c):[c e n => x^(y+c)=x^y*x^c]
Detach, 152, 154
156 z e n => x^(y+z)=x^y*x^z
U Spec, 155
157 x^(y+z)=x^y*x^z
Detach, 156, 149
158 x^y*x^z=x^(y+z)
Sym, 157
As Required:
159 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n & ~a=0 => a^b*a^c=a^(b+c)]
4 Conclusion, 146