THEOREM
*******
Given the set of natural numbers n, a binary function * that is closed on s, and binary function pow such that
for all x e s:
pow(x,1) = x
pow(x,2) = x*x
pow(x,3) = x*x*x
and so on.
Then
pow(x,y+z)=pow(x,y)*pow(x,z)
This formal proof was written and machine-verified with the aid of the author's DC Proof 2.0 available at http://www.dcproof.com
REQUIRED PROPERTIES OF N
************************
1 Set(n)
Axiom
2 1 e n
Axiom
Required properties of +
3 ALL(a):ALL(b):[a e n & b e n => a+b e n]
Axiom
4 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => a+b+c=a+(b+c)]
Axiom
Induction
5 ALL(a):[Set(a) & ALL(b):[b e a => b e n] => [1 e a & ALL(b):[b e a => b+1 e a] => ALL(b):[b e n => b e a]]]
Axiom
PROOF
*****
Prove: ALL(s):ALL(pow):[Set(s)
& ALL(a):ALL(b):[a e s & b e s => a*b e s]
& ALL(a):ALL(b):ALL(c):[a e s & b e s & c e s => a*b*c=a*(b*c)]
& ALL(a):ALL(b):[a e s & b e n => pow(a,b) e s]
& ALL(a):[a e s => pow(a,1)=a]
& ALL(a):ALL(b):[a e s & b e n => pow(a,b+1)=pow(a,b)*a]
=> ALL(a):ALL(b):ALL(c):[a e s & b e n & c e n => pow(a,b)*pow(a,c)=pow(a,b+c)]]
Suppose...
6 Set(s)
& ALL(a):ALL(b):[a e s & b e s => a*b e s]
& ALL(a):ALL(b):ALL(c):[a e s & b e s & c e s => a*b*c=a*(b*c)]
& ALL(a):ALL(b):[a e s & b e n => pow(a,b) e s]
& ALL(a):[a e s => pow(a,1)=a]
& ALL(a):ALL(b):[a e s & b e n => pow(a,b+1)=pow(a,b)*a]
Premise
(Not used)
7 Set(s)
Split, 6
(Not used)
8 ALL(a):ALL(b):[a e s & b e s => a*b e s]
Split, 6
9 ALL(a):ALL(b):ALL(c):[a e s & b e s & c e s => a*b*c=a*(b*c)]
Split, 6
10 ALL(a):ALL(b):[a e s & b e n => pow(a,b) e s]
Split, 6
11 ALL(a):[a e s => pow(a,1)=a]
Split, 6
12 ALL(a):ALL(b):[a e s & b e n => pow(a,b+1)=pow(a,b)*a]
Split, 6
Prove: ALL(a):ALL(b):[a e s & b e n
=> ALL(c):[c e n => pow(a,b+c)=pow(a,b)*pow(a,c)]]
Suppose...
13 x e s & y e n
Premise
14 x e s
Split, 13
15 y e n
Split, 13
Prove: (By induction) ALL(c):[c e n => pow(x,y+c)=pow(x,y)*pow(x,c)]
First, contruct subset p of n. Apply Subset Axiom.
16 EXIST(sub):[Set(sub) & ALL(c):[c e sub <=> c e n & pow(x,y+c)=pow(x,y)*pow(x,c)]]
Subset, 1
17 Set(p) & ALL(c):[c e p <=> c e n & pow(x,y+c)=pow(x,y)*pow(x,c)]
E Spec, 16
Define: p
18 Set(p)
Split, 17
19 ALL(c):[c e p <=> c e n & pow(x,y+c)=pow(x,y)*pow(x,c)]
Split, 17
Apply Induction Principle
20 Set(p) & ALL(b):[b e p => b e n] => [1 e p & ALL(b):[b e p => b+1 e p] => ALL(b):[b e n => b e p]]
U Spec, 5
Prove: p is a subset of n
Suppose...
21 z e p
Premise
Apply definition of p
22 z e p <=> z e n & pow(x,y+z)=pow(x,y)*pow(x,z)
U Spec, 19
23 [z e p => z e n & pow(x,y+z)=pow(x,y)*pow(x,z)]
& [z e n & pow(x,y+z)=pow(x,y)*pow(x,z) => z e p]
Iff-And, 22
24 z e p => z e n & pow(x,y+z)=pow(x,y)*pow(x,z)
Split, 23
25 z e n & pow(x,y+z)=pow(x,y)*pow(x,z) => z e p
Split, 23
26 z e n & pow(x,y+z)=pow(x,y)*pow(x,z)
Detach, 24, 21
27 z e n
Split, 26
As Required:
28 ALL(b):[b e p => b e n]
4 Conclusion, 21
29 Set(p) & ALL(b):[b e p => b e n]
Join, 18, 28
Sufficient: ALL(b):[b e n => b e p]
30 1 e p & ALL(b):[b e p => b+1 e p] => ALL(b):[b e n => b e p]
Detach, 20, 29
Base Case
*********
Prove: 1 e p
Apply definition of p
31 1 e p <=> 1 e n & pow(x,y+1)=pow(x,y)*pow(x,1)
U Spec, 19
32 [1 e p => 1 e n & pow(x,y+1)=pow(x,y)*pow(x,1)]
& [1 e n & pow(x,y+1)=pow(x,y)*pow(x,1) => 1 e p]
Iff-And, 31
33 1 e p => 1 e n & pow(x,y+1)=pow(x,y)*pow(x,1)
Split, 32
Sufficient: For 1 e p
34 1 e n & pow(x,y+1)=pow(x,y)*pow(x,1) => 1 e p
Split, 32
Apply property of pow function
35 ALL(b):[x e s & b e n => pow(x,b+1)=pow(x,b)*x]
U Spec, 12
36 x e s & y e n => pow(x,y+1)=pow(x,y)*x
U Spec, 35
37 pow(x,y+1)=pow(x,y)*x
Detach, 36, 13
Apply property of pow function
38 x e s => pow(x,1)=x
U Spec, 11
39 pow(x,1)=x
Detach, 38, 14
40 pow(x,y+1)=pow(x,y)*pow(x,1)
Substitute, 39, 37
41 1 e n & pow(x,y+1)=pow(x,y)*pow(x,1)
Join, 2, 40
As Required:
42 1 e p
Detach, 34, 41
Inductive Case
**************
Prove: ALL(b):[b e p => b+1 e p]
Suppose...
43 z e p
Premise
Apply definition of p
44 z e p <=> z e n & pow(x,y+z)=pow(x,y)*pow(x,z)
U Spec, 19
45 [z e p => z e n & pow(x,y+z)=pow(x,y)*pow(x,z)]
& [z e n & pow(x,y+z)=pow(x,y)*pow(x,z) => z e p]
Iff-And, 44
46 z e p => z e n & pow(x,y+z)=pow(x,y)*pow(x,z)
Split, 45
47 z e n & pow(x,y+z)=pow(x,y)*pow(x,z) => z e p
Split, 45
48 z e n & pow(x,y+z)=pow(x,y)*pow(x,z)
Detach, 46, 43
49 z e n
Split, 48
50 pow(x,y+z)=pow(x,y)*pow(x,z)
Split, 48
Apply definition of p
51 z+1 e p <=> z+1 e n & pow(x,y+(z+1))=pow(x,y)*pow(x,z+1)
U Spec, 19
52 [z+1 e p => z+1 e n & pow(x,y+(z+1))=pow(x,y)*pow(x,z+1)]
& [z+1 e n & pow(x,y+(z+1))=pow(x,y)*pow(x,z+1) => z+1 e p]
Iff-And, 51
53 z+1 e p => z+1 e n & pow(x,y+(z+1))=pow(x,y)*pow(x,z+1)
Split, 52
Sufficient: For z+1 e p
54 z+1 e n & pow(x,y+(z+1))=pow(x,y)*pow(x,z+1) => z+1 e p
Split, 52
55 ALL(b):[z e n & b e n => z+b e n]
U Spec, 3
56 z e n & 1 e n => z+1 e n
U Spec, 55
57 z e n & 1 e n
Join, 49, 2
58 z+1 e n
Detach, 56, 57
59 pow(x,y+(z+1))=pow(x,y+(z+1))
Reflex
Apply associativity of + on n
60 ALL(b):ALL(c):[y e n & b e n & c e n => y+b+c=y+(b+c)]
U Spec, 4
61 ALL(c):[y e n & z e n & c e n => y+z+c=y+(z+c)]
U Spec, 60
62 y e n & z e n & 1 e n => y+z+1=y+(z+1)
U Spec, 61
63 y e n & z e n
Join, 15, 49
64 y e n & z e n & 1 e n
Join, 63, 2
65 y+z+1=y+(z+1)
Detach, 62, 64
66 pow(x,y+(z+1))=pow(x,y+z+1)
Substitute, 65, 59
Apply property of pow function
67 ALL(b):[x e s & b e n => pow(x,b+1)=pow(x,b)*x]
U Spec, 12
68 x e s & y+z e n => pow(x,y+z+1)=pow(x,y+z)*x
U Spec, 67
69 ALL(b):[y e n & b e n => y+b e n]
U Spec, 3
70 y e n & z e n => y+z e n
U Spec, 69
71 y e n & z e n
Join, 15, 49
72 y+z e n
Detach, 70, 71
73 x e s & y+z e n
Join, 14, 72
74 pow(x,y+z+1)=pow(x,y+z)*x
Detach, 68, 73
75 pow(x,y+(z+1))=pow(x,y+z)*x
Substitute, 74, 66
76 pow(x,y+(z+1))=pow(x,y)*pow(x,z)*x
Substitute, 50, 75
Apply associativity of * on s
77 ALL(b):ALL(c):[pow(x,y) e s & b e s & c e s => pow(x,y)*b*c=pow(x,y)*(b*c)]
U Spec, 9
78 ALL(c):[pow(x,y) e s & pow(x,z) e s & c e s => pow(x,y)*pow(x,z)*c=pow(x,y)*(pow(x,z)*c)]
U Spec, 77
79 pow(x,y) e s & pow(x,z) e s & x e s => pow(x,y)*pow(x,z)*x=pow(x,y)*(pow(x,z)*x)
U Spec, 78
Apply property of pow function
80 ALL(b):[x e s & b e n => pow(x,b) e s]
U Spec, 10
81 x e s & y e n => pow(x,y) e s
U Spec, 80
82 x e s & y e n
Join, 14, 15
83 pow(x,y) e s
Detach, 81, 82
84 x e s & z e n => pow(x,z) e s
U Spec, 80
85 x e s & z e n
Join, 14, 49
86 pow(x,z) e s
Detach, 84, 85
87 pow(x,y) e s & pow(x,z) e s
Join, 83, 86
88 pow(x,y) e s & pow(x,z) e s & x e s
Join, 87, 14
89 pow(x,y)*pow(x,z)*x=pow(x,y)*(pow(x,z)*x)
Detach, 79, 88
90 pow(x,y+(z+1))=pow(x,y)*(pow(x,z)*x)
Substitute, 89, 76
Apply property of pow function
91 ALL(b):[x e s & b e n => pow(x,b+1)=pow(x,b)*x]
U Spec, 12
92 x e s & z e n => pow(x,z+1)=pow(x,z)*x
U Spec, 91
93 x e s & z e n
Join, 14, 49
94 pow(x,z+1)=pow(x,z)*x
Detach, 92, 93
95 pow(x,y+(z+1))=pow(x,y)*pow(x,z+1)
Substitute, 94, 90
96 z+1 e n & pow(x,y+(z+1))=pow(x,y)*pow(x,z+1)
Join, 58, 95
97 z+1 e p
Detach, 54, 96
98 ALL(b):[b e p => b+1 e p]
4 Conclusion, 43
99 1 e p & ALL(b):[b e p => b+1 e p]
Join, 42, 98
100 ALL(b):[b e n => b e p]
Detach, 30, 99
Prove: ALL(c):[c e n => pow(x,y+c)=pow(x,y)*pow(x,c)]
Suppose...
101 z e n
Premise
102 z e n => z e p
U Spec, 100
103 z e p
Detach, 102, 101
Apply definition of p
104 z e p <=> z e n & pow(x,y+z)=pow(x,y)*pow(x,z)
U Spec, 19
105 [z e p => z e n & pow(x,y+z)=pow(x,y)*pow(x,z)]
& [z e n & pow(x,y+z)=pow(x,y)*pow(x,z) => z e p]
Iff-And, 104
106 z e p => z e n & pow(x,y+z)=pow(x,y)*pow(x,z)
Split, 105
107 z e n & pow(x,y+z)=pow(x,y)*pow(x,z) => z e p
Split, 105
108 z e n & pow(x,y+z)=pow(x,y)*pow(x,z)
Detach, 106, 103
109 z e n
Split, 108
110 pow(x,y+z)=pow(x,y)*pow(x,z)
Split, 108
As Required:
111 ALL(c):[c e n => pow(x,y+c)=pow(x,y)*pow(x,c)]
4 Conclusion, 101
As Required:
112 ALL(a):ALL(b):[a e s & b e n
=> ALL(c):[c e n => pow(a,b+c)=pow(a,b)*pow(a,c)]]
4 Conclusion, 13
Prove: ALL(a):ALL(b):ALL(c):[a e s & b e n & c e n => pow(a,b)*pow(a,c)=pow(a,b+c)]
Suppose...
113 x e s & y e n & z e n
Premise
114 x e s
Split, 113
115 y e n
Split, 113
116 z e n
Split, 113
Apply previous result
117 ALL(b):[x e s & b e n
=> ALL(c):[c e n => pow(x,b+c)=pow(x,b)*pow(x,c)]]
U Spec, 112
118 x e s & y e n
=> ALL(c):[c e n => pow(x,y+c)=pow(x,y)*pow(x,c)]
U Spec, 117
119 x e s & y e n
Join, 114, 115
120 ALL(c):[c e n => pow(x,y+c)=pow(x,y)*pow(x,c)]
Detach, 118, 119
121 z e n => pow(x,y+z)=pow(x,y)*pow(x,z)
U Spec, 120
122 pow(x,y+z)=pow(x,y)*pow(x,z)
Detach, 121, 116
123 pow(x,y)*pow(x,z)=pow(x,y+z)
Sym, 122
As Required:
124 ALL(a):ALL(b):ALL(c):[a e s & b e n & c e n => pow(a,b)*pow(a,c)=pow(a,b+c)]
4 Conclusion, 113
As Required:
125 ALL(s):ALL(pow):[Set(s)
& ALL(a):ALL(b):[a e s & b e s => a*b e s]
& ALL(a):ALL(b):ALL(c):[a e s & b e s & c e s => a*b*c=a*(b*c)]
& ALL(a):ALL(b):[a e s & b e n => pow(a,b) e s]
& ALL(a):[a e s => pow(a,1)=a]
& ALL(a):ALL(b):[a e s & b e n => pow(a,b+1)=pow(a,b)*a]
=> ALL(a):ALL(b):ALL(c):[a e s & b e n & c e n => pow(a,b)*pow(a,c)=pow(a,b+c)]]
4 Conclusion, 6