The Mizar article:

Equalities and Inequalities in Real Numbers

by
Andrzej Kondracki

Received September 5, 1990

Copyright (c) 1990 Association of Mizar Users

MML identifier: REAL_2
[ 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;
 theorems REAL_1, SQUARE_1, SEQ_2, AXIOMS, TARSKI, XREAL_0, XCMPLX_0, XCMPLX_1;

begin

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

canceled 62;

Lm1: 1/1=1 & 1"=1 & 1/(-1)=-1 & (-1)"=-1 & (-1)*(-1)=1;

theorem
   for a,b ex e st a=b-e
  proof
   let a,b;
   take b-a;
   thus thesis by XCMPLX_1:18;
  end;

theorem
   for a,b st a<>0 & b<>0 ex e st a=b/e
  proof
   let a,b; assume A1:a<>0 & b<>0;
   then A2:a"<>0 by XCMPLX_1:203;
   take e=b/a;
     e=b*a" by XCMPLX_0:def 9;
   then A3:e<>0 by A1,A2,XCMPLX_1:6;
   thus a=a*1
        .=a*(e*e") by A3,XCMPLX_0:def 7
        .=a*e*e" by XCMPLX_1:4
        .=a*(a"*b)*e" by XCMPLX_0:def 9
        .=a*a"*b*e" by XCMPLX_1:4
        .=1*b*e" by A1,XCMPLX_0:def 7
        .=b/e by XCMPLX_0:def 9;
  end;

canceled 40;

theorem Th105:
 (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
 proof
  assume
  A1: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;
    now per cases by A1;
   suppose a+-b<=0; then a+-b+b<=0+b by AXIOMS:24;
    hence a<=b by XCMPLX_1:139;
   suppose b-a>=0; then b-a+a>=0+a by AXIOMS:24;
    hence b>=a by XCMPLX_1:27;
   suppose b+-a>=0; then b+-a+a>=0+a by AXIOMS:24;
    hence b>=a by XCMPLX_1:139;
   suppose a-e<=b+-e; then a-e<=b-e by XCMPLX_0:def 8;hence a<=b by REAL_1:54;
   suppose a+-e<=b-e; then a-e<=b-e by XCMPLX_0:def 8;hence a<=b by REAL_1:54;
   suppose e-a>=e-b; then -(e-a)<=-(e-b) by REAL_1:50;
    then a-e<=-(e-b) by XCMPLX_1:143; then a-e<=b-e by XCMPLX_1:143;
    hence a<=b by REAL_1:54;
  end;
  hence thesis;
 end;

theorem Th106:
 (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
 proof
  assume A1: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;
    now per cases by A1;
   suppose a+-b<0; then a+-b+b<0+b by REAL_1:53;
    hence a<b by XCMPLX_1:139;
   suppose b-a>0; then b-a+a>0+a by REAL_1:53;
    hence b>a by XCMPLX_1:27;
   suppose b+-a>0; then b+-a+a>0+a by REAL_1:53;
    hence b>a by XCMPLX_1:139;
   suppose a-e<b+-e; then a-e<b-e by XCMPLX_0:def 8;hence a<b by REAL_1:49;
   suppose a+-e<b-e; then a-e<b-e by XCMPLX_0:def 8;hence a<b by REAL_1:49;
   suppose e-a>e-b; then -(e-a)<-(e-b) by REAL_1:50;
    then a-e<-(e-b) by XCMPLX_1:143; then a-e<b-e by XCMPLX_1:143;
    hence a<b by REAL_1:49;
  end;
  hence thesis;
 end;

canceled 2;

theorem Th109:
 a<=-b implies a+b<=0 & -a>=b
  proof
   assume a<=-b; then a+b<=-b+b by AXIOMS:24;
   hence a+b<=0 by XCMPLX_0:def 6;
   then b--a<=0 by XCMPLX_1:151;hence b<=-a by SQUARE_1:11;
  end;

theorem Th110:
 a<-b implies a+b<0 & -a>b
  proof
   assume a<-b; then a+b<-b+b by REAL_1:53;
   hence a+b<0 by XCMPLX_0:def 6;
   then b--a<0 by XCMPLX_1:151;hence b<-a by SQUARE_1:12;
  end;

theorem
   -a<=b implies a+b>=0
  proof
   assume b>=-a; then b+a>=-a+a by AXIOMS:24;
   hence a+b>=0 by XCMPLX_0:def 6;
  end;

theorem
   -b<a implies a+b>0
  proof
   assume a>-b; then a+b>-b+b by REAL_1:53;
   hence a+b>0 by XCMPLX_0:def 6;
  end;

canceled 4;

theorem
   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)
  proof
   assume A1:b>0;
   A2:now assume a/b>1; then a/b*b>1*b by A1,REAL_1:70;
    hence a>b by A1,XCMPLX_1:88;end;
   A3:now assume a/b<1; then a/b*b<1*b by A1,REAL_1:70;
    hence a<b by A1,XCMPLX_1:88;end;
   A4:now assume a/b>-1; then a/b*b>(-1)*b by A1,REAL_1:70;
    then a>(-1)*b by A1,XCMPLX_1:88;hence a>-b by XCMPLX_1:180;
    hence b>-a by Th109;end;
     now assume a/b<-1; then a/b*b<(-1)*b by A1,REAL_1:70;
    then a<(-1)*b by A1,XCMPLX_1:88;hence a<-b by XCMPLX_1:180;
    hence -a>b by Th110;end;
   hence thesis by A2,A3,A4;
  end;

theorem
   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)
  proof
   assume A1:b>0;
   A2:now assume a/b>=1; then a/b*b>=1*b by A1,AXIOMS:25;
    hence a>=b by A1,XCMPLX_1:88;end;
   A3:now assume a/b<=1; then a/b*b<=1*b by A1,AXIOMS:25;
    hence a<=b by A1,XCMPLX_1:88;end;
   A4:now assume a/b>=-1; then a/b*b>=(-1)*b by A1,AXIOMS:25;
    then a>=(-1)*b by A1,XCMPLX_1:88;hence a>=-b by XCMPLX_1:180;
    hence b>=-a by Th110;end;
     now assume a/b<=-1; then a/b*b<=(-1)*b by A1,AXIOMS:25;
    then a<=(-1)*b by A1,XCMPLX_1:88;hence a<=-b by XCMPLX_1:180;
    hence -a>=b by Th109;end;
   hence thesis by A2,A3,A4;
  end;

theorem
   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)
  proof
   assume A1:b<0;
   A2:now assume a/b>1; then a/b*b<1*b by A1,REAL_1:71;
    hence a<b by A1,XCMPLX_1:88;end;
   A3:now assume a/b<1; then a/b*b>1*b by A1,REAL_1:71;
    hence a>b by A1,XCMPLX_1:88;end;
   A4:now assume a/b>-1; then a/b*b<(-1)*b by A1,REAL_1:71;
    then a<(-1)*b by A1,XCMPLX_1:88;hence a<-b by XCMPLX_1:180;
    hence b<-a by Th110;end;
     now assume a/b<-1; then a/b*b>(-1)*b by A1,REAL_1:71;
    then a>(-1)*b by A1,XCMPLX_1:88;hence a>-b by XCMPLX_1:180;
    hence -a<b by Th109;end;
   hence thesis by A2,A3,A4;
  end;

theorem
   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)
  proof
   assume A1:b<0;
   A2:now assume a/b>=1; then a/b*b<=1*b by A1,REAL_1:52;
    hence a<=b by A1,XCMPLX_1:88;end;
   A3:now assume a/b<=1; then a/b*b>=1*b by A1,REAL_1:52;
    hence a>=b by A1,XCMPLX_1:88;end;
   A4:now assume a/b>=-1; then a/b*b<=(-1)*b by A1,REAL_1:52;
    then a<=(-1)*b by A1,XCMPLX_1:88;hence a<=-b by XCMPLX_1:180;
    hence b<=-a by Th109;end;
     now assume a/b<=-1; then a/b*b>=(-1)*b by A1,REAL_1:52;
    then a>=(-1)*b by A1,XCMPLX_1:88;hence a>=-b by XCMPLX_1:180;
    hence -a<=b by Th110;end;
   hence thesis by A2,A3,A4;
  end;

theorem
   a>=0 & b>=0 or a<=0 & b<=0 implies a*b>=0
  proof
   assume A1: a>=0 & b>=0 or a<=0 & b<=0;
   per cases by A1;
    suppose a>=0 & b>=0; then a*b>=b*0 by AXIOMS:25;
     hence a*b>=0;
    suppose a<=0 & b<=0; then a*b>=b*0 by REAL_1:52;
     hence a*b>=0;
  end;

theorem
   a<0 & b<0 or a>0 & b>0 implies a*b>0
  proof
   A1:now assume a<0 & b<0; then a*b>0*b by REAL_1:71;
    hence a*b>0;end;
     now assume a>0 & b>0; then a*b>0*b by REAL_1:70;
    hence a*b>0;end;
   hence thesis by A1;
  end;

theorem
   a>=0 & b<=0 or a<=0 & b>=0 implies a*b<=0
  proof
   assume A1: a>=0 & b<=0 or a<=0 & b>=0;
   per cases by A1;
    suppose a>=0 & b<=0; then a*b<=b*0 by REAL_1:52;
     hence a*b<=0;
    suppose a<=0 & b>=0; then a*b<=b*0 by AXIOMS:25;
     hence a*b<=0;
  end;

canceled;

theorem Th125:
 a<=0 & b<=0 or a>=0 & b>=0 implies a/b>=0
  proof
   A1:now assume A2:a<=0 & b<=0;
      now per cases by A2;
         suppose a1: b < 0;
      now per cases by A2;
        suppose a<0; then a/b>0/b by a1,REAL_1:74;
      hence a/b>=0;
     suppose a=0;hence a/b>=0;
    end;hence a/b>=0;
    suppose b = 0; hence a/b>=0 by XCMPLX_1:49;
    end;
    hence a/b>=0;
   end;
     now assume A3:a>=0 & b>=0;
      per cases by A3;
       suppose b1: b > 0;
       now per cases by A3;
        suppose a>0;
        a/b>=0/b by b1,A3,REAL_1:73;
        hence a/b>=0;
        suppose a=0;hence a/b>=0;
      end;
      hence a/b>=0;
      suppose b = 0;
      hence a/b>=0 by XCMPLX_1:49;
   end;
   hence thesis by A1;
  end;

theorem Th126:
 a>=0 & b<0 or a<=0 & b>0 implies a/b<=0
  proof
   A1:now assume A2:a>=0 & b<0;
      now per cases by A2;
     suppose a>0; then a/b<0/b by A2,REAL_1:74;
      hence a/b<=0;
     suppose a=0;hence a/b<=0;
    end;
    hence a/b<=0;
   end;
     now assume A3:a<=0 & b>0;
      now per cases by A3;
     suppose a<0; then a/b<0/b by A3,REAL_1:73;
      hence a/b<=0;
     suppose a=0;hence a/b<=0;
    end;
    hence a/b<=0;
   end;
   hence thesis by A1;
  end;

theorem Th127:
 a>0 & b>0 or a<0 & b<0 implies a/b>0
  proof
   A1:now assume a>0 & b>0;
    then a/b>0/b by REAL_1:73;hence a/b>0;end;
     now assume a<0 & b<0;
    then a/b>0/b by REAL_1:74;hence a/b>0;end;
   hence thesis by A1;
  end;

theorem Th128:
 a<0 & b>0 implies a/b<0 & b/a<0
  proof
   assume A1:a<0 & b>0;
   then a/b<0/b by REAL_1:73;hence a/b<0;
     b/a<0/a by A1,REAL_1:74;hence b/a<0;
  end;

theorem
   a*b<=0 implies a>=0 & b<=0 or a<=0 & b>=0
  proof
   assume A1:a*b<=0;
   per cases;
    suppose A2:a<0; then a*b/a>=0 by A1,Th125;
     hence thesis by A2,XCMPLX_1:90;
    suppose A3:a>0; then a*b/a<=0 by A1,Th126;
     hence thesis by A3,XCMPLX_1:90;
    suppose a=0;
    hence thesis;
  end;

canceled 2;

theorem
   a*b<0 implies a>0 & b<0 or a<0 & b>0
  proof
   assume A1:a*b<0;
     now per cases;
    case A2:a<0; then a*b/a>0 by A1,Th127;
     hence thesis by A2,XCMPLX_1:90;
    case A3:a>0; then a*b/a<0 by A1,Th128;
     hence thesis by A3,XCMPLX_1:90;
    case a=0;
     hence contradiction by A1;
   end;
   hence thesis;
  end;

theorem
   b<>0 & a/b<=0 implies b>0 & a<=0 or b<0 & a>=0
  proof
   assume A1:b<>0 & a/b<=0;
   per cases;
    suppose A2:b<=0; then a/b*b>=0*b by A1,REAL_1:52;
     hence thesis by A1,A2,XCMPLX_1:88;
    suppose A3:b>=0; then a/b*b<=0*b by A1,AXIOMS:25;
     hence thesis by A1,A3,XCMPLX_1:88;
  end;

theorem
   b<>0 & a/b>=0 implies b>0 & a>=0 or b<0 & a<=0
  proof
   assume A1:b<>0 & a/b>=0;
   per cases;
    suppose A2:b<=0; then a/b*b<=0*b by A1,REAL_1:52;
     hence thesis by A1,A2,XCMPLX_1:88;
    suppose A3:b>=0; then a/b*b>=0*b by A1,AXIOMS:25;
     hence thesis by A1,A3,XCMPLX_1:88;
  end;

theorem
   b<>0 & a/b<0 implies b<0 & a>0 or b>0 & a<0
  proof
   assume A1:b<>0 & a/b<0;
   per cases by A1;
    case b<0; then a/b*b>0*b by A1,REAL_1:71;
     hence a>0 by A1,XCMPLX_1:88;
    case b>0; then a/b*b<0*b by A1,REAL_1:70;
     hence a<0 by A1,XCMPLX_1:88;
  end;

theorem
   b<>0 & a/b>0 implies b>0 & a>0 or b<0 & a<0
  proof
   assume A1:b<>0 & a/b>0;
   per cases by A1;
    suppose A2:b<0; then a/b*b<0*b by A1,REAL_1:71;
     hence thesis by A2,XCMPLX_1:88;
    suppose A3:b>0; then a/b*b>0*b by A1,REAL_1:70;
     hence thesis by A3,XCMPLX_1:88;
  end;

theorem
   a>1 & (b>1 or b>=1) or a<-1 & (b<-1 or b<=-1) implies a*b>1
  proof
   assume A1: a>1 & (b>1 or b>=1) or a<-1 & (b<-1 or b<=-1);
   per cases by A1;
    suppose A2:a>1 & b>=1;
     then b>0 by AXIOMS:22;
     then a*b>b*1 by A2,REAL_1:70;
     hence a*b>1 by A2,AXIOMS:22;
    suppose A3:a<-1 & b<=-1;
     then b<0 by AXIOMS:22;
     then a*b>b*(-1) by A3,REAL_1:71;
     then A4:a*b>-b by XCMPLX_1:180;
       -b>=--1 by A3,REAL_1:50;
     hence a*b>1 by A4,AXIOMS:22;
  end;

theorem
   a>=1 & b>=1 or a<=-1 & b<=-1 implies a*b>=1
  proof
   assume A1:a>=1 & b>=1 or a<=-1 & b<=-1;
   per cases by A1;
    suppose A2:a>=1 & b>=1; then b>=0 by AXIOMS:22;
     then a*b>=b*1 by A2,AXIOMS:25;
     hence a*b>=1 by A2,AXIOMS:22;
    suppose A3:a<=-1 & b<=-1;
     then 0>=b by AXIOMS:22;
     then a*b>=b*(-1) by A3,REAL_1:52;
     then A4:a*b>=-b by XCMPLX_1:180;
       -b>=--1 by A3,REAL_1:50;
     hence a*b>=1 by A4,AXIOMS:22;
  end;

theorem
    0<=a & a<1 & 0<=b & b<=1 or 0>=a & a>-1 & 0>=b & b>=-1 implies a*b<1
 proof
  assume A1: 0<=a & a<1 & 0<=b & b<=1
      or 0>=a & a>-1 & 0>=b & b>=-1;
  per cases by A1;
   suppose A2:0<=a & a<1 & 0<=b & b<=1;
    then a*b<=1*a by AXIOMS:25;
    hence a*b<1 by A2,AXIOMS:22;
   suppose A3:0>=a & a>-1 & 0>=b & b>=-1;
    then a*b<=(-1)*a by REAL_1:52;
    then A4:a*b<=-a by XCMPLX_1:180;
      -a<--1 by A3,REAL_1:50;
    hence a*b<1 by A4,AXIOMS:22;
 end;

theorem
    0<=a & a<=1 & 0<=b & b<=1 or 0>=a & a>=-1 & 0>=b & b>=-1 implies a*b<=1
  proof
   assume A1:0<=a & a<=1 & 0<=b & b<=1 or 0>=a & a>=-1 & 0>=b & b>=-1;
   per cases by A1;
   suppose A2:0<=a & a<=1 & 0<=b & b<=1;
    then a*b<=1*a by AXIOMS:25;
    hence a*b<=1 by A2,AXIOMS:22;
   suppose A3:0>=a & a>=-1 & 0>=b & b>=-1;
    then a*b<=(-1)*a by REAL_1:52;
    then A4:a*b<=-a by XCMPLX_1:180;
      -a<=--1 by A3,REAL_1:50;
    hence a*b<=1 by A4,AXIOMS:22;
  end;

canceled;

theorem
    0<a & a<b or b<a & a<0 implies a/b<1 & b/a>1
  proof
   assume A1:0<a & a<b or b<a & a<0;
   per cases by A1;
    suppose A2:0<a & a<b; then b>0 by AXIOMS:22;
     then a/b<b/b by A2,REAL_1:73;
     hence a/b<1 by A2,XCMPLX_1:60;
       b/a>a/a by A2,REAL_1:73;
     hence b/a>1 by A2,XCMPLX_1:60;
    suppose A3:0>a & a>b; then b<0 by AXIOMS:22;
     then a/b<b/b by A3,REAL_1:74;
     hence a/b<1 by A3,XCMPLX_1:60;
       b/a>a/a by A3,REAL_1:74;
     hence b/a>1 by A3,XCMPLX_1:60;
  end;

theorem
    0<a & a<=b or b<=a & a<0 implies a/b<=1 & b/a>=1
  proof
   assume A1:0<a & a<=b or b<=a & a<0;
   per cases by A1;
    suppose A2:0<a & a<=b; then b>0;
     then a/b<=b/b by A2,REAL_1:73;
     hence a/b<=1 by A2,XCMPLX_1:60;
       b/a>=a/a by A2,REAL_1:73;
     hence b/a>=1 by A2,XCMPLX_1:60;
    suppose A3:b<=a & a<0; then b<0;
     then a/b<=b/b by A3,REAL_1:74;
     hence a/b<=1 by A3,XCMPLX_1:60;
       b/a>=a/a by A3,REAL_1:74;
     hence b/a>=1 by A3,XCMPLX_1:60;
  end;

theorem
    a>0 & b>1 or a<0 & b<1 implies a*b>a
  proof
   assume A1:a>0 & b>1 or a<0 & b<1;
   per cases by A1;
    suppose a>0 & b>1; then a*b>a*1 by REAL_1:70;
     hence a*b>a;
    suppose a<0 & b<1; then a*b>a*1 by REAL_1:71;
     hence a*b>a;
  end;

theorem
    a>0 & b<1 or a<0 & b>1 implies a*b<a
  proof
   assume A1:a>0 & b<1 or a<0 & b>1;
   per cases by A1;
    suppose a>0 & b<1; then a*b<a*1 by REAL_1:70;
     hence a*b<a;
    suppose a<0 & b>1; then a*b<a*1 by REAL_1:71;
     hence a*b<a;
  end;

theorem
   a>=0 & b>=1 or a<=0 & b<=1 implies a*b>=a
  proof
   assume A1: a>=0 & b>=1 or a<=0 & b<=1;
   per cases by A1;
    suppose a>=0 & b>=1; then a*b>=a*1 by AXIOMS:25;
     hence a*b>=a;
    suppose a<=0 & b<=1; then a*b>=a*1 by REAL_1:52;
     hence a*b>=a;
  end;

theorem
   a>=0 & b<=1 or a<=0 & b>=1 implies a*b<=a
  proof
   assume A1: a>=0 & b<=1 or a<=0 & b>=1;
   per cases by A1;
    suppose a>=0 & b<=1; then a*b<=a*1 by AXIOMS:25;
     hence a*b<=a;
    suppose a<=0 & b>=1; then a*b<=a*1 by REAL_1:52;
     hence a*b<=a;
  end;

canceled;

theorem Th149:
 a<0 implies 1/a<0 & a"<0
  proof
   assume a<0;
    then 1/a<0 by Th128;
    hence 1/a<0 & a"<0 by XCMPLX_1:217;
  end;

theorem
   (1/a<0 implies a<0) & (1/a>0 implies a>0)
  proof
   A1:now assume 1/a<0; then 1/(1/a)<0 by Th149;
    hence a<0 by XCMPLX_1:56;
   end;
     now assume 1/a>0; then 1/(1/a)>0 by Th127;
    hence a>0 by XCMPLX_1:56;
   end;
   hence thesis by A1;
  end;

theorem Th151:
 (0<a or b<0) & a<b implies 1/a>1/b
  proof
   assume A1:(0<a or 0>b) & a<b;
   per cases by A1;
    suppose A2:0<a; then b>0 by A1,AXIOMS:22;
     then 1/b>0 by Th127; then a*(1/b)<b*(1/b) by A1,REAL_1:70;
     then A3:a*(1/b)<1 by A1,XCMPLX_1:88;
       1/a>0 by A2,Th127; then 1/a*(a*(1/b))<1*(1/a) by A3,REAL_1:70;
     hence 1/b<1/a by A2,XCMPLX_1:108;
    suppose A4:0>b; then a<0 by A1,AXIOMS:22;
     then 1/a<0 by Th149; then b*(1/a)<a*(1/a) by A1,REAL_1:71;
     then A5:b*(1/a)<1 by A1,XCMPLX_1:88;
       1/b<0 by A4,Th149; then 1/b*(b*(1/a))>1*(1/b) by A5,REAL_1:71;
     hence thesis by A4,XCMPLX_1:108;
  end;

theorem Th152:
 (0<a or b<0) & a<=b implies 1/a>=1/b
  proof
   assume A1:(0<a or 0>b) & a<=b;
   per cases by A1;
    suppose A2:0<a; then b>0 by A1;
     then 1/b>=0 by Th127;
     then a*(1/b)<=b*(1/b) by A1,AXIOMS:25;
     then A3:a*(1/b)<=1 by A1,XCMPLX_1:88;
       1/a>=0 by A2,Th127;
     then 1/a*(a*(1/b))<=1*(1/a) by A3,AXIOMS:25;
     hence thesis by A2,XCMPLX_1:108;
    suppose A4:0>b; then a<0 by A1;
     then 1/a<=0 by Th149;
     then b*(1/a)<=a*(1/a) by A1,REAL_1:52;
     then A5:b*(1/a)<=1 by A1,XCMPLX_1:88;
       1/b<=0 by A4,Th149;
     then 1/b*(b*(1/a))>=1*(1/b) by A5,REAL_1:52;
     hence thesis by A4,XCMPLX_1:108;
  end;

theorem Th153:
 a<0 & b>0 implies 1/a<1/b
  proof
   assume a<0 & b>0;
   then 1/a<0 & 1/b>0 by Th127,Th149;
   hence thesis by AXIOMS:22;
  end;

theorem
   (1/b>0 or 1/a<0) & 1/a>1/b implies a<b
  proof
   assume (1/b>0 or 1/a<0) & 1/a>1/b;
   then 1/(1/a)<1/(1/b) by Th151;
   then a<1/(1/b) by XCMPLX_1:56;hence thesis by XCMPLX_1:56;
  end;

theorem
   (1/b>0 or 1/a<0) & 1/a>=1/b implies a<=b
  proof
   assume (1/b>0 or 1/a<0) & 1/a>=1/b;
   then 1/(1/a)<=1/(1/b) by Th152;
   then a<=1/(1/b) by XCMPLX_1:56;hence thesis by XCMPLX_1:56;
  end;

theorem
    1/a<0 & 1/b>0 implies a<b
  proof
   assume 1/a<0 & 1/b>0;
   then 1/(1/a)<1/(1/b) by Th153;
   then a<1/(1/b) by XCMPLX_1:56;hence thesis by XCMPLX_1:56;
  end;

theorem
   a<-1 implies 1/a>-1 by Lm1,Th151;

theorem
   a<=-1 implies 1/a>=-1 by Lm1,Th152;

canceled 5;

theorem
   1<=a implies 1/a<=1 by Lm1,Th152;

theorem
   (b<=e-a implies a<=e-b) & (b>=e-a implies a>=e-b)
  proof
   A1:now assume b<=e-a; then b+a<=e by REAL_1:84;
      hence a<=e-b by REAL_1:84;end;
     now assume b>=e-a; then b+a>=e by REAL_1:86;
    hence a>=e-b by REAL_1:86;end;
   hence thesis by A1;
  end;

canceled;

theorem Th167:
 a+b<=e+d implies a-e<=d-b
  proof
   assume a+b<=e+d; then a<=e+d-b by REAL_1:84;
    then a<=e+(d-b) by XCMPLX_1:29;
   hence a-e<=d-b by REAL_1:86;
  end;

theorem Th168:
 a+b<e+d implies a-e<d-b
  proof
   assume a+b<e+d; then a<e+d-b by REAL_1:86;
    then a<e+(d-b) by XCMPLX_1:29;
   hence a-e<d-b by REAL_1:84;
  end;

theorem
   a-b<=e-d implies a+d<=e+b & a-e<=b-d & e-a>=d-b & b-a>=d-e
  proof
   assume a-b<=e-d; then a-b+d<=e by REAL_1:84;
   then a+d-b<=e by XCMPLX_1:29;
   hence
A1: a+d<=e+b by REAL_1:86;
   hence a-e<=b-d by Th167;
   thus e-a>=d-b by A1,Th167;thus thesis by A1,Th167;
  end;

theorem
   a-b<e-d implies a+d<e+b & a-e<b-d & e-a>d-b & b-a>d-e
  proof
   assume a-b<e-d; then a-b+d<e by REAL_1:86;
   then a+d-b<e by XCMPLX_1:29;
   hence
A1: a+d<e+b by REAL_1:84;
   hence a-e<b-d by Th168;
   thus e-a>d-b by A1,Th168;thus thesis by A1,Th168;
  end;

theorem
    (a+b<=e-d implies a+d<=e-b) & (a+b>=e-d implies a+d>=e-b)
   proof
    A1:now assume A2:a+b<=e-d or b+a<=e-d;
       per cases by A2;
        suppose a+b<=e-d; then a+b+d<=e by REAL_1:84;
         then a+d+b<=e by XCMPLX_1:1;hence a+d<=e-b by REAL_1:84;
        suppose b+a<=e-d;
         then a+b+d<=e by REAL_1:84;
         then a+d+b<=e by XCMPLX_1:1;hence a+d<=e-b by REAL_1:84;
    end;
      now assume A3:a+b>=e-d or b+a>=e-d;
       per cases by A3;
        suppose a+b>=e-d; then a+b+d>=e by REAL_1:86;
         then a+d+b>=e by XCMPLX_1:1;hence a+d>=e-b by REAL_1:86;
        suppose b+a>=e-d;
         then a+b+d>=e by REAL_1:86;
         then a+d+b>=e by XCMPLX_1:1;hence a+d>=e-b by REAL_1:86;
    end;
    hence thesis by A1;
   end;

canceled;

theorem
   (a<0 implies a+b<b & b-a>b) & (a+b<b or b-a>b implies a<0)
  proof
   hereby assume a<0; then b+a<0+b by REAL_1:53;
      hence a+b<b & b<b-a by REAL_1:86;
   end;
   assume A1:a+b<b or b-a>b;
    per cases by A1;
     suppose a+b<b; then a+b-b<0 by Th105;hence a<0 by XCMPLX_1:26;
     suppose b-a>b; then b-a-b>0 by SQUARE_1:11; then b+-a-b>0 by XCMPLX_0:def
8;
     then -a>0 by XCMPLX_1:26;hence a<0 by REAL_1:66;
  end;

theorem
   (a<=0 implies a+b<=b & b-a>=b) & (a+b<=b or b-a>=b implies a<=0)
  proof
   hereby assume a<=0; then b+a<=0+b by REAL_1:55;
      hence a+b<=b & b<=b-a by REAL_1:84;
   end;
   assume A1:a+b<=b or b-a>=b;
    per cases by A1;
     suppose a+b<=b; then a+b-b<=0 by Th106;hence a<=0 by XCMPLX_1:26;
     suppose b-a>=b; then b-a-b>=0 by SQUARE_1:12;
     then b+-a-b>=0 by XCMPLX_0:def 8;
     then -a>=0 by XCMPLX_1:26;hence a<=0 by REAL_1:26,50;
  end;

canceled 2;

theorem Th177:
  (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)
 proof
  hereby assume A1:b>0 & a*b<=e;
    then a*b/b<=e/b by REAL_1:73;
    hence a<=e/b by A1,XCMPLX_1:90;
  end;
  hereby assume A2:b<0 & a*b<=e;
    then a*b/b>=e/b by REAL_1:74;
     hence a>=e/b by A2,XCMPLX_1:90;
  end;
  hereby assume A3:b>0 & a*b>=e;
    then a*b/b>=e/b by REAL_1:73;
     hence a>=e/b by A3,XCMPLX_1:90;
  end;
  assume A4:b<0 & a*b>=e;
    then a*b/b<=e/b by REAL_1:74;
  hence a<=e/b by A4,XCMPLX_1:90;
 end;

theorem Th178:
  (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)
 proof
  hereby assume A1:b>0 & a*b<e;
    then a*b/b<e/b by REAL_1:73;
     hence a<e/b by A1,XCMPLX_1:90;
  end;
  hereby assume A2:b<0 & a*b<e;
    then a*b/b>e/b by REAL_1:74;
     hence a>e/b by A2,XCMPLX_1:90;
  end;
  hereby assume A3:b>0 & a*b>e;
    then a*b/b>e/b by REAL_1:73;
     hence a>e/b by A3,XCMPLX_1:90;
  end;
  assume A4:b<0 & a*b>e;
    then a*b/b<e/b by REAL_1:74;
  hence a<e/b by A4,XCMPLX_1:90;
 end;

canceled 2;

theorem
   (for a st a>0 holds b+a>=e) or (for a st a<0 holds b-a>=e) implies b>=e
  proof
   assume A1:(for a st a>0 holds b+a>=e) or (for a st a<0 holds b-a>=e);
   per cases by A1;
    suppose A2:for a st a>0 holds b+a>=e;
     assume b<e; then A3:0<e-b by SQUARE_1:11;
     set d=e-b; d/2<d by A3,SEQ_2:4;
     then b+d/2<b+d by REAL_1:53;
     then A4:b+d/2<e by XCMPLX_1:27;
       d/2>0 by A3,SEQ_2:3;
     hence contradiction by A2,A4;
    suppose A5:for a st a<0 holds b-a>=e;
     assume b<e; then A6:0>b-e by Th105;
     set d=b-e;A7:-d>0 by A6,REAL_1:66;
     then (-d)/2<-d by SEQ_2:4;
     then -d/2<-d by XCMPLX_1:188;
     then b+-d/2<b+-d by REAL_1:53;
     then b-d/2<b+-d by XCMPLX_0:def 8;
     then b-d/2<b-d by XCMPLX_0:def 8;
     then A8:b-d/2<e by XCMPLX_1:18;
       (-d)/2>0 by A7,SEQ_2:3;
     then -d/2>0 by XCMPLX_1:188;
     then d/2<0 by REAL_1:66;
     hence contradiction by A5,A8;
  end;

theorem
   (for a st a>0 holds b-a<=e) or (for a st a<0 holds b+a<=e) implies b<=e
  proof
   assume A1:(for a st a>0 holds b-a<=e) or (for a st a<0 holds b+a<=e);
   per cases by A1;
    suppose A2:for a st a>0 holds b-a<=e;
     assume b>e; then A3:0<b-e by SQUARE_1:11;
     set d=b-e; d/2<d by A3,SEQ_2:4;
     then e+d/2<e+d by REAL_1:53;
     then e+d/2<b by XCMPLX_1:27;
     then A4:e<b-d/2 by REAL_1:86;
       d/2>0 by A3,SEQ_2:3;
     hence contradiction by A2,A4;
    suppose A5:for a st a<0 holds b+a<=e;
     assume e<b; then A6:0>e-b by Th105;
     set d=e-b;A7:-d>0 by A6,REAL_1:66;
     then (-d)/2<-d by SEQ_2:4;
     then -d/2<-d by XCMPLX_1:188;
     then e+-d/2<e+-d by REAL_1:53;
     then e-d/2<e+-d by XCMPLX_0:def 8;
     then e-d/2<e-d by XCMPLX_0:def 8;
     then e-d/2<b by XCMPLX_1:18;
     then A8:e<b+d/2 by REAL_1:84;
       (-d)/2>0 by A7,SEQ_2:3;
     then -d/2>0 by XCMPLX_1:188;
     then d/2<0 by REAL_1:66;
     hence contradiction by A5,A8;
  end;

theorem Th183:
 (for a st a>1 holds b*a>=e) or (for a st 0<a & a<1 holds b/a>=e) implies
   b>=e
  proof
   A1:(for a st a>1 holds b*a>=e) implies b>=e
      proof
       assume A2:for a st a>1 holds b*a>=e;
       assume A3:not thesis;
       A4:b>=0
        proof
         assume b<0;
         then A5:b*2<0 by SQUARE_1:24;
A6:         e<=b*2 by A2;
          e<0 by A2,A5;
         then b/e>e/e by A3,REAL_1:74;
         then A7:b/e>1 by A5,A6,XCMPLX_1:60;
         then A8:b*(b/e)>=e by A2;
           b/e>0 by A7,AXIOMS:22;
         then b*(b/e)<e*(b/e) by A3,REAL_1:70;
         then b*(b/e)<b by A5,A6,XCMPLX_1:88;
         hence contradiction by A3,A8,AXIOMS:22;
        end;
        per cases by A4;
         suppose A9:b>0;
          then b/b<e/b by A3,REAL_1:73;
          then 1<e/b by A9,XCMPLX_1:60;
          then consider d being real number such that
          A10:1<d & d<e/b by REAL_1:75;
          reconsider d as Real by XREAL_0:def 1;
            b*d<b*(e/b) by A9,A10,REAL_1:70;
          then b*d<e by A9,XCMPLX_1:88;
          hence contradiction by A2,A10;
         suppose A11:b=0;
            b*2>=e by A2;
          hence contradiction by A3,A11;
      end;
     (for a st a>0 & a<1 holds b/a>=e) implies b>=e
    proof
     assume A12:for a st a>0 & a<1 holds b/a>=e;
       now let d; assume A13:d>1;
      then d > 0 by AXIOMS:22;
      then 1/d<1 & 1/d>0 by A13,Th127,SQUARE_1:2; then b/(1/d)>=e by A12;
      then b*d/1>=e by XCMPLX_1:78;
      hence b*d>=e;
     end;
      hence b>=e by A1;
    end;
   hence thesis by A1;
  end;

theorem
   (for a st 0<a & a<1 holds b*a<=e)
or (for a st a>1 holds b/a<=e) implies b<=e
  proof
   A1:(for a st 0<a & a<1 holds b*a<=e) implies b<=e
    proof
     assume A2:for a st 0<a & a<1 holds b*a<=e;
       now let d; assume A3:d>1;
      then A4:d>0 by AXIOMS:22;
      then 0<1/d & 1/d<1 by A3,Th127,SQUARE_1:2;
      then b*(1/d)<=e by A2;
      then b/d<=e by XCMPLX_1:100;
      hence b<=e*d by A4,Th178;
     end;
     hence thesis by Th183;
    end;
     (for a st a>1 holds b/a<=e) implies b<=e
    proof
     assume A5:for a st a>1 holds b/a<=e;
       now let d; assume A6:0<d & d<1;
      then 1/d>1 by Lm1,Th151;
      then b/(1/d)<=e by A5;
      then b*d/1<=e by XCMPLX_1:78;
      hence b<=e/d by A6,Th177;
     end;
     hence thesis by Th183;
    end;
   hence thesis by A1;
  end;

theorem
   (b>0 & d>0 or b<0 & d<0) & a*d<e*b implies a/b<e/d
  proof
   assume A1: (b>0 & d>0 or b<0 & d<0) & a*d<e*b;
   per cases by A1;
    suppose A2:b>0 & d>0;
     then a*d/b<e by A1,Th178;
     then a/b*d<e by XCMPLX_1:75;
     hence thesis by A2,Th178;
    suppose A3:b<0 & d<0;
     then a*d/b>e by A1,Th178;
     then a/b*d>e by XCMPLX_1:75;
     hence thesis by A3,Th178;
  end;

theorem
   (b>0 & d<0 or b<0 & d>0) & a*d<e*b implies a/b>e/d
  proof
   assume A1: (b>0 & d<0 or b<0 & d>0)
        & a*d<e*b;
   per cases by A1;
    suppose A2:b>0 & d<0;
     then a*d/b<e by A1,Th178;
     then a/b*d<e by XCMPLX_1:75;
     hence thesis by A2,Th178;
    suppose A3:b<0 & d>0;
     then a*d/b>e by A1,Th178;
     then a/b*d>e by XCMPLX_1:75;
     hence thesis by A3,Th178;
  end;

theorem
   (b>0 & d>0 or b<0 & d<0) & a*d<=e*b implies a/b<=e/d
  proof
   assume A1: (b>0 & d>0 or b<0 & d<0) & a*d<=e*b;
   per cases by A1;
    suppose A2:b>0 & d>0;
     then a*d/b<=e by A1,Th177;
     then a/b*d<=e by XCMPLX_1:75;
     hence thesis by A2,Th177;
    suppose A3:b<0 & d<0;
     then a*d/b>=e by A1,Th177;
     then a/b*d>=e by XCMPLX_1:75;
     hence thesis by A3,Th177;
  end;

theorem
   (b>0 & d<0 or b<0 & d>0) & a*d<=e*b implies a/b>=e/d
  proof
   assume A1: (b>0 & d<0 or b<0 & d>0) & a*d<=e*b;
   per cases by A1;
    suppose A2:b>0 & d<0;
     then a*d/b<=e by A1,Th177;
     then a/b*d<=e by XCMPLX_1:75;
     hence thesis by A2,Th177;
    suppose A3:b<0 & d>0;
     then a*d/b>=e by A1,Th177;
     then a/b*d>=e by XCMPLX_1:75;
     hence thesis by A3,Th177;
  end;

canceled 4;

theorem
   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)
  proof
   assume A1:b<0 & d<0 or b>0 & d>0;
   per cases by A1;
    suppose A2:b<0 & d<0;
     A3:now assume a*b<e/d or b*a<e/d;
      then a*b*d>e by A2,Th177;
      then a*d*b>e by XCMPLX_1:4;
      hence a*d<e/b by A2,Th178;
     end;
       now assume a*b>e/d or b*a>e/d;
      then a*b*d<e by A2,Th177;
      then a*d*b<e by XCMPLX_1:4;
      hence a*d>e/b by A2,Th178;
     end;
     hence thesis by A3;
    suppose A4:b>0 & d>0;
     A5:now assume a*b<e/d or b*a<e/d;
      then a*b*d<e by A4,Th177;
      then a*d*b<e by XCMPLX_1:4;
      hence a*d<e/b by A4,Th178;
     end;
       now assume a*b>e/d or b*a>e/d;
      then a*b*d>e by A4,Th177;
      then a*d*b>e by XCMPLX_1:4;
      hence a*d>e/b by A4,Th178;
     end;
     hence thesis by A5;
  end;

