THEOREM
*******
There exists a unique exponent
function on n with 0^0 left undefined.
Existence of exp(a,b):
EXIST(exp):[ALL(a):ALL(b):[a
e n & b e n =>
[~[a=0 & b=0] => exp(a,b) e n]]
& exp(0,1)=0
& ALL(a):[a e n => [~a=0 => exp(a,0)=1]]
& ALL(a):ALL(b):[a
e n & b e n =>
[~[a=0 & b=0] => exp(a,b+1)=exp(a,b)*a]]]
Uniqueness of exp(a,b):
ALL(exp):ALL(exp'):[ALL(a):ALL(b):[a
e n & b e n =>
[~[a=0 & b=0] => exp(a,b) e n]]
& exp(0,1)=0
& ALL(a):[a e n => [~a=0 => exp(a,0)=1]]
& ALL(a):ALL(b):[a
e n & b e n
=> [~[a=0 &
b=0] => exp(a,b+1)=exp(a,b)*a]]
& [ALL(a):ALL(b):[a
e n & b e n =>
[~[a=0 & b=0] => exp'(a,b) e n]]
& exp'(0,1)=0
& ALL(a):[a e n => [~a=0 => exp'(a,0)=1]]
& ALL(a):ALL(b):[a
e n & b e n
=> [~[a=0 &
b=0] => exp'(a,b+1)=exp'(a,b)*a]]]
=> ALL(a):ALL(b):[a
e n & b e n =>
[~[a=0 & b=0] => exp(a,b)=exp'(a,b)]]]
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-17
AXIOMS/DEFINITIONS
******************
Define: n, 0, 1
***************
1 Set(n)
Axiom
2 0 e n
Axiom
3 1 e n
Axiom
4 ~1=0
Axiom
5 0+1=1
Axiom
Properties of +
***************
Closed on n
6 ALL(a):ALL(b):[a e n & b e n => a+b e n]
Axiom
Adding 0
7 ALL(a):[a e n => a+0=a]
Axiom
+ Commutative
8 ALL(a):ALL(b):[a e n & b e n => a+b=b+a]
Axiom
+ Right cancelable
9 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => [a+b=c+b
=> a=c]]
Axiom
0 is "first" number
10 ALL(a):[a e n => ~a+1=0]
Axiom
Principle of Mathematical
Induction
11 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
Properties of *
***************
Closed on n
12 ALL(a):ALL(b):[a e n & b e n => a*b e n]
Axiom
Multiplying by 0
13 ALL(a):[a e n => a*0=0]
Axiom
Multiplying by 1
14 ALL(a):[a e n => a*1=a]
Axiom
* Commutative
15 ALL(a):ALL(b):[a e n & b e n => a*b=b*a]
Axiom
Function Axiom (2 varibles)
**************
16 ALL(f):ALL(dom):ALL(cod):[Set''(f) & Set'(dom) & Set(cod)
=>
[ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e f => (a1,a2) e dom & b e cod]
&
ALL(a1):ALL(a2):[(a1,a2) e dom =>
EXIST(b):[b e cod & (a1,a2,b) e f]]
&
ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e dom & b1 e cod & b2 e cod
=>
[(a1,a2,b1) e f &
(a1,a2,b2) e f => b1=b2]]
=>
ALL(a1):ALL(a2):ALL(b):[(a1,a2) e dom & b e cod => [f(a1,a2)=b <=>
(a1,a2,b) e f]]]]
Function
PREVIOUS RESULT
***************
There exists infinitely many
exponent-like functions starting with exponent 0 Proof
17 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
PROOF
*****
Suppose...
18 x0 e n
Premise
Apply previous result
19 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, 17
20 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, 19, 18
21 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, 20
Define: exp
***********
22 ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]
Split, 21
23 exp(0,0)=x0
Split, 21
24 ALL(a):[a e n => [~a=0 => exp(a,0)=1]]
Split, 21
25 ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]
Split, 21
Construct n2
26 ALL(a1):ALL(a2):[Set(a1) & Set(a2)
=> EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e a1 & c2 e a2]]]
Cart Prod
27 ALL(a2):[Set(n) & Set(a2)
=> EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e n & c2 e a2]]]
U Spec, 26
28 Set(n) & Set(n) => EXIST(b):[Set'(b) &
ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e n & c2 e n]]
U Spec, 27
29 Set(n) & Set(n)
Join, 1, 1
30 EXIST(b):[Set'(b) &
ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e n & c2 e n]]
Detach, 28, 29
31 Set'(n2) & ALL(c1):ALL(c2):[(c1,c2) e n2 <=> c1 e n & c2 e n]
E Spec, 30
Define: n2
32 Set'(n2)
Split, 31
33 ALL(c1):ALL(c2):[(c1,c2) e n2 <=> c1 e n & c2 e n]
Split, 31
Construct n3
34 ALL(a1):ALL(a2):ALL(a3):[Set(a1) &
Set(a2) & Set(a3) => EXIST(b):[Set''(b) &
ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e b <=> c1 e a1 & c2 e a2 & c3 e a3]]]
Cart Prod
35 ALL(a2):ALL(a3):[Set(n) & Set(a2)
& Set(a3) => EXIST(b):[Set''(b) &
ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e b <=> c1 e n & c2 e a2 & c3 e a3]]]
U Spec, 34
36 ALL(a3):[Set(n) & Set(n) & Set(a3)
=> EXIST(b):[Set''(b) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e b <=> c1 e n & c2 e n & c3 e a3]]]
U Spec, 35
37 Set(n) & Set(n) & Set(n) => EXIST(b):[Set''(b) &
ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e b <=> c1 e n & c2 e n & c3 e n]]
U Spec, 36
38 Set(n) & Set(n)
Join, 1, 1
39 Set(n) & Set(n) & Set(n)
Join, 38, 1
40 EXIST(b):[Set''(b) &
ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e b <=> c1 e n & c2 e n & c3 e n]]
Detach, 37, 39
41 Set''(n3) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e n3 <=> c1 e n & c2 e n & c3 e n]
E Spec, 40
Define: n3
42 Set''(n3)
Split, 41
43 ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e n3 <=> c1 e n & c2 e n & c3 e n]
Split, 41
Construct dom
44 EXIST(sub):[Set'(sub) &
ALL(a):ALL(b):[(a,b) e sub <=> (a,b) e n2 & ~[a=0 & b=0]]]
Subset, 32
45 Set'(dom) & ALL(a):ALL(b):[(a,b) e dom <=> (a,b) e n2 & ~[a=0 & b=0]]
E Spec, 44
Define: dom
46 Set'(dom)
Split, 45
47 ALL(a):ALL(b):[(a,b) e dom <=> (a,b) e n2 & ~[a=0 & b=0]]
Split, 45
Construct exp'
48 EXIST(sub):[Set''(sub) &
ALL(a):ALL(b):ALL(c):[(a,b,c) e sub
<=>
(a,b,c) e n3 & [~[a=0 & b=0] & c=exp(a,b)]]]
Subset, 42
49 Set''(exp') & ALL(a):ALL(b):ALL(c):[(a,b,c) e exp'
<=>
(a,b,c) e n3 & [~[a=0 & b=0] & c=exp(a,b)]]
E Spec, 48
Define: exp'
************
50 Set''(exp')
Split, 49
51 ALL(a):ALL(b):ALL(c):[(a,b,c) e exp'
<=>
(a,b,c) e n3 & [~[a=0 & b=0] & c=exp(a,b)]]
Split, 49
Apply Function Axioms (for 2 variables)
52 ALL(f):ALL(dom):ALL(cod):[Set''(f) &
Set'(dom) & Set(cod)
=>
[ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e f => (a1,a2) e dom & b e cod]
&
ALL(a1):ALL(a2):[(a1,a2) e dom =>
EXIST(b):[b e cod & (a1,a2,b) e f]]
&
ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e dom & b1 e cod & b2 e cod
=>
[(a1,a2,b1) e f &
(a1,a2,b2) e f => b1=b2]]
=>
ALL(a1):ALL(a2):ALL(b):[(a1,a2) e dom & b e cod => [f(a1,a2)=b <=>
(a1,a2,b) e f]]]]
Function
53 ALL(dom):ALL(cod):[Set''(exp') &
Set'(dom) & Set(cod)
=>
[ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e exp' => (a1,a2) e dom & b e cod]
&
ALL(a1):ALL(a2):[(a1,a2) e dom =>
EXIST(b):[b e cod & (a1,a2,b) e exp']]
&
ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e dom & b1 e cod & b2 e cod
=>
[(a1,a2,b1) e exp' & (a1,a2,b2) e exp' => b1=b2]]
=>
ALL(a1):ALL(a2):ALL(b):[(a1,a2) e dom & b e cod => [exp'(a1,a2)=b
<=> (a1,a2,b) e exp']]]]
U Spec, 52
54 ALL(cod):[Set''(exp') & Set'(dom) & Set(cod)
=>
[ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e exp' => (a1,a2) e dom & b e cod]
&
ALL(a1):ALL(a2):[(a1,a2) e dom =>
EXIST(b):[b e cod & (a1,a2,b) e exp']]
&
ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e dom & b1 e cod & b2 e cod
=>
[(a1,a2,b1) e exp' &
(a1,a2,b2) e exp' => b1=b2]]
=>
ALL(a1):ALL(a2):ALL(b):[(a1,a2) e dom & b e cod => [exp'(a1,a2)=b
<=> (a1,a2,b) e exp']]]]
U Spec, 53
55 Set''(exp') & Set'(dom) & Set(n)
=>
[ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e exp' => (a1,a2) e dom & b e n]
&
ALL(a1):ALL(a2):[(a1,a2) e dom =>
EXIST(b):[b e n & (a1,a2,b) e exp']]
&
ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e dom & b1 e n & b2 e n
=>
[(a1,a2,b1) e exp' &
(a1,a2,b2) e exp' => b1=b2]]
=>
ALL(a1):ALL(a2):ALL(b):[(a1,a2) e dom & b e n => [exp'(a1,a2)=b
<=> (a1,a2,b) e exp']]]
U Spec, 54
56 Set''(exp') & Set'(dom)
Join, 50, 46
57 Set''(exp') & Set'(dom) & Set(n)
Join, 56, 1
Sufficient: For functionality of exp'
58 ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e exp' => (a1,a2) e dom & b e n]
&
ALL(a1):ALL(a2):[(a1,a2) e dom =>
EXIST(b):[b e n & (a1,a2,b) e exp']]
&
ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e dom & b1 e n & b2 e n
=>
[(a1,a2,b1) e exp' &
(a1,a2,b2) e exp' => b1=b2]]
=>
ALL(a1):ALL(a2):ALL(b):[(a1,a2) e dom & b e n => [exp'(a1,a2)=b
<=> (a1,a2,b) e exp']]
Detach, 55, 57
Prove: ALL(a1):ALL(a2):ALL(b):[(a1,a2,b)
e exp' => (a1,a2) e dom & b e n]
Suppose...
59 (x,y,z) e exp'
Premise
Apply definition of exp'
60 ALL(b):ALL(c):[(x,b,c) e exp'
<=>
(x,b,c) e n3 & [~[x=0 & b=0] & c=exp(x,b)]]
U Spec, 51
61 ALL(c):[(x,y,c) e exp'
<=>
(x,y,c) e n3 & [~[x=0 & y=0] & c=exp(x,y)]]
U Spec, 60
62 (x,y,z) e exp'
<=>
(x,y,z) e n3 & [~[x=0 & y=0] & z=exp(x,y)]
U Spec, 61
63 [(x,y,z) e exp' => (x,y,z) e n3 & [~[x=0 & y=0] & z=exp(x,y)]]
&
[(x,y,z) e n3 & [~[x=0 & y=0] & z=exp(x,y)] => (x,y,z) e exp']
Iff-And, 62
64 (x,y,z) e exp' => (x,y,z) e n3 & [~[x=0 & y=0] & z=exp(x,y)]
Split, 63
65 (x,y,z) e n3 & [~[x=0 & y=0] & z=exp(x,y)] => (x,y,z) e exp'
Split, 63
66 (x,y,z) e n3 & [~[x=0 & y=0] & z=exp(x,y)]
Detach, 64, 59
67 (x,y,z) e n3
Split, 66
68 ~[x=0 & y=0] & z=exp(x,y)
Split, 66
69 ~[x=0 & y=0]
Split, 68
70 z=exp(x,y)
Split, 68
71 ALL(b):[(x,b) e dom <=> (x,b) e n2 & ~[x=0 & b=0]]
U Spec, 47
72 (x,y) e dom <=> (x,y) e n2 & ~[x=0 & y=0]
U Spec, 71
73 [(x,y) e dom => (x,y) e n2 & ~[x=0 & y=0]]
&
[(x,y) e n2 & ~[x=0 & y=0] => (x,y) e dom]
Iff-And, 72
74 (x,y) e dom => (x,y) e n2 & ~[x=0 & y=0]
Split, 73
Apply definition of n3
75 ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]
U Spec, 43
76 ALL(c3):[(x,y,c3) e n3 <=> x e n & y e n & c3 e n]
U Spec, 75
77 (x,y,z) e n3 <=> x e n & y e n & z e n
U Spec, 76
78 [(x,y,z) e n3 => x e n & y e n & z e n]
&
[x e n & y e n & z e n => (x,y,z) e n3]
Iff-And, 77
79 (x,y,z) e n3 => x e n & y e n & z e n
Split, 78
80 x e n & y e n & z e n => (x,y,z) e n3
Split, 78
81 x e n & y e n & z e n
Detach, 79, 67
82 x e n
Split, 81
83 y e n
Split, 81
84 z e n
Split, 81
Sufficient: For (x,y) e dom
85 (x,y) e n2 & ~[x=0 & y=0] => (x,y) e dom
Split, 73
Apply definition of n3
86 ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]
U Spec, 43
87 ALL(c3):[(x,y,c3) e n3 <=> x e n & y e n & c3 e n]
U Spec, 86
88 (x,y,z) e n3 <=> x e n & y e n & z e n
U Spec, 87
89 [(x,y,z) e n3 => x e n & y e n & z e n]
&
[x e n & y e n & z e n => (x,y,z) e n3]
Iff-And, 88
90 (x,y,z) e n3 => x e n & y e n & z e n
Split, 89
91 x e n & y e n & z e n => (x,y,z) e n3
Split, 89
92 x e n & y e n & z e n
Detach, 90, 67
93 x e n
Split, 92
94 y e n
Split, 92
95 z e n
Split, 92
Apply definition of n2
96 ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]
U Spec, 33
97 (x,y) e n2 <=> x e n & y e n
U Spec, 96
98 [(x,y) e n2 => x e n & y e n]
&
[x e n & y e n => (x,y) e n2]
Iff-And, 97
99 (x,y) e n2 => x e n & y e n
Split, 98
100 x e n & y e n => (x,y) e n2
Split, 98
101 x e n & y e n
Join, 82, 83
102 (x,y) e n2
Detach, 100, 101
103 (x,y) e n2 & ~[x=0 & y=0]
Join, 102, 69
104 (x,y) e dom
Detach, 85, 103
105 (x,y) e dom & z e n
Join, 104, 84
Functionality of exp', Part 1
106 ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e exp' => (a1,a2) e dom & b e n]
4 Conclusion, 59
Prove: ALL(a1):ALL(a2):[(a1,a2) e dom => EXIST(b):[b e n &
(a1,a2,b) e exp']]
Suppose...
107 (x,y) e dom
Premise
Apply definition of dom
108 ALL(b):[(x,b) e dom <=> (x,b) e n2 & ~[x=0 & b=0]]
U Spec, 47
109 (x,y) e dom <=> (x,y) e n2 & ~[x=0 & y=0]
U Spec, 108
110 [(x,y) e dom => (x,y) e n2 & ~[x=0 & y=0]]
&
[(x,y) e n2 & ~[x=0 & y=0] => (x,y) e dom]
Iff-And, 109
111 (x,y) e dom => (x,y) e n2 & ~[x=0 & y=0]
Split, 110
112 (x,y) e n2 & ~[x=0 & y=0] => (x,y) e dom
Split, 110
113 (x,y) e n2 & ~[x=0 & y=0]
Detach, 111, 107
114 (x,y) e n2
Split, 113
115 ~[x=0 & y=0]
Split, 113
Apply definition of exp'
116 ALL(b):ALL(c):[(x,b,c) e exp'
<=>
(x,b,c) e n3 & [~[x=0 & b=0] & c=exp(x,b)]]
U Spec, 51
117 ALL(c):[(x,y,c) e exp'
<=>
(x,y,c) e n3 & [~[x=0 & y=0] & c=exp(x,y)]]
U Spec, 116
118 ALL(b):[x e n & b e n => exp(x,b) e n]
U Spec, 22
119 x e n & y e n => exp(x,y) e n
U Spec, 118
Apply definition of n2
120 ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]
U Spec, 33
121 (x,y) e n2 <=> x e n & y e n
U Spec, 120
122 [(x,y) e n2 => x e n & y e n]
&
[x e n & y e n => (x,y) e n2]
Iff-And, 121
123 (x,y) e n2 => x e n & y e n
Split, 122
124 x e n & y e n => (x,y) e n2
Split, 122
125 x e n & y e n
Detach, 123, 114
126 x e n
Split, 125
127 y e n
Split, 125
128 exp(x,y) e n
Detach, 119, 125
129 (x,y,exp(x,y)) e exp'
<=>
(x,y,exp(x,y)) e n3 & [~[x=0 & y=0] & exp(x,y)=exp(x,y)]
U Spec, 117, 128
130 [(x,y,exp(x,y)) e exp' => (x,y,exp(x,y)) e n3 & [~[x=0 & y=0] & exp(x,y)=exp(x,y)]]
&
[(x,y,exp(x,y)) e n3 & [~[x=0 & y=0] & exp(x,y)=exp(x,y)] => (x,y,exp(x,y)) e exp']
Iff-And, 129
131 (x,y,exp(x,y)) e exp' => (x,y,exp(x,y)) e n3 & [~[x=0 & y=0] & exp(x,y)=exp(x,y)]
Split, 130
Sufficient: For (x,y,exp(x,y)) e exp'
132 (x,y,exp(x,y)) e n3 & [~[x=0 & y=0] & exp(x,y)=exp(x,y)] => (x,y,exp(x,y)) e exp'
Split, 130
Apply definition of n3
133 ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]
U Spec, 43
134 ALL(c3):[(x,y,c3) e n3 <=> x e n & y e n & c3 e n]
U Spec, 133
135 (x,y,exp(x,y)) e n3 <=> x e n & y e n & exp(x,y) e n
U Spec, 134, 128
136 [(x,y,exp(x,y)) e n3 => x e n & y e n & exp(x,y) e n]
&
[x e n & y e n & exp(x,y) e n => (x,y,exp(x,y)) e n3]
Iff-And, 135
137 (x,y,exp(x,y)) e n3 => x e n & y e n & exp(x,y) e n
Split, 136
Sufficient: For (x,y,exp(x,y)) e n3
138 x e n & y e n & exp(x,y) e n => (x,y,exp(x,y)) e n3
Split, 136
139 x e n & y e n & exp(x,y) e n
Join, 125, 128
140 (x,y,exp(x,y)) e n3
Detach, 138, 139
141 exp(x,y)=exp(x,y)
Reflex, 128
142 ~[x=0 & y=0] & exp(x,y)=exp(x,y)
Join, 115, 141
143 (x,y,exp(x,y)) e n3
&
[~[x=0 & y=0] & exp(x,y)=exp(x,y)]
Join, 140, 142
144 (x,y,exp(x,y)) e exp'
Detach, 132, 143
145 exp(x,y) e n & (x,y,exp(x,y)) e exp'
Join, 128, 144
146 EXIST(b):[b e n & (x,y,b) e exp']
E Gen, 145
Functionality of exp', Part 2
147 ALL(a1):ALL(a2):[(a1,a2) e dom => EXIST(b):[b e n & (a1,a2,b) e exp']]
4 Conclusion, 107
Prove: ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2)
e dom & b1 e n & b2 e n
=> [(a1,a2,b1) e exp' &
(a1,a2,b2) e exp' => b1=b2]]
Suppose...
148 (x,y) e dom & z1 e n & z2 e n
Premise
149 (x,y) e dom
Split, 148
150 z1 e n
Split, 148
151 z2 e n
Split, 148
Suppose...
152 (x,y,z1) e exp' & (x,y,z2) e exp'
Premise
153 (x,y,z1) e exp'
Split, 152
154 (x,y,z2) e exp'
Split, 152
Apply the definition of exp'
155 ALL(b):ALL(c):[(x,b,c) e exp'
<=>
(x,b,c) e n3 & [~[x=0 & b=0] & c=exp(x,b)]]
U Spec, 51
156 ALL(c):[(x,y,c) e exp'
<=>
(x,y,c) e n3 & [~[x=0 & y=0] & c=exp(x,y)]]
U Spec, 155
157 (x,y,z1) e exp'
<=>
(x,y,z1) e n3 & [~[x=0 & y=0] & z1=exp(x,y)]
U Spec, 156
158 [(x,y,z1) e exp' => (x,y,z1) e n3 & [~[x=0 & y=0] & z1=exp(x,y)]]
&
[(x,y,z1) e n3 & [~[x=0 & y=0] & z1=exp(x,y)] => (x,y,z1) e exp']
Iff-And, 157
159 (x,y,z1) e exp' => (x,y,z1) e n3 & [~[x=0 & y=0] & z1=exp(x,y)]
Split, 158
160 (x,y,z1) e n3 & [~[x=0 & y=0] & z1=exp(x,y)] => (x,y,z1) e exp'
Split, 158
161 (x,y,z1) e n3 & [~[x=0 & y=0] & z1=exp(x,y)]
Detach, 159, 153
162 (x,y,z1) e n3
Split, 161
163 ~[x=0 & y=0] & z1=exp(x,y)
Split, 161
164 ~[x=0 & y=0]
Split, 163
165 z1=exp(x,y)
Split, 163
166 (x,y,z2) e exp'
<=>
(x,y,z2) e n3 & [~[x=0 & y=0] & z2=exp(x,y)]
U Spec, 156
167 [(x,y,z2) e exp' => (x,y,z2) e n3 & [~[x=0 & y=0] & z2=exp(x,y)]]
&
[(x,y,z2) e n3 & [~[x=0 & y=0] & z2=exp(x,y)] => (x,y,z2) e exp']
Iff-And, 166
168 (x,y,z2) e exp' => (x,y,z2) e n3 & [~[x=0 & y=0] & z2=exp(x,y)]
Split, 167
169 (x,y,z2) e n3 & [~[x=0 & y=0] & z2=exp(x,y)] => (x,y,z2) e exp'
Split, 167
170 (x,y,z2) e n3 & [~[x=0 & y=0] & z2=exp(x,y)]
Detach, 168, 154
171 (x,y,z2) e n3
Split, 170
172 ~[x=0 & y=0] & z2=exp(x,y)
Split, 170
173 ~[x=0 & y=0]
Split, 172
174 z2=exp(x,y)
Split, 172
175 z1=z2
Substitute, 174,
165
176 (x,y,z1) e exp' & (x,y,z2) e exp' => z1=z2
4 Conclusion, 152
Functionality of exp', Part 3
177 ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e dom & b1 e n & b2 e n
=>
[(a1,a2,b1) e exp' &
(a1,a2,b2) e exp' => b1=b2]]
4 Conclusion, 148
Joining results...
178 ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e exp' => (a1,a2) e dom & b e n]
&
ALL(a1):ALL(a2):[(a1,a2) e dom =>
EXIST(b):[b e n & (a1,a2,b) e exp']]
Join, 106, 147
179 ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e exp' => (a1,a2) e dom & b e n]
&
ALL(a1):ALL(a2):[(a1,a2) e dom =>
EXIST(b):[b e n & (a1,a2,b) e exp']]
&
ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e dom & b1 e n & b2 e n
=>
[(a1,a2,b1) e exp' &
(a1,a2,b2) e exp' => b1=b2]]
Join, 178, 177
exp' is a partial binary function on n
As Required:
180 ALL(a1):ALL(a2):ALL(b):[(a1,a2) e dom & b e n => [exp'(a1,a2)=b
<=> (a1,a2,b) e exp']]
Detach, 58, 179
Prove: ALL(x):ALL(y):[x e n & y e n =>
[~[x=0 & y=0] => exp'(x,y) e n]]
Suppose...
181 x e n & y e n
Premise
Prove: ~[x=0 & y=0] => exp'(x,y)
e n
Suppose...
182 ~[x=0 & y=0]
Premise
Apply definition of exp'
183 ALL(a2):[(x,a2) e dom => EXIST(b):[b e n & (x,a2,b) e exp']]
U Spec, 147
184 (x,y) e dom => EXIST(b):[b e n & (x,y,b) e exp']
U Spec, 183
Apply definition of dom
185 ALL(b):[(x,b) e dom <=> (x,b) e n2 & ~[x=0 & b=0]]
U Spec, 47
186 (x,y) e dom <=> (x,y) e n2 & ~[x=0 & y=0]
U Spec, 185
187 [(x,y) e dom => (x,y) e n2 & ~[x=0 & y=0]]
&
[(x,y) e n2 & ~[x=0 & y=0] => (x,y) e dom]
Iff-And, 186
188 (x,y) e dom => (x,y) e n2 & ~[x=0 & y=0]
Split, 187
189 (x,y) e n2 & ~[x=0 & y=0] => (x,y) e dom
Split, 187
Apply definition of n2
190 ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]
U Spec, 33
191 (x,y) e n2 <=> x e n & y e n
U Spec, 190
192 [(x,y) e n2 => x e n & y e n]
&
[x e n & y e n => (x,y) e n2]
Iff-And, 191
193 (x,y) e n2 => x e n & y e n
Split, 192
194 x e n & y e n => (x,y) e n2
Split, 192
195 (x,y) e n2
Detach, 194, 181
196 (x,y) e n2 & ~[x=0 & y=0]
Join, 195, 182
197 (x,y) e dom
Detach, 189, 196
198 EXIST(b):[b e n & (x,y,b) e exp']
Detach, 184, 197
199 z e n & (x,y,z) e exp'
E Spec, 198
200 z e n
Split, 199
201 (x,y,z) e exp'
Split, 199
Apply previous result
202 ALL(a2):ALL(b):[(x,a2) e dom & b e n => [exp'(x,a2)=b <=>
(x,a2,b) e exp']]
U Spec, 180
203 ALL(b):[(x,y) e dom & b e n => [exp'(x,y)=b <=> (x,y,b) e exp']]
U Spec, 202
204 (x,y) e dom & z e n => [exp'(x,y)=z <=> (x,y,z) e exp']
U Spec, 203
205 (x,y) e dom & z e n
Join, 197, 200
206 exp'(x,y)=z <=> (x,y,z) e exp'
Detach, 204, 205
207 [exp'(x,y)=z => (x,y,z) e exp']
&
[(x,y,z) e exp' => exp'(x,y)=z]
Iff-And, 206
208 exp'(x,y)=z => (x,y,z) e exp'
Split, 207
209 (x,y,z) e exp' => exp'(x,y)=z
Split, 207
210 exp'(x,y)=z
Detach, 209, 201
211 exp'(x,y) e n
Substitute, 210,
200
As Required:
212 ~[x=0 & y=0] => exp'(x,y) e n
4 Conclusion, 182
As Required:
213 ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp'(a,b) e n]]
4 Conclusion, 181
Prove: exp'(0,1)=0
Apply definition of exp'
214 ALL(b):ALL(c):[(0,b,c) e exp'
<=>
(0,b,c) e n3 & [~[0=0 & b=0] & c=exp(0,b)]]
U Spec, 51
215 ALL(c):[(0,1,c) e exp'
<=>
(0,1,c) e n3 & [~[0=0 & 1=0] & c=exp(0,1)]]
U Spec, 214
216 (0,1,0) e exp'
<=>
(0,1,0) e n3 & [~[0=0 & 1=0] & 0=exp(0,1)]
U Spec, 215
217 [(0,1,0) e exp' => (0,1,0) e n3 & [~[0=0 & 1=0] & 0=exp(0,1)]]
&
[(0,1,0) e n3 & [~[0=0 & 1=0] & 0=exp(0,1)] => (0,1,0) e exp']
Iff-And, 216
218 (0,1,0) e exp' => (0,1,0) e n3 & [~[0=0 & 1=0] & 0=exp(0,1)]
Split, 217
Sufficient: For (0,1,0) e exp'
219 (0,1,0) e n3 & [~[0=0 & 1=0] & 0=exp(0,1)] => (0,1,0) e exp'
Split, 217
Apply definition of n3
220 ALL(c2):ALL(c3):[(0,c2,c3) e n3 <=> 0 e n & c2 e n & c3 e n]
U Spec, 43
221 ALL(c3):[(0,1,c3) e n3 <=> 0 e n & 1 e n & c3 e n]
U Spec, 220
222 (0,1,0) e n3 <=> 0 e n & 1 e n & 0 e n
U Spec, 221
223 [(0,1,0) e n3 => 0 e n & 1 e n & 0 e n]
&
[0 e n & 1 e n & 0 e n => (0,1,0) e n3]
Iff-And, 222
224 (0,1,0) e n3 => 0 e n & 1 e n & 0 e n
Split, 223
225 0 e n & 1 e n & 0 e n => (0,1,0) e n3
Split, 223
226 0 e n & 1 e n
Join, 2, 3
227 0 e n & 1 e n & 0 e n
Join, 226, 2
228 (0,1,0) e n3
Detach, 225, 227
Prove: ~[0=0 & 1=0]
Suppose to the contrary...
229 0=0 & 1=0
Premise
230 0=0
Split, 229
231 1=0
Split, 229
232 1=0 & ~1=0
Join, 231, 4
233 ~[0=0 & 1=0]
4 Conclusion, 229
Apply definition of exp
234 ALL(b):[0 e n & b e n => exp(0,b+1)=exp(0,b)*0]
U Spec, 25
235 0 e n & 0 e n => exp(0,0+1)=exp(0,0)*0
U Spec, 234
236 0 e n & 0 e n
Join, 2, 2
237 exp(0,0+1)=exp(0,0)*0
Detach, 235, 236
238 ALL(b):[0 e n & b e n => 0+b=b+0]
U Spec, 8
239 0 e n & 1 e n => 0+1=1+0
U Spec, 238
240 0 e n & 1 e n
Join, 2, 3
241 0+1=1+0
Detach, 239, 240
242 1 e n => 1+0=1
U Spec, 7
243 1+0=1
Detach, 242, 3
244 0+1=1
Substitute, 243,
241
245 exp(0,1)=exp(0,0)*0
Substitute, 244,
237
246 ALL(b):[0 e n & b e n => exp(0,b) e n]
U Spec, 22
247 0 e n & 0 e n => exp(0,0) e n
U Spec, 246
248 0 e n & 0 e n
Join, 2, 2
249 exp(0,0) e n
Detach, 247, 248
250 exp(0,0) e n => exp(0,0)*0=0
U Spec, 13, 249
251 exp(0,0)*0=0
Detach, 250, 249
252 exp(0,1)=0
Substitute, 251,
245
253 0=exp(0,1)
Sym, 252
254 ~[0=0 & 1=0] & 0=exp(0,1)
Join, 233, 253
255 (0,1,0) e n3 & [~[0=0 & 1=0] & 0=exp(0,1)]
Join, 228, 254
256 (0,1,0) e exp'
Detach, 219, 255
Apply previous result
257 ALL(a2):ALL(b):[(0,a2) e dom & b e n => [exp'(0,a2)=b <=>
(0,a2,b) e exp']]
U Spec, 180
258 ALL(b):[(0,1) e dom & b e n => [exp'(0,1)=b <=> (0,1,b) e exp']]
U Spec, 257
259 (0,1) e dom & 0 e n => [exp'(0,1)=0 <=> (0,1,0) e exp']
U Spec, 258
Apply defintion of dom
260 ALL(b):[(0,b) e dom <=> (0,b) e n2 & ~[0=0 & b=0]]
U Spec, 47
261 (0,1) e dom <=> (0,1) e n2 & ~[0=0 & 1=0]
U Spec, 260
262 [(0,1) e dom => (0,1) e n2 & ~[0=0 & 1=0]]
&
[(0,1) e n2 & ~[0=0 & 1=0] => (0,1) e dom]
Iff-And, 261
263 (0,1) e dom => (0,1) e n2 & ~[0=0 & 1=0]
Split, 262
264 (0,1) e n2 & ~[0=0 & 1=0] => (0,1) e dom
Split, 262
265 ALL(c2):[(0,c2) e n2 <=> 0 e n & c2 e n]
U Spec, 33
266 (0,1) e n2 <=> 0 e n & 1 e n
U Spec, 265
267 [(0,1) e n2 => 0 e n & 1 e n]
&
[0 e n & 1 e n => (0,1) e n2]
Iff-And, 266
268 (0,1) e n2 => 0 e n & 1 e n
Split, 267
269 0 e n & 1 e n => (0,1) e n2
Split, 267
270 0 e n & 1 e n
Join, 2, 3
271 (0,1) e n2
Detach, 269, 270
272 0=0 & 1=0
Premise
273 0=0
Split, 272
274 1=0
Split, 272
275 1=0 & ~1=0
Join, 274, 4
276 ~[0=0 & 1=0]
4 Conclusion, 272
277 (0,1) e n2 & ~[0=0 & 1=0]
Join, 271, 276
278 (0,1) e dom
Detach, 264, 277
279 (0,1) e dom & 0 e n
Join, 278, 2
280 exp'(0,1)=0 <=> (0,1,0) e exp'
Detach, 259, 279
281 [exp'(0,1)=0 => (0,1,0) e exp']
&
[(0,1,0) e exp' => exp'(0,1)=0]
Iff-And, 280
282 exp'(0,1)=0 => (0,1,0) e exp'
Split, 281
283 (0,1,0) e exp' => exp'(0,1)=0
Split, 281
As Required:
284 exp'(0,1)=0
Detach, 283, 256
Prove: ALL(a):[a e n => [~x=0 => exp'(x,0)=1]]
Suppose...
285 x e n
Premise
Prove: ~x=0 => exp'(x,0)=1
Suppose...
286 ~x=0
Premise
287 ALL(b):ALL(c):[(x,b,c) e exp'
<=>
(x,b,c) e n3 & [~[x=0 & b=0] & c=exp(x,b)]]
U Spec, 51
288 ALL(c):[(x,0,c) e exp'
<=>
(x,0,c) e n3 & [~[x=0 & 0=0] & c=exp(x,0)]]
U Spec, 287
289 (x,0,1) e exp'
<=>
(x,0,1) e n3 & [~[x=0 & 0=0] & 1=exp(x,0)]
U Spec, 288
290 [(x,0,1) e exp' => (x,0,1) e n3 & [~[x=0 & 0=0] & 1=exp(x,0)]]
&
[(x,0,1) e n3 & [~[x=0 & 0=0] & 1=exp(x,0)] => (x,0,1) e exp']
Iff-And, 289
291 (x,0,1) e exp' => (x,0,1) e n3 & [~[x=0 & 0=0] & 1=exp(x,0)]
Split, 290
Sufficient: For (x,0,1) e exp'
292 (x,0,1) e n3 & [~[x=0 & 0=0] & 1=exp(x,0)] => (x,0,1) e exp'
Split, 290
Apply definition of n3
293 ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]
U Spec, 43
294 ALL(c3):[(x,0,c3) e n3 <=> x e n & 0 e n & c3 e n]
U Spec, 293
295 (x,0,1) e n3 <=> x e n & 0 e n & 1 e n
U Spec, 294
296 [(x,0,1) e n3 => x e n & 0 e n & 1 e n]
&
[x e n & 0 e n & 1 e n => (x,0,1) e n3]
Iff-And, 295
297 [(x,0,1) e n3 => x e n & 0 e n & 1 e n]
&
[x e n & 0 e n & 1 e n => (x,0,1) e n3]
Iff-And, 295
298 (x,0,1) e n3 => x e n & 0 e n & 1 e n
Split, 297
299 x e n & 0 e n & 1 e n => (x,0,1) e n3
Split, 297
300 x e n & 0 e n
Join, 285, 2
301 x e n & 0 e n & 1 e n
Join, 300, 3
302 (x,0,1) e n3
Detach, 299, 301
303 x=0 & 0=0
Premise
304 x=0
Split, 303
305 0=0
Split, 303
306 x=0 & ~x=0
Join, 304, 286
307 ~[x=0 & 0=0]
4 Conclusion, 303
Apply definition of exp
308 x e n => [~x=0 => exp(x,0)=1]
U Spec, 24
309 ~x=0 => exp(x,0)=1
Detach, 308, 285
310 exp(x,0)=1
Detach, 309, 286
311 1=exp(x,0)
Sym, 310
312 ~[x=0 & 0=0] & 1=exp(x,0)
Join, 307, 311
313 (x,0,1) e n3 & [~[x=0 & 0=0] & 1=exp(x,0)]
Join, 302, 312
314 (x,0,1) e exp'
Detach, 292, 313
315 ALL(a2):ALL(b):[(x,a2) e dom & b e n => [exp'(x,a2)=b <=>
(x,a2,b) e exp']]
U Spec, 180
316 ALL(b):[(x,0) e dom & b e n => [exp'(x,0)=b <=> (x,0,b) e exp']]
U Spec, 315
317 (x,0) e dom & 1 e n => [exp'(x,0)=1 <=> (x,0,1) e exp']
U Spec, 316
Apply definition of dom
318 ALL(b):[(x,b) e dom <=> (x,b) e n2 & ~[x=0 & b=0]]
U Spec, 47
319 (x,0) e dom <=> (x,0) e n2 & ~[x=0 & 0=0]
U Spec, 318
320 [(x,0) e dom => (x,0) e n2 & ~[x=0 & 0=0]]
&
[(x,0) e n2 & ~[x=0 & 0=0] => (x,0) e dom]
Iff-And, 319
321 (x,0) e dom => (x,0) e n2 & ~[x=0 & 0=0]
Split, 320
322 (x,0) e n2 & ~[x=0 & 0=0] => (x,0) e dom
Split, 320
Apply definition of n2
323 ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]
U Spec, 33
324 (x,0) e n2 <=> x e n & 0 e n
U Spec, 323
325 [(x,0) e n2 => x e n & 0 e n]
&
[x e n & 0 e n => (x,0) e n2]
Iff-And, 324
326 (x,0) e n2 => x e n & 0 e n
Split, 325
327 x e n & 0 e n => (x,0) e n2
Split, 325
328 x e n & 0 e n
Join, 285, 2
329 (x,0) e n2
Detach, 327, 328
330 x=0 & 0=0
Premise
331 x=0
Split, 330
332 0=0
Split, 330
333 x=0 & ~x=0
Join, 331, 286
334 ~[x=0 & 0=0]
4 Conclusion, 330
335 (x,0) e n2 & ~[x=0 & 0=0]
Join, 329, 334
336 (x,0) e dom
Detach, 322, 335
337 (x,0) e dom & 1 e n
Join, 336, 3
338 exp'(x,0)=1 <=> (x,0,1