THEOREM
*******
Here, we construct an ordering lt (<) on the set of positive rational numbers qp
using the Cartesian product and Subset axioms, and the previously constructed set of
positive rational numbers qp, multiplication function * on n and ordering < on n.
Prove: EXIST(lt):ALL(a):ALL(b):[a e qp & b e qp
=> [(a,b) e lt
<=> ALL(c):ALL(d):ALL(e):ALL(f):[(c,d) e a & (e,f) e b => c*f<e*d]]]
In subsquent proofs, we will use the infix < notation for this ordering as well. Note that the '<' to the right of the biconditional is the ordering on the set of natural numbers. The variables c, d, e, f will always be natural numbers.
This proof is was written and verified with the aid of the author's DC Proof 2.0 software
available free at http://www.dcproof.com
FROM PREVIOUS RESULTS
*********************
Define: < on n
**************
1 ALL(a):ALL(b):[a e n & b e n => [a<b <=> EXIST(c):[c e n & a+c=b]]]
Axiom
Define: * on n
**************
2 ALL(a):ALL(b):[a e n & b e n => a*b e n]
Axiom
3 ALL(a):[a e n => a*1=a]
Axiom
4 ALL(a):ALL(b):[a e n & b e n => a*(b+1)=a*b+a]
Axiom
5 ALL(a):ALL(b):[a e n & b e n => a*b=b*a]
Axiom
Define: qp
**********
6 Set(qp)
Axiom
7 ALL(a):[a e qp
<=> Set'(a)
& ALL(b):ALL(c):[(b,c) e a => b e n & c e n]
& EXIST(b):EXIST(c):[(b,c) e a & ALL(d):ALL(e):[d e n & e e n => [(d,e) e a <=> b*e=d*c]]]]
Axiom
PROOF
*****
Apply Cartesian Product axiom
8
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
9
ALL(a2):[Set(qp)
& Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2)
e b
<=> c1
e qp
& c2 e
a2]]]
U Spec, 8
10 Set(qp) & Set(qp) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e qp & c2 e qp]]
U Spec, 9
11 Set(qp) & Set(qp)
Join, 6, 6
12 EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e qp & c2 e qp]]
Detach, 10, 11
13 Set'(qp2) & ALL(c1):ALL(c2):[(c1,c2) e qp2 <=> c1 e qp & c2 e qp]
E Spec, 12
Define: qp2
***********
The set of ordered pairs of positive rational numbers
14 Set'(qp2)
Split, 13
15 ALL(c1):ALL(c2):[(c1,c2) e qp2 <=> c1 e qp & c2 e qp]
Split, 13
Apply Subset axiom
16 EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) e sub <=> (a,b) e qp2 & ALL(c):ALL(d):ALL(e):ALL(f):[(c,d) e a & (e,f) e b => c*f<e*d]]]
Subset, 14
17
Set'(lt)
& ALL(a):ALL(b):[(a,b) e
lt
<=> (a,b) e
qp2
& ALL(c):ALL(d):ALL(e):ALL(f):[(c,d)
e a & (e,f)
e b => c*f<e*d]]
E Spec, 16
Define: lt
**********
18 Set'(lt)
Split, 17
19
ALL(a):ALL(b):[(a,b)
e lt
<=> (a,b) e
qp2
& ALL(c):ALL(d):ALL(e):ALL(f):[(c,d)
e a
& (e,f)
e b => c*f<e*d]]
Split, 17
Recast this definition without reference to qp2
Prove: ALL(a):ALL(b):[a e qp & b e qp
=> [(a,b) e lt
<=> ALL(c):ALL(d):ALL(e):ALL(f):[(c,d) e a & (e,f) e b => c*f<e*d]]]
Suppose...
20 x e qp & y e qp
Premise
21 x e qp
Split, 20
22 y e qp
Split, 20
'=>'
Prove: (x,y) e lt
=> ALL(c):ALL(d):ALL(e):ALL(f):[(c,d) e x & (e,f) e y => c*f<e*d]
Suppose...
23 (x,y) e lt
Premise
Apply original definition of lt
24
ALL(b):[(x,b)
e lt
<=> (x,b)
e qp2
& ALL(c):ALL(d):ALL(e):ALL(f):[(c,d)
e x
& (e,f) e
b => c*f<e*d]]
U Spec, 19
25
(x,y)
e lt
<=> (x,y)
e qp2
& ALL(c):ALL(d):ALL(e):ALL(f):[(c,d)
e x
& (e,f) e
y
=> c*f<e*d]
U Spec, 24
26
[(x,y)
e lt
=> (x,y)
e qp2
& ALL(c):ALL(d):ALL(e):ALL(f):[(c,d)
e x
& (e,f) e
y
=> c*f<e*d]]
& [(x,y)
e qp2
& ALL(c):ALL(d):ALL(e):ALL(f):[(c,d)
e x
& (e,f) e
y
=> c*f<e*d]
=> (x,y)
e lt]
Iff-And, 25
27
(x,y)
e lt
=> (x,y)
e qp2
& ALL(c):ALL(d):ALL(e):ALL(f):[(c,d)
e x
& (e,f) e
y
=> c*f<e*d]
Split, 26
28
(x,y)
e qp2
& ALL(c):ALL(d):ALL(e):ALL(f):[(c,d)
e x
& (e,f) e
y
=> c*f<e*d]
=> (x,y)
e lt
Split, 26
29 (x,y) e qp2 & ALL(c):ALL(d):ALL(e):ALL(f):[(c,d) e x & (e,f) e y => c*f<e*d]
Detach, 27, 23
30 (x,y) e qp2
Split, 29
31 ALL(c):ALL(d):ALL(e):ALL(f):[(c,d) e x & (e,f) e y => c*f<e*d]
Split, 29
As Required:
32 (x,y) e lt
=> ALL(c):ALL(d):ALL(e):ALL(f):[(c,d) e x & (e,f) e y => c*f<e*d]
4 Conclusion, 23
'<='
Prove: ALL(c):ALL(d):ALL(e):ALL(f):[(c,d) e x & (e,f) e y => c*f<e*d]
=> (x,y) e lt
Suppose...
33 ALL(c):ALL(d):ALL(e):ALL(f):[(c,d) e x & (e,f) e y => c*f<e*d]
Premise
Apply original definition of lt
34
ALL(b):[(x,b)
e lt
<=> (x,b)
e qp2
& ALL(c):ALL(d):ALL(e):ALL(f):[(c,d)
e x
& (e,f) e
b => c*f<e*d]]
U Spec, 19
35
(x,y)
e lt
<=> (x,y)
e qp2
& ALL(c):ALL(d):ALL(e):ALL(f):[(c,d)
e x
& (e,f) e
y
=> c*f<e*d]
U Spec, 34
36
[(x,y)
e lt
=> (x,y)
e qp2
& ALL(c):ALL(d):ALL(e):ALL(f):[(c,d)
e x
& (e,f) e
y
=> c*f<e*d]]
& [(x,y)
e qp2
& ALL(c):ALL(d):ALL(e):ALL(f):[(c,d)
e x
& (e,f) e
y
=> c*f<e*d]
=> (x,y)
e lt]
Iff-And, 35
37
(x,y)
e lt
=> (x,y)
e qp2
& ALL(c):ALL(d):ALL(e):ALL(f):[(c,d)
e x
& (e,f) e
y
=> c*f<e*d]
Split, 36
Sufficient For: (x,y) e lt
38
(x,y)
e qp2
& ALL(c):ALL(d):ALL(e):ALL(f):[(c,d)
e x
& (e,f) e
y
=> c*f<e*d]
=> (x,y)
e lt
Split, 36
39 ALL(c2):[(x,c2) e qp2 <=> x e qp & c2 e qp]
U Spec, 15
40 (x,y) e qp2 <=> x e qp & y e qp
U Spec, 39
41 [(x,y) e qp2 => x e qp & y e qp]
& [x e qp & y e qp => (x,y) e qp2]
Iff-And, 40
42 (x,y) e qp2 => x e qp & y e qp
Split, 41
43 x e qp & y e qp => (x,y) e qp2
Split, 41
44 (x,y) e qp2
Detach, 43, 20
45 (x,y) e qp2
& ALL(c):ALL(d):ALL(e):ALL(f):[(c,d) e x & (e,f) e y => c*f<e*d]
Join, 44, 33
46 (x,y) e lt
Detach, 38, 45
As Required:
47 ALL(c):ALL(d):ALL(e):ALL(f):[(c,d) e x & (e,f) e y => c*f<e*d]
=> (x,y) e lt
4 Conclusion, 33
Joining results...
48 [(x,y) e lt
=> ALL(c):ALL(d):ALL(e):ALL(f):[(c,d) e x & (e,f) e y => c*f<e*d]]
& [ALL(c):ALL(d):ALL(e):ALL(f):[(c,d) e x & (e,f) e y => c*f<e*d]
=> (x,y) e lt]
Join, 32, 47
Apply Iff-And rule
49 (x,y) e lt
<=> ALL(c):ALL(d):ALL(e):ALL(f):[(c,d) e x & (e,f) e y => c*f<e*d]
Iff-And, 48
As Required:
50 ALL(a):ALL(b):[a e qp & b e qp
=> [(a,b) e lt
<=> ALL(c):ALL(d):ALL(e):ALL(f):[(c,d) e a & (e,f) e b => c*f<e*d]]]
4 Conclusion, 20
Generalizing...
As Required:
51 EXIST(lt):ALL(a):ALL(b):[a e qp & b e qp
=> [(a,b) e lt
<=> ALL(c):ALL(d):ALL(e):ALL(f):[(c,d) e a & (e,f) e b => c*f<e*d]]]
E Gen, 50