LEMMA 2
*******
Equivalent definitions of
exponentiation (different "boundary conditions" indicated below)
ALL(x0):[x0 e n
=> ALL(exp):[ALL(a):ALL(b):[a e n & b e n => exp(a,b)
e n]
& exp(0,0)=x0
& ALL(a):[a e n => [~a=0 => exp(a,0)=1]] <----
& ALL(a):ALL(b):[a
e n & b e n => exp(a,b+1)=exp(a,b)*a]
<=> ALL(a):ALL(b):[a
e n & b e n => exp(a,b) e n]
& exp(0,0)=x0
& ALL(a):[a e n => exp(a,2)=a*a] <----
& ALL(a):ALL(b):[a
e n & b e n => exp(a,b+1)=exp(a,b)*a]]]
This machine-verified formal
proof was written with the aid of author's freeware DC Proof 2.0 available at http://www.dcproof.com
AXIOMS USED
***********
1 0 e n
Axiom
2 1 e n
Axiom
3 2 e n
Axiom
4 2=1+1
Axiom
5 ALL(a):[a e n => 0+a=a]
Axiom
6 ALL(a):[a e n => a*0=0]
Axiom
7 ALL(a):[a e n => 1*a=a]
Axiom
8 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => [~b=0 => [a*b=c*b
=> a=c]]]
Axiom
PROOF
*****
'=>'
Prove: ALL(exp):[ALL(a):ALL(b):[a
e n & b e n => exp(a,b) e n]
& exp(0,0)=x0
& ALL(a):[a e n => [~a=0 => exp(a,0)=1]]
& ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]
=> ALL(a):ALL(b):[a e n & b e n => exp(a,b)
e n]
& exp(0,0)=x0
& ALL(a):[a e n => exp(a,2)=a*a]
& ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]]
Suppose...
9 x0 e n
Premise
'=>'
10 ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
&
exp(0,0)=x0
&
ALL(a):[a e n => [~a=0 => exp(a,0)=1]]
&
ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]
Premise
11 ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
Split, 10
12 exp(0,0)=x0
Split, 10
13 ALL(a):[a e n => [~a=0 => exp(a,0)=1]]
Split, 10
14 ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]
Split, 10
Suppose...
15 x e n
Premise
16 ALL(b):[x e n & b e n => exp(x,b+1)=exp(x,b)*x]
U Spec, 14
17 x e n & 0 e n => exp(x,0+1)=exp(x,0)*x
U Spec, 16
18 x e n & 0 e n
Join, 15, 1
19 exp(x,0+1)=exp(x,0)*x
Detach, 17, 18
20 1 e n => 0+1=1
U Spec, 5
21 0+1=1
Detach, 20, 2
22 exp(x,1)=exp(x,0)*x
Substitute, 21,
19
Two cases:
23 x=0 | ~x=0
Or Not
Case 1
24 x=0
Premise
25 exp(x,0)=x0
Substitute, 24,
12
26 exp(x,1)=x0*x
Substitute, 25,
22
27 exp(0,1)=x0*0
Substitute, 24,
26
28 x0 e n => x0*0=0
U Spec, 6
29 x0*0=0
Detach, 28, 9
30 x0*x=0
Substitute, 24,
29
31 exp(x,1)=0
Substitute, 30,
26
32 ALL(b):[x e n & b e n => exp(x,b+1)=exp(x,b)*x]
U Spec, 14
33 x e n & 1 e n => exp(x,1+1)=exp(x,1)*x
U Spec, 32
34 x e n & 1 e n => exp(x,2)=exp(x,1)*x
Substitute, 4, 33
35 x e n & 1 e n
Join, 15, 2
36 exp(x,2)=exp(x,1)*x
Detach, 34, 35
37 exp(x,2)=exp(x,1)*0
Substitute, 24,
36
38 exp(x,2)=0*0
Substitute, 31,
37
39 exp(x,2)=x*x
Substitute, 24,
38
Case 1
As Required:
40 x=0 => exp(x,2)=x*x
4 Conclusion, 24
Case 2
41 ~x=0
Premise
42 x e n => [~x=0 => exp(x,0)=1]
U Spec, 13
43 ~x=0 => exp(x,0)=1
Detach, 42, 15
44 exp(x,0)=1
Detach, 43, 41
45 ALL(b):[x e n & b e n => exp(x,b+1)=exp(x,b)*x]
U Spec, 14
46 x e n & 0 e n => exp(x,0+1)=exp(x,0)*x
U Spec, 45
47 x e n & 0 e n
Join, 15, 1
48 exp(x,0+1)=exp(x,0)*x
Detach, 46, 47
49 1 e n => 0+1=1
U Spec, 5
50 0+1=1
Detach, 49, 2
51 exp(x,1)=exp(x,0)*x
Substitute, 50,
48
52 exp(x,1)=1*x
Substitute, 44,
51
53 x e n => 1*x=x
U Spec, 7
54 1*x=x
Detach, 53, 15
55 exp(x,1)=x
Substitute, 54,
52
56 ALL(b):[x e n & b e n => exp(x,b+1)=exp(x,b)*x]
U Spec, 14
57 x e n & 1 e n => exp(x,1+1)=exp(x,1)*x
U Spec, 56
58 x e n & 1 e n
Join, 15, 2
59 exp(x,1+1)=exp(x,1)*x
Detach, 57, 58
60 exp(x,2)=exp(x,1)*x
Substitute, 4, 59
61 exp(x,2)=x*x
Substitute, 55,
60
As Required:
62 ~x=0 => exp(x,2)=x*x
4 Conclusion, 41
63 [x=0 => exp(x,2)=x*x] & [~x=0 => exp(x,2)=x*x]
Join, 40, 62
64 exp(x,2)=x*x
Cases, 23, 63
65 ALL(a):[a e n => exp(a,2)=a*a]
4 Conclusion, 15
66 ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
&
exp(0,0)=x0
Join, 11, 12
67 ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
&
exp(0,0)=x0
&
ALL(a):[a e n => exp(a,2)=a*a]
Join, 66, 65
68 ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
&
exp(0,0)=x0
&
ALL(a):[a e n => exp(a,2)=a*a]
&
ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]
Join, 67, 14
69 ALL(exp):[ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
&
exp(0,0)=x0
&
ALL(a):[a e n => [~a=0 => exp(a,0)=1]]
&
ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]
=>
ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
&
exp(0,0)=x0
&
ALL(a):[a e n => exp(a,2)=a*a]
&
ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]]
4 Conclusion, 10
'<='
Prove: ALL(exp):[ALL(a):ALL(b):[a
e n & b e n => exp(a,b) e n]
& exp(0,0)=x0
& ALL(a):[a e n => exp(a,2)=a*a]
& ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]
=> ALL(a):ALL(b):[a e n & b e n => exp(a,b)
e n]
& exp(0,0)=x0
& ALL(a):[a e n => [~a=0 => exp(a,0)=1]]
& ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]]
Suppose...
70 ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
&
exp(0,0)=x0
&
ALL(a):[a e n => exp(a,2)=a*a]
&
ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]
Premise
71 ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
Split, 70
72 exp(0,0)=x0
Split, 70
73 ALL(a):[a e n => exp(a,2)=a*a]
Split, 70
74 ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]
Split, 70
Prove: ALL(a):[a e n => [~a=0 => exp(a,0)=1]]
Suppose...
75 x e n
Premise
Case 2:
Prove: ~x=0 => exp(x,0)=1
Suppose...
76 ~x=0
Premise
77 ALL(b):[x e n & b e n => exp(x,b+1)=exp(x,b)*x]
U Spec, 74
78 x e n & 1 e n => exp(x,1+1)=exp(x,1)*x
U Spec, 77
79 x e n & 1 e n
Join, 75, 2
80 exp(x,1+1)=exp(x,1)*x
Detach, 78, 79
81 exp(x,2)=exp(x,1)*x
Substitute, 4, 80
82 x e n => exp(x,2)=x*x
U Spec, 73
83 exp(x,2)=x*x
Detach, 82, 75
84 x*x=exp(x,1)*x
Substitute, 83,
81
85 ALL(b):ALL(c):[x e n & b e n & c e n => [~b=0 => [x*b=c*b => x=c]]]
U Spec, 8
86 ALL(c):[x e n & x e n & c e n => [~x=0 => [x*x=c*x => x=c]]]
U Spec, 85
87 x e n & x e n & exp(x,1) e n => [~x=0 => [x*x=exp(x,1)*x => x=exp(x,1)]]
U Spec, 86
88 ALL(b):[x e n & b e n => exp(x,b) e n]
U Spec, 71
89 x e n & 1 e n => exp(x,1) e n
U Spec, 88
90 x e n & 1 e n
Join, 75, 2
91 exp(x,1) e n
Detach, 89, 90
92 x e n & x e n
Join, 75, 75
93 x e n & x e n & exp(x,1) e n
Join, 92, 91
94 ~x=0 => [x*x=exp(x,1)*x => x=exp(x,1)]
Detach, 87, 93
95 x*x=exp(x,1)*x => x=exp(x,1)
Detach, 94, 76
96 x=exp(x,1)
Detach, 95, 84
97 exp(x,1)=x
Sym, 96
98 ALL(b):[x e n & b e n => exp(x,b+1)=exp(x,b)*x]
U Spec, 74
99 x e n & 0 e n => exp(x,0+1)=exp(x,0)*x
U Spec, 98
100 x e n & 0 e n
Join, 75, 1
101 exp(x,0+1)=exp(x,0)*x
Detach, 99, 100
102 1 e n => 0+1=1
U Spec, 5
103 0+1=1
Detach, 102, 2
104 exp(x,1)=exp(x,0)*x
Substitute, 103,
101
105 x=exp(x,0)*x
Substitute, 97,
104
106 x e n => 1*x=x
U Spec, 7
107 1*x=x
Detach, 106, 75
108 1*x=exp(x,0)*x
Substitute, 107,
105
109 ALL(b):ALL(c):[1 e n & b e n & c e n => [~b=0 => [1*b=c*b => 1=c]]]
U Spec, 8
110 ALL(c):[1 e n & x e n & c e n => [~x=0 => [1*x=c*x => 1=c]]]
U Spec, 109
111 1 e n & x e n & exp(x,0) e n => [~x=0 => [1*x=exp(x,0)*x => 1=exp(x,0)]]
U Spec, 110
112 ALL(b):[x e n & b e n => exp(x,b) e n]
U Spec, 71
113 x e n & 0 e n => exp(x,0) e n
U Spec, 112
114 x e n & 0 e n
Join, 75, 1
115 exp(x,0) e n
Detach, 113, 114
116 1 e n & x e n
Join, 2, 75
117 1 e n & x e n & exp(x,0) e n
Join, 116, 115
118 ~x=0 => [1*x=exp(x,0)*x => 1=exp(x,0)]
Detach, 111, 117
119 1*x=exp(x,0)*x => 1=exp(x,0)
Detach, 118, 76
120 1=exp(x,0)
Detach, 119, 108
121 exp(x,0)=1
Sym, 120
Case 2
As Required:
122 ~x=0 => exp(x,0)=1
4 Conclusion, 76
As Required:
123 ALL(a):[a e n => [~a=0 => exp(a,0)=1]]
4 Conclusion, 75
124 ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
&
exp(0,0)=x0
Join, 71, 72
125 ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
&
exp(0,0)=x0
&
ALL(a):[a e n => [~a=0 => exp(a,0)=1]]
Join, 124, 123
126 ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
&
exp(0,0)=x0
&
ALL(a):[a e n => [~a=0 => exp(a,0)=1]]
&
ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]
Join, 125, 74
As Required:
127 ALL(exp):[ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
&
exp(0,0)=x0
&
ALL(a):[a e n => exp(a,2)=a*a]
&
ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]
=>
ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
&
exp(0,0)=x0
&
ALL(a):[a e n => [~a=0 => exp(a,0)=1]]
&
ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]]
4 Conclusion, 70
128 ALL(exp):[[ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
&
exp(0,0)=x0
&
ALL(a):[a e n => [~a=0 => exp(a,0)=1]]
&
ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]
=>
ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
&
exp(0,0)=x0
&
ALL(a):[a e n => exp(a,2)=a*a]
&
ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]] &
[ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
&
exp(0,0)=x0
&
ALL(a):[a e n => exp(a,2)=a*a]
&
ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]
=>
ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
&
exp(0,0)=x0
&
ALL(a):[a e n => [~a=0 => exp(a,0)=1]]
&
ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]]]
Join, 69, 127
129 ALL(exp):[ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
&
exp(0,0)=x0
&
ALL(a):[a e n => [~a=0 => exp(a,0)=1]]
&
ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]
<=>
ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
&
exp(0,0)=x0
&
ALL(a):[a e n => exp(a,2)=a*a]
&
ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]]
Iff-And, 128
As Required:
130 ALL(x0):[x0 e n
=>
ALL(exp):[ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
&
exp(0,0)=x0
&
ALL(a):[a e n => [~a=0 => exp(a,0)=1]]
&
ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]
<=>
ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
&
exp(0,0)=x0
&
ALL(a):[a e n => exp(a,2)=a*a]
&
ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]]]
4 Conclusion, 9