Here, we derive the following lemmas of ordered field theory:

1. _0=0

2. ALL(a):[a e real => ~a<a]

3. ALL(a):ALL(b):[a e real & b e real => [a<b => _b<_a]]

4. ALL(a):ALL(b):[a e real & b e real => [0<a & 0<b => 0<b+a]]

5. ALL(a):[a e real => _(_a)=a]

6. ALL(a):[a e real => a*0=0]

7. ALL(a):ALL(b):[a e real & b e real => _a*_b=a*b]

8. 0<1

9. ALL(a):ALL(b):ALL(c):[a e real & b e real & c e real => [a<b & 0<c => a<b+c]]

This proof was written with the aid of DC Proof 2.0

The Field Axioms

----------------

1     Set(real)

Axiom

Define: '+' operator

2     ALL(a):ALL(b):[a e real & b e real => a+b e real]

Axiom

+ is associative

3     ALL(a):ALL(b):ALL(c):[a e real & b e real & c e real => a+b+c=a+(b+c)]

Axiom

+ is commutative

4     ALL(a):ALL(b):[a e real & b e real => a+b=b+a]

Axiom

Define: 0

5     0 e real

Axiom

6     ALL(a):[a e real => a+0=a]

Axiom

Define: '_' operator, the additive inverse (not to be confused with subtraction)

7     ALL(a):[a e real => _a e real]

Axiom

8     ALL(a):[a e real => a+_a=0]

Axiom

Define: * operator (multiplication)

9     ALL(a):ALL(b):[a e real & b e real => a*b e real]

Axiom

* is associative

10    ALL(a):ALL(b):ALL(c):[a e real & b e real & c e real => a*b*c=a*(b*c)]

Axiom

* is commutative

11    ALL(a):ALL(b):[a e real & b e real => a*b=b*a]

Axiom

* is distributive over +

12    ALL(a):ALL(b):ALL(c):[a e real & b e real & c e real => a*(b+c)=a*b+a*c]

Axiom

Define: 1

13    1 e real

Axiom

14    ~0=1

Axiom

15    ALL(a):[a e real => a*1=a]

Axiom

Define: 'recip' operator (multiplicative inverse)

16    ALL(a):[a e real & ~a=0 => recip(a) e real]

Axiom

17    ALL(a):[a e real & ~a=0 => a*recip(a)=1]

Axiom

Order Axioms

------------

Trichotomy Rule for '<'

18    ALL(a):ALL(b):[a e real & b e real

=> [a<b | a=b | b<a]

& ~[a<b & a=b]

& ~[a<b & b<a]

& ~[a=b & b<a]]

Axiom

Transitivity Rule for '<'

19    ALL(a):ALL(b):ALL(c):[a e real & b e real & c e real

=> [a<b & b<c => a<c]]

Axiom

20    ALL(a):ALL(b):ALL(c):[a e real & b e real & c e real

=> [a<b => a+c<b+c]]

Axiom

Multiplicitive Compatiblity

21    ALL(a):ALL(b):ALL(c):[a e real & b e real & c e real

=> [a<b & 0<c => a*c<b*c]]

Axiom

Define: '<='

22    ALL(a):ALL(b):[a e real & b e real => [a<=b <=> a<b | a=b]]

Axiom

Completeness Axiom (Least Upper Bound)

--------------------------------------

23    ALL(a):[Set(a)

& ALL(b):[b e a => b e real]

& EXIST(b):b e a

& EXIST(b):[b e real & ALL(c):[c e a => c<=b]]

=> EXIST(b):[b e real & ALL(c):[c e a => c<=b]

& ALL(c):[c e real & ALL(d):[d e a => d<=c] => b<=c]]]

Axiom

Lemma 1

-------

Prove: _0=0

24    0 e real => 0+_0=0

U Spec, 8

25    0+_0=0

Detach, 24, 5

26    ALL(b):[0 e real & b e real => 0+b=b+0]

U Spec, 4

27    0 e real & _0 e real => 0+_0=_0+0

U Spec, 26

28    0 e real => _0 e real

U Spec, 7

29    _0 e real

Detach, 28, 5

30    0 e real & _0 e real

Join, 5, 29

31    0+_0=_0+0

Detach, 27, 30

32    _0+0=0

Substitute, 31, 25

33    _0 e real => _0+0=_0

U Spec, 6

34    _0+0=_0

Detach, 33, 29

Lemma 1

-------

As Required:

35    _0=0

Substitute, 34, 32

Lemma 2

-------

Prove: ALL(a):[a e real => ~a<a]

Suppose...

36    x e real

Premise

Apply trichotomy rule