theorem
   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)
  proof
   assume A1:b<0 & d>0 or b>0 & d<0;
   per cases by A1;
    suppose A2:b<0 & d>0;
     A3:now assume a*b<e/d or b*a<e/d;
      then a*b*d<e by A2,Th177;
      then a*d*b<e by XCMPLX_1:4;
      hence a*d>e/b by A2,Th178;
     end;
       now assume a*b>e/d or b*a>e/d;
      then a*b*d>e by A2,Th177;
      then a*d*b>e by XCMPLX_1:4;
      hence a*d<e/b by A2,Th178;
     end;
     hence thesis by A3;
    suppose A4:b>0 & d<0;
     A5:now assume a*b<e/d or b*a<e/d;
      then a*b*d>e by A4,Th177;
      then a*d*b>e by XCMPLX_1:4;
      hence a*d>e/b by A4,Th178;
     end;
       now assume a*b>e/d or b*a>e/d;
      then a*b*d<e by A4,Th177;
      then a*d*b<e by XCMPLX_1:4;
      hence a*d<e/b by A4,Th178;
     end;
     hence thesis by A5;
  end;

canceled 2;

theorem Th197:
 (0<a or 0<=a) & (a<b or a<=b) & (0<e or 0<=e) & e<=d implies a*e<=b*d
  proof
   assume A1: (0<a or 0<=a) & (a<b or a<=b) & (0<e or 0<=e) & e<=d;
   then A2:a*e<=b*e by AXIOMS:25;
     b>=0 by A1,AXIOMS:22;
   then b*e<=b*d by A1,AXIOMS:25;
   hence a*e<=b*d by A2,AXIOMS:22;
  end;

