THEOREM
*******
The Power of a Product Rule: (x*y)^z = x^z * y*z
ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n & ~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 software available at http://www.dcproof.com
AXIOMS / DEFINITIONS USED
*************************
Define: ^ (partial function on n)
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
Multiplying by 1
10 ALL(a):[a e n => a*1=a]
Axiom
* is associative
11 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => a*b*c=a*(b*c)]
Axiom
* is commutative
12 ALL(a):ALL(b):[a e n & b e n => a*b=b*a]
Axiom
Zero-product Rule
13 ALL(a):ALL(b):[a e n & b e n => [a*b=0 => a=0 | b=0]]
Axiom
The principle of mathematical induction (starting at 0)
14 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 & ~b=0
=> ALL(c):[c e n => (a*b)^c=a^c*b^c]]
Suppose...
15 x e n & y e n & ~x=0 & ~y=0
Premise
16 x e n
Split, 15
17 y e n
Split, 15
18 ~x=0
Split, 15
19 ~y=0
Split, 15
20 EXIST(sub):[Set(sub) & ALL(c):[c e sub <=> c e n & (x*y)^c=x^c*y^c]]
Subset, 5
21 Set(p) & ALL(c):[c e p <=> c e n & (x*y)^c=x^c*y^c]
E Spec, 20
Define: p
22 Set(p)
Split, 21
23 ALL(c):[c e p <=> c e n & (x*y)^c=x^c*y^c]
Split, 21
24 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, 14
Prove: ALL(b):[b e p => b e n]
Suppose...
25 t e p
Premise
26 t e p <=> t e n & (x*y)^t=x^t*y^t
U Spec, 23
27 [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, 26
28 t e p => t e n & (x*y)^t=x^t*y^t
Split, 27
29 t e n & (x*y)^t=x^t*y^t => t e p
Split, 27
30 t e n & (x*y)^t=x^t*y^t
Detach, 28, 25
31 t e n
Split, 30
As Required:
32 ALL(b):[b e p => b e n]
4 Conclusion, 25
33 Set(p) & ALL(b):[b e p => b e n]
Join, 22, 32
Sufficient: ALL(b):[b e n => b e p]
34 0 e p & ALL(b):[b e p => b+1 e p]
=> ALL(b):[b e n => b e p]
Detach, 24, 33
35 0 e p <=> 0 e n & (x*y)^0=x^0*y^0
U Spec, 23
36 [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, 35
37 0 e p => 0 e n & (x*y)^0=x^0*y^0
Split, 36
Sufficient: 0 e p
38 0 e n & (x*y)^0=x^0*y^0 => 0 e p
Split, 36
LHS
39 (x*y)^0=(x*y)^0
Reflex
40 x*y e n & ~x*y=0 => (x*y)^0=1
U Spec, 2
41 ALL(b):[x e n & b e n => x*b e n]
U Spec, 8
42 x e n & y e n => x*y e n
U Spec, 41
43 x e n & y e n
Join, 16, 17
44 x*y e n
Detach, 42, 43
45 ALL(b):[x e n & b e n => [x*b=0 => x=0 | b=0]]
U Spec, 13
46 x e n & y e n => [x*y=0 => x=0 | y=0]
U Spec, 45
47 x e n & y e n
Join, 16, 17
48 x*y=0 => x=0 | y=0
Detach, 46, 47
49 ~[x=0 | y=0] => ~x*y=0
Contra, 48
50 ~~[~x=0 & ~y=0] => ~x*y=0
DeMorgan, 49
51 ~x=0 & ~y=0 => ~x*y=0
Rem DNeg, 50
52 ~x=0 & ~y=0
Join, 18, 19
53 ~x*y=0
Detach, 51, 52
54 x*y e n & ~x*y=0
Join, 44, 53
LHS
55 (x*y)^0=1
Detach, 40, 54
RHS
56 x^0*y^0=x^0*y^0
Reflex
57 x e n & ~x=0 => x^0=1
U Spec, 2
58 x e n & ~x=0
Join, 16, 18
59 x^0=1
Detach, 57, 58
60 x^0*y^0=1*y^0
Substitute, 59, 56
61 y e n & ~y=0 => y^0=1
U Spec, 2
62 y e n & ~y=0
Join, 17, 19
63 y^0=1
Detach, 61, 62
64 x^0*y^0=1*1
Substitute, 63, 60
65 1 e n => 1*1=1
U Spec, 10
66 1*1=1
Detach, 65, 9
RHS
67 x^0*y^0=1
Substitute, 66, 64
68 (x*y)^0=x^0*y^0
Substitute, 67, 55
69 0 e n & (x*y)^0=x^0*y^0
Join, 6, 68
As Required:
70 0 e p
Detach, 38, 69
Prove: ALL(b):[b e p => b+1 e p]
Suppose...
71 t e p
Premise
72 t e p <=> t e n & (x*y)^t=x^t*y^t
U Spec, 23
73 [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, 72
74 t e p => t e n & (x*y)^t=x^t*y^t
Split, 73
75 t e n & (x*y)^t=x^t*y^t => t e p
Split, 73
76 t e n & (x*y)^t=x^t*y^t
Detach, 74, 71
77 t e n
Split, 76
78 (x*y)^t=x^t*y^t
Split, 76
79 t+1 e p <=> t+1 e n & (x*y)^(t+1)=x^(t+1)*y^(t+1)
U Spec, 23
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:
82 t+1 e n & (x*y)^(t+1)=x^(t+1)*y^(t+1) => t+1 e p
Split, 80
83 ALL(b):[t e n & b e n => t+b e n]
U Spec, 7
84 t e n & 1 e n => t+1 e n
U Spec, 83
85 t e n & 1 e n
Join, 77, 9
86 t+1 e n
Detach, 84, 85
LHS
87 (x*y)^(t+1)=(x*y)^(t+1)
Reflex
88 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, 4
89 x*y e n & t e n & ~[x*y=0 & t=0] => (x*y)^(t+1)=(x*y)^t*(x*y)
U Spec, 88
Prove: ~[x*y=0 & t=0]
Suppose to contrary...
90 x*y=0 & t=0
Premise
91 x*y=0
Split, 90
92 t=0
Split, 90
93 x*y=0 & ~x*y=0
Join, 91, 53
As Required:
94 ~[x*y=0 & t=0]
4 Conclusion, 90
95 x*y e n & t e n
Join, 44, 77
96 x*y e n & t e n & ~[x*y=0 & t=0]
Join, 95, 94
97 (x*y)^(t+1)=(x*y)^t*(x*y)
Detach, 89, 96
98 (x*y)^(t+1)=(x*y)^t*(x*y)
Substitute, 97, 87
99 (x*y)^(t+1)=x^t*y^t*(x*y)
Substitute, 78, 98
RHS
100 x^(t+1)*y^(t+1)=x^(t+1)*y^(t+1)
Reflex
101 ALL(b):[x e n & b e n & ~[x=0 & b=0] => x^(b+1)=x^b*x]
U Spec, 4
102 x e n & t e n & ~[x=0 & t=0] => x^(t+1)=x^t*x
U Spec, 101
Prove: ~[x=0 & t=0]
Suppose to the contrary...
103 x=0 & t=0
Premise
104 x=0
Split, 103
105 t=0
Split, 103
106 x=0 & ~x=0
Join, 104, 18
As Required:
107 ~[x=0 & t=0]
4 Conclusion, 103
108 x e n & t e n
Join, 16, 77
109 x e n & t e n & ~[x=0 & t=0]
Join, 108, 107
110 x^(t+1)=x^t*x
Detach, 102, 109
111 x^(t+1)*y^(t+1)=x^t*x*y^(t+1)
Substitute, 110, 100
112 ALL(b):[y e n & b e n & ~[y=0 & b=0] => y^(b+1)=y^b*y]
U Spec, 4
113 y e n & t e n & ~[y=0 & t=0] => y^(t+1)=y^t*y
U Spec, 112
Prove: ~[y=0 & t=0]
Suppose...
114 y=0 & t=0
Premise
115 y=0
Split, 114
116 t=0
Split, 114
117 y=0 & ~y=0
Join, 115, 19
As Required:
118 ~[y=0 & t=0]
4 Conclusion, 114
119 y e n & t e n
Join, 17, 77
120 y e n & t e n & ~[y=0 & t=0]
Join, 119, 118
121 y^(t+1)=y^t*y
Detach, 113, 120
122 x^(t+1)*y^(t+1)=x^t*x*(y^t*y)
Substitute, 121, 111
123 ALL(b):ALL(c):[x^t e n & b e n & c e n => x^t*b*c=x^t*(b*c)]
U Spec, 11
124 ALL(c):[x^t e n & x e n & c e n => x^t*x*c=x^t*(x*c)]
U Spec, 123
125 x^t e n & x e n & y^t*y e n => x^t*x*(y^t*y)=x^t*(x*(y^t*y))
U Spec, 124
126 ALL(b):[x e n & b e n & ~[x=0 & b=0] => x^b e n]
U Spec, 1
127 x e n & t e n & ~[x=0 & t=0] => x^t e n
U Spec, 126
128 x^t e n
Detach, 127, 109
129 ALL(b):[y^t e n & b e n => y^t*b e n]
U Spec, 8
130 y^t e n & y e n => y^t*y e n
U Spec, 129
131 ALL(b):[y e n & b e n & ~[y=0 & b=0] => y^b e n]
U Spec, 1
132 y e n & t e n & ~[y=0 & t=0] => y^t e n
U Spec, 131
133 y^t e n
Detach, 132, 120
134 y^t e n & y e n
Join, 133, 17
135 y^t*y e n
Detach, 130, 134
136 x^t e n & x e n
Join, 128, 16
137 x^t e n & x e n & y^t*y e n
Join, 136, 135
138 x^t*x*(y^t*y)=x^t*(x*(y^t*y))
Detach, 125, 137
139 x^(t+1)*y^(t+1)=x^t*(x*(y^t*y))
Substitute, 138, 122
140 ALL(b):[x e n & b e n => x*b=b*x]
U Spec, 12
141 x e n & y^t*y e n => x*(y^t*y)=y^t*y*x
U Spec, 140
142 x e n & y^t*y e n
Join, 16, 135
143 x*(y^t*y)=y^t*y*x
Detach, 141, 142
144 x^(t+1)*y^(t+1)=x^t*(y^t*y*x)
Substitute, 143, 139
145 ALL(b):ALL(c):[y^t e n & b e n & c e n => y^t*b*c=y^t*(b*c)]
U Spec, 11
146 ALL(c):[y^t e n & y e n & c e n => y^t*y*c=y^t*(y*c)]
U Spec, 145
147 y^t e n & y e n & x e n => y^t*y*x=y^t*(y*x)
U Spec, 146
148 y^t e n & y e n
Join, 133, 17
149 y^t e n & y e n & x e n
Join, 148, 16
150 y^t*y*x=y^t*(y*x)
Detach, 147, 149
151 x^(t+1)*y^(t+1)=x^t*(y^t*(y*x))
Substitute, 150, 144
152 ALL(b):[x e n & b e n => x*b=b*x]
U Spec, 12
153 x e n & y e n => x*y=y*x
U Spec, 152
154 x e n & y e n
Join, 16, 17
155 x*y=y*x
Detach, 153, 154
156 x^(t+1)*y^(t+1)=x^t*(y^t*(x*y))
Substitute, 155, 151
157 ALL(b):ALL(c):[x^t e n & b e n & c e n => x^t*b*c=x^t*(b*c)]
U Spec, 11
158 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, 157
159 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, 158
160 ALL(b):[x e n & b e n => x*b e n]
U Spec, 8
161 x e n & y e n => x*y e n
U Spec, 160
162 x e n & y e n
Join, 16, 17
163 x*y e n
Detach, 161, 162
164 x^t e n & y^t e n
Join, 128, 133
165 x^t e n & y^t e n & x*y e n
Join, 164, 163
166 x^t*y^t*(x*y)=x^t*(y^t*(x*y))
Detach, 159, 165
167 x^(t+1)*y^(t+1)=x^t*y^t*(x*y)
Substitute, 166, 156
168 (x*y)^(t+1)=x^(t+1)*y^(t+1)
Substitute, 167, 99
169 t+1 e n & (x*y)^(t+1)=x^(t+1)*y^(t+1)
Join, 86, 168
170 t+1 e p
Detach, 82, 169
As Required:
171 ALL(b):[b e p => b+1 e p]
4 Conclusion, 71
172 0 e p & ALL(b):[b e p => b+1 e p]
Join, 70, 171
As Required:
173 ALL(b):[b e n => b e p]
Detach, 34, 172
Prove: ALL(c):[c e n => (x*y)^c=x^c*y^c]
Suppose...
174 t e n
Premise
175 t e n => t e p
U Spec, 173
176 t e p
Detach, 175, 174
177 t e p <=> t e n & (x*y)^t=x^t*y^t
U Spec, 23
178 [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, 177
179 t e p => t e n & (x*y)^t=x^t*y^t
Split, 178
180 t e n & (x*y)^t=x^t*y^t => t e p
Split, 178
181 t e n & (x*y)^t=x^t*y^t
Detach, 179, 176
182 t e n
Split, 181
183 (x*y)^t=x^t*y^t
Split, 181
As Required:
184 ALL(c):[c e n => (x*y)^c=x^c*y^c]
4 Conclusion, 174
As Required:
185 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, 15
Prove: ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n & ~a=0 & ~b=0
=> (a*b)^c=a^c*b^c]
Suppose...
186 x e n & y e n & z e n & ~x=0 & ~y=0
Premise
187 x e n
Split, 186
188 y e n
Split, 186
189 z e n
Split, 186
190 ~x=0
Split, 186
191 ~y=0
Split, 186
192 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, 185
193 x e n & y e n & ~x=0 & ~y=0
=> ALL(c):[c e n => (x*y)^c=x^c*y^c]
U Spec, 192
194 x e n & y e n
Join, 187, 188
195 x e n & y e n & ~x=0
Join, 194, 190
196 x e n & y e n & ~x=0 & ~y=0
Join, 195, 191
197 ALL(c):[c e n => (x*y)^c=x^c*y^c]
Detach, 193, 196
198 z e n => (x*y)^z=x^z*y^z
U Spec, 197
199 (x*y)^z=x^z*y^z
Detach, 198, 189
As Required:
200 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n & ~a=0 & ~b=0
=> (a*b)^c=a^c*b^c]
4 Conclusion, 186