37    ALL(b):[x e real & b e real

=> [x<b | x=b | b<x]

& ~[x<b & x=b]

& ~[x<b & b<x]

& ~[x=b & b<x]]

U Spec, 18

38    x e real & x e real

=> [x<x | x=x | x<x]

& ~[x<x & x=x]

& ~[x<x & x<x]

& ~[x=x & x<x]

U Spec, 37

39    x e real & x e real

Join, 36, 36

40    [x<x | x=x | x<x]

& ~[x<x & x=x]

& ~[x<x & x<x]

& ~[x=x & x<x]

Detach, 38, 39

41    x<x | x=x | x<x

Split, 40

42    ~[x<x & x=x]

Split, 40

43    ~[x<x & x<x]

Split, 40

44    ~[x=x & x<x]

Split, 40

45    ~~[x=x => ~x<x]

Imply-And, 44

46    x=x => ~x<x

Rem DNeg, 45

47    x=x

Reflex

48    ~x<x

Detach, 46, 47

Lemma 2

-------

As Required:

49    ALL(a):[a e real => ~a<a]

4 Conclusion, 36

Lemma 3

-------

Prove: ALL(a):ALL(b):[a e real & b e real => [a<b => _b<_a]]

Suppose...

50    x e real & y e real

Premise

51    x e real

Split, 50

52    y e real

Split, 50

Prove: x<y => _y<_x

Suppose...

53    x<y

Premise

54    ALL(b):ALL(c):[x e real & b e real & c e real

=> [x<b => x+c<b+c]]

U Spec, 20

55    ALL(c):[x e real & y e real & c e real

=> [x<y => x+c<y+c]]

U Spec, 54

56    x e real & y e real & _x e real

=> [x<y => x+_x<y+_x]

U Spec, 55

57    x e real => _x e real

U Spec, 7

58    _x e real

Detach, 57, 51

59    x e real & y e real & _x e real

Join, 50, 58

60    x<y => x+_x<y+_x

Detach, 56, 59

61    x+_x<y+_x

Detach, 60, 53

Apply definition of '_'

62    x e real => x+_x=0

U Spec, 8

63    x+_x=0

Detach, 62, 51

64    0<y+_x

Substitute, 63, 61

65    ALL(b):ALL(c):[0 e real & b e real & c e real

=> [0<b => 0+c<b+c]]

U Spec, 20

66    ALL(c):[0 e real & y+_x e real & c e real

=> [0<y+_x => 0+c<y+_x+c]]

U Spec, 65

67    0 e real & y+_x e real & _y e real

=> [0<y+_x => 0+_y<y+_x+_y]

U Spec, 66

68    ALL(b):[y e real & b e real => y+b e real]

U Spec, 2

69    y e real & _x e real => y+_x e real

U Spec, 68

70    y e real & _x e real

Join, 52, 58

71    y+_x e real

Detach, 69, 70

72    y e real => _y e real

U Spec, 7

73    _y e real

Detach, 72, 52

74    0 e real & y+_x e real

Join, 5, 71

75    0 e real & y+_x e real & _y e real

Join, 74, 73

76    0<y+_x => 0+_y<y+_x+_y

Detach, 67, 75

77    0+_y<y+_x+_y

Detach, 76, 64

Apply commutativity of +

78    ALL(b):[0 e real & b e real => 0+b=b+0]

U Spec, 4

79    0 e real & _y e real => 0+_y=_y+0

U Spec, 78

80    y e real => _y e real

U Spec, 7

81    _y e real

Detach, 80, 52

82    0 e real & _y e real

Join, 5, 81

83    0+_y=_y+0

Detach, 79, 82

84    _y+0<y+_x+_y

Substitute, 83, 77

Apply definition of 0

85    _y e real => _y+0=_y

U Spec, 6

86    _y+0=_y

Detach, 85, 81

87    _y<y+_x+_y

Substitute, 86, 84

Apply commutativity of +

88    ALL(b):[y e real & b e real => y+b=b+y]

U Spec, 4

89    y e real & _x e real => y+_x=_x+y

U Spec, 88

90    y e real & _x e real

Join, 52, 58

91    y+_x=_x+y

Detach, 89, 90

92    _y<_x+y+_y

Substitute, 91, 87

Apply associativity of +

93    ALL(b):ALL(c):[_x e real & b e real & c e real => _x+b+c=_x+(b+c)]

U Spec, 3

94    ALL(c):[_x e real & y e real & c e real => _x+y+c=_x+(y+c)]

U Spec, 93

95    _x e real & y e real & _y e real => _x+y+_y=_x+(y+_y)

U Spec, 94

96    _x e real & y e real

Join, 58, 52

97    _x e real & y e real & _y e real

Join, 96, 81

