THEOREM
*******
EXIST(subt):ALL(a):ALL(b):[a e n & b e n => [b<=a => subt(a,b) e n & a=b+subt(a,b)]]
where subt
is a partial function (subtraction) on the set of natural numbers.
This machine-verified formal
proof was written with the aid of the author's DC Proof 2.0 software available
at http://www.dcproof.com
REQUIRED AXIOMS
***************
Proposed Axiom for Partial
Functions where:
func = function
dom = domain of function
cod = codomain of function
1 ALL(func):ALL(a1):ALL(a2):ALL(dom):ALL(cod):[Set''(func) &
Set(a1) & Set(a2) & Set'(dom) & Set(cod)
=>
[ALL(b1):ALL(b2):[(b1,b2) e dom => b1 e a1 & b2 e a2]
&
ALL(b1):ALL(b2):ALL(c):[(b1,b2,c) e func => (b1,b2) e dom & c e cod]
&
ALL(b1):ALL(b2):[(b1,b2) e dom => EXIST(c):[c e cod &
(b1,b2,c) e func]]
&
ALL(b1):ALL(b2):ALL(c1):ALL(c2):[(b1,b2,c1) e func &
(b1,b2,c2) e func => c1=c2]
=>
ALL(b1):ALL(b2):ALL(c):[(b1,b2) e dom & c e cod => [func(b1,b2)=c <=>
(b1,b2,c) e func]]]]
Axiom
Properties of addition and
<= on n
2 Set(n)
Axiom
Define: + on n
3 ALL(a):ALL(b):[a e n & b e n => a+b e n]
Axiom
Define: <= on n
4 ALL(a):ALL(b):[a e n & b e n => [a<=b <=> EXIST(c):[c e n & a+c=b]]]
Axiom
Left cancelability of + on n
5 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => [a+b=a+c => b=c]]
Axiom
PROOF
*****
Construct Cartesian product n2
Apply Cartesian Product Axiom
6 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
7 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, 6
8 Set(n) & Set(n) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e n & c2 e n]]
U Spec, 7
9 Set(n) & Set(n)
Join, 2, 2
10 EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e n & c2 e n]]
Detach, 8, 9
11 Set'(n2) & ALL(c1):ALL(c2):[(c1,c2) e n2 <=> c1 e n & c2 e n]
E Spec, 10
Define: n2 (Order pairs of n)
12 Set'(n2)
Split, 11
13 ALL(c1):ALL(c2):[(c1,c2) e n2 <=> c1 e n & c2 e n]
Split, 11
Construct domain of function
14 EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) e sub <=> (a,b) e n2 & b<=a]]
Subset, 12
15 Set'(dom) & ALL(a):ALL(b):[(a,b) e dom <=> (a,b) e n2 & b<=a]
E Spec, 14
Define: dom
(The domain of the subtraction function)
16 Set'(dom)
Split, 15
17 ALL(a):ALL(b):[(a,b) e dom <=> (a,b) e n2 & b<=a]
Split, 15
Construct Cartesian product n3
Apply Cartesian Product Axiom
18 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
19 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, 18
20 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, 19
21 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, 20
22 Set(n) & Set(n) & Set(n)
Join, 9, 2
23 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, 21, 22
24 Set''(n3) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e n3 <=> c1 e n & c2 e n & c3 e n]
E Spec, 23
Define: n3 (Ordered triples of n)
25 Set''(n3)
Split, 24
26 ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e n3 <=> c1 e n & c2 e n & c3 e n]
Split, 24
Construct subt (Subset of n3)
Apply Subset Axiom
27 EXIST(sub):[Set''(sub) & ALL(a):ALL(b):ALL(c):[(a,b,c) e sub
<=>
(a,b,c) e n3 & [(a,b) e dom & a=b+c]]]
Subset, 25
28 Set''(subt) & ALL(a):ALL(b):ALL(c):[(a,b,c) e subt
<=>
(a,b,c) e n3 & [(a,b) e dom & a=b+c]]
E Spec, 27
Define: subt
29 Set''(subt)
Split, 28
30 ALL(a):ALL(b):ALL(c):[(a,b,c) e subt
<=>
(a,b,c) e n3 & [(a,b) e dom & a=b+c]]
Split, 28
Apply Partial Function Axiom
31 ALL(a1):ALL(a2):ALL(dom):ALL(cod):[Set''(subt) & Set(a1) & Set(a2) & Set'(dom) & Set(cod)
=>
[ALL(b1):ALL(b2):[(b1,b2) e dom => b1 e a1 & b2 e a2]
&
ALL(b1):ALL(b2):ALL(c):[(b1,b2,c) e subt => (b1,b2) e dom & c e cod]
&
ALL(b1):ALL(b2):[(b1,b2) e dom => EXIST(c):[c e cod &
(b1,b2,c) e subt]]
&
ALL(b1):ALL(b2):ALL(c1):ALL(c2):[(b1,b2,c1) e subt &
(b1,b2,c2) e subt => c1=c2]
=>
ALL(b1):ALL(b2):ALL(c):[(b1,b2) e dom & c e cod => [subt(b1,b2)=c
<=> (b1,b2,c) e subt]]]]
U Spec, 1
32 ALL(a2):ALL(dom):ALL(cod):[Set''(subt) & Set(n) & Set(a2) & Set'(dom) & Set(cod)
=>
[ALL(b1):ALL(b2):[(b1,b2) e dom => b1 e n & b2 e a2]
&
ALL(b1):ALL(b2):ALL(c):[(b1,b2,c) e subt => (b1,b2) e dom & c e cod]
&
ALL(b1):ALL(b2):[(b1,b2) e dom => EXIST(c):[c e cod &
(b1,b2,c) e subt]]
&
ALL(b1):ALL(b2):ALL(c1):ALL(c2):[(b1,b2,c1) e subt &
(b1,b2,c2) e subt => c1=c2]
=>
ALL(b1):ALL(b2):ALL(c):[(b1,b2) e dom & c e cod => [subt(b1,b2)=c
<=> (b1,b2,c) e subt]]]]
U Spec, 31
33 ALL(dom):ALL(cod):[Set''(subt) & Set(n) & Set(n) & Set'(dom) & Set(cod)
=>
[ALL(b1):ALL(b2):[(b1,b2) e dom => b1 e n & b2 e n]
&
ALL(b1):ALL(b2):ALL(c):[(b1,b2,c) e subt => (b1,b2) e dom & c e cod]
&
ALL(b1):ALL(b2):[(b1,b2) e dom => EXIST(c):[c e cod &
(b1,b2,c) e subt]]
&
ALL(b1):ALL(b2):ALL(c1):ALL(c2):[(b1,b2,c1) e subt &
(b1,b2,c2) e subt => c1=c2]
=>
ALL(b1):ALL(b2):ALL(c):[(b1,b2) e dom & c e cod => [subt(b1,b2)=c
<=> (b1,b2,c) e subt]]]]
U Spec, 32
34 ALL(cod):[Set''(subt) & Set(n) & Set(n) & Set'(dom) & Set(cod)
=>
[ALL(b1):ALL(b2):[(b1,b2) e dom => b1 e n & b2 e n]
&
ALL(b1):ALL(b2):ALL(c):[(b1,b2,c) e subt => (b1,b2) e dom & c e cod]
&
ALL(b1):ALL(b2):[(b1,b2) e dom => EXIST(c):[c e cod &
(b1,b2,c) e subt]]
&
ALL(b1):ALL(b2):ALL(c1):ALL(c2):[(b1,b2,c1) e subt &
(b1,b2,c2) e subt => c1=c2]
=>
ALL(b1):ALL(b2):ALL(c):[(b1,b2) e dom & c e cod => [subt(b1,b2)=c
<=> (b1,b2,c) e subt]]]]
U Spec, 33
35 Set''(subt) & Set(n) & Set(n) & Set'(dom) & Set(n)
=>
[ALL(b1):ALL(b2):[(b1,b2) e dom => b1 e n & b2 e n]
&
ALL(b1):ALL(b2):ALL(c):[(b1,b2,c) e subt => (b1,b2) e dom & c e n]
&
ALL(b1):ALL(b2):[(b1,b2) e dom => EXIST(c):[c e n & (b1,b2,c) e subt]]
&
ALL(b1):ALL(b2):ALL(c1):ALL(c2):[(b1,b2,c1) e subt &
(b1,b2,c2) e subt => c1=c2]
=>
ALL(b1):ALL(b2):ALL(c):[(b1,b2) e dom & c e n => [subt(b1,b2)=c
<=> (b1,b2,c) e subt]]]
U Spec, 34
36 Set''(subt) & Set(n)
Join, 29, 2
37 Set''(subt) & Set(n) & Set(n)
Join, 36, 2
38 Set''(subt) & Set(n) & Set(n) & Set'(dom)
Join, 37, 16
39 Set''(subt) & Set(n) & Set(n) & Set'(dom)
&
Set(n)
Join, 38, 2
Sufficient: For functionality
of subt
40 ALL(b1):ALL(b2):[(b1,b2) e dom => b1 e n & b2 e n]
&
ALL(b1):ALL(b2):ALL(c):[(b1,b2,c) e subt => (b1,b2) e dom & c e n]
&
ALL(b1):ALL(b2):[(b1,b2) e dom => EXIST(c):[c e n & (b1,b2,c) e subt]]
&
ALL(b1):ALL(b2):ALL(c1):ALL(c2):[(b1,b2,c1) e subt &
(b1,b2,c2) e subt => c1=c2]
=>
ALL(b1):ALL(b2):ALL(c):[(b1,b2) e dom & c e n => [subt(b1,b2)=c
<=> (b1,b2,c) e subt]]
Detach, 35, 39
Part 1
Prove: ALL(b1):ALL(b2):[(b1,b2) e dom => b1 e n & b2 e n]
Suppose...
41 (x,y) e dom
Premise
42 ALL(b):[(x,b) e dom <=> (x,b) e n2 & b<=x]
U Spec, 17
43 (x,y) e dom <=> (x,y) e n2 & y<=x
U Spec, 42
44 [(x,y) e dom => (x,y) e n2 & y<=x]
&
[(x,y) e n2 & y<=x => (x,y) e dom]
Iff-And, 43
45 (x,y) e dom => (x,y) e n2 & y<=x
Split, 44
46 (x,y) e n2 & y<=x => (x,y) e dom
Split, 44
47 (x,y) e n2 & y<=x
Detach, 45, 41
48 (x,y) e n2
Split, 47
49 y<=x
Split, 47
50 ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]
U Spec, 13
51 (x,y) e n2 <=> x e n & y e n
U Spec, 50
52 [(x,y) e n2 => x e n & y e n]
&
[x e n & y e n => (x,y) e n2]
Iff-And, 51
53 (x,y) e n2 => x e n & y e n
Split, 52
54 x e n & y e n => (x,y) e n2
Split, 52
55 x e n & y e n
Detach, 53, 48
Part 1
56 ALL(b1):ALL(b2):[(b1,b2) e dom => b1 e n & b2 e n]
4 Conclusion, 41
Part 2
Prove: ALL(b1):ALL(b2):ALL(c):[(b1,b2,c)
e subt => (b1,b2) e dom & c e n]
Suppose...
57 (x,y,z) e subt
Premise
58 ALL(b):ALL(c):[(x,b,c) e subt
<=>
(x,b,c) e n3 & [(x,b) e dom & x=b+c]]
U Spec, 30
59 ALL(c):[(x,y,c) e subt
<=>
(x,y,c) e n3 & [(x,y) e dom & x=y+c]]
U Spec, 58
60 (x,y,z) e subt
<=>
(x,y,z) e n3 & [(x,y) e dom & x=y+z]
U Spec, 59
61 [(x,y,z) e subt => (x,y,z) e n3 & [(x,y) e dom & x=y+z]]
&
[(x,y,z) e n3 & [(x,y) e dom & x=y+z] => (x,y,z) e subt]
Iff-And, 60
62 (x,y,z) e subt => (x,y,z) e n3 & [(x,y) e dom & x=y+z]
Split, 61
63 (x,y,z) e n3 & [(x,y) e dom & x=y+z] => (x,y,z) e subt
Split, 61
64 (x,y,z) e n3 & [(x,y) e dom & x=y+z]
Detach, 62, 57
65 (x,y,z) e n3
Split, 64
66 (x,y) e dom & x=y+z
Split, 64
67 (x,y) e dom
Split, 66
68 x=y+z
Split, 66
69 ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]
U Spec, 26
70 ALL(c3):[(x,y,c3) e n3 <=> x e n & y e n & c3 e n]
U Spec, 69
71 (x,y,z) e n3 <=> x e n & y e n & z e n
U Spec, 70
72 [(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, 71
73 (x,y,z) e n3 => x e n & y e n & z e n
Split, 72
74 x e n & y e n & z e n => (x,y,z) e n3
Split, 72
75 x e n & y e n & z e n
Detach, 73, 65
76 x e n
Split, 75
77 y e n
Split, 75
78 z e n
Split, 75
79 (x,y) e dom & z e n
Join, 67, 78
Part 2
80 ALL(b1):ALL(b2):ALL(c):[(b1,b2,c) e subt => (b1,b2) e dom & c e n]
4 Conclusion, 57
Part 3
Prove: ALL(b1):ALL(b2):[(b1,b2) e dom => EXIST(c):[c e n & (b1,b2,c) e subt]]
Suppose...
81 (x,y) e dom
Premise
82 ALL(b):[(x,b) e dom <=> (x,b) e n2 & b<=x]
U Spec, 17
83 (x,y) e dom <=> (x,y) e n2 & y<=x
U Spec, 82
84 [(x,y) e dom => (x,y) e n2 & y<=x]
&
[(x,y) e n2 & y<=x => (x,y) e dom]
Iff-And, 83
85 (x,y) e dom => (x,y) e n2 & y<=x
Split, 84
86 (x,y) e n2 & y<=x => (x,y) e dom
Split, 84
87 (x,y) e n2 & y<=x
Detach, 85, 81
88 (x,y) e n2
Split, 87
89 y<=x
Split, 87
90 ALL(b):[y e n & b e n => [y<=b <=> EXIST(c):[c e n & y+c=b]]]
U Spec, 4
91 y e n & x e n => [y<=x <=>
EXIST(c):[c e n & y+c=x]]
U Spec, 90
92 ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]
U Spec, 13
93 (x,y) e n2 <=> x e n & y e n
U Spec, 92
94 [(x,y) e n2 => x e n & y e n]
&
[x e n & y e n => (x,y) e n2]
Iff-And, 93
95 (x,y) e n2 => x e n & y e n
Split, 94
96 x e n & y e n => (x,y) e n2
Split, 94
97 x e n & y e n
Detach, 95, 88
98 x e n
Split, 97
99 y e n
Split, 97
100 ALL(b):[y e n & b e n => [y<=b <=> EXIST(c):[c e n & y+c=b]]]
U Spec, 4
101 y e n & x e n => [y<=x <=>
EXIST(c):[c e n & y+c=x]]
U Spec, 100
102 y e n & x e n
Join, 99, 98
103 y<=x <=> EXIST(c):[c e n & y+c=x]
Detach, 101, 102
104 [y<=x => EXIST(c):[c e n & y+c=x]]
&
[EXIST(c):[c e n & y+c=x] => y<=x]
Iff-And, 103
105 y<=x => EXIST(c):[c e n & y+c=x]
Split, 104
106 EXIST(c):[c e n & y+c=x] => y<=x
Split, 104
107 EXIST(c):[c e n & y+c=x]
Detach, 105, 89
108 z e n & y+z=x
E Spec, 107
109 z e n
Split, 108
110 y+z=x
Split, 108
111 ALL(b):ALL(c):[(x,b,c) e subt
<=>
(x,b,c) e n3 & [(x,b) e dom & x=b+c]]
U Spec, 30
112 ALL(c):[(x,y,c) e subt
<=>
(x,y,c) e n3 & [(x,y) e dom & x=y+c]]
U Spec, 111
113 (x,y,z) e subt
<=>
(x,y,z) e n3 & [(x,y) e dom & x=y+z]
U Spec, 112
114 [(x,y,z) e subt => (x,y,z) e n3 & [(x,y) e dom & x=y+z]]
&
[(x,y,z) e n3 & [(x,y) e dom & x=y+z] => (x,y,z) e subt]
Iff-And, 113
115 (x,y,z) e subt => (x,y,z) e n3 & [(x,y) e dom & x=y+z]
Split, 114
116 (x,y,z) e n3 & [(x,y) e dom & x=y+z] => (x,y,z) e subt
Split, 114
117 ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]
U Spec, 26
118 ALL(c3):[(x,y,c3) e n3 <=> x e n & y e n & c3 e n]
U Spec, 117
119 (x,y,z) e n3 <=> x e n & y e n & z e n
U Spec, 118
120 [(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, 119
121 (x,y,z) e n3 => x e n & y e n & z e n
Split, 120
122 x e n & y e n & z e n => (x,y,z) e n3
Split, 120
123 x e n & y e n
Join, 98, 99
124 x e n & y e n & z e n
Join, 123, 109
125 (x,y,z) e n3
Detach, 122, 124
126 x=y+z
Sym, 110
127 (x,y) e dom & x=y+z
Join, 81, 126
128 (x,y,z) e n3 & [(x,y) e dom & x=y+z]
Join, 125, 127
129 (x,y,z) e subt
Detach, 116, 128
130 z e n & (x,y,z) e subt
Join, 109, 129
Part 3
131 ALL(b1):ALL(b2):[(b1,b2) e dom =>
EXIST(c):[c e n & (b1,b2,c) e subt]]
4 Conclusion, 81
Part 4
Prove: ALL(b1):ALL(b2):ALL(c1):ALL(c2):[(b1,b2,c1)
e subt & (b1,b2,c2) e subt => c1=c2]
Suppose...
132 (x,y,z1) e subt & (x,y,z2) e subt
Premise
133 (x,y,z1) e subt
Split, 132
134 (x,y,z2) e subt
Split, 132
135 ALL(b):ALL(c):[(x,b,c) e subt
<=>
(x,b,c) e n3 & [(x,b) e dom & x=b+c]]
U Spec, 30
136 ALL(c):[(x,y,c) e subt
<=>
(x,y,c) e n3 & [(x,y) e dom & x=y+c]]
U Spec, 135
137 (x,y,z1) e subt
<=>
(x,y,z1) e n3 & [(x,y) e dom & x=y+z1]
U Spec, 136
138 [(x,y,z1) e subt => (x,y,z1) e n3 & [(x,y) e dom & x=y+z1]]
&
[(x,y,z1) e n3 & [(x,y) e dom & x=y+z1] => (x,y,z1) e subt]
Iff-And, 137
139 (x,y,z1) e subt => (x,y,z1) e n3 & [(x,y) e dom & x=y+z1]
Split, 138
140 (x,y,z1) e n3 & [(x,y) e dom & x=y+z1] => (x,y,z1) e subt
Split, 138
141 (x,y,z1) e n3 & [(x,y) e dom & x=y+z1]
Detach, 139, 133
142 (x,y,z1) e n3
Split, 141
143 (x,y) e dom & x=y+z1
Split, 141
144 (x,y) e dom
Split, 143
145 x=y+z1
Split, 143
146 (x,y,z2) e subt
<=>
(x,y,z2) e n3 & [(x,y) e dom & x=y+z2]
U Spec, 136
147 [(x,y,z2) e subt => (x,y,z2) e n3 & [(x,y) e dom & x=y+z2]]
&
[(x,y,z2) e n3 & [(x,y) e dom & x=y+z2] => (x,y,z2) e subt]
Iff-And, 146
148 (x,y,z2) e subt => (x,y,z2) e n3 & [(x,y) e dom & x=y+z2]
Split, 147
149 (x,y,z2) e n3 & [(x,y) e dom & x=y+z2] => (x,y,z2) e subt
Split, 147
150 (x,y,z2) e n3 & [(x,y) e dom & x=y+z2]
Detach, 148, 134
151 (x,y,z2) e n3
Split, 150
152 (x,y) e dom & x=y+z2
Split, 150
153 (x,y) e dom
Split, 152
154 x=y+z2
Split, 152
155 y+z1=y+z2
Substitute, 145,
154
156 ALL(b):ALL(c):[y e n & b e n & c e n => [y+b=y+c => b=c]]
U Spec, 5
157 ALL(c):[y e n & z1 e n & c e n => [y+z1=y+c => z1=c]]
U Spec, 156
158 y e n & z1 e n & z2 e n => [y+z1=y+z2 => z1=z2]
U Spec, 157
159 ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]
U Spec, 26
160 ALL(c3):[(x,y,c3) e n3 <=> x e n & y e n & c3 e n]
U Spec, 159
161 (x,y,z1) e n3 <=> x e n & y e n & z1 e n
U Spec, 160
162 [(x,y,z1) e n3 => x e n & y e n & z1 e n]
&
[x e n & y e n & z1 e n => (x,y,z1) e n3]
Iff-And, 161
163 (x,y,z1) e n3 => x e n & y e n & z1 e n
Split, 162
164 x e n & y e n & z1 e n => (x,y,z1) e n3
Split, 162
165 x e n & y e n & z1 e n
Detach, 163, 142
166 x e n
Split, 165
167 y e n
Split, 165
168 z1 e n
Split, 165
169 (x,y,z2) e n3 <=> x e n & y e n & z2 e n
U Spec, 160
170 [(x,y,z2) e n3 => x e n & y e n & z2 e n]
&
[x e n & y e n & z2 e n => (x,y,z2) e n3]
Iff-And, 169
171 (x,y,z2) e n3 => x e n & y e n & z2 e n
Split, 170
172 x e n & y e n & z2 e n => (x,y,z2) e n3
Split, 170
173 x e n & y e n & z2 e n
Detach, 171, 151
174 x e n
Split, 173
175 y e n
Split, 173
176 z2 e n
Split, 173
177 y e n & z1 e n
Join, 167, 168
178 y e n & z1 e n & z2 e n
Join, 177, 176
179 y+z1=y+z2 => z1=z2
Detach, 158, 178
180 z1=z2
Detach, 179, 155
Part 4
181 ALL(b1):ALL(b2):ALL(c1):ALL(c2):[(b1,b2,c1) e subt &
(b1,b2,c2) e subt => c1=c2]
4 Conclusion, 132
182 ALL(b1):ALL(b2):[(b1,b2) e dom => b1 e n & b2 e n]
&
ALL(b1):ALL(b2):ALL(c):[(b1,b2,c) e subt => (b1,b2) e dom & c e n]
Join, 56, 80
183 ALL(b1):ALL(b2):[(b1,b2) e dom => b1 e n & b2 e n]
&
ALL(b1):ALL(b2):ALL(c):[(b1,b2,c) e subt => (b1,b2) e dom & c e n]
&
ALL(b1):ALL(b2):[(b1,b2) e dom => EXIST(c):[c e n & (b1,b2,c) e subt]]
Join, 182, 131
184 ALL(b1):ALL(b2):[(b1,b2) e dom => b1 e n & b2 e n]
&
ALL(b1):ALL(b2):ALL(c):[(b1,b2,c) e subt => (b1,b2) e dom & c e n]
&
ALL(b1):ALL(b2):[(b1,b2) e dom => EXIST(c):[c e n & (b1,b2,c) e subt]]
&
ALL(b1):ALL(b2):ALL(c1):ALL(c2):[(b1,b2,c1) e subt & (b1,b2,c2) e subt => c1=c2]
Join, 183, 181
As Required: subt is a function
185 ALL(b1):ALL(b2):ALL(c):[(b1,b2) e dom & c e n => [subt(b1,b2)=c
<=> (b1,b2,c) e subt]]
Detach, 40, 184
Prove: ALL(a):ALL(b):[(a,b) e dom => subt(a,b) e n]
Suppose...
186 (x,y) e dom
Premise
187 ALL(b2):[(x,b2) e dom =>
EXIST(c):[c e n & (x,b2,c) e subt]]
U Spec, 131
188 (x,y) e dom =>
EXIST(c):[c e n & (x,y,c) e subt]
U Spec, 187
189 EXIST(c):[c e n & (x,y,c) e subt]
Detach, 188, 186
190 z e n & (x,y,z) e subt
E Spec, 189
191 z e n
Split, 190
192 (x,y,z) e subt
Split, 190
193 ALL(b2):ALL(c):[(x,b2) e dom & c e n => [subt(x,b2)=c <=>
(x,b2,c) e subt]]
U Spec, 185
194 ALL(c):[(x,y) e dom & c e n => [subt(x,y)=c <=> (x,y,c) e subt]]
U Spec, 193
195 (x,y) e dom & z e n => [subt(x,y)=z <=> (x,y,z) e subt]
U Spec, 194
196 (x,y) e dom & z e n
Join, 186, 191
197 subt(x,y)=z <=> (x,y,z) e subt
Detach, 195, 196
198 [subt(x,y)=z => (x,y,z) e subt]
&
[(x,y,z) e subt => subt(x,y)=z]
Iff-And, 197
199 subt(x,y)=z => (x,y,z) e subt
Split, 198
200 (x,y,z) e subt => subt(x,y)=z
Split, 198
201 subt(x,y)=z
Detach, 200, 192
202 subt(x,y) e n
Substitute, 201,
191
As Required:
203 ALL(a):ALL(b):[(a,b) e dom => subt(a,b) e n]
4 Conclusion, 186
Prove: ALL(a):ALL(b):[(a,b) e dom =>
a=b+subt(a,b)]
Suppose...
204 (x,y) e dom
Premise
205 ALL(b2):[(x,b2) e dom =>
EXIST(c):[c e n & (x,b2,c) e subt]]
U Spec, 131
206 (x,y) e dom =>
EXIST(c):[c e n & (x,y,c) e subt]
U Spec, 205
207 EXIST(c):[c e n & (x,y,c) e subt]
Detach, 206, 204
208 z e n & (x,y,z) e subt
E Spec, 207
209 z e n
Split, 208
210 (x,y,z) e subt
Split, 208
211 ALL(b2):ALL(c):[(x,b2) e dom & c e n => [subt(x,b2)=c <=>
(x,b2,c) e subt]]
U Spec, 185
212 ALL(c):[(x,y) e dom & c e n => [subt(x,y)=c <=> (x,y,c) e subt]]
U Spec, 211
213 (x,y) e dom & z e n => [subt(x,y)=z <=> (x,y,z) e subt]
U Spec, 212
214 (x,y) e dom & z e n
Join, 204, 209
215 subt(x,y)=z <=> (x,y,z) e subt
Detach, 213, 214
216 [subt(x,y)=z => (x,y,z) e subt]
&
[(x,y,z) e subt => subt(x,y)=z]
Iff-And, 215
217 subt(x,y)=z => (x,y,z) e subt
Split, 216
218 (x,y,z) e subt => subt(x,y)=z
Split, 216
219 subt(x,y)=z
Detach, 218, 210
220 ALL(b):ALL(c):[(x,b,c) e subt
<=>
(x,b,c) e n3 & [(x,b) e dom & x=b+c]]
U Spec, 30
221 ALL(c):[(x,y,c) e subt
<=>
(x,y,c) e n3 & [(x,y) e dom & x=y+c]]
U Spec, 220
222 (x,y,z) e subt
<=>
(x,y,z) e n3 & [(x,y) e dom & x=y+z]
U Spec, 221
223 [(x,y,z) e subt => (x,y,z) e n3 & [(x,y) e dom & x=y+z]]
&
[(x,y,z) e n3 & [(x,y) e dom & x=y+z] => (x,y,z) e subt]
Iff-And, 222
224 (x,y,z) e subt => (x,y,z) e n3 & [(x,y) e dom & x=y+z]
Split, 223
225 (x,y,z) e n3 & [(x,y) e dom & x=y+z] => (x,y,z) e subt
Split, 223
226 (x,y,z) e n3 & [(x,y) e dom & x=y+z]
Detach, 224, 210
227 (x,y,z) e n3
Split, 226
228 (x,y) e dom & x=y+z
Split, 226
229 (x,y) e dom
Split, 228
230 x=y+z
Split, 228
231 x=y+subt(x,y)
Substitute, 219,
230
As Required:
232 ALL(a):ALL(b):[(a,b) e dom => a=b+subt(a,b)]
4 Conclusion, 204
Prove: ALL(a):ALL(b):[a e n & b e n =>
[b<=a => a=b+subt(a,b)]]
Suppose...
233 x e n & y e n
Premise
234 x e n
Split, 233
235 y e n
Split, 233
Prove: y<=x => x=y+subt(x,y)
Suppose...
236 y<=x
Premise
237 ALL(b):[(x,b) e dom => x=b+subt(x,b)]
U Spec, 232
238 (x,y) e dom => x=y+subt(x,y)
U Spec, 237
239 ALL(b):[(x,b) e dom <=> (x,b) e n2 & b<=x]
U Spec, 17
240 (x,y) e dom <=> (x,y) e n2 & y<=x
U Spec, 239
241 [(x,y) e dom => (x,y) e n2 & y<=x]
&
[(x,y) e n2 & y<=x => (x,y) e dom]
Iff-And, 240
242 (x,y) e dom => (x,y) e n2 & y<=x
Split, 241
243 (x,y) e n2 & y<=x => (x,y) e dom
Split, 241
244 ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]
U Spec, 13
245 (x,y) e n2 <=> x e n & y e n
U Spec, 244
246 [(x,y) e n2 => x e n & y e n]
&
[x e n & y e n => (x,y) e n2]
Iff-And, 245
247 (x,y) e n2 => x e n & y e n
Split, 246
248 x e n & y e n => (x,y) e n2
Split, 246
249 (x,y) e n2
Detach, 248, 233
250 (x,y) e n2 & y<=x
Join, 249, 236
251 (x,y) e dom
Detach, 243, 250
252 x=y+subt(x,y)
Detach, 238, 251
253 ALL(b):[(x,b) e dom => subt(x,b) e n]
U Spec, 203
254 (x,y) e dom => subt(x,y) e n
U Spec, 253
255 subt(x,y) e n
Detach, 254, 251
256 subt(x,y) e n & x=y+subt(x,y)
Join, 255, 252
As Required:
257 y<=x => subt(x,y) e n & x=y+subt(x,y)
4 Conclusion, 236
As Required:
258 ALL(a):ALL(b):[a e n & b e n
=>
[b<=a => subt(a,b) e n & a=b+subt(a,b)]]
4 Conclusion, 233
As Required:
259 EXIST(subt):ALL(a):ALL(b):[a e n & b e n
=>
[b<=a => subt(a,b) e n & a=b+subt(a,b)]]
E Gen, 258