THEOREM
*******
Starting from Peano's Axioms,
we can prove:
EXIST(add):[ALL(a):ALL(b):[a
e n & b e n =>
add(a,b) e n]
& ALL(a):[a e n => add(a,0)=a]
& ALL(a):ALL(b):[a e n & b e n =>
add(a,s(b))=s(add(a,b))]]
By Dan Christensen
2022-02-02
This machine-verified formal
proof was written with the aid of the author's DC Proof 2.0 freeware available http://www.dcproof.com
OUTLINE OF PROOF
****************
1. Starting from Peano's
Axioms, construct the set of ordered triples add, the graph set of the required
function. (Lines 1-28)
2. Establish some elementary
properties of the set add. (Lines 29-122)
3. Prove that the set add meets
the requirements of functionality. (Lines 123-646)
4. Introduce the function
operator fadd. (Lines 647-668)
5. Establish the required
properties of fadd. (Lines 669-End)
PROOF
*****
Peano's Axioms for (n,s,0)
1 Set(n)
Axiom
2 0 e n
Axiom
3 ALL(a):[a e n => s(a) e n]
Axiom
4 ALL(a):ALL(b):[a e n & b e n => [s(a)=s(b) => a=b]]
Axiom
5 ALL(a):[a e n => ~s(a)=0]
Axiom
6 ALL(a):[Set(a) &
ALL(b):[b e a => b e n]
=>
[0 e a & ALL(b):[b e a => s(b) e a]
=>
ALL(b):[b e n => b e a]]]
Axiom
Construct n2, the Cartesian
product of n with itself
Apply Cartesian Product Axiom
for ordered pairs
7 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
8 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, 7
9 Set(n) & Set(n) =>
EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e n & c2 e n]]
U Spec, 8
10 Set(n) & Set(n)
Join, 1, 1
11 EXIST(b):[Set'(b)
& ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e n & c2 e n]]
Detach, 9, 10
12 Set'(n2) & ALL(c1):ALL(c2):[(c1,c2) e n2 <=> c1 e n & c2 e n]
E Spec, 11
Define: n2
13 Set'(n2)
Split, 12
14 ALL(c1):ALL(c2):[(c1,c2) e n2 <=> c1 e n & c2 e n]
Split, 12
Construct n3
Apply Cartesian Product Axiom
for ordered triples
15 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
16 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, 15
17 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, 16
18 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, 17
19 Set(n) & Set(n)
Join, 1, 1
20 Set(n) & Set(n) & Set(n)
Join, 19, 1
21 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, 18, 20
22 Set''(n3) &
ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e n3 <=> c1 e n & c2 e n & c3 e n]
E Spec, 21
Define: n3
23 Set''(n3)
Split, 22
24 ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e n3 <=> c1 e n & c2 e n & c3 e n]
Split, 22
Construct add, a set of ordered
triples, the graph set for the required function
Apply Subset Axiom
25 EXIST(sub):[Set''(sub)
& ALL(a):ALL(b):ALL(c):[(a,b,c) e sub
<=>
(a,b,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(a,b,c) e d]]]
Subset, 23
26 Set''(add) &
ALL(a):ALL(b):ALL(c):[(a,b,c) e add
<=>
(a,b,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(a,b,c) e d]]
E Spec, 25
Define: add
27 Set''(add)
Split, 26
28 ALL(a):ALL(b):ALL(c):[(a,b,c) e add
<=>
(a,b,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(a,b,c) e d]]
Split, 26
Establish some useful properties of the add set
Prove: ALL(a):ALL(b):ALL(c):[(a,b,c) e add => a e n & b e n & c e n]
Suppose...
29 (x,y,z) e add
Premise
30 ALL(b):ALL(c):[(x,b,c) e add
<=>
(x,b,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,b,c) e d]]
U Spec, 28
31 ALL(c):[(x,y,c) e add
<=>
(x,y,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,y,c) e d]]
U Spec, 30
32 (x,y,z) e add
<=>
(x,y,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,y,z) e d]
U Spec, 31
33 [(x,y,z) e add => (x,y,z) e n3 &
ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,y,z) e d]]
&
[(x,y,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,y,z) e d] => (x,y,z) e add]
Iff-And, 32
34 (x,y,z) e add => (x,y,z) e n3 &
ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,y,z) e d]
Split, 33
35 (x,y,z) e n3 & ALL(d):[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,y,z) e d] => (x,y,z) e add
Split, 33
36 (x,y,z) e n3 & ALL(d):[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,y,z) e d]
Detach, 34, 29
37 (x,y,z) e n3
Split, 36
38 ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,y,z) e d]
Split, 36
39 ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]
U Spec, 24
40 ALL(c3):[(x,y,c3) e n3 <=> x e n & y e n & c3 e n]
U Spec, 39
41 (x,y,z) e n3 <=> x e n & y e n & z e n
U Spec, 40
42 [(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, 41
43 (x,y,z) e n3 => x e n & y e n & z e n
Split, 42
44 x e n & y e n & z e n => (x,y,z) e n3
Split, 42
45 x e n & y e n & z e n
Detach, 43, 37
As Required:
46 ALL(a):ALL(b):ALL(c):[(a,b,c) e add => a e n & b e n & c e n]
4 Conclusion, 29
Prove: ALL(a):[aen => (a,0,a)eadd]
Suppose...
47 x e n
Premise
48 ALL(b):ALL(c):[(x,b,c) e add
<=>
(x,b,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,b,c) e d]]
U Spec, 28
49 ALL(c):[(x,0,c) e add
<=>
(x,0,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,0,c) e d]]
U Spec, 48
50 (x,0,x) e add
<=>
(x,0,x) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,0,x) e d]
U Spec, 49
51 [(x,0,x) e add => (x,0,x) e n3 &
ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,0,x) e d]]
&
[(x,0,x) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,0,x) e d] => (x,0,x) e add]
Iff-And, 50
52 (x,0,x) e add => (x,0,x) e n3 &
ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,0,x) e d]
Split, 51
Sufficient: For (x,0,x) e add
53 (x,0,x) e n3 & ALL(d):[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,0,x) e d] => (x,0,x) e add
Split, 51
54 ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]
U Spec, 24
55 ALL(c3):[(x,0,c3) e n3 <=> x e n & 0 e n & c3 e n]
U Spec, 54
56 (x,0,x) e n3 <=> x e n & 0 e n & x e n
U Spec, 55
57 [(x,0,x) e n3 => x e n & 0 e n & x e n]
&
[x e n & 0 e n & x e n => (x,0,x) e n3]
Iff-And, 56
58 (x,0,x) e n3 => x e n & 0 e n & x e n
Split, 57
59 x e n & 0 e n & x e n => (x,0,x) e n3
Split, 57
60 x e n & 0 e n
Join, 47, 2
61 x e n & 0 e n & x e n
Join, 60, 47
62 (x,0,x) e n3
Detach, 59, 61
63 Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
Premise
64 Set''(d)
Split, 63
65 ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
Split, 63
66 ALL(e):[e e n => (e,0,e) e d]
Split, 63
67 ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
Split, 63
68 x e n => (x,0,x) e d
U Spec, 66
69 (x,0,x) e d
Detach, 68, 47
70 ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,0,x) e d]
4 Conclusion, 63
71 (x,0,x) e n3
&
ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,0,x) e d]
Join, 62, 70
72 (x,0,x) e add
Detach, 53, 71
As Required:
73 ALL(a):[a e n => (a,0,a) e add]
4 Conclusion, 47
Prove: ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n
=> [(a,b,c) e add => (a,s(b),s(c)) e add]]
Suppose...
74 x e n & y e n & z e n
Premise
75 x e n
Split, 74
76 y e n
Split, 74
77 z e n
Split, 74
Prove: (x,y,z) e add => (x,s(y),s(z)) e add
Suppose...
78 (x,y,z) e add
Premise
79 ALL(b):ALL(c):[(x,b,c) e add
<=>
(x,b,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,b,c) e d]]
U Spec, 28
80 ALL(c):[(x,y,c) e add
<=>
(x,y,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,y,c) e d]]
U Spec, 79
81 (x,y,z) e add
<=>
(x,y,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,y,z) e d]
U Spec, 80
82 [(x,y,z) e add => (x,y,z) e n3 &
ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,y,z) e d]]
&
[(x,y,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,y,z) e d] => (x,y,z) e add]
Iff-And, 81
83 (x,y,z) e add => (x,y,z) e n3 &
ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,y,z) e d]
Split, 82
84 (x,y,z) e n3 & ALL(d):[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,y,z) e d] => (x,y,z) e add
Split, 82
85 (x,y,z) e n3 & ALL(d):[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,y,z) e d]
Detach, 83, 78
86 (x,y,z) e n3
Split, 85
87 ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,y,z) e d]
Split, 85
88 ALL(b):ALL(c):[(x,b,c) e add
<=>
(x,b,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,b,c) e d]]
U Spec, 28
89 y e n => s(y) e n
U Spec, 3
90 s(y) e n
Detach, 89, 76
91 ALL(c):[(x,s(y),c) e add
<=>
(x,s(y),c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,s(y),c) e d]]
U Spec, 88, 90
92 z e n => s(z) e n
U Spec, 3
93 s(z) e n
Detach, 92, 77
94 (x,s(y),s(z)) e add
<=>
(x,s(y),s(z)) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,s(y),s(z)) e d]
U Spec, 91, 93
95 [(x,s(y),s(z)) e add => (x,s(y),s(z)) e n3 &
ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,s(y),s(z)) e d]]
&
[(x,s(y),s(z)) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,s(y),s(z)) e d] => (x,s(y),s(z)) e add]
Iff-And, 94
96 (x,s(y),s(z)) e add => (x,s(y),s(z)) e n3 &
ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,s(y),s(z)) e d]
Split, 95
Sufficient: For (x,s(y),s(z)) e add
97 (x,s(y),s(z)) e n3 & ALL(d):[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,s(y),s(z)) e d] => (x,s(y),s(z)) e add
Split, 95
98 ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]
U Spec, 24
99 ALL(c3):[(x,s(y),c3) e n3 <=> x e n & s(y) e n & c3 e n]
U Spec, 98, 97
100 (x,s(y),s(z)) e n3 <=> x e n & s(y) e n & s(z) e n
U Spec, 99, 97
101 [(x,s(y),s(z)) e n3 => x e n & s(y) e n & s(z) e n]
&
[x e n & s(y) e n & s(z) e n => (x,s(y),s(z)) e n3]
Iff-And, 100
102 (x,s(y),s(z)) e n3 => x e n & s(y) e n & s(z) e n
Split, 101
Sufficient: For (x,s(y),s(z)) e n3
103 x e n & s(y) e n & s(z) e n => (x,s(y),s(z)) e n3
Split, 101
104 x e n & s(y) e n
Join, 75, 90
105 x e n & s(y) e n & s(z) e n
Join, 104, 93
106 (x,s(y),s(z)) e n3
Detach, 103, 105
Prove: ALL(d):[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
& ALL(e):[e e n =>
(e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d =>
(e,s(f),s(g)) e d]
=> (x,s(y),s(z)) e d]
107 Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
Premise
108 Set''(d)
Split, 107
109 ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
Split, 107
110 ALL(e):[e e n => (e,0,e) e d]
Split, 107
111 ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
Split, 107
112 ALL(f):ALL(g):[(x,f,g) e d => (x,s(f),s(g)) e d]
U Spec, 111
113 ALL(g):[(x,y,g) e d => (x,s(y),s(g)) e d]
U Spec, 112
114 (x,y,z) e d => (x,s(y),s(z)) e d
U Spec, 113
115 Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,y,z) e d
U Spec, 87
116 (x,y,z) e d
Detach, 115, 107
117 (x,s(y),s(z)) e d
Detach, 114, 116
As Required:
118 ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,s(y),s(z)) e d]
4 Conclusion, 107
119 (x,s(y),s(z)) e n3
&
ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,s(y),s(z)) e d]
Join, 106, 118
120 (x,s(y),s(z)) e add
Detach, 97, 119
As Required:
121 (x,y,z) e add => (x,s(y),s(z)) e add
4 Conclusion, 78
As Required:
122 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n
=>
[(a,b,c) e add => (a,s(b),s(c)) e add]]
4 Conclusion, 74
123 Set''(add) & Set'(n2)
Join, 27, 13
124 Set''(add) & Set'(n2) & Set(n)
Join, 123, 1
Part 1
Prove: ALL(a):ALL(b):ALL(c):[(a,b,c) e add => (a,b) e n2 & c e n]
Suppose...
125 (x,y,z) e add
Premise
126 ALL(b):ALL(c):[(x,b,c) e add => x e n & b e n & c e n]
U Spec, 46
127 ALL(c):[(x,y,c) e add => x e n & y e n & c e n]
U Spec, 126
128 (x,y,z) e add => x e n & y e n & z e n
U Spec, 127
129 x e n & y e n & z e n
Detach, 128, 125
130 x e n
Split, 129
131 y e n
Split, 129
132 z e n
Split, 129
133 ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]
U Spec, 14
134 (x,y) e n2 <=> x e n & y e n
U Spec, 133
135 [(x,y) e n2 => x e n & y e n]
&
[x e n & y e n => (x,y) e n2]
Iff-And, 134
136 (x,y) e n2 => x e n & y e n
Split, 135
137 x e n & y e n => (x,y) e n2
Split, 135
138 x e n & y e n
Join, 130, 131
139 (x,y) e n2
Detach, 137, 138
140 (x,y) e n2 & z e n
Join, 139, 132
Part 1
As Required:
141 ALL(a):ALL(b):ALL(c):[(a,b,c) e add => (a,b) e n2 & c e n]
4 Conclusion, 125
142 x e n
Premise
143 EXIST(sub):[Set(sub) & ALL(b):[b e sub <=> b e n &
EXIST(c):[c e n & (x,b,c) e add]]]
Subset, 1
144 Set(p1) & ALL(b):[b e p1 <=> b e n & EXIST(c):[c e n & (x,b,c) e add]]
E Spec, 143
Define: p1
145 Set(p1)
Split, 144
146 ALL(b):[b e p1 <=> b e n & EXIST(c):[c e n & (x,b,c) e add]]
Split, 144
147 y e p1
Premise
148 y e p1 <=> y e n & EXIST(c):[c e n & (x,y,c) e add]
U Spec, 146
149 [y e p1 => y e n & EXIST(c):[c e n & (x,y,c) e add]]
&
[y e n & EXIST(c):[c e n & (x,y,c) e add] => y e p1]
Iff-And, 148
150 y e p1 => y e n & EXIST(c):[c e n & (x,y,c) e add]
Split, 149
151 y e n & EXIST(c):[c e n & (x,y,c) e add] => y e p1
Split, 149
152 y e n & EXIST(c):[c e n & (x,y,c) e add]
Detach, 150, 147
153 y e n
Split, 152
154 ALL(b):[b e p1 => b e n]
4 Conclusion, 147
155 Set(p1) & ALL(b):[b e p1 => b e n]
=>
[0 e p1 & ALL(b):[b e p1 => s(b) e p1]
=>
ALL(b):[b e n => b e p1]]
U Spec, 6
156 Set(p1) & ALL(b):[b e p1 => b e n]
Join, 145, 154
Sufficient: For ALL(b):[b e n => b e p1]
157 0 e p1 & ALL(b):[b e p1 => s(b) e p1]
=>
ALL(b):[b e n => b e p1]
Detach, 155, 156
158 0 e p1 <=> 0 e n & EXIST(c):[c e n & (x,0,c) e add]
U Spec, 146
159 [0 e p1 => 0 e n & EXIST(c):[c e n & (x,0,c) e add]]
&
[0 e n & EXIST(c):[c e n & (x,0,c) e add] => 0 e p1]
Iff-And, 158
160 0 e p1 => 0 e n & EXIST(c):[c e n & (x,0,c) e add]
Split, 159
Sufficient:
161 0 e n & EXIST(c):[c e n & (x,0,c) e add] => 0 e p1
Split, 159
162 x e n => (x,0,x) e add
U Spec, 73
163 (x,0,x) e add
Detach, 162, 142
164 x e n & (x,0,x) e add
Join, 142, 163
165 EXIST(b):[b e n & (x,0,b) e add]
E Gen, 164
166 0 e n & EXIST(b):[b e n & (x,0,b) e add]
Join, 2, 165
As Required:
167 0 e p1
Detach, 161, 166
168 y e p1
Premise
169 y e p1 <=> y e n & EXIST(c):[c e n & (x,y,c) e add]
U Spec, 146
170 [y e p1 => y e n & EXIST(c):[c e n & (x,y,c) e add]]
&
[y e n & EXIST(c):[c e n & (x,y,c) e add] => y e p1]
Iff-And, 169
171 y e p1 => y e n & EXIST(c):[c e n & (x,y,c) e add]
Split, 170
172 y e n & EXIST(c):[c e n & (x,y,c) e add] => y e p1
Split, 170
173 y e n & EXIST(c):[c e n & (x,y,c) e add]
Detach, 171, 168
174 y e n
Split, 173
175 EXIST(c):[c e n & (x,y,c) e add]
Split, 173
176 z e n & (x,y,z) e add
E Spec, 175
177 z e n
Split, 176
178 (x,y,z) e add
Split, 176
179 y e n => s(y) e n
U Spec, 3
180 s(y) e n
Detach, 179, 174
181 s(y) e p1 <=> s(y) e n & EXIST(c):[c e n & (x,s(y),c) e add]
U Spec, 146, 180
182 [s(y) e p1 => s(y) e n & EXIST(c):[c e n & (x,s(y),c) e add]]
&
[s(y) e n & EXIST(c):[c e n & (x,s(y),c) e add] => s(y) e p1]
Iff-And, 181
183 s(y) e p1 => s(y) e n & EXIST(c):[c e n & (x,s(y),c) e add]
Split, 182
Sufficient:
184 s(y) e n & EXIST(c):[c e n & (x,s(y),c) e add] => s(y) e p1
Split, 182
185 ALL(b):ALL(c):[x e n & b e n & c e n
=>
[(x,b,c) e add => (x,s(b),s(c)) e add]]
U Spec, 122
186 ALL(c):[x e n & y e n & c e n
=>
[(x,y,c) e add => (x,s(y),s(c)) e add]]
U Spec, 185
187 x e n & y e n & z e n
=>
[(x,y,z) e add => (x,s(y),s(z)) e add]
U Spec, 186
188 x e n & y e n
Join, 142, 174
189 x e n & y e n & z e n
Join, 188, 177
190 (x,y,z) e add => (x,s(y),s(z)) e add
Detach, 187, 189
191 (x,s(y),s(z)) e add
Detach, 190, 178
192 z e n => s(z) e n
U Spec, 3
193 s(z) e n
Detach, 192, 177
194 s(z) e n & (x,s(y),s(z)) e add
Join, 193, 191
195 EXIST(c):[c e n & (x,s(y),c) e add]
E Gen, 194
196 s(y) e n & EXIST(c):[c e n & (x,s(y),c) e add]
Join, 180, 195
197 s(y) e p1
Detach, 184, 196
As Required:
198 ALL(b):[b e p1 => s(b) e p1]
4 Conclusion, 168
199 0 e p1 & ALL(b):[b e p1 => s(b) e p1]
Join, 167, 198
200 ALL(b):[b e n => b e p1]
Detach, 157, 199
201 y e n
Premise
202 y e n => y e p1
U Spec, 200
203 y e p1
Detach, 202, 201
204 y e p1 <=> y e n & EXIST(c):[c e n & (x,y,c) e add]
U Spec, 146
205 [y e p1 => y e n & EXIST(c):[c e n & (x,y,c) e add]]
&
[y e n & EXIST(c):[c e n & (x,y,c) e add] => y e p1]
Iff-And, 204
206 y e p1 => y e n & EXIST(c):[c e n & (x,y,c) e add]
Split, 205
207 y e n & EXIST(c):[c e n & (x,y,c) e add] => y e p1
Split, 205
208 y e n & EXIST(c):[c e n & (x,y,c) e add]
Detach, 206, 203
209 y e n
Split, 208
210 EXIST(c):[c e n & (x,y,c) e add]
Split, 208
211 ALL(b):[b e n =>
EXIST(c):[c e n & (x,b,c) e add]]
4 Conclusion, 201
212 ALL(a):[a e n
=>
ALL(b):[b e n =>
EXIST(c):[c e n & (a,b,c) e add]]]
4 Conclusion, 142
Part 2
Prove: ALL(a1):ALL(a2):[(a1,a2) e n2 => EXIST(c):[c e n &
(a1,a2,c) e add]]
Suppose...
213 (x,y) e n2
Premise
214 ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]
U Spec, 14
215 (x,y) e n2 <=> x e n & y e n
U Spec, 214
216 [(x,y) e n2 => x e n & y e n]
&
[x e n & y e n => (x,y) e n2]
Iff-And, 215
217 (x,y) e n2 => x e n & y e n
Split, 216
218 x e n & y e n => (x,y) e n2
Split, 216
219 x e n & y e n
Detach, 217, 213
220 x e n
Split, 219
221 y e n
Split, 219
222 x e n
=>
ALL(b):[b e n =>
EXIST(c):[c e n & (x,b,c) e add]]
U Spec, 212
223 ALL(b):[b e n =>
EXIST(c):[c e n & (x,b,c) e add]]
Detach, 222, 220
224 y e n => EXIST(c):[c e n & (x,y,c) e add]
U Spec, 223
225 EXIST(c):[c e n & (x,y,c) e add]
Detach, 224, 221
As Required: Part 2
226 ALL(a1):ALL(a2):[(a1,a2) e n2 =>
EXIST(c):[c e n & (a1,a2,c) e add]]
4 Conclusion, 213
Suppose...
227 x e n
Premise
Suppose to the contrary...
228 ~[z e n => [(x,0,z) e add => z=x]]
Premise
229 ~~[z e n & ~[(x,0,z) e add => z=x]]
Imply-And, 228
230 z e n & ~[(x,0,z) e add => z=x]
Rem DNeg, 229
231 z e n & ~~[(x,0,z) e add & ~z=x]
Imply-And, 230
232 z e n & [(x,0,z) e add & ~z=x]
Rem DNeg, 231
233 z e n
Split, 232
234 (x,0,z) e add & ~z=x
Split, 232
235 (x,0,z) e add
Split, 234
236 ~z=x
Split, 234
237 ALL(b):ALL(c):[(x,b,c) e add
<=>
(x,b,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,b,c) e d]]
U Spec, 28
238 ALL(c):[(x,0,c) e add
<=>
(x,0,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,0,c) e d]]
U Spec, 237
239 (x,0,z) e add
<=>
(x,0,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,0,z) e d]
U Spec, 238
240 [(x,0,z) e add => (x,0,z) e n3 &
ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,0,z) e d]]
&
[(x,0,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,0,z) e d] => (x,0,z) e add]
Iff-And, 239
241 (x,0,z) e add => (x,0,z) e n3 &
ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,0,z) e d]
Split, 240
242 (x,0,z) e n3 & ALL(d):[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,0,z) e d] => (x,0,z) e add
Split, 240
243 ~[(x,0,z) e n3 & ALL(d):[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,0,z) e d]] => ~(x,0,z) e add
Contra, 241
244 ~~[(x,0,z) e n3 => ~ALL(d):[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,0,z) e d]] => ~(x,0,z) e add
Imply-And, 243
245 (x,0,z) e n3 => ~ALL(d):[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,0,z) e d] => ~(x,0,z) e add
Rem DNeg, 244
246 (x,0,z) e n3 => ~~EXIST(d):~[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,0,z) e d] => ~(x,0,z) e add
Quant, 245
247 (x,0,z) e n3 => EXIST(d):~[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,0,z) e d] => ~(x,0,z) e add
Rem DNeg, 246
248 (x,0,z) e n3 => EXIST(d):~~[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d] & ~(x,0,z) e d] => ~(x,0,z) e add
Imply-And, 247
Sufficient: For ~(x,0,z) e add (to obtain a
contradiction)
249 (x,0,z) e n3 => EXIST(d):[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d] & ~(x,0,z) e d] => ~(x,0,z) e add
Rem DNeg, 248
Suppose...
250 (x,0,z) e n3
Premise
251 EXIST(sub):[Set''(sub) & ALL(a):ALL(b):ALL(c):[(a,b,c) e sub
<=>
(a,b,c) e add & ~[a=x & b=0 & c=z]]]
Subset, 27
252 Set''(q1) & ALL(a):ALL(b):ALL(c):[(a,b,c) e q1
<=>
(a,b,c) e add & ~[a=x & b=0 & c=z]]
E Spec, 251
Define: q1
253 Set''(q1)
Split, 252
254 ALL(a):ALL(b):ALL(c):[(a,b,c) e q1
<=>
(a,b,c) e add & ~[a=x & b=0 & c=z]]
Split, 252
Suppose...
255 (t,u,v) e q1
Premise
256 ALL(b):ALL(c):[(t,b,c) e q1
<=>
(t,b,c) e add & ~[t=x & b=0 & c=z]]
U Spec, 254
257 ALL(c):[(t,u,c) e q1
<=>
(t,u,c) e add & ~[t=x & u=0 & c=z]]
U Spec, 256
258 (t,u,v) e q1
<=>
(t,u,v) e add & ~[t=x & u=0 & v=z]
U Spec, 257
259 [(t,u,v) e q1 => (t,u,v) e add & ~[t=x & u=0 & v=z]]
&
[(t,u,v) e add & ~[t=x & u=0 & v=z] => (t,u,v) e q1]
Iff-And, 258
260 (t,u,v) e q1 => (t,u,v) e add & ~[t=x & u=0 & v=z]
Split, 259
261 (t,u,v) e add & ~[t=x & u=0 & v=z] => (t,u,v) e q1
Split, 259
262 (t,u,v) e add & ~[t=x & u=0 & v=z]
Detach, 260, 255
263 (t,u,v) e add
Split, 262
264 ~[t=x & u=0 & v=z]
Split, 262
265 ALL(b):ALL(c):[(t,b,c) e add => t e n & b e n & c e n]
U Spec, 46
266 ALL(c):[(t,u,c) e add => t e n & u e n & c e n]
U Spec, 265
267 (t,u,v) e add => t e n & u e n & v e n
U Spec, 266
268 t e n & u e n & v e n
Detach, 267, 263
As Required:
269 ALL(e):ALL(f):ALL(g):[(e,f,g) e q1 => e e n & f e n & g e n]
4 Conclusion, 255
270 t e n
Premise
271 ALL(b):ALL(c):[(t,b,c) e q1
<=>
(t,b,c) e add & ~[t=x & b=0 & c=z]]
U Spec, 254
272 ALL(c):[(t,0,c) e q1
<=>
(t,0,c) e add & ~[t=x & 0=0 & c=z]]
U Spec, 271
273 (t,0,t) e q1
<=>
(t,0,t) e add & ~[t=x & 0=0 & t=z]
U Spec, 272
274 [(t,0,t) e q1 => (t,0,t) e add & ~[t=x & 0=0 & t=z]]
&
[(t,0,t) e add & ~[t=x & 0=0 & t=z] => (t,0,t) e q1]
Iff-And, 273
275 (t,0,t) e q1 => (t,0,t) e add & ~[t=x & 0=0 & t=z]
Split, 274
Sufficient:
276 (t,0,t) e add & ~[t=x & 0=0 & t=z] => (t,0,t) e q1
Split, 274
277 t e n => (t,0,t) e add
U Spec, 73
278 (t,0,t) e add
Detach, 277, 270
Suppose to the contrary...
279 t=x & 0=0 & t=z
Premise
280 t=x
Split, 279
281 0=0
Split, 279
282 t=z
Split, 279
283 z=x
Substitute, 282,
280
284 z=x & ~z=x
Join, 283, 236
As Required:
285 ~[t=x & 0=0 & t=z]
4 Conclusion, 279
286 (t,0,t) e add & ~[t=x & 0=0 & t=z]
Join, 278, 285
287 (t,0,t) e q1
Detach, 276, 286
As Required:
288 ALL(e):[e e n => (e,0,e) e q1]
4 Conclusion, 270
Suppose...
289 (t,u,v) e q1
Premise
290 ALL(b):ALL(c):[(t,b,c) e q1
<=>
(t,b,c) e add & ~[t=x & b=0 & c=z]]
U Spec, 254
291 ALL(c):[(t,u,c) e q1
<=>
(t,u,c) e add & ~[t=x & u=0 & c=z]]
U Spec, 290
292 (t,u,v) e q1
<=>
(t,u,v) e add & ~[t=x & u=0 & v=z]
U Spec, 291
293 [(t,u,v) e q1 => (t,u,v) e add & ~[t=x & u=0 & v=z]]
&
[(t,u,v) e add & ~[t=x & u=0 & v=z] => (t,u,v) e q1]
Iff-And, 292
294 (t,u,v) e q1 => (t,u,v) e add & ~[t=x & u=0 & v=z]
Split, 293
295 (t,u,v) e add & ~[t=x & u=0 & v=z] => (t,u,v) e q1
Split, 293
296 (t,u,v) e add & ~[t=x & u=0 & v=z]
Detach, 294, 289
297 (t,u,v) e add
Split, 296
298 ~[t=x & u=0 & v=z]
Split, 296
299 ALL(b):ALL(c):[(t,b,c) e add
<=>
(t,b,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(t,b,c) e d]]
U Spec, 28
300 ALL(c):[(t,u,c) e add
<=>
(t,u,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(t,u,c) e d]]
U Spec, 299
301 (t,u,v) e add
<=>
(t,u,v) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(t,u,v) e d]
U Spec, 300
302 [(t,u,v) e add => (t,u,v) e n3 &
ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(t,u,v) e d]]
& [(t,u,v) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(t,u,v) e d] => (t,u,v) e add]
Iff-And, 301
303 (t,u,v) e add => (t,u,v) e n3 &
ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(t,u,v) e d]
Split, 302
304 (t,u,v) e n3 & ALL(d):[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(t,u,v) e d] => (t,u,v) e add
Split, 302
305 (t,u,v) e n3 & ALL(d):[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(t,u,v) e d]
Detach, 303, 297
306 (t,u,v) e n3
Split, 305
307 ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(t,u,v) e d]
Split, 305
308 ALL(b):ALL(c):[(t,b,c) e q1
<=>
(t,b,c) e add & ~[t=x & b=0 & c=z]]
U Spec, 254
309 ALL(b):ALL(c):[(t,b,c) e add => t e n & b e n & c e n]
U Spec, 46
310 ALL(c):[(t,u,c) e add => t e n & u e n & c e n]
U Spec, 309
311 (t,u,v) e add => t e n & u e n & v e n
U Spec, 310
312 t e n & u e n & v e n
Detach, 311, 297
313 t e n
Split, 312
314 u e n
Split, 312
315 v e n
Split, 312
316 u e n => s(u) e n
U Spec, 3
317 s(u) e n
Detach, 316, 314
318 v e n => s(v) e n
U Spec, 3
319 s(v) e n
Detach, 318, 315
320 ALL(b):ALL(c):[(t,b,c) e q1
<=>
(t,b,c) e add & ~[t=x & b=0 & c=z]]
U Spec, 254
321 ALL(c):[(t,s(u),c) e q1
<=>
(t,s(u),c) e add & ~[t=x & s(u)=0 & c=z]]
U Spec, 320, 317
322 (t,s(u),s(v)) e q1
<=>
(t,s(u),s(v)) e add & ~[t=x & s(u)=0 & s(v)=z]
U Spec, 321, 319
323 [(t,s(u),s(v)) e q1 => (t,s(u),s(v)) e add & ~[t=x & s(u)=0 & s(v)=z]]
&
[(t,s(u),s(v)) e add & ~[t=x & s(u)=0 & s(v)=z] => (t,s(u),s(v)) e q1]
Iff-And, 322
324 (t,s(u),s(v)) e q1 => (t,s(u),s(v)) e add & ~[t=x & s(u)=0 & s(v)=z]
Split, 323
Sufficient:
325 (t,s(u),s(v)) e add & ~[t=x & s(u)=0 & s(v)=z] => (t,s(u),s(v)) e q1
Split, 323
326 ALL(b):ALL(c):[t e n & b e n & c e n
=>
[(t,b,c) e add => (t,s(b),s(c)) e add]]
U Spec, 122
327 ALL(c):[t e n & u e n & c e n
=>
[(t,u,c) e add => (t,s(u),s(c)) e add]]
U Spec, 326
328 t e n & u e n & v e n
=>
[(t,u,v) e add => (t,s(u),s(v)) e add]
U Spec, 327
329 (t,u,v) e add => (t,s(u),s(v)) e add
Detach, 328, 312
As Required:
330 (t,s(u),s(v)) e add
Detach, 329, 297
Suppose to the contrary...
331 t=x & s(u)=0 & s(v)=z
Premise
332 t=x
Split, 331
333 s(u)=0
Split, 331
334 s(v)=z
Split, 331
335 u e n => ~s(u)=0
U Spec, 5
336 ~s(u)=0
Detach, 335, 314
337 s(u)=0 & ~s(u)=0
Join, 333, 336
As Required:
338 ~[t=x & s(u)=0 & s(v)=z]
4 Conclusion, 331
339 (t,s(u),s(v)) e add & ~[t=x & s(u)=0 & s(v)=z]
Join, 330, 338
340 (t,s(u),s(v)) e q1
Detach, 325, 339
As Required:
341 ALL(e):ALL(f):ALL(g):[(e,f,g) e q1 => (e,s(f),s(g)) e q1]
4 Conclusion, 289
342 ALL(b):ALL(c):[(x,b,c) e q1
<=>
(x,b,c) e add & ~[x=x & b=0 & c=z]]
U Spec, 254
343 ALL(c):[(x,0,c) e q1
<=>
(x,0,c) e add & ~[x=x & 0=0 & c=z]]
U Spec, 342
344 (x,0,z) e q1
<=>
(x,0,z) e add & ~[x=x & 0=0 & z=z]
U Spec, 343
345 [(x,0,z) e q1 => (x,0,z) e add & ~[x=x & 0=0 & z=z]]
&
[(x,0,z) e add & ~[x=x & 0=0 & z=z] => (x,0,z) e q1]
Iff-And, 344
346 (x,0,z) e q1 => (x,0,z) e add & ~[x=x & 0=0 & z=z]
Split, 345
347 (x,0,z) e add & ~[x=x & 0=0 & z=z] => (x,0,z) e q1
Split, 345
348 ~[(x,0,z) e add & ~[x=x & 0=0 & z=z]] => ~(x,0,z) e q1
Contra, 346
349 ~~[~(x,0,z) e add | ~~[x=x & 0=0 & z=z]] => ~(x,0,z) e q1
DeMorgan, 348
350 ~(x,0,z) e add | ~~[x=x & 0=0 & z=z] => ~(x,0,z) e q1
Rem DNeg, 349
351 ~(x,0,z) e add | x=x & 0=0 & z=z => ~(x,0,z) e q1
Rem DNeg, 350
352 x=x
Reflex
353 0=0
Reflex
354 z=z
Reflex
355 x=x & 0=0
Join, 352, 353
356 x=x & 0=0 & z=z
Join, 355, 354
357 ~(x,0,z) e add | x=x & 0=0 & z=z
Arb Or, 356
As Required:
358 ~(x,0,z) e q1
Detach, 351, 357
359 Set''(q1)
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e q1 => e e n & f e n & g e n]
Join, 253, 269
360 Set''(q1)
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e q1 => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e q1]
Join, 359, 288
361 Set''(q1)
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e q1 => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e q1]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e q1 => (e,s(f),s(g)) e q1]
Join, 360, 341
362 Set''(q1)
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e q1 => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e q1]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e q1 => (e,s(f),s(g)) e q1]
&
~(x,0,z) e q1
Join, 361, 358
363 EXIST(d):[Set''(d)
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
&
~(x,0,z) e d]
E Gen, 362
364 (x,0,z) e n3
=>
EXIST(d):[Set''(d)
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
&
~(x,0,z) e d]
4 Conclusion, 250
365 ~(x,0,z) e add
Detach, 249, 364
366 (x,0,z) e add & ~(x,0,z) e add
Join, 235, 365
367 ~EXIST(c):~[c e n => [(x,0,c) e add => c=x]]
4 Conclusion, 228
368 ~~ALL(c):~~[c e n => [(x,0,c) e add => c=x]]
Quant, 367
369 ALL(c):~~[c e n => [(x,0,c) e add => c=x]]
Rem DNeg, 368
370 ALL(c):[c e n => [(x,0,c) e add => c=x]]
Rem DNeg, 369
As Required:
371 ALL(a):[a e n => ALL(c):[c e n => [(a,0,c) e add => c=a]]]
4 Conclusion, 227
Prove: ALL(a):[a e n
=> ALL(b):[b e n
=> ALL(c):ALL(d):[(a,b,c) e add &
(a,b,d) e add => c=d]]]
Suppose...
372 x e n
Premise
373 EXIST(sub):[Set(sub) & ALL(b):[b e sub <=> b e n & ALL(c):ALL(d):[(x,b,c) e add & (x,b,d) e add => c=d]]]
Subset, 1
374 Set(p2) & ALL(b):[b e p2 <=> b e n & ALL(c):ALL(d):[(x,b,c) e add & (x,b,d) e add => c=d]]
E Spec, 373
Define: p2
375 Set(p2)
Split, 374
376 ALL(b):[b e p2 <=> b e n & ALL(c):ALL(d):[(x,b,c) e add & (x,b,d) e add => c=d]]
Split, 374
377 Set(p2) & ALL(b):[b e p2 => b e n]
=>
[0 e p2 & ALL(b):[b e p2 => s(b) e p2]
=>
ALL(b):[b e n => b e p2]]
U Spec, 6
378 y e p2
Premise
379 y e p2 <=> y e n & ALL(c):ALL(d):[(x,y,c) e add & (x,y,d) e add => c=d]
U Spec, 376
380 [y e p2 => y e n &
ALL(c):ALL(d):[(x,y,c) e add & (x,y,d) e add => c=d]]
&
[y e n & ALL(c):ALL(d):[(x,y,c) e add & (x,y,d) e add => c=d] => y e p2]
Iff-And, 379
381 y e p2 => y e n &
ALL(c):ALL(d):[(x,y,c) e add & (x,y,d) e add => c=d]
Split, 380
382 y e n & ALL(c):ALL(d):[(x,y,c) e add & (x,y,d) e add => c=d] => y e p2
Split, 380
383 y e n & ALL(c):ALL(d):[(x,y,c) e add & (x,y,d) e add => c=d]
Detach, 381, 378
384 y e n
Split, 383
As Required:
385 ALL(b):[b e p2 => b e n]
4 Conclusion, 378
386 Set(p2) & ALL(b):[b e p2 => b e n]
Join, 375, 385
Sufficient: For ALL(b):[b e n => b e p2]
387 0 e p2 & ALL(b):[b e p2 => s(b) e p2]
=>
ALL(b):[b e n => b e p2]
Detach, 377, 386
388 0 e p2 <=> 0 e n & ALL(c):ALL(d):[(x,0,c) e add & (x,0,d) e add => c=d]
U Spec, 376
389 [0 e p2 => 0 e n &
ALL(c):ALL(d):[(x,0,c) e add & (x,0,d) e add => c=d]]
&
[0 e n & ALL(c):ALL(d):[(x,0,c) e add & (x,0,d) e add => c=d] => 0 e p2]
Iff-And, 388
390 0 e p2 => 0 e n &
ALL(c):ALL(d):[(x,0,c) e add & (x,0,d) e add => c=d]
Split, 389
Sufficient:
391 0 e n & ALL(c):ALL(d):[(x,0,c) e add & (x,0,d) e add => c=d] => 0 e p2
Split, 389
392 (x,0,z1) e add & (x,0,z2) e add
Premise
393 (x,0,z1) e add
Split, 392
394 (x,0,z2) e add
Split, 392
395 ALL(b):ALL(c):[(x,b,c) e add => x e n & b e n & c e n]
U Spec, 46
396 ALL(c):[(x,0,c) e add => x e n & 0 e n & c e n]
U Spec, 395
397 (x,0,z1) e add => x e n & 0 e n & z1 e n
U Spec, 396
398 x e n & 0 e n & z1 e n
Detach, 397, 393
399 x e n
Split, 398
400 0 e n
Split, 398
401 z1 e n
Split, 398
402 (x,0,z2) e add => x e n & 0 e n & z2 e n
U Spec, 396
403 x e n & 0 e n & z2 e n
Detach, 402, 394
404 x e n
Split, 403
405 0 e n
Split, 403
406 z2 e n
Split, 403
407 x e n => ALL(c):[c e n => [(x,0,c) e add => c=x]]
U Spec, 371
408 ALL(c):[c e n => [(x,0,c) e add => c=x]]
Detach, 407, 372
409 z1 e n => [(x,0,z1) e add => z1=x]
U Spec, 408
410 (x,0,z1) e add => z1=x
Detach, 409, 401
411 z1=x
Detach, 410, 393
412 z2 e n => [(x,0,z2) e add => z2=x]
U Spec, 408
413 (x,0,z2) e add => z2=x
Detach, 412, 406
414 z2=x
Detach, 413, 394
415 z1=z2
Substitute, 414,
411
416 ALL(c):ALL(d):[(x,0,c) e add & (x,0,d) e add => c=d]
4 Conclusion, 392
417 0 e n
&
ALL(c):ALL(d):[(x,0,c) e add & (x,0,d) e add => c=d]
Join, 2, 416
As Required:
418 0 e p2
Detach, 391, 417
Suppose... line
397
419 y e p2
Premise
420 y e p2 <=> y e n & ALL(c):ALL(d):[(x,y,c) e add & (x,y,d) e add => c=d]
U Spec, 376
421 [y e p2 => y e n &
ALL(c):ALL(d):[(x,y,c) e add & (x,y,d) e add => c=d]]
&
[y e n & ALL(c):ALL(d):[(x,y,c) e add & (x,y,d) e add => c=d] => y e p2]
Iff-And, 420
422 y e p2 => y e n &
ALL(c):ALL(d):[(x,y,c) e add & (x,y,d) e add => c=d]
Split, 421
423 y e n & ALL(c):ALL(d):[(x,y,c) e add & (x,y,d) e add => c=d] => y e p2
Split, 421
424 y e n & ALL(c):ALL(d):[(x,y,c) e add & (x,y,d) e add => c=d]
Detach, 422, 419
425 y e n
Split, 424
426 ALL(c):ALL(d):[(x,y,c) e add & (x,y,d) e add => c=d]
Split, 424
427 ALL(a2):[(x,a2) e n2 => EXIST(c):[c e n & (x,a2,c) e add]]
U Spec, 226
428 (x,y) e n2 =>
EXIST(c):[c e n & (x,y,c) e add]
U Spec, 427
429 ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]
U Spec, 14
430 (x,y) e n2 <=> x e n & y e n
U Spec, 429
431 [(x,y) e n2 => x e n & y e n]
&
[x e n & y e n => (x,y) e n2]
Iff-And, 430
432 (x,y) e n2 => x e n & y e n
Split, 431
433 x e n & y e n => (x,y) e n2
Split, 431
434 x e n & y e n
Join, 372, 425
435 (x,y) e n2
Detach, 433, 434
436 EXIST(c):[c e n & (x,y,c) e add]
Detach, 428, 435
437 z e n & (x,y,z) e add
E Spec, 436
Define: z
438 z e n
Split, 437
439 (x,y,z) e add
Split, 437
440 ALL(d):[(x,y,z) e add & (x,y,d) e add => z=d]
U Spec, 426
Suppose...
441 z' e n
Premise
Suppose the contrary...
442 ~[(x,s(y),z') e add => z'=s(z)]
Premise
443 ~~[(x,s(y),z') e add & ~z'=s(z)]
Imply-And, 442
444 (x,s(y),z') e add & ~z'=s(z)
Rem DNeg, 443
445 (x,s(y),z') e add
Split, 444
446 ~z'=s(z)
Split, 444
447 ALL(b):ALL(c):[(x,b,c) e add
<=>
(x,b,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,b,c) e d]]
U Spec, 28
448 ALL(c):[(x,s(y),c) e add
<=>
(x,s(y),c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,s(y),c) e d]]
U Spec, 447, 445
449 (x,s(y),z') e add
<=>
(x,s(y),z') e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,s(y),z') e d]
U Spec, 448
450 [(x,s(y),z') e add => (x,s(y),z') e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,s(y),z') e d]]
&
[(x,s(y),z') e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
& ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,s(y),z') e d] => (x,s(y),z') e add]
Iff-And, 449
451 (x,s(y),z') e add => (x,s(y),z') e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,s(y),z') e d]
Split, 450
452 (x,s(y),z') e n3 & ALL(d):[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,s(y),z') e d] => (x,s(y),z') e add
Split, 450
453 ~[(x,s(y),z') e n3 & ALL(d):[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,s(y),z') e d]] => ~(x,s(y),z') e add
Contra, 451
454 ~~[(x,s(y),z') e n3 => ~ALL(d):[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,s(y),z') e d]] => ~(x,s(y),z') e add
Imply-And, 453
455 (x,s(y),z') e n3 => ~ALL(d):[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,s(y),z') e d] => ~(x,s(y),z') e add
Rem DNeg, 454
456 (x,s(y),z') e n3 => ~~EXIST(d):~[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,s(y),z') e d] => ~(x,s(y),z') e add
Quant, 455
457 (x,s(y),z') e n3 => EXIST(d):~[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
=>
(x,s(y),z') e d] => ~(x,s(y),z') e add
Rem DNeg, 456
458 (x,s(y),z') e n3 => EXIST(d):~~[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d] & ~(x,s(y),z') e d] => ~(x,s(y),z') e add
Imply-And, 457
Sufficient: For ~(x,s(y),z')
e add (to obtain a
contradiction)
459 (x,s(y),z') e n3 => EXIST(d):[Set''(d) &
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d] & ~(x,s(y),z') e d] => ~(x,s(y),z') e add
Rem DNeg, 458
Suppose... (line 434)
460 (x,s(y),z') e n3
Premise
461 EXIST(sub):[Set''(sub) & ALL(a):ALL(b):ALL(c):[(a,b,c) e sub
<=>
(a,b,c) e add & ~[a=x & b=s(y) & c=z']]]
Subset, 27
462 Set''(q2) & ALL(a):ALL(b):ALL(c):[(a,b,c) e q2
<=>
(a,b,c) e add & ~[a=x & b=s(y) & c=z']]
E Spec, 461
Define: q2
463 Set''(q2)
Split, 462
464 ALL(a):ALL(b):ALL(c):[(a,b,c) e q2
<=>
(a,b,c) e add & ~[a=x & b=s(y) & c=z']]
Split, 462
465 (t,u,v) e q2
Premise
466 ALL(b):ALL(c):[(t,b,c) e q2
<=>
(t,b,c) e add & ~[t=x & b=s(y) & c=z']]
U Spec, 464
467 ALL(c):[(t,u,c) e q2
<=>
(t,u,c) e add & ~[t=x & u=s(y) & c=z']]
U Spec, 466
468 (t,u,v) e q2
<=>
(t,u,v) e add & ~[t=x & u=s(y) & v=z']
U Spec, 467
469 [(t,u,v) e q2 => (t,u,v) e add & ~[t=x & u=s(y) & v=z']]
&
[(t,u,v) e add & ~[t=x & u=s(y) & v=z'] => (t,u,v) e q2]
Iff-And, 468
470 (t,u,v) e q2 => (t,u,v) e add & ~[t=x & u=s(y) & v=z']
Split, 469
471 (t,u,v) e add & ~[t=x & u=s(y) & v=z'] => (t,u,v) e q2
Split, 469
472 (t,u,v) e add & ~[t=x & u=s(y) & v=z']
Detach, 470, 465
473 (t,u,v) e add
Split, 472
474 ~[t=x & u=s(y) & v=z']
Split, 472
475 ALL(b):ALL(c):[(t,b,c) e add => t e n & b e n & c e n]
U Spec, 46
476 ALL(c):[(t,u,c) e add => t e n & u e n & c e n]
U Spec, 475
477 (t,u,v) e add => t e n & u e n & v e n
U Spec, 476
478 t e n & u e n & v e n
Detach, 477, 473
As Required:
479 ALL(e):ALL(f):ALL(g):[(e,f,g) e q2 => e e n & f e n & g e n]
4 Conclusion, 465
Suppose...
480 t e n
Premise
481 ALL(b):ALL(c):[(t,b,c) e q2
<=>
(t,b,c) e add & ~[t=x & b=s(y) & c=z']]
U Spec, 464
482 ALL(c):[(t,0,c) e q2
<=>
(t,0,c) e add & ~[t=x & 0=s(y) & c=z']]
U Spec, 481
483 (t,0,t) e q2
<=>
(t,0,t) e add & ~[t=x & 0=s(y) & t=z']
U Spec, 482
484 [(t,0,t) e q2 => (t,0,t) e add & ~[t=x & 0=s(y) & t=z']]
&
[(t,0,t) e add & ~[t=x & 0=s(y) & t=z'] => (t,0,t) e q2]
Iff-And, 483
485 (t,0,t) e q2 => (t,0,t) e add & ~[t=x & 0=s(y) & t=z']
Split, 484
Sufficient: For (t,0,t)
e q2
486 (t,0,t) e add & ~[t=x & 0=s(y) & t=z'] => (t,0,t) e q2
Split, 484
487 t e n => (t,0,t) e add
U Spec, 73
488 (t,0,t) e add
Detach, 487, 480
Suppose to the contrary...
489 t=x & 0=s(y) & t=z'
Premise
490 t=x
Split, 489
491 0=s(y)
Split, 489
492 t=z'
Split, 489
493 y e n => ~s(y)=0
U Spec, 5
494 ~s(y)=0
Detach, 493, 425
495 s(y)=0
Sym, 491
496 s(y)=0 & ~s(y)=0
Join, 495, 494
497 ~[t=x & 0=s(y) & t=z']
4 Conclusion, 489
498 (t,0,t) e add & ~[t=x & 0=s(y) & t=z']
Join, 488, 497
499 (t,0,t) e q2
Detach, 486, 498
As Required:
500 ALL(e):[e e n => (e,0,e) e q2]
4 Conclusion, 480
Suppose... (line 476)
501 (t,u,v) e q2
Premise
502 ALL(b):ALL(c):[(t,b,c) e q2
<=>
(t,b,c) e add & ~[t=x & b=s(y) & c=z']]
U Spec, 464
503 ALL(c):[(t,u,c) e q2
<=>
(t,u,c) e add & ~[t=x & u=s(y) & c=z']]
U Spec, 502
504 (t,u,v) e q2
<=>
(t,u,v) e add & ~[t=x & u=s(y) & v=z']
U Spec, 503
505 [(t,u,v) e q2 => (t,u,v) e add & ~[t=x & u=s(y) & v=z']]
&
[(t,u,v) e add & ~[t=x & u=s(y) & v=z'] => (t,u,v) e q2]
Iff-And, 504
506 (t,u,v) e q2 => (t,u,v) e add & ~[t=x & u=s(y) & v=z']
Split, 505
507 (t,u,v) e add & ~[t=x & u=s(y) & v=z'] => (t,u,v) e q2
Split, 505
508 (t,u,v) e add & ~[t=x & u=s(y) & v=z']
Detach, 506, 501
509 (t,u,v) e add
Split, 508
510 ~[t=x & u=s(y) & v=z']
Split, 508
511 ALL(b):ALL(c):[(t,b,c) e add => t e n & b e n & c e n]
U Spec, 46
512 ALL(c):[(t,u,c) e add => t e n & u e n & c e n]
U Spec, 511
513 (t,u,v) e add => t e n & u e n & v e n
U Spec, 512
514 t e n & u e n & v e n
Detach, 513, 509
515 t e n
Split, 514
516 u e n
Split, 514
517 v e n
Split, 514
518 ALL(b):ALL(c):[(t,b,c) e q2
<=>
(t,b,c) e add & ~[t=x & b=s(y) & c=z']]
U Spec, 464
519 u e n => s(u) e n
U Spec, 3
520 s(u) e n
Detach, 519, 516
521 ALL(c):[(t,s(u),c) e q2
<=>
(t,s(u),c) e add & ~[t=x & s(u)=s(y) & c=z']]
U Spec, 518, 520
522 v e n => s(v) e n
U Spec, 3
523 s(v) e n
Detach, 522, 517
524 (t,s(u),s(v)) e q2
<=>
(t,s(u),s(v)) e add & ~[t=x & s(u)=s(y) & s(v)=z']
U Spec, 521, 523
525 [(t,s(u),s(v)) e q2 => (t,s(u),s(v)) e add & ~[t=x & s(u)=s(y) & s(v)=z']]
&
[(t,s(u),s(v)) e add & ~[t=x & s(u)=s(y) & s(v)=z'] => (t,s(u),s(v)) e q2]
Iff-And, 524
526 (t,s(u),s(v)) e q2 => (t,s(u),s(v)) e add & ~[t=x & s(u)=s(y) & s(v)=z']
Split, 525
Sufficient: For (t,s(u),s(v))
e q2
527 (t,s(u),s(v)) e add & ~[t=x & s(u)=s(y) & s(v)=z'] => (t,s(u),s(v)) e q2
Split, 525
528 ALL(b):ALL(c):[t e n & b e n & c e n
=>
[(t,b,c) e add => (t,s(b),s(c)) e add]]
U Spec, 122
529 ALL(c):[t e n & u e n & c e n
=>
[(t,u,c) e add => (t,s(u),s(c)) e add]]
U Spec, 528
530 t e n & u e n & v e n
=>
[(t,u,v) e add => (t,s(u),s(v)) e add]
U Spec, 529
531 (t,u,v) e add => (t,s(u),s(v)) e add
Detach, 530, 514
532 (t,s(u),s(v)) e add
Detach, 531, 509
Suppose to the contrary...
533 t=x & s(u)=s(y) & s(v)=z'
Premise
534 t=x
Split, 533
535 s(u)=s(y)
Split, 533
536 s(v)=z'
Split, 533
537 ALL(b):[u e n & b e n => [s(u)=s(b) => u=b]]
U Spec, 4
538 u e n & y e n => [s(u)=s(y) => u=y]
U Spec, 537
539 u e n & y e n
Join, 516, 425
540 s(u)=s(y) => u=y
Detach, 538, 539
541 u=y
Detach, 540, 535
542 (x,u,v) e add
Substitute, 534,
509
543 (x,y,v) e add
Substitute, 541,
542
544 (x,y,z) e add & (x,y,v) e add => z=v
U Spec, 440
545 (x,y,z) e add & (x,y,v) e add
Join, 439, 543
546 z=v
Detach, 544, 545
547 s(z)=z'
Substitute, 546,
536
548 z'=s(z)
Sym, 547
549 ~z'=s(z) & z'=s(z)
Join, 446, 548
As Required:
550 ~[t=x & s(u)=s(y) & s(v)=z']
4 Conclusion, 533
551 (t,s(u),s(v)) e add
&
~[t=x & s(u)=s(y) & s(v)=z']
Join, 532, 550
552 (t,s(u),s(v)) e q2
Detach, 527, 551
As Required:
553 ALL(e):ALL(f):ALL(g):[(e,f,g) e q2 => (e,s(f),s(g)) e q2]
4 Conclusion, 501
554 ALL(b):ALL(c):[(x,b,c) e q2
<=>
(x,b,c) e add & ~[x=x & b=s(y) & c=z']]
U Spec, 464
555 ALL(c):[(x,s(y),c) e q2
<=>
(x,s(y),c) e add & ~[x=x & s(y)=s(y) & c=z']]
U Spec, 554, 554
556 (x,s(y),z') e q2
<=>
(x,s(y),z') e add & ~[x=x & s(y)=s(y) & z'=z']
U Spec, 555
557 [(x,s(y),z') e q2 => (x,s(y),z') e add & ~[x=x & s(y)=s(y) & z'=z']]
&
[(x,s(y),z') e add & ~[x=x & s(y)=s(y) & z'=z'] => (x,s(y),z') e q2]
Iff-And, 556
558 (x,s(y),z') e q2 => (x,s(y),z') e add & ~[x=x & s(y)=s(y) & z'=z']
Split, 557
559 (x,s(y),z') e add & ~[x=x & s(y)=s(y) & z'=z'] => (x,s(y),z') e q2
Split, 557
560 ~[(x,s(y),z') e add & ~[x=x & s(y)=s(y) & z'=z']] => ~(x,s(y),z') e q2
Contra, 558
561 ~~[~(x,s(y),z') e add | ~~[x=x & s(y)=s(y) & z'=z']] => ~(x,s(y),z') e q2
DeMorgan, 560
562 ~(x,s(y),z') e add | ~~[x=x & s(y)=s(y) & z'=z'] => ~(x,s(y),z') e q2
Rem DNeg, 561
Sufficient: For ~(x,s(y),z')
e q2
563 ~(x,s(y),z') e add | x=x & s(y)=s(y) & z'=z' => ~(x,s(y),z') e q2
Rem DNeg, 562
564 x=x
Reflex
565 s(y)=s(y)
Reflex, 563
566 z'=z'
Reflex
567 x=x & s(y)=s(y)
Join, 564, 565
568 x=x & s(y)=s(y) & z'=z'
Join, 567, 566
569 ~(x,s(y),z') e add | x=x & s(y)=s(y) & z'=z'
Arb Or, 568
As Required:
570 ~(x,s(y),z') e q2
Detach, 563, 569
571 Set''(q2)
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e q2 => e e n & f e n & g e n]
Join, 463, 479
572 Set''(q2)
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e q2 => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e q2]
Join, 571, 500
573 Set''(q2)
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e q2 => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e q2]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e q2 => (e,s(f),s(g)) e q2]
Join, 572, 553
574 Set''(q2)
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e q2 => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e q2]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e q2 => (e,s(f),s(g)) e q2]
&
~(x,s(y),z') e q2
Join, 573, 570
575 EXIST(d):[Set''(d)
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
&
~(x,s(y),z') e d]
E Gen, 574
576 (x,s(y),z') e n3
=>
EXIST(d):[Set''(d)
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]
&
ALL(e):[e e n => (e,0,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,s(f),s(g)) e d]
&
~(x,s(y),z') e d]
4 Conclusion, 460
As Required:
577 ~(x,s(y),z') e add
Detach, 459, 576
578 (x,s(y),z') e add & ~(x,s(y),z') e add
Join, 445, 577
As Required:
579 ~~[(x,s(y),z') e add => z'=s(z)]
4 Conclusion, 442
580 (x,s(y),z') e add => z'=s(z)
Rem DNeg, 579
As Required: (line 558)
581 ALL(d):[d e n => [(x,s(y),d) e add => d=s(z)]]
4 Conclusion, 441
582 s(y) e p2 <=> s(y) e n & ALL(c):ALL(d):[(x,s(y),c) e add & (x,s(y),d) e add => c=d]
U Spec, 376, 581
583 [s(y) e p2 => s(y) e n &
ALL(c):ALL(d):[(x,s(y),c) e add & (x,s(y),d) e add => c=d]]
&
[s(y) e n & ALL(c):ALL(d):[(x,s(y),c) e add & (x,s(y),d) e add => c=d] => s(y) e p2]
Iff-And, 582
584 s(y) e p2 => s(y) e n &
ALL(c):ALL(d):[(x,s(y),c) e add & (x,s(y),d) e add => c=d]
Split, 583
Sufficient: For s(y) e p2
585 s(y) e n & ALL(c):ALL(d):[(x,s(y),c) e add & (x,s(y),d) e add => c=d] => s(y) e p2
Split, 583
586 y e n => s(y) e n
U Spec, 3
587 s(y) e n
Detach, 586, 425
Suppose...
588 (x,s(y),z1) e add & (x,s(y),z2) e add
Premise
589 (x,s(y),z1) e add
Split, 588
590 (x,s(y),z2) e add
Split, 588
591 ALL(b):ALL(c):[(x,b,c) e add => x e n & b e n & c e n]
U Spec, 46
592 ALL(c):[(x,s(y),c) e add => x e n & s(y) e n & c e n]
U Spec, 591, 590
593 (x,s(y),z1) e add => x e n & s(y) e n & z1 e n
U Spec, 592
594 x e n & s(y) e n & z1 e n
Detach, 593, 589
595 x e n
Split, 594
596 s(y) e n
Split, 594
597 z1 e n
Split, 594
598 (x,s(y),z2) e add => x e n & s(y) e n & z2 e n
U Spec, 592
599 x e n & s(y) e n & z2 e n
Detach, 598, 590
600 x e n
Split, 599
601 s(y) e n
Split, 599
602 z2 e n
Split, 599
603 z1 e n => [(x,s(y),z1) e add => z1=s(z)]
U Spec, 581
604 (x,s(y),z1) e add => z1=s(z)
Detach, 603, 597
605 z1=s(z)
Detach, 604, 589
606 z2 e n => [(x,s(y),z2) e add => z2=s(z)]
U Spec, 581
607 (x,s(y),z2) e add => z2=s(z)
Detach, 606, 602
608 z2=s(z)
Detach, 607, 590
609 z1=z2
Substitute, 608,
605
610 ALL(c):ALL(d):[(x,s(y),c) e add & (x,s(y),d) e add => c=d]
4 Conclusion, 588
611 s(y) e n
&
ALL(c):ALL(d):[(x,s(y),c) e add & (x,s(y),d) e add => c=d]
Join, 587, 610
612 s(y) e p2
Detach, 585, 611
613 ALL(b):[b e p2 => s(b) e p2]
4 Conclusion, 419
614 0 e p2 & ALL(b):[b e p2 => s(b) e p2]
Join, 418, 613
615 ALL(b):[b e n => b e p2]
Detach, 387, 614
616 y e n
Premise
617 y e n => y e p2
U Spec, 615
618 y e p2
Detach, 617, 616
619 y e p2 <=> y e n & ALL(c):ALL(d):[(x,y,c) e add & (x,y,d) e add => c=d]
U Spec, 376
620 [y e p2 => y e n &
ALL(c):ALL(d):[(x,y,c) e add & (x,y,d) e add => c=d]]
&
[y e n & ALL(c):ALL(d):[(x,y,c) e add & (x,y,d) e add => c=d] => y e p2]
Iff-And, 619
621 y e p2 => y e n &
ALL(c):ALL(d):[(x,y,c) e add & (x,y,d) e add => c=d]
Split, 620
622 y e n & ALL(c):ALL(d):[(x,y,c) e add & (x,y,d) e add => c=d] => y e p2
Split, 620
623 y e n & ALL(c):ALL(d):[(x,y,c) e add & (x,y,d) e add => c=d]
Detach, 621, 618
624 y e n
Split, 623
625 ALL(c):ALL(d):[(x,y,c) e add & (x,y,d) e add => c=d]
Split, 623
As Required:
626 ALL(b):[b e n
=>
ALL(c):ALL(d):[(x,b,c) e add & (x,b,d) e add => c=d]]
4 Conclusion, 616
As Required:
627 ALL(a):[a e n
=>
ALL(b):[b e n
=>
ALL(c):ALL(d):[(a,b,c) e add & (a,b,d) e add => c=d]]]
4 Conclusion, 372
Part 3
Prove: ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e n2 & b1 e n & b2 e n
=> [(a1,a2,b1) e add &
(a1,a2,b2) e add => b1=b2]]
Suppose...
628 (x,y) e n2 & z1 e n & z2 e n
Premise
629 (x,y) e n2
Split, 628
630 z1 e n
Split, 628
631 z2 e n
Split, 628
632 ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]
U Spec, 14
633 (x,y) e n2 <=> x e n & y e n
U Spec, 632
634 [(x,y) e n2 => x e n & y e n]
&
[x e n & y e n => (x,y) e n2]
Iff-And, 633
635 (x,y) e n2 => x e n & y e n
Split, 634
636 x e n & y e n => (x,y) e n2
Split, 634
637 x e n & y e n
Detach, 635, 629
638 x e n
Split, 637
639 y e n
Split, 637
640 x e n
=>
ALL(b):[b e n
=>
ALL(c):ALL(d):[(x,b,c) e add & (x,b,d) e add => c=d]]
U Spec, 627
641 ALL(b):[b e n
=>
ALL(c):ALL(d):[(x,b,c) e add & (x,b,d) e add => c=d]]
Detach, 640, 638
642 y e n
=>
ALL(c):ALL(d):[(x,y,c) e add & (x,y,d) e add => c=d]
U Spec, 641
643 ALL(c):ALL(d):[(x,y,c) e add & (x,y,d) e add => c=d]
Detach, 642, 639
644 ALL(d):[(x,y,z1) e add & (x,y,d) e add => z1=d]
U Spec, 643
645 (x,y,z1) e add & (x,y,z2) e add => z1=z2
U Spec, 644
Part 3
As Required:
646 ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e n2 & b1 e n & b2 e n
=>
[(a1,a2,b1) e add &
(a1,a2,b2) e add => b1=b2]]
4 Conclusion, 628
Apply new Function Axiom (for 2
variables)
647 ALL(dom):ALL(cod):ALL(gra):[Set'(dom) &
EXIST(a1):EXIST(a2):(a1,a2) e dom
&
Set(cod) & EXIST(a):a e cod & Set''(gra)
=>
[ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e gra =>
(a1,a2) e dom & b e cod]
&
ALL(a1):ALL(a2):[(a1,a2) e dom => EXIST(b):[b e cod & (a1,a2,b) e gra]]
&
ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e dom & b1 e cod & b2 e cod
=>
[(a1,a2,b1) e gra &
(a1,a2,b2) e gra => b1=b2]]
=>
EXIST(fun):ALL(a1):ALL(a2):ALL(b):[(a1,a2) e dom & b e cod
=>
[fun(a1,a2)=b <=> (a1,a2,b) e gra]]]]
Function
648 ALL(cod):ALL(gra):[Set'(n2) &
EXIST(a1):EXIST(a2):(a1,a2) e n2
&
Set(cod) & EXIST(a):a e cod & Set''(gra)
=>
[ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e gra =>
(a1,a2) e n2 & b e cod]
&
ALL(a1):ALL(a2):[(a1,a2) e n2 => EXIST(b):[b e cod & (a1,a2,b) e gra]]
&
ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e n2 & b1 e cod & b2 e cod
=>
[(a1,a2,b1) e gra &
(a1,a2,b2) e gra => b1=b2]]
=>
EXIST(fun):ALL(a1):ALL(a2):ALL(b):[(a1,a2) e n2 & b e cod
=>
[fun(a1,a2)=b <=> (a1,a2,b) e gra]]]]
U Spec, 647
649 ALL(gra):[Set'(n2) &
EXIST(a1):EXIST(a2):(a1,a2) e n2
&
Set(n) & EXIST(a):a e n &
Set''(gra)
=>
[ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e gra =>
(a1,a2) e n2 & b e n]
&
ALL(a1):ALL(a2):[(a1,a2) e n2 => EXIST(b):[b e n & (a1,a2,b) e gra]]
&
ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e n2 & b1 e n & b2 e n
=>
[(a1,a2,b1) e gra &
(a1,a2,b2) e gra => b1=b2]]
=>
EXIST(fun):ALL(a1):ALL(a2):ALL(b):[(a1,a2) e n2 & b e n
=>
[fun(a1,a2)=b <=> (a1,a2,b) e gra]]]]
U Spec, 648
The set of ordered triples
'add' is a GRAPH set mapping n2 to n
650 Set'(n2) & EXIST(a1):EXIST(a2):(a1,a2) e n2
&
Set(n) & EXIST(a):a e n & Set''(add)
=>
[ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e add => (a1,a2) e n2 & b e n]
&
ALL(a1):ALL(a2):[(a1,a2) e n2 => EXIST(b):[b e n & (a1,a2,b) e add]]
&
ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e n2 & b1 e n & b2 e n
=>
[(a1,a2,b1) e add &
(a1,a2,b2) e add => b1=b2]]
=>
EXIST(fun):ALL(a1):ALL(a2):ALL(b):[(a1,a2) e n2 & b e n
=>
[fun(a1,a2)=b <=> (a1,a2,b) e add]]]
U Spec, 649
Prove: EXIST(a1):EXIST(a2):(a1,a2)
e n2
Apply definition of n2
651 ALL(c2):[(0,c2) e n2 <=> 0 e n & c2 e n]
U Spec, 14
652 (0,0) e n2 <=> 0 e n & 0 e n
U Spec, 651
653 [(0,0) e n2 => 0 e n & 0 e n]
&
[0 e n & 0 e n => (0,0) e n2]
Iff-And, 652
654 0 e n & 0 e n => (0,0) e n2
Split, 653
655 0 e n & 0 e n
Join, 2, 2
656 (0,0) e n2
Detach, 654, 655
657 EXIST(a2):(0,a2) e n2
E Gen, 656
As Required:
658 EXIST(a1):EXIST(a2):(a1,a2) e n2
E Gen, 657
As Required:
659 EXIST(a):a e n
E Gen, 2
660 Set'(n2) & EXIST(a1):EXIST(a2):(a1,a2) e n2
Join, 13, 658
661 Set'(n2) & EXIST(a1):EXIST(a2):(a1,a2) e n2
&
Set(n)
Join, 660, 1
662 Set'(n2) & EXIST(a1):EXIST(a2):(a1,a2) e n2
&
Set(n)
&
EXIST(a):a e n
Join, 661, 659
663 Set'(n2) & EXIST(a1):EXIST(a2):(a1,a2) e n2
&
Set(n)
&
EXIST(a):a e n
&
Set''(add)
Join, 662, 27
664 ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e add => (a1,a2) e n2 & b e n]
&
ALL(a1):ALL(a2):[(a1,a2) e n2 => EXIST(b):[b e n & (a1,a2,b) e add]]
&
ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e n2 & b1 e n & b2 e n
=>
[(a1,a2,b1) e add &
(a1,a2,b2) e add => b1=b2]]
=>
EXIST(fun):ALL(a1):ALL(a2):ALL(b):[(a1,a2) e n2 & b e n
=>
[fun(a1,a2)=b <=> (a1,a2,b) e add]]
Detach, 650, 663
665 ALL(a):ALL(b):ALL(c):[(a,b,c) e add => (a,b) e n2 & c e n]
&
ALL(a1):ALL(a2):[(a1,a2) e n2 => EXIST(c):[c e n & (a1,a2,c) e add]]
Join, 141, 226
666 ALL(a):ALL(b):ALL(c):[(a,b,c) e add => (a,b) e n2 & c e n]
&
ALL(a1):ALL(a2):[(a1,a2) e n2 => EXIST(c):[c e n & (a1,a2,c) e add]]
&
ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e n2 & b1 e n & b2 e n
=>
[(a1,a2,b1) e add &
(a1,a2,b2) e add => b1=b2]]
Join, 665, 646
667 EXIST(fun):ALL(a1):ALL(a2):ALL(b):[(a1,a2) e n2 & b e n
=>
[fun(a1,a2)=b <=> (a1,a2,b) e add]]
Detach, 664, 666
There exists a function addf
mapping n2 to n
668 ALL(a1):ALL(a2):ALL(b):[(a1,a2) e n2 & b e n
=>
[addf(a1,a2)=b <=> (a1,a2,b) e add]]
E Spec, 667
Prove: ALL(a):ALL(b):[a e n & b e n =>
addf(a,b) e n]
Suppose...
669 t e n & u e n
Premise
670 ALL(a2):[(t,a2) e n2 => EXIST(c):[c e n & (t,a2,c) e add]]
U Spec, 226
671 (t,u) e n2 =>
EXIST(c):[c e n & (t,u,c) e add]
U Spec, 670
672 ALL(c2):[(t,c2) e n2 <=> t e n & c2 e n]
U Spec, 14
673 (t,u) e n2 <=> t e n & u e n
U Spec, 672
674 [(t,u) e n2 => t e n & u e n]
&
[t e n & u e n => (t,u) e n2]
Iff-And, 673
675 t e n & u e n => (t,u) e n2
Split, 674
676 (t,u) e n2
Detach, 675, 669
677 EXIST(c):[c e n & (t,u,c) e add]
Detach, 671, 676
678 v e n & (t,u,v) e add
E Spec, 677
679 v e n
Split, 678
680 (t,u,v) e add
Split, 678
681 ALL(a2):ALL(b):[(t,a2) e n2 & b e n
=>
[addf(t,a2)=b <=> (t,a2,b) e add]]
U Spec, 668
682 ALL(b):[(t,u) e n2 & b e n
=>
[addf(t,u)=b <=> (t,u,b) e add]]
U Spec, 681
683 (t,u) e n2 & v e n
=>
[addf(t,u)=v <=> (t,u,v) e add]
U Spec, 682
684 (t,u) e n2 & v e n
Join, 676, 679
685 addf(t,u)=v <=> (t,u,v) e add
Detach, 683, 684
686 [addf(t,u)=v => (t,u,v) e add]
&
[(t,u,v) e add => addf(t,u)=v]
Iff-And, 685
687 addf(t,u)=v => (t,u,v) e add
Split, 686
688 (t,u,v) e add => addf(t,u)=v
Split, 686
689 addf(t,u)=v
Detach, 688, 680
690 addf(t,u) e n
Substitute, 689,
679
As Required:
691 ALL(a):ALL(b):[a e n & b e n => addf(a,b) e n]
4 Conclusion, 669
Prove: ALL(a):[a e n => addf(a,0)=a]
Suppose...
692 t e n
Premise
693 ALL(a2):ALL(b):[(t,a2) e n2 & b e n
=>
[addf(t,a2)=b <=> (t,a2,b) e add]]
U Spec, 668
694 ALL(b):[(t,0) e n2 & b e n
=>
[addf(t,0)=b <=> (t,0,b) e add]]
U Spec, 693
695 (t,0) e n2 & t e n
=>
[addf(t,0)=t <=> (t,0,t) e add]
U Spec, 694
696 ALL(c2):[(t,c2) e n2 <=> t e n & c2 e n]
U Spec, 14
697 (t,0) e n2 <=> t e n & 0 e n
U Spec, 696
698 [(t,0) e n2 => t e n & 0 e n]
&
[t e n & 0 e n => (t,0) e n2]
Iff-And, 697
699 (t,0) e n2 => t e n & 0 e n
Split, 698
700 t e n & 0 e n => (t,0) e n2
Split, 698
701 t e n & 0 e n
Join, 692, 2
702 (t,0) e n2
Detach, 700, 701
703 (t,0) e n2 & t e n
Join, 702, 692
704 addf(t,0)=t <=> (t,0,t) e add
Detach, 695, 703
705 [addf(t,0)=t => (t,0,t) e add]
&
[(t,0,t) e add => addf(t,0)=t]
Iff-And, 704
706 addf(t,0)=t => (t,0,t) e add
Split, 705
Sufficient:
707 (t,0,t) e add => addf(t,0)=t
Split, 705
708 t e n => (t,0,t) e add
U Spec, 73
709 (t,0,t) e add
Detach, 708, 692
710 addf(t,0)=t
Detach, 707, 709
As Required:
711 ALL(a):[a e n => addf(a,0)=a]
4 Conclusion, 692
Prove: ALL(a):ALL(b):[a e n & b e n => addf(a,s(b))=s(addf(a,b))]
Suppose...
712 t e n & u e n
Premise
713 t e n
Split, 712
714 u e n
Split, 712
715 ALL(a2):[(t,a2) e n2 => EXIST(c):[c e n & (t,a2,c) e add]]
U Spec, 226
716 (t,u) e n2 =>
EXIST(c):[c e n & (t,u,c) e add]
U Spec, 715
717 ALL(c2):[(t,c2) e n2 <=> t e n & c2 e n]
U Spec, 14
718 (t,u) e n2 <=> t e n & u e n
U Spec, 717
719 [(t,u) e n2 => t e n & u e n]
&
[t e n & u e n => (t,u) e n2]
Iff-And, 718
720 t e n & u e n => (t,u) e n2
Split, 719
721 (t,u) e n2
Detach, 720, 712
722 EXIST(c):[c e n & (t,u,c) e add]
Detach, 716, 721
723 v e n & (t,u,v) e add
E Spec, 722
724 v e n
Split, 723
725 (t,u,v) e add
Split, 723
726 ALL(a2):ALL(b):[(t,a2) e n2 & b e n
=>
[addf(t,a2)=b <=> (t,a2,b) e add]]
U Spec, 668
727 ALL(b):[(t,u) e n2 & b e n
=>
[addf(t,u)=b <=> (t,u,b) e add]]
U Spec, 726
728 (t,u) e n2 & v e n
=>
[addf(t,u)=v <=> (t,u,v) e add]
U Spec, 727
729 (t,u) e n2 & v e n
Join, 721, 724
730 addf(t,u)=v <=> (t,u,v) e add
Detach, 728, 729
731 [addf(t,u)=v => (t,u,v) e add]
&
[(t,u,v) e add => addf(t,u)=v]
Iff-And, 730
732 (t,u,v) e add => addf(t,u)=v
Split, 731
733 addf(t,u)=v
Detach, 732, 725
734 ALL(b):ALL(c):[t e n & b e n & c e n
=>
[(t,b,c) e add => (t,s(b),s(c)) e add]]
U Spec, 122
735 ALL(c):[t e n & u e n & c e n
=>
[(t,u,c) e add => (t,s(u),s(c)) e add]]
U Spec, 734
736 t e n & u e n & v e n
=>
[(t,u,v) e add => (t,s(u),s(v)) e add]
U Spec, 735
737 t e n & u e n & v e n
Join, 712, 724
738 (t,u,v) e add => (t,s(u),s(v)) e add
Detach, 736, 737
739 (t,s(u),s(v)) e add
Detach, 738, 725
740 u e n => s(u) e n
U Spec, 3
741 s(u) e n
Detach, 740, 714
742 v e n => s(v) e n
U Spec, 3
743 s(v) e n
Detach, 742, 724
744 ALL(a2):ALL(b):[(t,a2) e n2 & b e n
=>
[addf(t,a2)=b <=> (t,a2,b) e add]]
U Spec, 668
745 ALL(b):[(t,s(u)) e n2 & b e n
=>
[addf(t,s(u))=b <=> (t,s(u),b) e add]]
U Spec, 744, 741
Sufficient: For addf(t,s(u))=s(v)
<=> (t,s(u),s(v)) e add
746 (t,s(u)) e n2 & s(v) e n
=>
[addf(t,s(u))=s(v) <=> (t,s(u),s(v)) e add]
U Spec, 745, 743
747 ALL(c2):[(t,c2) e n2 <=> t e n & c2 e n]
U Spec, 14
748 (t,s(u)) e n2 <=> t e n & s(u) e n
U Spec, 747, 741
749 [(t,s(u)) e n2 => t e n & s(u) e n]
&
[t e n & s(u) e n => (t,s(u)) e n2]
Iff-And, 748
750 t e n & s(u) e n => (t,s(u)) e n2
Split, 749
751 t e n & s(u) e n
Join, 713, 741
752 (t,s(u)) e n2
Detach, 750, 751
753 (t,s(u)) e n2 & s(v) e n
Join, 752, 743
754 addf(t,s(u))=s(v) <=> (t,s(u),s(v)) e add
Detach, 746, 753
755 [addf(t,s(u))=s(v) => (t,s(u),s(v)) e add]
&
[(t,s(u),s(v)) e add => addf(t,s(u))=s(v)]
Iff-And, 754
756 (t,s(u),s(v)) e add => addf(t,s(u))=s(v)
Split, 755
757 addf(t,s(u))=s(v)
Detach, 756, 739
758 addf(t,s(u))=s(addf(t,u))
Substitute, 733,
757
As Required:
759 ALL(a):ALL(b):[a e n & b e n => addf(a,s(b))=s(addf(a,b))]
4 Conclusion, 712
760 ALL(a):ALL(b):[a e n & b e n => addf(a,b) e n]
&
ALL(a):[a e n => addf(a,0)=a]
Join, 691, 711
761 ALL(a):ALL(b):[a e n & b e n => addf(a,b) e n]
&
ALL(a):[a e n => addf(a,0)=a]
&
ALL(a):ALL(b):[a e n & b e n => addf(a,s(b))=s(addf(a,b))]
Join, 760, 759
As Required:
762 EXIST(add):[ALL(a):ALL(b):[a e n & b e n => add(a,b) e n]
&
ALL(a):[a e n => add(a,0)=a]
&
ALL(a):ALL(b):[a e n & b e n => add(a,s(b))=s(add(a,b))]]
E Gen, 761