THEOREM
*******
The Power of a Power Rule: x^y^z = x^(y*z)
ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n & ~a=0 => a^b^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)
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 0
10 ALL(a):[a e n => a*0=0]
Axiom
Multiplying by 1
11 ALL(a):[a e n => a*1=a]
Axiom
* is distributive over +
12 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => a*(b+c)=a*b+a*c]
Axiom
The principle of mathematical induction (starting at 0)
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
PREVIOUS RESULTS
****************
Powers of a non-zero base are non-zero PROOF
14 ALL(a):ALL(b):[a e n & b e n & ~a=0 => ~a^b=0]
Axiom
Product of Powers Rule PROOF
15 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n & ~a=0 => a^b*a^c=a^(b+c)]
Axiom
PROOF
*****
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...
16 x e n & y e n & ~x=0
Premise
17 x e n
Split, 16
18 y e n
Split, 16
19 ~x=0
Split, 16
20 EXIST(sub):[Set(sub) & ALL(c):[c e sub <=> c e n & x^(y*c)=x^y^c]]
Subset, 5
21 Set(p) & ALL(c):[c e p <=> c e n & x^(y*c)=x^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^y^c]
Split, 21
Apply Principle of Mathmatical Induction
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, 13
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^y^t
U Spec, 23
27 [t e p => t e n & x^(y*t)=x^y^t]
& [t e n & x^(y*t)=x^y^t => t e p]
Iff-And, 26
28 t e p => t e n & x^(y*t)=x^y^t
Split, 27
29 t e n & x^(y*t)=x^y^t => t e p
Split, 27
30 t e n & x^(y*t)=x^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^y^0
U Spec, 23
36 [0 e p => 0 e n & x^(y*0)=x^y^0]
& [0 e n & x^(y*0)=x^y^0 => 0 e p]
Iff-And, 35
37 0 e p => 0 e n & x^(y*0)=x^y^0
Split, 36
38 0 e n & x^(y*0)=x^y^0 => 0 e p
Split, 36
39 x^(y*0)=x^(y*0)
Reflex
40 y e n => y*0=0
U Spec, 10
41 y*0=0
Detach, 40, 18
42 x^(y*0)=x^0
Substitute, 41, 39
43 x e n & ~x=0 => x^0=1
U Spec, 2
44 x e n & ~x=0
Join, 17, 19
45 x^0=1
Detach, 43, 44
46 x^(y*0)=1
Substitute, 45, 42
47 x^y^0=x^y^0
Reflex
48 x^y e n & ~x^y=0 => x^y^0=1
U Spec, 2
49 ALL(b):[x e n & b e n & ~[x=0 & b=0] => x^b e n]
U Spec, 1
50 x e n & y e n & ~[x=0 & y=0] => x^y e n
U Spec, 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, 19
As Required:
55 ~[x=0 & y=0]
4 Conclusion, 51
56 x e n & y e n
Join, 17, 18
57 x e n & y e n & ~[x=0 & y=0]
Join, 56, 55
58 x^y e n
Detach, 50, 57
59 ALL(b):[x e n & b e n & ~x=0 => ~x^b=0]
U Spec, 14
60 x e n & y e n & ~x=0 => ~x^y=0
U Spec, 59
61 ~x^y=0
Detach, 60, 16
62 x^y e n & ~x^y=0
Join, 58, 61
63 x^y^0=1
Detach, 48, 62
64 x^(y*0)=x^y^0
Substitute, 63, 46
65 0 e n & x^(y*0)=x^y^0
Join, 6, 64
As Required:
66 0 e p
Detach, 38, 65
Prove: ALL(b):[b e p => b+1 e p]
Suppose...
67 t e p
Premise
68 t e p <=> t e n & x^(y*t)=x^y^t
U Spec, 23
69 [t e p => t e n & x^(y*t)=x^y^t]
& [t e n & x^(y*t)=x^y^t => t e p]
Iff-And, 68
70 t e p => t e n & x^(y*t)=x^y^t
Split, 69
71 t e n & x^(y*t)=x^y^t => t e p
Split, 69
72 t e n & x^(y*t)=x^y^t
Detach, 70, 67
73 t e n
Split, 72
74 x^(y*t)=x^y^t
Split, 72
75 t+1 e p <=> t+1 e n & x^(y*(t+1))=x^y^(t+1)
U Spec, 23
76 [t+1 e p => t+1 e n & x^(y*(t+1))=x^y^(t+1)]
& [t+1 e n & x^(y*(t+1))=x^y^(t+1) => t+1 e p]
Iff-And, 75
77 t+1 e p => t+1 e n & x^(y*(t+1))=x^y^(t+1)
Split, 76
Sufficient: t+1 e p
78 t+1 e n & x^(y*(t+1))=x^y^(t+1) => t+1 e p
Split, 76
79 ALL(b):[t e n & b e n => t+b e n]
U Spec, 7
80 t e n & 1 e n => t+1 e n
U Spec, 79
81 t e n & 1 e n
Join, 73, 9
82 t+1 e n
Detach, 80, 81
83 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
84 x^y e n & t e n & ~[x^y=0 & t=0] => x^y^(t+1)=x^y^t*x^y
U Spec, 83
85 x^y e n & t e n & ~~[~x^y=0 | ~t=0] => x^y^(t+1)=x^y^t*x^y
DeMorgan, 84
86 x^y e n & t e n & [~x^y=0 | ~t=0] => x^y^(t+1)=x^y^t*x^y
Rem DNeg, 85
87 ALL(b):[x e n & b e n & ~[x=0 & b=0] => x^b e n]
U Spec, 1
88 x e n & y e n & ~[x=0 & y=0] => x^y e n
U Spec, 87
Prove: ~[x=0 & y=0]
Suppose to the contrary...
89 x=0 & y=0
Premise
90 x=0
Split, 89
91 y=0
Split, 89
92 x=0 & ~x=0
Join, 90, 19
As Required:
93 ~[x=0 & y=0]
4 Conclusion, 89
94 x e n & y e n
Join, 17, 18
95 x e n & y e n & ~[x=0 & y=0]
Join, 94, 93
96 x^y e n
Detach, 88, 95
97 ALL(b):[x e n & b e n & ~x=0 => ~x^b=0]
U Spec, 14
98 x e n & y e n & ~x=0 => ~x^y=0
U Spec, 97
99 x e n & y e n
Join, 17, 18
100 x e n & y e n & ~x=0
Join, 99, 19
101 ~x^y=0
Detach, 98, 100
102 ~x^y=0 | ~t=0
Arb Or, 101
103 x^y e n & t e n
Join, 96, 73
104 x^y e n & t e n & [~x^y=0 | ~t=0]
Join, 103, 102
105 x^y^(t+1)=x^y^t*x^y
Detach, 86, 104
RHS
106 x^y^(t+1)=x^(y*t)*x^y
Substitute, 74, 105
107 x^(y*(t+1))=x^(y*(t+1))
Reflex
108 ALL(b):ALL(c):[y e n & b e n & c e n => y*(b+c)=y*b+y*c]
U Spec, 12
109 ALL(c):[y e n & t e n & c e n => y*(t+c)=y*t+y*c]
U Spec, 108
110 y e n & t e n & 1 e n => y*(t+1)=y*t+y*1
U Spec, 109
111 y e n & t e n
Join, 18, 73
112 y e n & t e n & 1 e n
Join, 111, 9
113 y e n & t e n & 1 e n
Join, 111, 9
114 y*(t+1)=y*t+y*1
Detach, 110, 113
115 x^(y*(t+1))=x^(y*t+y*1)
Substitute, 114, 107
116 y e n => y*1=y
U Spec, 11
117 y*1=y
Detach, 116, 18
118 x^(y*(t+1))=x^(y*t+y)
Substitute, 117, 115
119 ALL(b):ALL(c):[x e n & b e n & c e n & ~x=0 => x^b*x^c=x^(b+c)]
U Spec, 15
120 ALL(c):[x e n & y*t e n & c e n & ~x=0 => x^(y*t)*x^c=x^(y*t+c)]
U Spec, 119
121 x e n & y*t e n & y e n & ~x=0 => x^(y*t)*x^y=x^(y*t+y)
U Spec, 120
122 ALL(b):[y e n & b e n => y*b e n]
U Spec, 8
123 y e n & t e n => y*t e n
U Spec, 122
124 y e n & t e n
Join, 18, 73
125 y*t e n
Detach, 123, 124
126 x e n & y*t e n
Join, 17, 125
127 x e n & y*t e n & y e n
Join, 126, 18
128 x e n & y*t e n & y e n & ~x=0
Join, 127, 19
129 x^(y*t)*x^y=x^(y*t+y)
Detach, 121, 128
LHS
130 x^(y*(t+1))=x^(y*t)*x^y
Substitute, 129, 118
LHS=RHS
131 x^(y*(t+1))=x^y^(t+1)
Substitute, 106, 130
132 t+1 e n & x^(y*(t+1))=x^y^(t+1)
Join, 82, 131
133 t+1 e p
Detach, 78, 132
As Required:
134 ALL(b):[b e p => b+1 e p]
4 Conclusion, 67
135 0 e p & ALL(b):[b e p => b+1 e p]
Join, 66, 134
As Required:
136 ALL(b):[b e n => b e p]
Detach, 34, 135
Prove: ALL(c):[c e n => x^(y*c)=x^y^c]
Suppose...
137 t e n
Premise
138 t e n => t e p
U Spec, 136
139 t e p
Detach, 138, 137
140 t e p <=> t e n & x^(y*t)=x^y^t
U Spec, 23
141 [t e p => t e n & x^(y*t)=x^y^t]
& [t e n & x^(y*t)=x^y^t => t e p]
Iff-And, 140
142 t e p => t e n & x^(y*t)=x^y^t
Split, 141
143 t e n & x^(y*t)=x^y^t => t e p
Split, 141
144 t e n & x^(y*t)=x^y^t
Detach, 142, 139
145 t e n
Split, 144
146 x^(y*t)=x^y^t
Split, 144
As Required:
147 ALL(c):[c e n => x^(y*c)=x^y^c]
4 Conclusion, 137
As Required:
148 ALL(a):ALL(b):[a e n & b e n & ~a=0
=> ALL(c):[c e n => a^(b*c)=a^b^c]]
4 Conclusion, 16
149 x e n & y e n & z e n & ~x=0
Premise
150 x e n
Split, 149
151 y e n
Split, 149
152 z e n
Split, 149
153 ~x=0
Split, 149
154 ALL(b):[x e n & b e n & ~x=0
=> ALL(c):[c e n => x^(b*c)=x^b^c]]
U Spec, 148
155 x e n & y e n & ~x=0
=> ALL(c):[c e n => x^(y*c)=x^y^c]
U Spec, 154
156 x e n & y e n
Join, 150, 151
157 x e n & y e n & ~x=0
Join, 156, 153
158 ALL(c):[c e n => x^(y*c)=x^y^c]
Detach, 155, 157
159 z e n => x^(y*z)=x^y^z
U Spec, 158
160 x^(y*z)=x^y^z
Detach, 159, 152
161 x^y^z=x^(y*z)
Sym, 160
As Required:
162 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n & ~a=0 => a^b^c=a^(b*c)]
4 Conclusion, 149