98    _x+y+_y=_x+(y+_y)

Detach, 95, 97

99    _y<_x+(y+_y)

Substitute, 98, 92

Apply definition of '_'

100  y e real => y+_y=0

U Spec, 8

101  y+_y=0

Detach, 100, 52

102  _y<_x+0

Substitute, 101, 99

103  _x e real => _x+0=_x

U Spec, 6

104  _x+0=_x

Detach, 103, 58

105  _y<_x

Substitute, 104, 102

As Required:

106  x<y => _y<_x

4 Conclusion, 53

Lemma 3

-------

As Required:

107  ALL(a):ALL(b):[a e real & b e real => [a<b => _b<_a]]

4 Conclusion, 50

Lemma 4

-------

Prove: ALL(a):ALL(b):[a e real & b e real => [0<a & 0<b => 0<b+a]]

positive + postive = positive

Suppose...

108  x e real & y e real

Premise

109  x e real

Split, 108

110  y e real

Split, 108

Prove: 0<x & 0<y => 0<y+x

Suppose...

111  0<x & 0<y

Premise

112  0<x

Split, 111

113  0<y

Split, 111

Apply Lemma 3

114  ALL(b):[0 e real & b e real => [0<b => _b<_0]]

U Spec, 107

115  0 e real & x e real => [0<x => _x<_0]

U Spec, 114

116  0 e real & x e real

Join, 5, 109

117  0<x => _x<_0

Detach, 115, 116

118  _x<_0

Detach, 117, 112

119  _x<0

Substitute, 35, 118

Apply transitivity of '<'

120  ALL(b):ALL(c):[_x e real & b e real & c e real

=> [_x<b & b<c => _x<c]]

U Spec, 19

121  ALL(c):[_x e real & 0 e real & c e real

=> [_x<0 & 0<c => _x<c]]

U Spec, 120

122  _x e real & 0 e real & y e real

=> [_x<0 & 0<y => _x<y]

U Spec, 121

123  x e real => _x e real

U Spec, 7

124  _x e real

Detach, 123, 109

125  _x e real & 0 e real

Join, 124, 5

126  _x e real & 0 e real & y e real

Join, 125, 110

127  _x<0 & 0<y => _x<y

Detach, 122, 126

128  _x<0 & 0<y

Join, 119, 113

129  _x<y

Detach, 127, 128

Apply Lemma 3

130  ALL(b):ALL(c):[_x e real & b e real & c e real

=> [_x<b => _x+c<b+c]]

U Spec, 20

131  ALL(c):[_x e real & y e real & c e real

=> [_x<y => _x+c<y+c]]

U Spec, 130

132  _x e real & y e real & x e real

=> [_x<y => _x+x<y+x]

U Spec, 131

133  _x e real & y e real

Join, 124, 110

134  _x e real & y e real & x e real

Join, 133, 109

135  _x<y => _x+x<y+x

Detach, 132, 134

136  _x+x<y+x

Detach, 135, 129

Apply commutativity of +

137  ALL(b):[_x e real & b e real => _x+b=b+_x]

U Spec, 4

138  _x e real & x e real => _x+x=x+_x

U Spec, 137

139  _x e real & x e real

Join, 124, 109

140  _x+x=x+_x

Detach, 138, 139

141  x+_x<y+x

Substitute, 140, 136

Apply definition of '_'

142  x e real => x+_x=0

U Spec, 8

143  x+_x=0

Detach, 142, 109

144  0<y+x

Substitute, 143, 141

As Required:

145  0<x & 0<y => 0<y+x

4 Conclusion, 111

Lemma 4

-------

positive + positive = positive

As Required:

146  ALL(a):ALL(b):[a e real & b e real => [0<a & 0<b => 0<b+a]]

4 Conclusion, 108

Lemma 5

-------

Prove: ALL(a):[a e real => _(_a)=a]

Suppose...

147  x e real

Premise

Apply definiton of '_' for _x

148  _x e real => _x+_(_x)=0

U Spec, 8

149  x e real => _x e real

U Spec, 7

150  _x e real

Detach, 149, 147

151  _x+_(_x)=0

Detach, 148, 150

Apply commutativity of +

152  ALL(b):[_x e real & b e real => _x+b=b+_x]

U Spec, 4

153  _x e real & _(_x) e real => _x+_(_x)=_(_x)+_x

U Spec, 152

154  _x e real => _(_x) e real

U Spec, 7

155  _(_x) e real

Detach, 154, 150

156  _x e real & _(_x) e real

Join, 150, 155

157  _x+_(_x)=_(_x)+_x

Detach, 153, 156

158  _(_x)+_x=0

Substitute, 157, 151

159  0+x=0+x

