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