Copyright (c) 1990 Association of Mizar Users
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;