Reflex

160  _(_x)+_x+x=0+x

Substitute, 158, 159

Apply associativity of +

161  ALL(b):ALL(c):[_(_x) e real & b e real & c e real => _(_x)+b+c=_(_x)+(b+c)]

U Spec, 3

162  ALL(c):[_(_x) e real & _x e real & c e real => _(_x)+_x+c=_(_x)+(_x+c)]

U Spec, 161

163  _(_x) e real & _x e real & x e real => _(_x)+_x+x=_(_x)+(_x+x)

U Spec, 162

164  _(_x) e real & _x e real

Join, 155, 150

165  _(_x) e real & _x e real & x e real

Join, 164, 147

166  _(_x)+_x+x=_(_x)+(_x+x)

Detach, 163, 165

167  _(_x)+(_x+x)=0+x

Substitute, 166, 160

Apply commutativity of +

168  ALL(b):[_x e real & b e real => _x+b=b+_x]

U Spec, 4

169  _x e real & x e real => _x+x=x+_x

U Spec, 168

170  _x e real & x e real

Join, 150, 147

171  _x+x=x+_x

Detach, 169, 170

172  _(_x)+(x+_x)=0+x

Substitute, 171, 167

Apply definition of '_' for x

173  x e real => x+_x=0

U Spec, 8

174  x+_x=0

Detach, 173, 147

175  _(_x)+0=0+x

Substitute, 174, 172

Apply definition of 0

176  _(_x) e real => _(_x)+0=_(_x)

U Spec, 6

177  _(_x)+0=_(_x)

Detach, 176, 155

178  _(_x)=0+x

Substitute, 177, 175

Apply commutativity of +

179  ALL(b):[0 e real & b e real => 0+b=b+0]

U Spec, 4

180  0 e real & x e real => 0+x=x+0

U Spec, 179

181  0 e real & x e real

Join, 5, 147

182  0+x=x+0

Detach, 180, 181

183  _(_x)=x+0

Substitute, 182, 178

Apply definiton of 0

184  x e real => x+0=x

U Spec, 6

185  x+0=x

Detach, 184, 147

186  _(_x)=x

Substitute, 185, 183

Lemma 5

-------

As Required:

187  ALL(a):[a e real => _(_a)=a]

4 Conclusion, 147

Lemma 6

-------

Prove: ALL(a):[a e real => a*0=0]

Suppose...

188  x e real

Premise

189  x*0=x*0

Reflex

Apply definiton of 0

190  0 e real => 0+0=0

U Spec, 6

191  0+0=0

Detach, 190, 5

192  x*0=x*(0+0)

Substitute, 191, 189

Apply distributivity

193  ALL(b):ALL(c):[x e real & b e real & c e real => x*(b+c)=x*b+x*c]

U Spec, 12

194  ALL(c):[x e real & 0 e real & c e real => x*(0+c)=x*0+x*c]

U Spec, 193

195  x e real & 0 e real & 0 e real => x*(0+0)=x*0+x*0

U Spec, 194

196  x e real & 0 e real

Join, 188, 5

197  x e real & 0 e real & 0 e real

Join, 196, 5

198  x*(0+0)=x*0+x*0

Detach, 195, 197

199  x*0=x*0+x*0

Substitute, 198, 192

200  x*0+_(x*0)=x*0+_(x*0)

Reflex

201  x*0+_(x*0)=x*0+x*0+_(x*0)

Substitute, 199, 200

Apply definition of '_'

202  x*0 e real => x*0+_(x*0)=0

U Spec, 8

203  ALL(b):[x e real & b e real => x*b e real]

U Spec, 9

204  x e real & 0 e real => x*0 e real

U Spec, 203

205  x e real & 0 e real

Join, 188, 5

206  x*0 e real

Detach, 204, 205

207  x*0+_(x*0)=0

Detach, 202, 206

208  0=x*0+x*0+_(x*0)

Substitute, 207, 201

Apply associativity of +

209  ALL(b):ALL(c):[x*0 e real & b e real & c e real => x*0+b+c=x*0+(b+c)]

U Spec, 3

210  ALL(c):[x*0 e real & x*0 e real & c e real => x*0+x*0+c=x*0+(x*0+c)]

U Spec, 209

211  x*0 e real & x*0 e real & _(x*0) e real => x*0+x*0+_(x*0)=x*0+(x*0+_(x*0))

U Spec, 210

212  x*0 e real => _(x*0) e real

U Spec, 7

213  _(x*0) e real

Detach, 212, 206

214  x*0 e real & x*0 e real

Join, 206, 206

215  x*0 e real & x*0 e real & _(x*0) e real

Join, 214, 213