theorem
   0>=a & a>=b & 0>=e & e>=d implies a*e<=b*d
  proof
   assume 0>=a & a>=b & 0>=e & e>=d;
   then 0<=-a & -a<=-b & 0<=-e & -e<=-d by REAL_1:26,50;
   then (-a)*(-e)<=(-b)*(-d) & (-a)*(-e)<=(-d)*(-b) & (-e)*(-a)<=(-d)*(-b)
      & (-e)*(-a)<=(-b)*(-d) by Th197;
   then a*e<=(-b)*(-d) & a*e<=(-d)*(-b) & e*a<=(-d)*(-b)
      & e*a<=(-b)*(-d) by XCMPLX_1:177;
   hence thesis by XCMPLX_1:177;
  end;

theorem
   0<a & a<=b & 0<e & e<d or 0>a & a>=b & 0>e & e>d implies a*e<b*d
  proof
   assume A1: 0<a & a<=b & 0<e & e<d or 0>a & a>=b & 0>e & e>d;
   per cases by A1;
    suppose A2:0<a & a<=b & 0<e & e<d;
     then A3:a*e<a*d by REAL_1:70;
       0<=d by A2,AXIOMS:22;
     then a*d<=b*d by A2,AXIOMS:25;
     hence a*e<b*d by A3,AXIOMS:22;
    suppose A4:0>a & a>=b & 0>e & e>d;
     then A5:a*e<a*d by REAL_1:71;
       0>=d by A4,AXIOMS:22;
     then a*d<=b*d by A4,REAL_1:52;
     hence a*e<b*d by A5,AXIOMS:22;
  end;

