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

Download at http://www.dcproof.com

 

 

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

 

Additive Compatibility

 

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

 

          Apply additive compatibility

 

            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

 

          Apply additive compatibility

 

            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

 

     Add x to both sides

 

      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

 

     Add _(x*0) to both sides

 

      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

 

     Add _(x*y) to both sides

 

      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

 

     Obtain contradiction...

 

      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

 

          Apply additive compatiblity

 

            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

 

          Apply additive compatibility

 

            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