THEOREM 4
*********
The Product of Powers Rule: x^y * x^z = x^(y+z+)
ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n
=> [~a=0 => a^b*a^c=a^(b+c)]]
By Dan Christensen
October 2013
(This proof was written with the aid the author's DC Proof software available 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
Associativity of *
11 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => a*b*c=a*(b*c)]
Axiom
Commutativity of *
12 ALL(a):ALL(b):[a e n & b e n => a*b=b*a]
Axiom
Right cancelability of +
13 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
14 ALL(a):[a e n => ~a+1=0]
Axiom
Existence of a predecessor
15 ALL(a):[a e n => [~a=0 => EXIST(b):[b e n & b+1=a]]]
Axiom
Define: ^ (0^0 is an unspecified natural number)
*********
16 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
17 ALL(a):ALL(b):[a e n & b e n => a^b e n]
Split, 16
18 ALL(a):[a e n => [~a=0 => a^0=1]]
Split, 16
19 ALL(a):ALL(b):[a e n & b e n => a^(b+1)=a^b*a]
Split, 16
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...
20 x e n & y e n
Premise
21 x e n
Split, 20
22 y e n
Split, 20
Prove: ~x=0 => ALL(c):[c e n => x^(y+c)=x^y*x^c]
Suppose...
23 ~x=0
Premise
24 EXIST(sub):[Set(sub) & ALL(c):[c e sub <=> c e n & x^(y+c)=x^y*x^c]]
Subset, 1
25 Set(p) & ALL(c):[c e p <=> c e n & x^(y+c)=x^y*x^c]
E Spec, 24
Define: p
26 Set(p)
Split, 25
27 ALL(c):[c e p <=> c e n & x^(y+c)=x^y*x^c]
Split, 25
28 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...
29 t e p
Premise
30 t e p <=> t e n & x^(y+t)=x^y*x^t
U Spec, 27
31 [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, 30
32 t e p => t e n & x^(y+t)=x^y*x^t
Split, 31
33 t e n & x^(y+t)=x^y*x^t => t e p
Split, 31
34 t e n & x^(y+t)=x^y*x^t
Detach, 32, 29
35 t e n
Split, 34
As Required:
36 ALL(b):[b e p => b e n]
4 Conclusion, 29
37 Set(p) & ALL(b):[b e p => b e n]
Join, 26, 36
Sufficient: ALL(b):[b e n => b e p]
38 0 e p & ALL(b):[b e p => b+1 e p]
=> ALL(b):[b e n => b e p]
Detach, 28, 37
39 0 e p <=> 0 e n & x^(y+0)=x^y*x^0
U Spec, 27
40 [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, 39
41 0 e p => 0 e n & x^(y+0)=x^y*x^0
Split, 40
Sufficient: 0 e p
42 0 e n & x^(y+0)=x^y*x^0 => 0 e p
Split, 40
43 x^(y+0)=x^(y+0)
Reflex
44 y e n => y+0=y
U Spec, 6
45 y+0=y
Detach, 44, 22
LHS
46 x^(y+0)=x^y
Substitute, 45, 43
47 x^y*x^0=x^y*x^0
Reflex
48 x e n => [~x=0 => x^0=1]
U Spec, 18
49 ~x=0 => x^0=1
Detach, 48, 21
50 x^0=1
Detach, 49, 23
51 x^y*x^0=x^y*1
Substitute, 50, 47
52 x^y e n => x^y*1=x^y
U Spec, 8
53 ALL(b):[x e n & b e n => x^b e n]
U Spec, 17
54 x e n & y e n => x^y e n
U Spec, 53
55 x^y e n
Detach, 54, 20
56 x^y*1=x^y
Detach, 52, 55
RHS
57 x^y*x^0=x^y
Substitute, 56, 51
58 x^(y+0)=x^y*x^0
Substitute, 57, 46
59 0 e n & x^(y+0)=x^y*x^0
Join, 4, 58
As Required:
60 0 e p
Detach, 42, 59
Prove: ALL(b):[b e p => b+1 e p]
Suppose...
61 t e p
Premise
62 t e p <=> t e n & x^(y+t)=x^y*x^t
U Spec, 27
63 [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, 62
64 t e p => t e n & x^(y+t)=x^y*x^t
Split, 63
65 t e n & x^(y+t)=x^y*x^t => t e p
Split, 63
66 t e n & x^(y+t)=x^y*x^t
Detach, 64, 61
67 t e n
Split, 66
68 x^(y+t)=x^y*x^t
Split, 66
69 t+1 e p <=> t+1 e n & x^(y+(t+1))=x^y*x^(t+1)
U Spec, 27
70 [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, 69
71 t+1 e p => t+1 e n & x^(y+(t+1))=x^y*x^(t+1)
Split, 70
Sufficient: t+1 e p
72 t+1 e n & x^(y+(t+1))=x^y*x^(t+1) => t+1 e p
Split, 70
73 ALL(b):[t e n & b e n => t+b e n]
U Spec, 2
74 t e n & 1 e n => t+1 e n
U Spec, 73
75 t e n & 1 e n
Join, 67, 5
76 t+1 e n
Detach, 74, 75
77 x^(y+(t+1))=x^(y+(t+1))
Reflex
78 ALL(b):ALL(c):[y e n & b e n & c e n => y+b+c=y+(b+c)]
U Spec, 10
79 ALL(c):[y e n & t e n & c e n => y+t+c=y+(t+c)]
U Spec, 78
80 y e n & t e n & 1 e n => y+t+1=y+(t+1)
U Spec, 79
81 y e n & t e n
Join, 22, 67
82 y e n & t e n & 1 e n
Join, 81, 5
83 y+t+1=y+(t+1)
Detach, 80, 82
84 x^(y+(t+1))=x^(y+t+1)
Substitute, 83, 77
85 ALL(b):[x e n & b e n => x^(b+1)=x^b*x]
U Spec, 19
86 x e n & y+t e n => x^(y+t+1)=x^(y+t)*x
U Spec, 85
87 ALL(b):[y e n & b e n => y+b e n]
U Spec, 2
88 y e n & t e n => y+t e n
U Spec, 87
89 y e n & t e n
Join, 22, 67
90 y+t e n
Detach, 88, 89
91 x e n & y+t e n
Join, 21, 90
92 x^(y+t+1)=x^(y+t)*x
Detach, 86, 91
93 x^(y+(t+1))=x^(y+t)*x
Substitute, 92, 84
LHS
94 x^(y+(t+1))=x^y*x^t*x
Substitute, 68, 93
95 x^y*x^(t+1)=x^y*x^(t+1)
Reflex
96 ALL(b):[x e n & b e n => x^(b+1)=x^b*x]
U Spec, 19
97 x e n & t e n => x^(t+1)=x^t*x
U Spec, 96
98 x e n & t e n
Join, 21, 67
99 x^(t+1)=x^t*x
Detach, 97, 98
100 x^y*x^(t+1)=x^y*(x^t*x)
Substitute, 99, 95
101 ALL(b):ALL(c):[x^y e n & b e n & c e n => x^y*b*c=x^y*(b*c)]
U Spec, 11
102 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, 101
103 x^y e n & x^t e n & x e n => x^y*x^t*x=x^y*(x^t*x)
U Spec, 102
104 ALL(b):[x e n & b e n => x^b e n]
U Spec, 17
105 x e n & y e n => x^y e n
U Spec, 104
106 x^y e n
Detach, 105, 20
107 x e n & t e n => x^t e n
U Spec, 104
108 x e n & t e n
Join, 21, 67
109 x^t e n
Detach, 107, 108
110 x^y e n & x^t e n
Join, 106, 109
111 x^y e n & x^t e n & x e n
Join, 110, 21
112 x^y*x^t*x=x^y*(x^t*x)
Detach, 103, 111
RHS
113 x^y*x^(t+1)=x^y*x^t*x
Substitute, 112, 100
114 x^(y+(t+1))=x^y*x^(t+1)
Substitute, 113, 94
115 t+1 e n & x^(y+(t+1))=x^y*x^(t+1)
Join, 76, 114
116 t+1 e p
Detach, 72, 115
As Required:
117 ALL(b):[b e p => b+1 e p]
4 Conclusion, 61
118 0 e p & ALL(b):[b e p => b+1 e p]
Join, 60, 117
As Required:
119 ALL(b):[b e n => b e p]
Detach, 38, 118
Prove: ALL(c):[c e n => x^(y+c)=x^y*x^c]
Suppose...
120 t e n
Premise
121 t e n => t e p
U Spec, 119
122 t e p
Detach, 121, 120
123 t e p <=> t e n & x^(y+t)=x^y*x^t
U Spec, 27
124 [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, 123
125 t e p => t e n & x^(y+t)=x^y*x^t
Split, 124
126 t e n & x^(y+t)=x^y*x^t => t e p
Split, 124
127 t e n & x^(y+t)=x^y*x^t
Detach, 125, 122
128 t e n
Split, 127
129 x^(y+t)=x^y*x^t
Split, 127
As Required:
130 ALL(c):[c e n => x^(y+c)=x^y*x^c]
4 Conclusion, 120
As Required:
131 ~x=0 => ALL(c):[c e n => x^(y+c)=x^y*x^c]
4 Conclusion, 23
As Required:
132 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, 20
Prove: ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => [~a=0 => a^(b+c)=a^b*a^c]]
Suppose...
133 x e n & y e n & z e n
Premise
134 x e n
Split, 133
135 y e n
Split, 133
136 z e n
Split, 133
Prove: ~x=0 => x^(y+z)=x^y*x^z
Suppose...
137 ~x=0
Premise
138 ALL(b):[x e n & b e n
=> [~x=0 => ALL(c):[c e n => x^(b+c)=x^b*x^c]]]
U Spec, 132
139 x e n & y e n
=> [~x=0 => ALL(c):[c e n => x^(y+c)=x^y*x^c]]
U Spec, 138
140 x e n & y e n
Join, 134, 135
141 ~x=0 => ALL(c):[c e n => x^(y+c)=x^y*x^c]
Detach, 139, 140
142 ALL(c):[c e n => x^(y+c)=x^y*x^c]
Detach, 141, 137
143 z e n => x^(y+z)=x^y*x^z
U Spec, 142
144 x^(y+z)=x^y*x^z
Detach, 143, 136
As Required:
145 ~x=0 => x^(y+z)=x^y*x^z
4 Conclusion, 137
As Required:
146 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => [~a=0 => a^(b+c)=a^b*a^c]]
4 Conclusion, 133
As Required:
147 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => [~a=0 => a^b*a^c=a^(b+c)]]
Sym, 146