Proof of 0<1 in an Ordered Field
Here we prove that 0<1 in any ordered field. This proof makes use of six previously
established lemmas.
Here we make use of the Trichotomy Rule and the fact that 0 and 1 are distinct to establish
that either 0<1 or 1<0. We then suppose that 1<0 is true and obtain a contradiction.
Then we are left with 0<1.
Notation:
P & Q --> P and Q
P | Q --> P or Q
~P --> not P
Set(x) --> x is a set
Field Axioms:
1 Set(f)
& ALL(a):ALL(b):[a 
f & b f => a+b f]
& ALL(a):ALL(b):ALL(c):[a f & b f & c f => a+b+c=a+(b+c)]
& ALL(a):ALL(b):[a f & b f => a+b=b+a]
& 0 f
& ALL(a):[a f => a+0=a]
& ALL(a):[a f => _a f]
& ALL(a):[a f => a+_a=0]
& ALL(a):ALL(b):[a f & b f => a*b f]
& ALL(a):ALL(b):ALL(c):[a f & b f & c f => a*b*c=a*(b*c)]
& ALL(a):ALL(b):[a f & b f => a*b=b*a]
& ALL(a):ALL(b):ALL(c):[a f & b f & c f => a*(b+c)=a*b+a*c]
& 1 f
& ~0=1
& ALL(a):[a f => a*1=a]
& ALL(a):[a f & ~a=0 => 1/a f]
& ALL(a):[a f => a*(1/a)=1]
Premise
Splitting out individual axioms...
f is a set
2 Set(f)
Split, 1
Define: + operator on f
3 ALL(a):ALL(b):[a f & b f => a+b f]
Split, 1
+ is associative
4 ALL(a):ALL(b):ALL(c):[a f & b f & c f => a+b+c=a+(b+c)]
Split, 1
+ is commutative
5 ALL(a):ALL(b):[a f & b f => a+b=b+a]
Split, 1
Define: 0
6 0 f
Split, 1
7 ALL(a):[a f => a+0=a]
Split, 1
Define: _ operator on f
8 ALL(a):[a f => _a f]
Split, 1
9 ALL(a):[a f => a+_a=0]
Split, 1
Define: * operator on f
10 ALL(a):ALL(b):[a f & b f => a*b f]
Split, 1
* is associative
11 ALL(a):ALL(b):ALL(c):[a f & b f & c f => a*b*c=a*(b*c)]
Split, 1
* is commutative
12 ALL(a):ALL(b):[a f & b f => a*b=b*a]
Split, 1
* is distributive over +
13 ALL(a):ALL(b):ALL(c):[a f & b f & c f => a*(b+c)=a*b+a*c]
Split, 1
Define: 1
14 1 f
Split, 1
15 ~0=1
Split, 1
16 ALL(a):[a f => a*1=a]
Split, 1
Define: 1/ operator
17 ALL(a):[a f & ~a=0 => 1/a f]
Split, 1
18 ALL(a):[a f => a*(1/a)=1]
Split, 1
Applying definition of _ operator...
Define: _1
19 1 f => _1 f
U Spec, 8
20 _1 f
Detach, 19, 14
Order Axioms:
21 Set(pos)
& ALL(a):[a pos => a f]
& ALL(a):[a f
=> [a=0 | a pos | _a pos]
& ~[a=0 & a pos]
& ~[a=0 & _a pos]
& ~[a pos & _a pos]]
& ALL(a):ALL(b):[a f & b f & a pos & b pos => a+b pos]
& ALL(a):ALL(b):[a f & b f & a pos & b pos => a*b pos]
& ALL(a):ALL(b):[a f & b f => [a<b <=> b+_a pos]]
Premise
Splitting out individual axioms...
pos is a set (the set of positive elements of f)
22 Set(pos)
Split, 21
pos is a subset of f
23 ALL(a):[a pos => a f]
Split, 21
Trichotomy Rule
24 ALL(a):[a f
=> [a=0 | a pos | _a pos]
& ~[a=0 & a pos]
& ~[a=0 & _a pos]
& ~[a pos & _a pos]]
Split, 21
Closure under +
25 ALL(a):ALL(b):[a f & b f & a pos & b pos => a+b pos]
Split, 21
Closure under *
26 ALL(a):ALL(b):[a f & b f & a pos & b pos => a*b pos]
Split, 21
Define: <
27 ALL(a):ALL(b):[a f & b f => [a<b <=> b+_a pos]]
Split, 21
Previous Results:
Lemma 1: 0<x <=> xpose
28 ALL(a):[a f => [0<a <=> a pos]]
Premise
Lemma 2: x<0 <=> _xpos
29 ALL(a):[a f => [a<0 <=> _a pos]]
Premise
Lemma 3: Additivity of <
30 ALL(a):ALL(b):ALL(c):[a f & b f & c f & a<b => a+c<b+c]
Premise
Lemma 4: Multiplicivity of <
31 ALL(a):ALL(b):ALL(c):[a f & b f & c f & a<b
=> [0<c => a*c<b*c] & [c<0 => b*c<a*c]]
Premise
Lemma 5: x*0=0
32 ALL(a):[a f => a*0=0]
Premise
Lemma 6: _x*_y=x*y
33 ALL(a):ALL(b):[a f & b f => _a*_b=a*b]
Premise
Prove: 0<1 | 1<0
Applying the Trichotomy Rule...
34 1 f
=> [1=0 | 1 pos | _1 pos]
& ~[1=0 & 1 pos]
& ~[1=0 & _1 pos]
& ~[1 pos & _1 pos]
U Spec, 24
35 [1=0 | 1 pos | _1 pos]
& ~[1=0 & 1 pos]
& ~[1=0 & _1 pos]
& ~[1 pos & _1 pos]
Detach, 34, 14
36 1=0 | 1 pos | _1 pos
Split, 35
37 ~[1=0 & 1 pos]
Split, 35
38 ~[1=0 & _1 pos]
Split, 35
39 ~[1 pos & _1 pos]
Split, 35
40 ~[~1=0 & ~1 pos] | _1 pos
DeMorgan, 36
41 ~[~~[~1=0 & ~1 pos] & ~_1 pos]
DeMorgan, 40
42 ~[~1=0 & ~1 pos & ~_1 pos]
Rem DNeg, 41
Prove: 0<1 | 1<0
Suppose to the contrary...
43 ~[0<1 | 1<0]
Premise
44 ~~[~0<1 & ~1<0]
DeMorgan, 43
45 ~0<1 & ~1<0
Rem DNeg, 44
46 ~0<1
Split, 45
47 ~1<0
Split, 45
48 ~1=0
Sym, 15
Applying Lemma 1...
49 1 f => [0<1 <=> 1 pos]
U Spec, 28
50 0<1 <=> 1 pos
Detach, 49, 14
51 [0<1 => 1 pos] & [1 pos => 0<1]
Iff-And, 50
52 0<1 => 1 pos
Split, 51
53 1 pos => 0<1
Split, 51
54 ~0<1 => ~1 pos
Contra, 53
55 ~1 pos
Detach, 54, 46
Applying Lemma 2...
56 1 f => [1<0 <=> _1 pos]
U Spec, 29
57 1<0 <=> _1 pos
Detach, 56, 14
58 [1<0 => _1 pos] & [_1 pos => 1<0]
Iff-And, 57
59 1<0 => _1 pos
Split, 58
60 _1 pos => 1<0
Split, 58
61 ~1<0 => ~_1 pos
Contra, 60
62 ~_1 pos
Detach, 61, 47
63 ~1=0 & ~1 pos
Join, 48, 55
64 ~1=0 & ~1 pos & ~_1 pos
Join, 63, 62
Obtain the contradiction...
65 ~1=0 & ~1 pos & ~_1 pos
& ~[~1=0 & ~1 pos & ~_1 pos]
Join, 64, 42
66 ~~[0<1 | 1<0]
Conclusion, 43
As Required:
67 0<1 | 1<0
Rem DNeg, 66
Prove: ~1<0
Suppose to the contrary...
68 1<0
Premise
69 ALL(b):ALL(c):[1 f & b f & c f & 1<b => 1+c<b+c]
U Spec, 30
70 ALL(c):[1 f & 0 f & c f & 1<0 => 1+c<0+c]
U Spec, 69
71 1 f & 0 f & _1 f & 1<0 => 1+_1<0+_1
U Spec, 70
72 1 f & 0 f
Join, 14, 6
73 1 f & 0 f & _1 f
Join, 72, 20
74 1 f & 0 f & _1 f & 1<0
Join, 73, 68
75 1+_1<0+_1
Detach, 71, 74
Applying definition of _ operator...
76 1 f => 1+_1=0
U Spec, 9
77 1+_1=0
Detach, 76, 14
78 0<0+_1
Substitute, 77, 75
Applying the defintion of 0...
79 _1 f => _1+0=_1
U Spec, 7
80 _1+0=_1
Detach, 79, 20
Applying commutativity of +...
81 ALL(b):[0 f & b f => 0+b=b+0]
U Spec, 5
82 0 f & _1 f => 0+_1=_1+0
U Spec, 81
83 0 f & _1 f
Join, 6, 20
84 0+_1=_1+0
Detach, 82, 83
85 0+_1=_1
Substitute, 84, 80
86 0<_1
Substitute, 85, 78
Applying the multiplicity of >...
87 ALL(b):ALL(c):[0 f & b f & c f & 0<b
=> [0<c => 0*c<b*c] & [c<0 => b*c<0*c]]
U Spec, 31
88 ALL(c):[0 f & _1 f & c f & 0<_1
=> [0<c => 0*c<_1*c] & [c<0 => _1*c<0*c]]
U Spec, 87
89 0 f & _1 f & _1 f & 0<_1
=> [0<_1 => 0*_1<_1*_1] & [_1<0 => _1*_1<0*_1]
U Spec, 88
90 0 f & _1 f
Join, 6, 20
91 0 f & _1 f & _1 f
Join, 90, 20
92 0 f & _1 f & _1 f & 0<_1
Join, 91, 86
93 [0<_1 => 0*_1<_1*_1] & [_1<0 => _1*_1<0*_1]
Detach, 89, 92
94 0<_1 => 0*_1<_1*_1
Split, 93
95 _1<0 => _1*_1<0*_1
Split, 93
96 0*_1<_1*_1
Detach, 94, 86
Applying 0 multiplication...
97 _1 f => _1*0=0
U Spec, 32
98 _1*0=0
Detach, 97, 20
Applying commutativity of *...
99 ALL(b):[_1 f & b f => _1*b=b*_1]
U Spec, 12
100 _1 f & 0 f => _1*0=0*_1
U Spec, 99
101 _1 f & 0 f
Join, 20, 6
102 _1*0=0*_1
Detach, 100, 101
103 0*_1=0
Substitute, 102, 98
104 0<_1*_1
Substitute, 103, 96
105 ALL(b):[1 f & b f => _1*_b=1*b]
U Spec, 33
Applying double negatives multiplied...
106 1 f & 1 f => _1*_1=1*1
U Spec, 105
107 1 f & 1 f
Join, 14, 14
108 _1*_1=1*1
Detach, 106, 107
109 0<1*1
Substitute, 108, 104
Applying the definition of 1...
110 1 f => 1*1=1
U Spec, 16
111 1*1=1
Detach, 110, 14
112 0<1
Substitute, 111, 109
Applying Lemma 1...
113 1 f => [0<1 <=> 1 pos]
U Spec, 28
114 0<1 <=> 1 pos
Detach, 113, 14
115 [0<1 => 1 pos] & [1 pos => 0<1]
Iff-And, 114
116 0<1 => 1 pos
Split, 115
117 1 pos => 0<1
Split, 115
118 1 pos
Detach, 116, 112
119 1 f => [1<0 <=> _1 pos]
U Spec, 29
120 1<0 <=> _1 pos
Detach, 119, 14
121 [1<0 => _1 pos] & [_1 pos => 1<0]
Iff-And, 120
122 1<0 => _1 pos
Split, 121
123 _1 pos => 1<0
Split, 121
124 _1 pos
Detach, 122, 68
Applying the trichotomy rule...
125 1 f
=> [1=0 | 1 pos | _1 pos]
& ~[1=0 & 1 pos]
& ~[1=0 & _1 pos]
& ~[1 pos & _1 pos]
U Spec, 24
126 [1=0 | 1 pos | _1 pos]
& ~[1=0 & 1 pos]
& ~[1=0 & _1 pos]
& ~[1 pos & _1 pos]
Detach, 125, 14
127 1=0 | 1 pos | _1 pos
Split, 126
128 ~[1=0 & 1 pos]
Split, 126
129 ~[1=0 & _1 pos]
Split, 126
130 ~[1 pos & _1 pos]
Split, 126
131 1 pos & _1 pos
Join, 118, 124
Obtain the contradiction...
132 1 pos & _1 pos & ~[1 pos & _1 pos]
Join, 131, 130
By contradiction...
133 ~1<0
Conclusion, 68
134 ~0<1 => 1<0
Imply-Or, 67
135 ~1<0 => ~~0<1
Contra, 134
136 ~1<0 => 0<1
Rem DNeg, 135
As Required:
137 0<1
Detach, 136, 133