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