The abstract of the Mizar article:

Equalities and Inequalities in Real Numbers

by

Andrzej Kondracki

Received September 5, 1990

MML identifier: REAL_2

[ Mizar article, MML identifier index ]

environ

 vocabulary ARYTM, ARYTM_1, ARYTM_3, RELAT_1, BOOLE;
 notation XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1;
 constructors REAL_1, XREAL_0, MEMBERED, XBOOLE_0;
 clusters XREAL_0, MEMBERED, ZFMISC_1, XBOOLE_0;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin

 reserve a,b,d,e for real number;

canceled 62;

theorem :: REAL_2:63
   for a,b ex e st a=b-e;

theorem :: REAL_2:64
   for a,b st a<>0 & b<>0 ex e st a=b/e;

canceled 40;

theorem :: REAL_2:105
 (a+-b<=0 or b-a>=0 or b+-a>=0
or a-e<=b+-e or a+-e<=b-e or e-a>=e-b) implies a<=b;

theorem :: REAL_2:106
 (a+-b<0 or b-a>0 or -a+b>0 or a-e<b+-e or a+-e<b-e or e-a>e-b) implies a<b;

canceled 2;

theorem :: REAL_2:109
 a<=-b implies a+b<=0 & -a>=b;

theorem :: REAL_2:110
 a<-b implies a+b<0 & -a>b;

theorem :: REAL_2:111
   -a<=b implies a+b>=0;

theorem :: REAL_2:112
   -b<a implies a+b>0;

canceled 4;

theorem :: REAL_2:117
   b>0 implies (a/b>1 implies a>b) & (a/b<1 implies a<b)
           & (a/b>-1 implies a>-b & b>-a) & (a/b<-1 implies a<-b & b<-a);

theorem :: REAL_2:118
   b>0 implies (a/b>=1 implies a>=b) & (a/b<=1 implies a<=b)
           & (a/b>=-1 implies a>=-b & b>=-a) & (a/b<=-1 implies a<=-b & b<=-a);

theorem :: REAL_2:119
   b<0 implies (a/b>1 implies a<b) & (a/b<1 implies a>b)
      & (a/b>-1 implies a<-b & b<-a) & (a/b<-1 implies a>-b & b>-a);

theorem :: REAL_2:120
   b<0 implies (a/b>=1 implies a<=b) & (a/b<=1 implies a>=b)
           & (a/b>=-1 implies a<=-b & b<=-a) & (a/b<=-1 implies a>=-b & b>=-a);

theorem :: REAL_2:121
   a>=0 & b>=0 or a<=0 & b<=0 implies a*b>=0;

theorem :: REAL_2:122
   a<0 & b<0 or a>0 & b>0 implies a*b>0;

theorem :: REAL_2:123
   a>=0 & b<=0 or a<=0 & b>=0 implies a*b<=0;

canceled;

theorem :: REAL_2:125
 a<=0 & b<=0 or a>=0 & b>=0 implies a/b>=0;

theorem :: REAL_2:126
 a>=0 & b<0 or a<=0 & b>0 implies a/b<=0;

theorem :: REAL_2:127
 a>0 & b>0 or a<0 & b<0 implies a/b>0;

theorem :: REAL_2:128
 a<0 & b>0 implies a/b<0 & b/a<0;

theorem :: REAL_2:129
   a*b<=0 implies a>=0 & b<=0 or a<=0 & b>=0;

canceled 2;

theorem :: REAL_2:132
   a*b<0 implies a>0 & b<0 or a<0 & b>0;

theorem :: REAL_2:133
   b<>0 & a/b<=0 implies b>0 & a<=0 or b<0 & a>=0;

theorem :: REAL_2:134
   b<>0 & a/b>=0 implies b>0 & a>=0 or b<0 & a<=0;

theorem :: REAL_2:135
   b<>0 & a/b<0 implies b<0 & a>0 or b>0 & a<0;

theorem :: REAL_2:136
   b<>0 & a/b>0 implies b>0 & a>0 or b<0 & a<0;

theorem :: REAL_2:137
   a>1 & (b>1 or b>=1) or a<-1 & (b<-1 or b<=-1) implies a*b>1;

theorem :: REAL_2:138
   a>=1 & b>=1 or a<=-1 & b<=-1 implies a*b>=1;

theorem :: REAL_2:139
    0<=a & a<1 & 0<=b & b<=1 or 0>=a & a>-1 & 0>=b & b>=-1 implies a*b<1;

theorem :: REAL_2:140
    0<=a & a<=1 & 0<=b & b<=1 or 0>=a & a>=-1 & 0>=b & b>=-1 implies a*b<=1;

canceled;

theorem :: REAL_2:142
    0<a & a<b or b<a & a<0 implies a/b<1 & b/a>1;

theorem :: REAL_2:143
    0<a & a<=b or b<=a & a<0 implies a/b<=1 & b/a>=1;

theorem :: REAL_2:144
    a>0 & b>1 or a<0 & b<1 implies a*b>a;

theorem :: REAL_2:145
    a>0 & b<1 or a<0 & b>1 implies a*b<a;

theorem :: REAL_2:146
   a>=0 & b>=1 or a<=0 & b<=1 implies a*b>=a;

theorem :: REAL_2:147
   a>=0 & b<=1 or a<=0 & b>=1 implies a*b<=a;

canceled;