216  x*0+x*0+_(x*0)=x*0+(x*0+_(x*0))

Detach, 211, 215

217  0=x*0+(x*0+_(x*0))

Substitute, 216, 208

218  0=x*0+0

Substitute, 207, 217

Apply definition of 0

219  x*0 e real => x*0+0=x*0

U Spec, 6

220  x*0+0=x*0

Detach, 219, 206

221  0=x*0

Substitute, 220, 218

222  x*0=0

Sym, 221

Lemma 6

-------

As Required:

223  ALL(a):[a e real => a*0=0]

4 Conclusion, 188

Lemma 7

-------

negative * negative = positive

First, prove: ALL(a):ALL(b):[a e real & b e real => _(a*b)=a*_b]

Suppose...

224  x e real & y e real

Premise

225  x e real

Split, 224

226  y e real

Split, 224

Apply Lemma 6

227  x e real => x*0=0

U Spec, 223

228  x*0=0

Detach, 227, 225

229  0=x*0

Sym, 228

Apply definition of '_'

230  y e real => y+_y=0

U Spec, 8

231  y+_y=0

Detach, 230, 226

232  0=x*(y+_y)

Substitute, 231, 229

Apply distributivity

233  ALL(b):ALL(c):[x e real & b e real & c e real => x*(b+c)=x*b+x*c]

U Spec, 12

234  ALL(c):[x e real & y e real & c e real => x*(y+c)=x*y+x*c]

U Spec, 233

235  x e real & y e real & _y e real => x*(y+_y)=x*y+x*_y

U Spec, 234

236  y e real => _y e real

U Spec, 7

237  _y e real

Detach, 236, 226

238  x e real & y e real & _y e real

Join, 224, 237

239  x*(y+_y)=x*y+x*_y

Detach, 235, 238

240  0=x*y+x*_y

Substitute, 239, 232

241  0+_(x*y)=0+_(x*y)

Reflex

242  0+_(x*y)=x*y+x*_y+_(x*y)

Substitute, 240, 241

Apply commutativity of +

243  ALL(b):[0 e real & b e real => 0+b=b+0]

U Spec, 4

244  0 e real & _(x*y) e real => 0+_(x*y)=_(x*y)+0

U Spec, 243

245  ALL(b):[x e real & b e real => x*b e real]

U Spec, 9

246  x e real & y e real => x*y e real

U Spec, 245

247  x*y e real

Detach, 246, 224

248  x*y e real => _(x*y) e real

U Spec, 7

249  _(x*y) e real

Detach, 248, 247

250  0 e real & _(x*y) e real

Join, 5, 249

251  0+_(x*y)=_(x*y)+0

Detach, 244, 250

252  _(x*y)+0=x*y+x*_y+_(x*y)

Substitute, 251, 242

Apply definition of 0

253  _(x*y) e real => _(x*y)+0=_(x*y)

U Spec, 6

254  _(x*y)+0=_(x*y)

Detach, 253, 249

255  _(x*y)=x*y+x*_y+_(x*y)

Substitute, 254, 252

Apply commutativity of +

256  ALL(b):[x*y e real & b e real => x*y+b=b+x*y]

U Spec, 4

257  x*y e real & x*_y e real => x*y+x*_y=x*_y+x*y

U Spec, 256

258  ALL(b):[x e real & b e real => x*b e real]

U Spec, 9

259  x e real & _y e real => x*_y e real

U Spec, 258

260  x e real & _y e real

Join, 225, 237

261  x*_y e real

Detach, 259, 260

262  x*y e real & x*_y e real

Join, 247, 261

263  x*y+x*_y=x*_y+x*y

Detach, 257, 262

264  _(x*y)=x*_y+x*y+_(x*y)

Substitute, 263, 255

Apply associativity of +

265  ALL(b):ALL(c):[x*_y e real & b e real & c e real => x*_y+b+c=x*_y+(b+c)]

U Spec, 3

266  ALL(c):[x*_y e real & x*y e real & c e real => x*_y+x*y+c=x*_y+(x*y+c)]

U Spec, 265

267  x*_y e real & x*y e real & _(x*y) e real => x*_y+x*y+_(x*y)=x*_y+(x*y+_(x*y))

U Spec, 266

268  x*_y e real & x*y e real

Join, 261, 247

269  x*_y e real & x*y e real & _(x*y) e real

Join, 268, 249

270  x*_y+x*y+_(x*y)=x*_y+(x*y+_(x*y))

Detach, 267, 269

271  _(x*y)=x*_y+(x*y+_(x*y))

Substitute, 270, 264

Apply definition of '_'

272  x*y e real => x*y+_(x*y)=0

U Spec, 8

273  x*y+_(x*y)=0

