Some Simple Results from the Ordered Field Axioms
Introduction:
From the axioms for an ordered field (f,+,0,*,1), we obtain the following results:
1. _0=0
2. ALL(a):[a 
f => [0<a <=> a pos]]
3. ALL(a):[a f => [a<0 <=> _a pos]]
4. ALL(a):[a f => _(_a)=a]
5. ALL(a):[a f & 0<a => _a<0]
6. ALL(a):[a f & a<0 => 0<_a]
Where:
pos = the set of positive elements of f
_x = the additive inverse of x
The 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
The Order Axioms:
19 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]]
& ALL(a):ALL(b):[a f & b f => [a>b <=> b<a]]
& ALL(a):ALL(b):[a f & b f => [a<=b <=> a<b | a=b]]
& ALL(a):ALL(b):[a f & b f => [a>=b <=> a>b | a=b]]
Premise
Splitting out individual axioms...
pos is the subset of positive elements in f
20 Set(pos)
Split, 19
21 ALL(a):[a pos => a f]
Split, 19
Trichotomy
22 ALL(a):[a f
=> [a=0 | a pos | _a pos]
& ~[a=0 & a pos]
& ~[a=0 & _a pos]
& ~[a pos & _a pos]]
Split, 19
Closure under +
23 ALL(a):ALL(b):[a f & b f & a pos & b pos => a+b pos]
Split, 19
Closure under *
24 ALL(a):ALL(b):[a f & b f & a pos & b pos => a*b pos]
Split, 19
Define: <
25 ALL(a):ALL(b):[a f & b f => [a<b <=> b+_a pos]]
Split, 19
Prove: _0=0
26 0 f => 0+_0=0
U Spec, 9
27 0+_0=0
Detach, 26, 6
28 ALL(b):[0 f & b f => 0+b=b+0]
U Spec, 5
29 0 f & _0 f => 0+_0=_0+0
U Spec, 28
30 0 f => _0 f
U Spec, 8
31 _0 f
Detach, 30, 6
32 0 f & _0 f
Join, 6, 31
33 0+_0=_0+0
Detach, 29, 32
34 _0+0=0
Substitute, 33, 27
35 _0 f => _0+0=_0
U Spec, 7
36 _0+0=_0
Detach, 35, 31
37 0 f => 0+_0=0
U Spec, 9
38 0+_0=0
Detach, 37, 6
39 ALL(b):[0 f & b f => 0+b=b+0]
U Spec, 5
40 0 f & _0 f => 0+_0=_0+0
U Spec, 39
41 0 f => _0 f
U Spec, 8
42 _0 f
Detach, 41, 6
43 0 f & _0 f
Join, 6, 42
44 0+_0=_0+0
Detach, 40, 43
45 _0+0=0
Substitute, 44, 38
46 _0 f => _0+0=_0
U Spec, 7
47 _0+0=_0
Detach, 46, 42
Theorem 1:
48 _0=0
Substitute, 47, 45
Prove: x f => [0<x <=> x pos]
Suppose...
49 x f
Premise
50 ALL(b):[0 f & b f => [0<b <=> b+_0 pos]]
U Spec, 25
51 0 f & x f => [0<x <=> x+_0 pos]
U Spec, 50
52 0 f & x f
Join, 6, 49
53 0<x <=> x+_0 pos
Detach, 51, 52
54 0<x <=> x+0 pos
Substitute, 48, 53
55 x f => x+0=x
U Spec, 7
56 x+0=x
Detach, 55, 49
57 0<x <=> x pos
Substitute, 56, 54
As Required:
58 x f => [0<x <=> x pos]
Conclusion, 49
Theorem 2:
59 ALL(a):[a f => [0<a <=> a pos]]
U Gen, 58
Prove: x f => [x<0 <=> _x pos]
Suppose...
60 x f
Premise
61 ALL(b):[x f & b f => [x<b <=> b+_x pos]]
U Spec, 25
62 x f & 0 f => [x<0 <=> 0+_x pos]
U Spec, 61
63 x f & 0 f
Join, 60, 6
64 x<0 <=> 0+_x pos
Detach, 62, 63
65 ALL(b):[0 f & b f => 0+b=b+0]
U Spec, 5
66 0 f & _x f => 0+_x=_x+0
U Spec, 65
67 x f => _x f
U Spec, 8
68 _x f
Detach, 67, 60
69 0 f & _x f
Join, 6, 68
70 0+_x=_x+0
Detach, 66, 69
71 x<0 <=> _x+0 pos
Substitute, 70, 64
72 _x f => _x+0=_x
U Spec, 7
73 _x+0=_x
Detach, 72, 68
74 x<0 <=> _x pos
Substitute, 73, 71
As Required:
75 x f => [x<0 <=> _x pos]
Conclusion, 60
Theorem 3:
76 ALL(a):[a f => [a<0 <=> _a pos]]
U Gen, 75
Prove: x f => _(_x)=x
Suppose...
77 x f
Premise
78 _x f => _x+_(_x)=0
U Spec, 9
79 x f => _x f
U Spec, 8
80 _x f
Detach, 79, 77
81 _x+_(_x)=0
Detach, 78, 80
82 x+0=x+0
Reflex
83 x+(_x+_(_x))=x+0
Substitute, 81, 82
84 x f => x+0=x
U Spec, 7
85 x+0=x
Detach, 84, 77
86 x+(_x+_(_x))=x
Substitute, 85, 83
87 ALL(b):ALL(c):[x f & b f & c f => x+b+c=x+(b+c)]
U Spec, 4
88 ALL(c):[x f & _x f & c f => x+_x+c=x+(_x+c)]
U Spec, 87
89 x f & _x f & _(_x) f => x+_x+_(_x)=x+(_x+_(_x))
U Spec, 88
90 _x f => _(_x) f
U Spec, 8
91 _(_x) f
Detach, 90, 80
92 x f & _x f
Join, 77, 80
93 x f & _x f & _(_x) f
Join, 92, 91
94 x+_x+_(_x)=x+(_x+_(_x))
Detach, 89, 93
95 x+_x+_(_x)=x
Substitute, 94, 86
96 x f => x+_x=0
U Spec, 9
97 x+_x=0
Detach, 96, 77
98 0+_(_x)=x
Substitute, 97, 95
99 ALL(b):[0 f & b f => 0+b=b+0]
U Spec, 5
100 0 f & _(_x) f => 0+_(_x)=_(_x)+0
U Spec, 99
101 0 f & _(_x) f
Join, 6, 91
102 0+_(_x)=_(_x)+0
Detach, 100, 101
103 _(_x)+0=x
Substitute, 102, 98
104 _(_x) f => _(_x)+0=_(_x)
U Spec, 7
105 _(_x)+0=_(_x)
Detach, 104, 91
106 _(_x)=x
Substitute, 105, 103
As Required:
107 x f => _(_x)=x
Conclusion, 77
Theorem 4:
108 ALL(a):[a f => _(_a)=a]
U Gen, 107
Prove: x f & 0<x => _x<0
Suppose...
109 x f & 0<x
Premise
110 x f
Split, 109
111 0<x
Split, 109
112 x f => [0<x <=> x pos]
U Spec, 59
113 0<x <=> x pos
Detach, 112, 110
114 [0<x => x pos] & [x pos => 0<x]
Iff-And, 113
115 0<x => x pos
Split, 114
116 x pos => 0<x
Split, 114
117 x pos
Detach, 115, 111
118 _x f => [_x<0 <=> _(_x) pos]
U Spec, 76
119 x f => _x f
U Spec, 8
120 _x f
Detach, 119, 110
121 _x<0 <=> _(_x) pos
Detach, 118, 120
122 [_x<0 => _(_x) pos] & [_(_x) pos => _x<0]
Iff-And, 121
123 _x<0 => _(_x) pos
Split, 122
Sufficient:
124 _(_x) pos => _x<0
Split, 122
125 x f => _(_x)=x
U Spec, 108
126 _(_x)=x
Detach, 125, 110
127 x pos => _x<0
Substitute, 126, 124
128 _x<0
Detach, 127, 117
As Required:
129 x f & 0<x => _x<0
Conclusion, 109
Theorem 5:
130 ALL(a):[a f & 0<a => _a<0]
U Gen, 129
Prove: x f & x<0 => 0<_x
Suppose...
131 x f & x<0
Premise
132 x f
Split, 131
133 x<0
Split, 131
134 x f => [x<0 <=> _x pos]
U Spec, 76
135 x<0 <=> _x pos
Detach, 134, 132
136 [x<0 => _x pos] & [_x pos => x<0]
Iff-And, 135
137 x<0 => _x pos
Split, 136
138 _x pos => x<0
Split, 136
139 _x pos
Detach, 137, 133
140 _x f => [0<_x <=> _x pos]
U Spec, 59
141 x f => _x f
U Spec, 8
142 _x f
Detach, 141, 132
143 0<_x <=> _x pos
Detach, 140, 142
144 [0<_x => _x pos] & [_x pos => 0<_x]
Iff-And, 143
145 0<_x => _x pos
Split, 144
146 _x pos => 0<_x
Split, 144
147 0<_x
Detach, 146, 139
As Required:
148 x f & x<0 => 0<_x
Conclusion, 131
Theorem 6:
149 ALL(a):[a f & a<0 => 0<_a]
U Gen, 148