theorem :: REAL_2:149
 a<0 implies 1/a<0 & a"<0;

theorem :: REAL_2:150
   (1/a<0 implies a<0) & (1/a>0 implies a>0);

theorem :: REAL_2:151
 (0<a or b<0) & a<b implies 1/a>1/b;

theorem :: REAL_2:152
 (0<a or b<0) & a<=b implies 1/a>=1/b;

theorem :: REAL_2:153
 a<0 & b>0 implies 1/a<1/b;

theorem :: REAL_2:154
   (1/b>0 or 1/a<0) & 1/a>1/b implies a<b;

theorem :: REAL_2:155
   (1/b>0 or 1/a<0) & 1/a>=1/b implies a<=b;

theorem :: REAL_2:156
    1/a<0 & 1/b>0 implies a<b;

theorem :: REAL_2:157
   a<-1 implies 1/a>-1;

theorem :: REAL_2:158
   a<=-1 implies 1/a>=-1;

canceled 5;

theorem :: REAL_2:164
   1<=a implies 1/a<=1;

theorem :: REAL_2:165
   (b<=e-a implies a<=e-b) & (b>=e-a implies a>=e-b);

canceled;

theorem :: REAL_2:167
 a+b<=e+d implies a-e<=d-b;

theorem :: REAL_2:168
 a+b<e+d implies a-e<d-b;

theorem :: REAL_2:169
   a-b<=e-d implies a+d<=e+b & a-e<=b-d & e-a>=d-b & b-a>=d-e;

theorem :: REAL_2:170
   a-b<e-d implies a+d<e+b & a-e<b-d & e-a>d-b & b-a>d-e;

theorem :: REAL_2:171
    (a+b<=e-d implies a+d<=e-b) & (a+b>=e-d implies a+d>=e-b);

canceled;

theorem :: REAL_2:173
   (a<0 implies a+b<b & b-a>b) & (a+b<b or b-a>b implies a<0);

theorem :: REAL_2:174
   (a<=0 implies a+b<=b & b-a>=b) & (a+b<=b or b-a>=b implies a<=0);

canceled 2;

theorem :: REAL_2:177
  (b>0 & a*b<=e implies a<=e/b) & (b<0 & a*b<=e implies a>=e/b) &
  (b>0 & a*b>=e implies a>=e/b) & (b<0 & a*b>=e implies a<=e/b);

theorem :: REAL_2:178
  (b>0 & a*b<e implies a<e/b) & (b<0 & a*b<e implies a>e/b) &
  (b>0 & a*b>e implies a>e/b) & (b<0 & a*b>e implies a<e/b);

canceled 2;

theorem :: REAL_2:181
   (for a st a>0 holds b+a>=e) or (for a st a<0 holds b-a>=e) implies b>=e;

theorem :: REAL_2:182
   (for a st a>0 holds b-a<=e) or (for a st a<0 holds b+a<=e) implies b<=e;

theorem :: REAL_2:183
 (for a st a>1 holds b*a>=e) or (for a st 0<a & a<1 holds b/a>=e) implies
   b>=e;

theorem :: REAL_2:184
   (for a st 0<a & a<1 holds b*a<=e)
or (for a st a>1 holds b/a<=e) implies b<=e;

theorem :: REAL_2:185
   (b>0 & d>0 or b<0 & d<0) & a*d<e*b implies a/b<e/d;

theorem :: REAL_2:186
   (b>0 & d<0 or b<0 & d>0) & a*d<e*b implies a/b>e/d;

theorem :: REAL_2:187
   (b>0 & d>0 or b<0 & d<0) & a*d<=e*b implies a/b<=e/d;

theorem :: REAL_2:188
   (b>0 & d<0 or b<0 & d>0) & a*d<=e*b implies a/b>=e/d;

canceled 4;

theorem :: REAL_2:193
   b<0 & d<0 or b>0 & d>0 implies
       (a*b<e/d implies a*d<e/b) & (a*b>e/d implies a*d>e/b);

theorem :: REAL_2:194
   b<0 & d>0 or b>0 & d<0 implies
       (a*b<e/d implies a*d>e/b) & (a*b>e/d implies a*d<e/b);

canceled 2;

theorem :: REAL_2:197
 (0<a or 0<=a) & (a<b or a<=b) & (0<e or 0<=e) & e<=d implies a*e<=b*d;

theorem :: REAL_2:198
   0>=a & a>=b & 0>=e & e>=d implies a*e<=b*d;

theorem :: REAL_2:199
   0<a & a<=b & 0<e & e<d or 0>a & a>=b & 0>e & e>d implies a*e<b*d;

theorem :: REAL_2:200
    (e>0 & a>0 & a<b implies e/a>e/b) &
    (e>0 & b<0 & a<b implies e/a>e/b);

theorem :: REAL_2:201
   e>=0 & (a>0 or b<0) & a<=b implies e/a>=e/b;

theorem :: REAL_2:202
   e<0 & (a>0 or b<0) & a<b implies e/a<e/b;

theorem :: REAL_2:203
   e<=0 & (a>0 or b<0) & a<=b implies e/a<=e/b;

theorem :: REAL_2:204
   for X,Y being Subset of REAL st
  X<>{} & Y<>{} & for a,b st a in X & b in Y holds a<=b
 holds ex d st (for a st a in X holds a<=d) & for b st b in Y holds d<=b;