THEOREM 5
*********
The Power of a Power Rule (x^y^z =x^(y*z)
ALL(a):ALL(b):[a e n & b e n
=> [~a=0 => ALL(c):[c e n => a^b^c=a^(b*c)]]]
Note: In DC Proof, the order of precedence is such that x^y^z=(x^y)^z
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
Distributivity of * over +
10 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => a*(b+c)=a*b+a*c]
Axiom
Product of Powers Rule (previous result)
11 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)
12 ALL(a):ALL(b):[a e n & b e n => [~a=0 => ~a^b=0]]
Axiom
Define: ^ (0^0 is an uspecified natural number)
*********
13 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
14 ALL(a):ALL(b):[a e n & b e n => a^b e n]
Split, 13
15 ALL(a):[a e n => [~a=0 => a^0=1]]
Split, 13
16 ALL(a):ALL(b):[a e n & b e n => a^(b+1)=a^b*a]
Split, 13
Prove: ALL(a):ALL(b):[a e n & b e n
=> [~a=0 => ALL(c):[c e n => a^(b*c)=a^b^c]]]
Suppose...
17 x e n & y e n
Premise
18 x e n
Split, 17
19 y e n
Split, 17
Prove: ~x=0 => ALL(c):[c e n => x^(y*c)=x^y^c]
Suppose...
20 ~x=0
Premise
Apply Subset Axiom (to do proof by induction)
21 EXIST(sub):[Set(sub) & ALL(c):[c e sub <=> c e n & x^(y*c)=x^y^c]]
Subset, 1
22 Set(p) & ALL(c):[c e p <=> c e n & x^(y*c)=x^y^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^c]
Split, 22
Apply PMI
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, 9
Prove: ALL(b):[b e p => b e n]
Suppose...
26 t e p
Premise
Apply definition of p
27 t e p <=> t e n & x^(y*t)=x^y^t
U Spec, 24
28 [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, 27
29 t e p => t e n & x^(y*t)=x^y^t
Split, 28
30 t e n & x^(y*t)=x^y^t => t e p
Split, 28
31 t e n & x^(y*t)=x^y^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
Prove: 0 e p
Apply definition of p
36 0 e p <=> 0 e n & x^(y*0)=x^y^0
U Spec, 24
37 [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, 36
38 0 e p => 0 e n & x^(y*0)=x^y^0
Split, 37
Sufficient: 0 e p
39 0 e n & x^(y*0)=x^y^0 => 0 e p
Split, 37
Prove: x^(y*0)=1
40 x^(y*0)=x^(y*0)
Reflex
41 y e n => y*0=0
U Spec, 7
42 y*0=0
Detach, 41, 19
43 x^(y*0)=x^0
Substitute, 42, 40
44 x e n => [~x=0 => x^0=1]
U Spec, 15
45 ~x=0 => x^0=1
Detach, 44, 18
46 x^0=1
Detach, 45, 20
LHS
As Required:
47 x^(y*0)=1
Substitute, 46, 43
48 x^y^0=x^y^0
Reflex
Apply previous result
49 ALL(b):[x e n & b e n => [~x=0 => ~x^b=0]]
U Spec, 12
50 x e n & y e n => [~x=0 => ~x^y=0]
U Spec, 49
51 ~x=0 => ~x^y=0
Detach, 50, 17
52 ~x^y=0
Detach, 51, 20
53 x^y e n => [~x^y=0 => x^y^0=1]
U Spec, 15
Apply definition of ^
54 ALL(b):[x e n & b e n => x^b e n]
U Spec, 14
55 x e n & y e n => x^y e n
U Spec, 54
56 x^y e n
Detach, 55, 17
57 ~x^y=0 => x^y^0=1
Detach, 53, 56
RHS
As Required:
58 x^y^0=1
Detach, 57, 52
59 x^(y*0)=x^y^0
Substitute, 58, 47
60 0 e n & x^(y*0)=x^y^0
Join, 4, 59
As Required:
61 0 e p
Detach, 39, 60
Prove: ALL(b):[b e p => b+1 e p]
Suppose...
62 t e p
Premise
Apply definition of p
63 t e p <=> t e n & x^(y*t)=x^y^t
U Spec, 24
64 [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, 63
65 t e p => t e n & x^(y*t)=x^y^t
Split, 64
66 t e n & x^(y*t)=x^y^t => t e p
Split, 64
67 t e n & x^(y*t)=x^y^t
Detach, 65, 62
68 t e n
Split, 67
69 x^(y*t)=x^y^t
Split, 67
Apply definition of p
70 t+1 e p <=> t+1 e n & x^(y*(t+1))=x^y^(t+1)
U Spec, 24
71 [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, 70
72 t+1 e p => t+1 e n & x^(y*(t+1))=x^y^(t+1)
Split, 71
Sufficient: t+1 e p
73 t+1 e n & x^(y*(t+1))=x^y^(t+1) => t+1 e p
Split, 71
74 ALL(b):[t e n & b e n => t+b e n]
U Spec, 2
75 t e n & 1 e n => t+1 e n
U Spec, 74
76 t e n & 1 e n
Join, 68, 5
77 t+1 e n
Detach, 75, 76
78 x^(y*(t+1))=x^(y*(t+1))
Reflex
Apply distributitivity
79 ALL(b):ALL(c):[y e n & b e n & c e n => y*(b+c)=y*b+y*c]
U Spec, 10
80 ALL(c):[y e n & t e n & c e n => y*(t+c)=y*t+y*c]
U Spec, 79
81 y e n & t e n & 1 e n => y*(t+1)=y*t+y*1
U Spec, 80
82 y e n & t e n
Join, 19, 68
83 y e n & t e n & 1 e n
Join, 82, 5
84 y*(t+1)=y*t+y*1
Detach, 81, 83
85 x^(y*(t+1))=x^(y*t+y*1)
Substitute, 84, 78
86 y e n => y*1=y
U Spec, 8
87 y*1=y
Detach, 86, 19
88 x^(y*(t+1))=x^(y*t+y)
Substitute, 87, 85
Apply previous result
89 ALL(b):ALL(c):[x e n & b e n & c e n => [~x=0 => x^(b+c)=x^b*x^c]]
U Spec, 11
90 ALL(c):[x e n & y*t e n & c e n => [~x=0 => x^(y*t+c)=x^(y*t)*x^c]]
U Spec, 89
91 x e n & y*t e n & y e n => [~x=0 => x^(y*t+y)=x^(y*t)*x^y]
U Spec, 90
92 ALL(b):[y e n & b e n => y*b e n]
U Spec, 3
93 y e n & t e n => y*t e n
U Spec, 92
94 y e n & t e n
Join, 19, 68
95 y*t e n
Detach, 93, 94
96 x e n & y*t e n
Join, 18, 95
97 x e n & y*t e n & y e n
Join, 96, 19
98 ~x=0 => x^(y*t+y)=x^(y*t)*x^y
Detach, 91, 97
99 x^(y*t+y)=x^(y*t)*x^y
Detach, 98, 20
100 x^(y*(t+1))=x^(y*t)*x^y
Substitute, 99, 88
101 x^(y*(t+1))=x^y^t*x^y
Substitute, 69, 100
Apply definition of ^
102 ALL(b):[x^y e n & b e n => x^y^(b+1)=x^y^b*x^y]
U Spec, 16
103 x^y e n & t e n => x^y^(t+1)=x^y^t*x^y
U Spec, 102
104 ALL(b):[x e n & b e n => x^b e n]
U Spec, 14
105 x e n & y e n => x^y e n
U Spec, 104
106 x^y e n
Detach, 105, 17
107 x^y e n & t e n
Join, 106, 68
108 x^y^(t+1)=x^y^t*x^y
Detach, 103, 107
109 x^(y*(t+1))=x^y^(t+1)
Substitute, 108, 101
110 t+1 e n & x^(y*(t+1))=x^y^(t+1)
Join, 77, 109
111 t+1 e p
Detach, 73, 110
As Required:
112 ALL(b):[b e p => b+1 e p]
4 Conclusion, 62
113 0 e p & ALL(b):[b e p => b+1 e p]
Join, 61, 112
114 ALL(b):[b e n => b e p]
Detach, 35, 113
Prove: ALL(c):[c e n => x^y^c=x^(y*c)]
Suppose...
115 t e n
Premise
116 t e n => t e p
U Spec, 114
117 t e p
Detach, 116, 115
Apply definition of p
118 t e p <=> t e n & x^(y*t)=x^y^t
U Spec, 24
119 [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, 118
120 t e p => t e n & x^(y*t)=x^y^t
Split, 119
121 t e n & x^(y*t)=x^y^t => t e p
Split, 119
122 t e n & x^(y*t)=x^y^t
Detach, 120, 117
123 t e n
Split, 122
124 x^(y*t)=x^y^t
Split, 122
125 x^y^t=x^(y*t)
Sym, 124
As Required:
126 ALL(c):[c e n => x^y^c=x^(y*c)]
4 Conclusion, 115
As Required:
127 ~x=0 => ALL(c):[c e n => x^y^c=x^(y*c)]
4 Conclusion, 20
As Required:
128 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, 17
Prove: ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => [~a=0 => a^b^c=a^(b*c)]]
Suppose...
129 x e n & y e n & z e n
Premise
130 x e n
Split, 129
131 y e n
Split, 129
132 z e n
Split, 129
133 x e n & y e n
Join, 130, 131
Prove: ~x=0 => x^y^z=x^(y*z)
Suppose...
134 ~x=0
Premise
135 ALL(b):[x e n & b e n
=> [~x=0 => ALL(c):[c e n => x^b^c=x^(b*c)]]]
U Spec, 128
136 x e n & y e n
=> [~x=0 => ALL(c):[c e n => x^y^c=x^(y*c)]]
U Spec, 135
137 x e n & y e n
Join, 130, 131
138 ~x=0 => ALL(c):[c e n => x^y^c=x^(y*c)]
Detach, 136, 137
139 ALL(c):[c e n => x^y^c=x^(y*c)]
Detach, 138, 134
140 z e n => x^y^z=x^(y*z)
U Spec, 139
141 x^y^z=x^(y*z)
Detach, 140, 132
As Required:
142 ~x=0 => x^y^z=x^(y*z)
4 Conclusion, 134
As Required:
143 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, 129