Detach, 272, 247

274  _(x*y)=x*_y+0

Substitute, 273, 271

Apply definition of 0

275  x*_y e real => x*_y+0=x*_y

U Spec, 6

276  x*_y+0=x*_y

Detach, 275, 261

277  _(x*y)=x*_y

Substitute, 276, 274

As Required:

278  ALL(a):ALL(b):[a e real & b e real => _(a*b)=a*_b]

4 Conclusion, 224

Prove: ALL(a):ALL(b):[a e real & b e real => _a*_b=a*b]

Suppose...

279  x e real & y e real

Premise

280  x e real

Split, 279

281  y e real

Split, 279

282  x e real => _x e real

U Spec, 7

283  _x e real

Detach, 282, 280

284  y e real => _y e real

U Spec, 7

285  _y e real

Detach, 284, 281

Apply previous result for _x and y

286  ALL(b):[_x e real & b e real => _(_x*b)=_x*_b]

U Spec, 278

287  _x e real & y e real => _(_x*y)=_x*_y

U Spec, 286

288  _x e real & y e real

Join, 283, 281

289  _(_x*y)=_x*_y

Detach, 287, 288

Apply previous result for y and x

290  ALL(b):[y e real & b e real => _(y*b)=y*_b]

U Spec, 278

291  y e real & x e real => _(y*x)=y*_x

U Spec, 290

292  y e real & x e real

Join, 281, 280

293  _(y*x)=y*_x

Detach, 291, 292

Apply commutativity of *

294  ALL(b):[y e real & b e real => y*b=b*y]

U Spec, 11

295  y e real & x e real => y*x=x*y

U Spec, 294

296  y e real & x e real

Join, 281, 280

297  y*x=x*y

Detach, 295, 296

298  _(x*y)=y*_x

Substitute, 297, 293

299  y e real & _x e real => y*_x=_x*y

U Spec, 294

300  y e real & _x e real

Join, 281, 283

301  y*_x=_x*y

Detach, 299, 300

302  _(x*y)=_x*y

Substitute, 301, 298

303  _(_(x*y))=_x*_y

Substitute, 302, 289

Apply Lemma 5

304  x*y e real => _(_(x*y))=x*y

U Spec, 187

305  ALL(b):[x e real & b e real => x*b e real]

U Spec, 9

306  x e real & y e real => x*y e real

U Spec, 305

307  x*y e real

Detach, 306, 279

308  _(_(x*y))=x*y

Detach, 304, 307

309  x*y=_x*_y

Substitute, 308, 303

310  _x*_y=x*y

Sym, 309

Lemma 7

-------

negative * negative = positive

As Required:

311  ALL(a):ALL(b):[a e real & b e real => _a*_b=a*b]

4 Conclusion, 279

Lemma 8

-------

Prove: 0<1

Suppose...

312  1<0

Premise

Apply Lemma 3

313  ALL(b):[1 e real & b e real => [1<b => _b<_1]]

U Spec, 107

314  1 e real & 0 e real => [1<0 => _0<_1]

U Spec, 313

315  1 e real & 0 e real

Join, 13, 5

316  1<0 => _0<_1

Detach, 314, 315

317  _0<_1

Detach, 316, 312

318  0<_1

Substitute, 35, 317

Apply multiplicative compatibility

319  ALL(b):ALL(c):[0 e real & b e real & c e real

=> [0<b & 0<c => 0*c<b*c]]

U Spec, 21

320  ALL(c):[0 e real & _1 e real & c e real

=> [0<_1 & 0<c => 0*c<_1*c]]

U Spec, 319

321  0 e real & _1 e real & _1 e real

=> [0<_1 & 0<_1 => 0*_1<_1*_1]

U Spec, 320

322  1 e real => _1 e real

U Spec, 7

323  _1 e real

Detach, 322, 13

324  0 e real & _1 e real

Join, 5, 323

325  0 e real & _1 e real & _1 e real

Join, 324, 323

326  0<_1 & 0<_1 => 0*_1<_1*_1

Detach, 321, 325

327  0<_1 & 0<_1

Join, 318, 318

328  0*_1<_1*_1

Detach, 326, 327

Apply commutativity of *

329  ALL(b):[0 e real & b e real => 0*b=b*0]

U Spec, 11

330  0 e real & _1 e real => 0*_1=_1*0

U Spec, 329

331  0 e real & _1 e real

Join, 5, 323

332  0*_1=_1*0

Detach, 330, 331

333  _1*0<_1*_1

Substitute, 332, 328

Apply Lemma 6

334  _1 e real => _1*0=0

U Spec, 223

335  _1*0=0

Detach, 334, 323

336  0<_1*_1

