THEOREM
*******
There exists infinitely many
exponent-like functions starting at exponent 2.
This machine-verified, formal
proof was written with the aid of the author's DC Proof 2.0 freeware available
at http://www.dcproof.com
Dan Christensen
2019-10-16
PREVIOUS RESULTS
****************
There exists infinitely many
exponent-like functions starting at exponent zero. Proof
1 ALL(x0):[x0 e n
=>
EXIST(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]]]
Axiom
Starting at exponent zero is
equivalent to starting at exponent two. Proof
2 ALL(exp):[ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
=>
[ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]
=>
[ALL(a):[a e n => [~a=0 => exp(a,0)=1]]
<=>
ALL(a):[a e n => exp(a,2)=a*a]]]]
Axiom
PROOF
*****
Suppose...
3 x0 e n
Premise
Apply previous result
4 x0 e n
=>
EXIST(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]]
U Spec, 1
5 EXIST(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]]
Detach, 4, 3
6 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]
E Spec, 5
Define: exp
7 ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
Split, 6
8 exp(0,0)=x0
Split, 6
9 ALL(a):[a e n => [~a=0 => exp(a,0)=1]]
Split, 6
10 ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]
Split, 6
Apply previous result
11 ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
=>
[ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]
=>
[ALL(a):[a e n => [~a=0 => exp(a,0)=1]]
<=>
ALL(a):[a e n => exp(a,2)=a*a]]]
U Spec, 2
12 ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]
=>
[ALL(a):[a e n => [~a=0 => exp(a,0)=1]]
<=>
ALL(a):[a e n => exp(a,2)=a*a]]
Detach, 11, 7
13 ALL(a):[a e n => [~a=0 => exp(a,0)=1]]
<=>
ALL(a):[a e n => exp(a,2)=a*a]
Detach, 12, 10
14 [ALL(a):[a e n => [~a=0 => exp(a,0)=1]] => ALL(a):[a e n => exp(a,2)=a*a]]
&
[ALL(a):[a e n => exp(a,2)=a*a] => ALL(a):[a e n => [~a=0 => exp(a,0)=1]]]
Iff-And, 13
15 ALL(a):[a e n => [~a=0 => exp(a,0)=1]] => ALL(a):[a e n => exp(a,2)=a*a]
Split, 14
16 ALL(a):[a e n => exp(a,2)=a*a] => ALL(a):[a e n => [~a=0 => exp(a,0)=1]]
Split, 14
17 ALL(a):[a e n => exp(a,2)=a*a]
Detach, 15, 9
Joining results...
18 ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
&
exp(0,0)=x0
Join, 7, 8
19 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, 18, 17
20 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, 19, 10
As Required:
21 ALL(x0):[x0 e n
=>
EXIST(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]]]
4 Conclusion, 3