Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

### Equalities and Inequalities in Real Numbers

by
Andrzej Kondracki

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;

```