Substitute, 335, 333

Apply Lemma 7

337  ALL(b):[1 e real & b e real => _1*_b=1*b]

U Spec, 311

338  1 e real & 1 e real => _1*_1=1*1

U Spec, 337

339  1 e real & 1 e real

Join, 13, 13

340  _1*_1=1*1

Detach, 338, 339

341  0<1*1

Substitute, 340, 336

Apply definition of 1

342  1 e real => 1*1=1

U Spec, 15

343  1*1=1

Detach, 342, 13

344  0<1

Substitute, 343, 341

Apply transitivity

345  ALL(b):ALL(c):[1 e real & b e real & c e real

=> [1<b & b<c => 1<c]]

U Spec, 19

346  ALL(c):[1 e real & 0 e real & c e real

=> [1<0 & 0<c => 1<c]]

U Spec, 345

347  1 e real & 0 e real & 1 e real

=> [1<0 & 0<1 => 1<1]

U Spec, 346

348  1 e real & 0 e real

Join, 13, 5

349  1 e real & 0 e real & 1 e real

Join, 348, 13

350  1<0 & 0<1 => 1<1

Detach, 347, 349

351  1<0 & 0<1

Join, 312, 344

352  1<1

Detach, 350, 351

Apply Lemma 2

353  1 e real => ~1<1

U Spec, 49

354  ~1<1

Detach, 353, 13

355  1<1 & ~1<1

Join, 352, 354

As Required:

356  ~1<0

4 Conclusion, 312

Apply trichotomy rule

357  ALL(b):[1 e real & b e real

=> [1<b | 1=b | b<1]

& ~[1<b & 1=b]

& ~[1<b & b<1]

& ~[1=b & b<1]]

U Spec, 18

358  1 e real & 0 e real

=> [1<0 | 1=0 | 0<1]

& ~[1<0 & 1=0]

& ~[1<0 & 0<1]

& ~[1=0 & 0<1]

U Spec, 357

359  1 e real & 0 e real

Join, 13, 5

360  [1<0 | 1=0 | 0<1]

& ~[1<0 & 1=0]

& ~[1<0 & 0<1]

& ~[1=0 & 0<1]

Detach, 358, 359

361  1<0 | 1=0 | 0<1

Split, 360

362  ~[1<0 & 1=0]

Split, 360

363  ~[1<0 & 0<1]

Split, 360

364  ~[1=0 & 0<1]

Split, 360

365  ~1=0

Sym, 14

366  ~1<0 & ~1=0

Join, 356, 365

367  ~[1<0 | 1=0] => 0<1

Imply-Or, 361

368  ~~[~1<0 & ~1=0] => 0<1

DeMorgan, 367

369  ~1<0 & ~1=0 => 0<1

Rem DNeg, 368

Lemma 8

-------

370  0<1

Detach, 369, 366

Lemma 9

-------

Prove: ALL(a):ALL(b):ALL(c):[a e real & b e real & c e real => [a<b & 0<c => a<b+c]]

Suppose...

371  x e real & y e real & z e real

Premise

372  x e real

Split, 371

373  y e real

Split, 371

374  z e real

Split, 371

Prove: x<y & 0<z => x<y+z

Suppose...

375  x<y & 0<z

Premise

376  x<y

Split, 375

377  0<z

Split, 375

378  ALL(b):ALL(c):[x e real & b e real & c e real

=> [x<b => x+c<b+c]]

U Spec, 20

379  ALL(c):[x e real & y e real & c e real

=> [x<y => x+c<y+c]]

U Spec, 378

380  x e real & y e real & _x e real

=> [x<y => x+_x<y+_x]

U Spec, 379

381  x e real => _x e real

U Spec, 7

382  _x e real

Detach, 381, 372

383  x e real & y e real

Join, 372, 373

384  x e real & y e real & _x e real

Join, 383, 382

385  x<y => x+_x<y+_x

Detach, 380, 384

386  x+_x<y+_x

Detach, 385, 376

Apply definition of '_'

387  x e real => x+_x=0

U Spec, 8

388  x+_x=0

Detach, 387, 372

389  0<y+_x

Substitute, 388, 386

Apply Lemma 6

390  ALL(b):[y+_x e real & b e real => [0<y+_x & 0<b => 0<b+(y+_x)]]

U Spec, 146

391  y+_x e real & z e real => [0<y+_x & 0<z => 0<z+(y+_x)]

U Spec, 390

Apply definition of +

392  ALL(b):[y e real & b e real => y+b e real]

U Spec, 2

393  y e real & _x e real => y+_x e real

U Spec, 392

394  y e real & _x e real

Join, 373, 382

395  y+_x e real