theorem
    (e>0 & a>0 & a<b implies e/a>e/b) &
    (e>0 & b<0 & a<b implies e/a>e/b)
  proof
   hereby assume A1: e>0 & a>0 & a<b;
    then 1/a>1/b by Th151;
    then 1/a*e>1/b*e by A1,REAL_1:70;
    then e/a>1/b*e by XCMPLX_1:100;
    hence e/a>e/b by XCMPLX_1:100;
   end;
   assume A2:e>0 & b<0 & a<b;
   then 1/a>1/b by Th151;
   then 1/a*e>1/b*e by A2,REAL_1:70;
   then e/a>1/b*e by XCMPLX_1:100;
   hence e/a>e/b by XCMPLX_1:100;
  end;

theorem
   e>=0 & (a>0 or b<0) & a<=b implies e/a>=e/b
  proof
   assume A1: e>=0 & (a>0 or b<0) & a<=b;
   then 1/a>=1/b by Th152;
   then 1/a*e>=1/b*e by A1,AXIOMS:25;
   then e/a>=1/b*e by XCMPLX_1:100;
   hence e/a>=e/b by XCMPLX_1:100;
  end;

theorem
   e<0 & (a>0 or b<0) & a<b implies e/a<e/b
  proof
   assume A1:e<0 & (a>0 or b<0) & a<b;
   then 1/a>1/b by Th151;
   then 1/a*e<1/b*e by A1,REAL_1:71;
   then e/a<1/b*e by XCMPLX_1:100;
   hence e/a<e/b by XCMPLX_1:100;
  end;

theorem
   e<=0 & (a>0 or b<0) & a<=b implies e/a<=e/b
  proof
   assume A1: e<=0 & (a>0 or b<0) & a<=b;
   then 1/a>=1/b by Th152;
   then 1/a*e<=1/b*e by A1,REAL_1:52;
   then e/a<=1/b*e by XCMPLX_1:100;
   hence e/a<=e/b by XCMPLX_1:100;
  end;

theorem
   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
 proof
  let X,Y be Subset of REAL; assume
   A1: X<>{} & Y<>{};
  assume
A2: for a,b st a in X & b in Y holds a<=b;
  consider x being Element of X;
  reconsider a=x as Real by A1,TARSKI:def 3;
  A3:a in X by A1;
  consider y being Element of Y;
  reconsider b=y as Real by A1,TARSKI:def 3;
  A4:b in Y by A1;
  consider d being real number such that
     A5:for a,b being real number st a in X & b in Y holds a<=d & d<=b
      by A2,AXIOMS:26;
  reconsider d as Real by XREAL_0:def 1;
  take d;
  thus thesis by A3,A4,A5;
 end;


Back to top