Detach, 393, 394

396  y+_x e real & z e real

Join, 395, 374

397  0<y+_x & 0<z => 0<z+(y+_x)

Detach, 391, 396

398  0<y+_x & 0<z

Join, 389, 377

399  0<z+(y+_x)

Detach, 397, 398

Apply associativity of +

400  ALL(b):ALL(c):[z e real & b e real & c e real => z+b+c=z+(b+c)]

U Spec, 3

401  ALL(c):[z e real & y e real & c e real => z+y+c=z+(y+c)]

U Spec, 400

402  z e real & y e real & _x e real => z+y+_x=z+(y+_x)

U Spec, 401

403  z e real & y e real

Join, 374, 373

404  z e real & y e real & _x e real

Join, 403, 382

405  z+y+_x=z+(y+_x)

Detach, 402, 404

406  0<z+y+_x

Substitute, 405, 399

407  ALL(b):ALL(c):[0 e real & b e real & c e real

=> [0<b => 0+c<b+c]]

U Spec, 20

408  ALL(c):[0 e real & z+y+_x e real & c e real

=> [0<z+y+_x => 0+c<z+y+_x+c]]

U Spec, 407

409  0 e real & z+y+_x e real & x e real

=> [0<z+y+_x => 0+x<z+y+_x+x]

U Spec, 408

Apply definition of +

410  ALL(b):[z e real & b e real => z+b e real]

U Spec, 2

411  z e real & y e real => z+y e real

U Spec, 410

412  z e real & y e real

Join, 374, 373

413  z+y e real

Detach, 411, 412

Apply definition of +

414  ALL(b):[z+y e real & b e real => z+y+b e real]

U Spec, 2

415  z+y e real & _x e real => z+y+_x e real

U Spec, 414

416  z+y e real & _x e real

Join, 413, 382

417  z+y+_x e real

Detach, 415, 416

418  0 e real & z+y+_x e real

Join, 5, 417

419  0 e real & z+y+_x e real & x e real

Join, 418, 372

420  0<z+y+_x => 0+x<z+y+_x+x

Detach, 409, 419

421  0+x<z+y+_x+x

Detach, 420, 406

Apply associativity of +

422  ALL(b):ALL(c):[z+y e real & b e real & c e real => z+y+b+c=z+y+(b+c)]

U Spec, 3

423  ALL(c):[z+y e real & _x e real & c e real => z+y+_x+c=z+y+(_x+c)]

U Spec, 422

424  z+y e real & _x e real & x e real => z+y+_x+x=z+y+(_x+x)

U Spec, 423

425  z+y e real & _x e real

Join, 413, 382

426  z+y e real & _x e real & x e real

Join, 425, 372

427  z+y+_x+x=z+y+(_x+x)

Detach, 424, 426

428  0+x<z+y+(_x+x)

Substitute, 427, 421

Apply commutativity of +

429  ALL(b):[_x e real & b e real => _x+b=b+_x]

U Spec, 4

430  _x e real & x e real => _x+x=x+_x

U Spec, 429

431  _x e real & x e real

Join, 382, 372

432  _x+x=x+_x

Detach, 430, 431

433  0+x<z+y+(x+_x)

Substitute, 432, 428

Apply definition of '_'

434  x e real => x+_x=0

U Spec, 8

435  x+_x=0

Detach, 434, 372

436  0+x<z+y+0

Substitute, 435, 433

Apply definition of 0

437  z+y e real => z+y+0=z+y

U Spec, 6

438  z+y+0=z+y

Detach, 437, 413

439  0+x<z+y

Substitute, 438, 436

Apply commutativity of +

440  ALL(b):[z e real & b e real => z+b=b+z]

U Spec, 4

441  z e real & y e real => z+y=y+z

U Spec, 440

442  z e real & y e real

Join, 374, 373

443  z+y=y+z

Detach, 441, 442

444  0+x<y+z

Substitute, 443, 439

Apply commutativity of +

445  ALL(b):[0 e real & b e real => 0+b=b+0]

U Spec, 4

446  0 e real & x e real => 0+x=x+0

U Spec, 445

447  0 e real & x e real

Join, 5, 372

448  0+x=x+0

Detach, 446, 447

449  x+0<y+z

Substitute, 448, 444

Apply definition of 0

450  x e real => x+0=x

U Spec, 6

451  x+0=x

Detach, 450, 372

452  x<y+z

Substitute, 451, 449

As Required:

453  x<y & 0<z => x<y+z

4 Conclusion, 375

Lemma 9

-------

As Required:

454  ALL(a):ALL(b):ALL(c):[a e real & b e real & c e real => [a<b & 0<c => a<b+c]]

4 Conclusion, 371