:: Real Numbers - Basic Theorems
:: by Library Committee
::
:: Received February 9, 2005
:: Copyright (c) 2005-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, ARYTM_2, SUBSET_1, ARYTM_3, ZFMISC_1, CARD_1, XXREAL_0,
ARYTM_0, FUNCOP_1, XBOOLE_0, ARYTM_1, RELAT_1, REAL_1, XCMPLX_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, FUNCT_4, ARYTM_2,
ARYTM_1, ARYTM_0, XCMPLX_0, XREAL_0, NUMBERS, XXREAL_0;
constructors FUNCT_4, ARYTM_1, ARYTM_0, XCMPLX_0, XXREAL_0, XREAL_0;
registrations ARYTM_2, XCMPLX_0, XXREAL_0, XREAL_0, ORDINAL1;
requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
definitions XXREAL_0;
equalities ORDINAL1;
theorems TARSKI, ARYTM_2, ARYTM_1, ARYTM_0, XBOOLE_0, XCMPLX_0, XCMPLX_1,
XREAL_0, ZFMISC_1, XXREAL_0, XTUPLE_0;
begin
reserve a,b,c,d for Real;
reserve r,s for Real;
Lm1: (r in REAL+ & s in REAL+ & ex x9,y9 being Element of REAL+ st r = x9 & s
= y9 & x9 <=' y9) or (r in [:{0},REAL+:] & s in [:{0},REAL+:] & ex x9,y9 being
Element of REAL+ st r = [0,x9] & s = [0,y9] & y9 <=' x9) or s in REAL+ & r in
[:{0},REAL+:] implies r <= s
proof
assume
A1: (r in REAL+ & s in REAL+ & ex x9,y9 being Element of REAL+ st r = x9
& s = y9 & x9 <=' y9) or (r in [:{0},REAL+:] & s in [:{0},REAL+:] &
ex x9,y9 being Element of REAL+ st r = [0,x9] & s = [0,y9] & y9 <=' x9) or
s in REAL+ & r in [:{0},REAL+:];
per cases;
case
r in REAL+ & s in REAL+;
hence thesis by A1,ARYTM_0:5,XBOOLE_0:3;
end;
case
r in [:{0},REAL+:] & s in [:{0},REAL+:];
hence thesis by A1,ARYTM_0:5,XBOOLE_0:3;
end;
case
not(r in REAL+ & s in REAL+) & not (r in [:{0},REAL+:] &
s in [:{0},REAL+:]);
hence thesis by A1;
end;
end;
Lm2: for x1,x2 being Element of REAL st a = [*x1,x2*] holds x2 = 0 & a = x1
proof
let x1,x2 being Element of REAL;
assume
A1: a = [*x1,x2*];
A2: a in REAL by XREAL_0:def 1;
thus now
assume x2 <> 0;
then a = (0,1) --> (x1,x2) by A1,ARYTM_0:def 5;
hence contradiction by A2,ARYTM_0:8;
end;
hence thesis by A1,ARYTM_0:def 5;
end;
Lm3:
for a9,b9 being Element of REAL, a,b st a9 = a & b9 = b holds +(a9,b9) = a + b
proof
let a9,b9 be Element of REAL, a,b such that
A1: a9 = a and
A2: b9 = b;
consider x1,x2,y1,y2 being Element of REAL such that
A3: a = [* x1,x2 *] and
A4: b = [*y1,y2*] and
A5: a+b = [*+(x1,y1),+(x2,y2)*] by XCMPLX_0:def 4;
A6: y2 = 0 by A4,Lm2;
x2 = 0 by A3,Lm2;
then
A7: +(x2,y2) = 0 by A6,ARYTM_0:11;
A8: b = y1 by A4,Lm2;
a = x1 by A3,Lm2;
hence thesis by A1,A2,A5,A8,A7,ARYTM_0:def 5;
end;
Lm4: {} in {{}} by TARSKI:def 1;
Lm5: a <= b implies a + c <= b + c
proof
reconsider x1=a, y1=b, z1=c as Element of REAL by XREAL_0:def 1;
A1: +(y1,z1) = b + c by Lm3;
A2: +(x1,z1) = a + c by Lm3;
assume
A3: a <= b;
per cases by A3,XXREAL_0:def 5;
suppose that
A4: a in REAL+ and
A5: b in REAL+ and
A6: c in REAL+;
consider b9,c99 being Element of REAL+ such that
A7: b = b9 and
A8: c = c99 and
A9: +(y1,z1) = b9 + c99 by A5,A6,ARYTM_0:def 1;
consider a9,c9 being Element of REAL+ such that
A10: a = a9 and
A11: c = c9 and
A12: +(x1,z1) = a9 + c9 by A4,A6,ARYTM_0:def 1;
ex a99,b99 being Element of REAL+ st a = a99 & b = b99 & a99 <='
b99 by A3,A4,A5,XXREAL_0:def 5;
then a9 + c9 <=' b9 + c99 by A10,A11,A7,A8,ARYTM_1:7;
hence thesis by A1,A2,A12,A9,Lm1;
end;
suppose that
A13: a in [:{0},REAL+:] and
A14: b in REAL+ and
A15: c in REAL+;
consider b9,c99 being Element of REAL+ such that
b = b9 and
A16: c = c99 and
A17: +(y1,z1) = b9 + c99 by A14,A15,ARYTM_0:def 1;
consider a9,c9 being Element of REAL+ such that
a = [0,a9] and
A18: c = c9 and
A19: +(x1,z1) = c9 - a9 by A13,A15,ARYTM_0:def 1;
now
per cases;
suppose
A20: a9 <=' c9;
A21: c9 -' a9 <=' c9 by ARYTM_1:11;
c9 <=' b9 + c99 by A18,A16,ARYTM_2:19;
then
A22: c9 -' a9 <=' b9 + c99 by A21,ARYTM_1:3;
c9 - a9 = c9 -' a9 by A20,ARYTM_1:def 2;
hence thesis by A1,A2,A19,A17,A22,Lm1;
end;
suppose
not a9 <=' c9;
then c9 - a9 = [0,a9 -' c9] by ARYTM_1:def 2;
then c9 - a9 in [:{0},REAL+:] by Lm4,ZFMISC_1:87;
then
A23: not a + c in REAL+ by A2,A19,ARYTM_0:5,XBOOLE_0:3;
not b + c in [:{0},REAL+:] by A1,A17,ARYTM_0:5,XBOOLE_0:3;
hence thesis by A23,XXREAL_0:def 5;
end;
end;
hence thesis;
end;
suppose that
A24: a in [:{0},REAL+:] and
A25: b in [:{0},REAL+:] and
A26: c in REAL+;
consider b9,c99 being Element of REAL+ such that
A27: b = [0,b9] and
A28: c = c99 and
A29: +(y1,z1) = c99 - b9 by A25,A26,ARYTM_0:def 1;
consider a99,b99 being Element of REAL+ such that
A30: a = [0,a99] and
A31: b = [0,b99] and
A32: b99 <=' a99 by A3,A24,A25,XXREAL_0:def 5;
consider a9,c9 being Element of REAL+ such that
A33: a = [0,a9] and
A34: c = c9 and
A35: +(x1,z1) = c9 - a9 by A24,A26,ARYTM_0:def 1;
A36: a9 = a99 by A30,A33,XTUPLE_0:1;
A37: b9 = b99 by A31,A27,XTUPLE_0:1;
now
per cases;
suppose
A38: a9 <=' c9;
then b9 <=' c9 by A32,A36,A37,ARYTM_1:3;
then
A39: c9 - b9 = c9 -' b9 by ARYTM_1:def 2;
A40: c9 - a9 = c9 -' a9 by A38,ARYTM_1:def 2;
c9 -' a9 <=' c99 -' b9 by A32,A34,A28,A36,A37,ARYTM_1:16;
hence thesis by A1,A2,A34,A35,A28,A29,A40,A39,Lm1;
end;
suppose
not a9 <=' c9;
then
A41: +(x1,z1) = [0,a9 -' c9] by A35,ARYTM_1:def 2;
then
A42: +(x1,z1) in [:{0},REAL+:] by Lm4,ZFMISC_1:87;
now
per cases;
suppose
b9 <=' c9;
then c9 - b9 = c9 -' b9 by ARYTM_1:def 2;
then
A43: not +(y1,z1) in [:{0},REAL+:] by A34,A28,A29,ARYTM_0:5,XBOOLE_0:3;
not +(x1,z1) in REAL+ by A42,ARYTM_0:5,XBOOLE_0:3;
hence thesis by A1,A2,A43,XXREAL_0:def 5;
end;
suppose
A44: not b9 <=' c9;
A45: b9 -' c9 <=' a9 -' c9 by A32,A36,A37,ARYTM_1:17;
A46: +(y1,z1) = [0,b9 -' c9] by A34,A28,A29,A44,ARYTM_1:def 2;
then +(y1,z1) in [:{0},REAL+:] by Lm4,ZFMISC_1:87;
hence thesis by A1,A2,A41,A42,A46,A45,Lm1;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
suppose that
A47: a in REAL+ and
A48: b in REAL+ and
A49: c in [:{0},REAL+:];
consider b9,c99 being Element of REAL+ such that
A50: b = b9 and
A51: c = [0,c99] and
A52: +(y1,z1) = b9 - c99 by A48,A49,ARYTM_0:def 1;
consider a9,c9 being Element of REAL+ such that
A53: a = a9 and
A54: c = [0,c9] and
A55: +(x1,z1) = a9 - c9 by A47,A49,ARYTM_0:def 1;
A56: c9 = c99 by A54,A51,XTUPLE_0:1;
A57: ex a99,b99 being Element of REAL+ st a = a99 & b = b99 & a99 <='
b99 by A3,A47,A48,XXREAL_0:def 5;
now
per cases;
suppose
A58: c9 <=' a9;
then c9 <=' b9 by A57,A53,A50,ARYTM_1:3;
then
A59: b9 - c9 = b9 -' c9 by ARYTM_1:def 2;
A60: a9 - c9 = a9 -' c9 by A58,ARYTM_1:def 2;
a9 -' c9 <=' b9 -' c99 by A57,A53,A50,A56,ARYTM_1:17;
hence thesis by A1,A2,A55,A52,A56,A60,A59,Lm1;
end;
suppose
not c9 <=' a9;
then
A61: +(x1,z1) = [0,c9 -' a9] by A55,ARYTM_1:def 2;
then
A62: +(x1,z1) in [:{0},REAL+:] by Lm4,ZFMISC_1:87;
now
per cases;
suppose
c9 <=' b9;
then b9 - c9 = b9 -' c9 by ARYTM_1:def 2;
then
A63: not +(y1,z1) in [:{0},REAL+:] by A52,A56,ARYTM_0:5,XBOOLE_0:3;
not +(x1,z1) in REAL+ by A62,ARYTM_0:5,XBOOLE_0:3;
hence thesis by A1,A2,A63,XXREAL_0:def 5;
end;
suppose
A64: not c9 <=' b9;
A65: c9 -' b9 <=' c9 -' a9 by A57,A53,A50,ARYTM_1:16;
A66: +(y1,z1) = [0,c9 -' b9] by A52,A56,A64,ARYTM_1:def 2;
then +(y1,z1) in [:{0},REAL+:] by Lm4,ZFMISC_1:87;
hence thesis by A1,A2,A61,A62,A66,A65,Lm1;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
suppose that
A67: a in [:{0},REAL+:] and
A68: b in REAL+ and
A69: c in [:{0},REAL+:];
A70: not c in REAL+ by A69,ARYTM_0:5,XBOOLE_0:3;
not a in REAL+ by A67,ARYTM_0:5,XBOOLE_0:3;
then consider a9,c9 being Element of REAL+ such that
a = [0,a9] and
A71: c = [0,c9] and
A72: +(x1,z1) = [0,a9 + c9] by A70,ARYTM_0:def 1;
A73: +(x1,z1) in [:{0},REAL+:] by A72,Lm4,ZFMISC_1:87;
consider b9,c99 being Element of REAL+ such that
b = b9 and
A74: c = [0,c99] and
A75: +(y1,z1) = b9 - c99 by A68,A69,ARYTM_0:def 1;
A76: c9 = c99 by A71,A74,XTUPLE_0:1;
now
per cases;
suppose
c9 <=' b9;
then b9 - c99 = b9 -' c99 by A76,ARYTM_1:def 2;
then
A77: not +(y1,z1) in [:{0},REAL+:] by A75,ARYTM_0:5,XBOOLE_0:3;
not +(x1,z1) in REAL+ by A73,ARYTM_0:5,XBOOLE_0:3;
hence thesis by A1,A2,A77,XXREAL_0:def 5;
end;
suppose
A78: not c9 <=' b9;
A79: c9 <=' c9 + a9 by ARYTM_2:19;
c9 -' b9 <=' c9 by ARYTM_1:11;
then
A80: c9 -' b9 <=' c9 + a9 by A79,ARYTM_1:3;
A81: +(y1,z1) = [0,c9 -' b9] by A75,A76,A78,ARYTM_1:def 2;
then +(y1,z1) in [:{0},REAL+:] by Lm4,ZFMISC_1:87;
hence thesis by A1,A2,A72,A73,A81,A80,Lm1;
end;
end;
hence thesis;
end;
suppose that
A82: a in [:{0},REAL+:] and
A83: b in [:{0},REAL+:] and
A84: c in [:{0},REAL+:];
A85: not c in REAL+ by A84,ARYTM_0:5,XBOOLE_0:3;
A86: not c in REAL+ by A84,ARYTM_0:5,XBOOLE_0:3;
not a in REAL+ by A82,ARYTM_0:5,XBOOLE_0:3;
then consider a9,c9 being Element of REAL+ such that
A87: a = [0,a9] and
A88: c = [0,c9] and
A89: +(x1,z1) = [0,a9 + c9] by A86,ARYTM_0:def 1;
A90: +(x1,z1) in [:{0},REAL+:] by A89,Lm4,ZFMISC_1:87;
not b in REAL+ by A83,ARYTM_0:5,XBOOLE_0:3;
then consider b9,c99 being Element of REAL+ such that
A91: b = [0,b9] and
A92: c = [0,c99] and
A93: +(y1,z1) = [0,b9 + c99] by A85,ARYTM_0:def 1;
A94: +(y1,z1) in [:{0},REAL+:] by A93,Lm4,ZFMISC_1:87;
A95: c9 = c99 by A88,A92,XTUPLE_0:1;
consider a99,b99 being Element of REAL+ such that
A96: a = [0,a99] and
A97: b = [0,b99] and
A98: b99 <=' a99 by A3,A82,A83,XXREAL_0:def 5;
A99: b9 = b99 by A97,A91,XTUPLE_0:1;
a9 = a99 by A96,A87,XTUPLE_0:1;
then b9 + c9 <=' a9 + c99 by A98,A99,A95,ARYTM_1:7;
hence thesis by A1,A2,A89,A93,A95,A90,A94,Lm1;
end;
end;
Lm6: a <= b & c <= d implies a+c <= b+d
proof
assume a <= b;
then
A1: a+c <= b+c by Lm5;
assume c <= d;
then b+c <= b+d by Lm5;
hence thesis by A1,XXREAL_0:2;
end;
Lm7: a <= b implies a-c <= b-c
proof
a <= b implies a + -c <= b + -c by Lm5;
hence thesis;
end;
Lm8: a < b & c <= d implies a+c < b+d
proof
assume that
A1: a < b and
A2: c <= d;
for a,b,c,d holds a < b & c <= d implies a+c < b+d
proof
let a,b,c,d;
assume
A3: a < b;
assume
A4: c <= d;
A5: a+c <> b+d
proof
a+c <= d+a by A4,Lm5;
then a+c-d <= a+d-d by Lm7;
hence thesis by A3;
end;
a+c <= b+d by A3,A4,Lm6;
hence thesis by A5,XXREAL_0:1;
end;
hence thesis by A1,A2;
end;
Lm9: 0 < a implies b < b+a
proof
assume 0 < a;
then b+0 < b+a by Lm8;
hence thesis;
end;
theorem Th1:
ex b st a < b
proof
take a+1;
a+0 < a+1 by Lm8;
hence thesis;
end;
theorem Th2:
ex b st b < a
proof
take a-1;
a+-1 < a+-0 by Lm8;
hence thesis;
end;
theorem
ex c st a < c & b < c
proof
per cases;
suppose
A1: a <= b;
take z = b + 1;
b < z by Lm9;
hence thesis by A1,XXREAL_0:2;
end;
suppose
A2: b <= a;
take z = a + 1;
a < z by Lm9;
hence thesis by A2,XXREAL_0:2;
end;
end;
Lm10: a+c <= b+c implies a <= b
proof
assume a+c <= b+c;
then a+c+-c <= b+c+-c by Lm5;
hence thesis;
end;
theorem
ex c st c < a & c < b
proof
per cases;
suppose
A1: a <= b;
take z = a+-1;
z < a+0 by Lm10;
hence thesis by A1,XXREAL_0:2;
end;
suppose
A2: b <= a;
take z = b+-1;
z < b+0 by Lm10;
hence thesis by A2,XXREAL_0:2;
end;
end;
Lm11:
for a9,b9 being Element of REAL, a,b st a9 = a & b9 = b holds *(a9,b9) = a * b
proof
let a9,b9 be Element of REAL, a,b such that
A1: a9 = a and
A2: b9 = b;
consider x1,x2,y1,y2 being Element of REAL such that
A3: a = [* x1,x2 *] and
A4: b = [*y1,y2*] and
A5: a*b = [* +(*(x1,y1),opp*(x2,y2)), +(*(x1,y2),*(x2,y1)) *]
by XCMPLX_0:def 5;
A6: b = y1 by A4,Lm2;
x2 = 0 by A3,Lm2;
then
A7: *(x2,y1) = 0 by ARYTM_0:12;
A8: y2 = 0 by A4,Lm2;
then *(x1,y2) = 0 by ARYTM_0:12;
then
A9: +(*(x1,y2),*(x2,y1)) = 0 by A7,ARYTM_0:11;
a = x1 by A3,Lm2;
hence *(a9,b9) = +(*(x1,y1),*(opp x2,y2)) by A1,A2,A6,A8,ARYTM_0:11,12
.= +(*(x1,y1),opp*(x2,y2)) by ARYTM_0:15
.= a * b by A5,A9,ARYTM_0:def 5;
end;
Lm12: a <= b & 0 <= c implies a*c <= b*c
proof
assume that
A1: a <= b and
A2: 0 <= c;
0 is Element of REAL+ by ARYTM_2:20;
then not 0 in [:{0},REAL+:] by ARYTM_0:5,XBOOLE_0:3;
then
A3: c in REAL+ by A2,XXREAL_0:def 5;
reconsider x1=a, y1=b, z1=c as Element of REAL by XREAL_0:def 1;
A4: *(y1,z1) = b * c by Lm11;
A5: *(x1,z1) = a * c by Lm11;
assume
A6: not thesis;
then
A7: c <> 0;
per cases by A1,XXREAL_0:def 5;
suppose that
A8: a in REAL+ and
A9: b in REAL+;
consider b9,c99 being Element of REAL+ such that
A10: b = b9 and
A11: c = c99 and
A12: *(y1,z1) = b9 *' c99 by A3,A9,ARYTM_0:def 2;
consider a9,c9 being Element of REAL+ such that
A13: a = a9 and
A14: c = c9 and
A15: *(x1,z1) = a9 *' c9 by A3,A8,ARYTM_0:def 2;
ex a99,b99 being Element of REAL+ st a = a99 & b = b99 & a99 <='
b99 by A1,A8,A9,XXREAL_0:def 5;
then a9 *' c9 <=' b9 *' c9 by A13,A10,ARYTM_1:8;
hence contradiction by A4,A5,A6,A14,A15,A11,A12,Lm1;
end;
suppose that
A16: a in [:{0},REAL+:] and
A17: b in REAL+;
ex a9,c9 being Element of REAL+ st a = [0,a9] & c = c9 & *(x1,z1)
= [0,c9 *' a9] by A3,A7,A16,ARYTM_0:def 2;
then *(x1,z1) in [:{0},REAL+:] by Lm4,ZFMISC_1:87;
then
A18: not *(x1,z1) in REAL+ by ARYTM_0:5,XBOOLE_0:3;
ex b9,c99 being Element of REAL+ st b = b9 & c = c99 & * (y1,z1) =
b9 *' c99 by A3,A17,ARYTM_0:def 2;
then not *(y1,z1) in [:{0},REAL+:] by ARYTM_0:5,XBOOLE_0:3;
hence contradiction by A4,A5,A6,A18,XXREAL_0:def 5;
end;
suppose that
A19: a in [:{0},REAL+:] and
A20: b in [:{0},REAL+:];
consider b9,c99 being Element of REAL+ such that
A21: b = [0,b9] and
A22: c = c99 and
A23: *(y1,z1) = [0,c99 *' b9] by A3,A7,A20,ARYTM_0:def 2;
A24: *(y1,z1) in [:{0},REAL+:] by A23,Lm4,ZFMISC_1:87;
consider a99,b99 being Element of REAL+ such that
A25: a = [0,a99] and
A26: b = [0,b99] and
A27: b99 <=' a99 by A1,A19,A20,XXREAL_0:def 5;
A28: b9 = b99 by A26,A21,XTUPLE_0:1;
consider a9,c9 being Element of REAL+ such that
A29: a = [0,a9] and
A30: c = c9 and
A31: *(x1,z1) = [0,c9 *' a9] by A3,A7,A19,ARYTM_0:def 2;
A32: *(x1,z1) in [:{0},REAL+:] by A31,Lm4,ZFMISC_1:87;
a9 = a99 by A25,A29,XTUPLE_0:1;
then b9 *' c9 <=' a9 *' c9 by A27,A28,ARYTM_1:8;
hence contradiction by A4,A5,A6,A30,A31,A22,A23,A32,A24,Lm1;
end;
end;
Lm13: 0 < c & a < b implies a*c < b*c
proof
assume
A1: 0 < c;
assume
A2: a < b;
A3: a*c <> b*c
proof
assume a*c = b*c;
then a*(c*c") = b*c*c" by XCMPLX_1:4;
then a*1 = b*(c*c") by A1,XCMPLX_0:def 7;
then a = b*1 by A1,XCMPLX_0:def 7;
hence contradiction by A2;
end;
a*c <= b*c by A1,A2,Lm12;
hence thesis by A3,XXREAL_0:1;
end;
theorem Th5:
a < b implies ex c st a < c & c < b
proof
assume
A1: a < b;
take z = (a+b)/2;
1*a+a < a+b by A1,Lm10;
then 2"*(2*a) < 2"*(a+b) by Lm13;
hence a < z;
a+b < 1*b+b by A1,Lm10;
then 2"*(a+b) < 2"*(2*b) by Lm13;
hence thesis;
end;
begin
theorem
a <= b iff a + c <= b + c by Lm5,Lm10;
theorem
a <= b & c <= d implies a+c <= b+d by Lm6;
theorem
a < b & c <= d implies a+c < b+d by Lm8;
Lm14: a <= b implies -b <= -a
proof
assume a <= b;
then a-b <= b-b by Lm7;
then a-b-a <= 0-a by Lm7;
hence thesis;
end;
Lm15: -b <= -a implies a <= b
proof
assume -b <= -a;
then --a <= --b by Lm14;
hence thesis;
end;
begin
theorem Th9:
a <= b iff a-c <= b-c
proof
thus a <= b implies a-c <= b-c by Lm7;
assume a-c <= b-c;
then a+ (-c) + c <= b+ (-c)+c by Lm5;
hence thesis;
end;
theorem
a <= b iff c-b <= c-a
proof
hereby
assume a <= b;
then -b <= -a by Lm14;
then c+-b <= c+-a by Lm5;
hence c-b <= c-a;
end;
assume c-b <= c-a;
then c-b-c <= c-a-c by Th9;
then -b <= -a;
hence thesis by Lm15;
end;
Lm16: a+b <= c implies a <= c-b
proof
assume a+b <= c;
then a+b-b <= c-b by Lm7;
hence thesis;
end;
Lm17: a <= b-c implies a+c <= b
proof
assume a <= b-c;
then a+c <= b-c+c by Lm5;
hence thesis;
end;
Lm18: a <= b+c implies a-b <= c
proof
assume a<=b+c;
then a-b <= c+b-b by Lm7;
hence thesis;
end;
Lm19: a-b <= c implies a <= b+c
proof
assume a-b <= c;
then a-b+b <= c+b by Lm5;
hence thesis;
end;
theorem
a <= b-c implies c <= b-a
proof
assume a <= b-c;
then a+c <= b by Lm17;
hence thesis by Lm16;
end;
theorem
a-b <= c implies a-c <= b
proof
assume c >= a-b;
then c+b >= a by Lm19;
hence thesis by Lm18;
end;
theorem Th13:
a <= b & c <= d implies a-d <= b-c
proof
assume
A1: a <= b;
assume c <= d;
then -d <= -c by Lm14;
then a+-d <= b+-c by A1,Lm6;
hence thesis;
end;
theorem
a < b & c <= d implies a-d < b-c
proof
assume
A1: a < b;
assume c <= d;
then -d <= -c by Lm14;
then a+-d < b+-c by A1,Lm8;
hence thesis;
end;
theorem Th15:
a <= b & c < d implies a-d < b-c
proof
assume
A1: a <= b;
assume c < d;
then -d < -c by Lm15;
then a+-d < b+-c by A1,Lm8;
hence thesis;
end;
Lm20: a+b <= c+d implies a-c <= d-b
proof
assume a+b <= c+d;
then a <= c+d-b by Lm16;
then a <= c+(d-b);
hence thesis by Lm18;
end;
theorem Tk1:
a-b <= c-d implies a-c <= b-d
proof
assume a-b <= c-d;
then a-b+b <= c-d+b by Lm5;
then a-c <= c-d+b-c by Th9;
hence thesis;
end;
theorem
a-b <= c-d implies d-b <= c-a
proof
assume a-b <= c-d;
then -(b-d) <= -(a-c) by Tk1,Lm14;
hence thesis;
end;
theorem
a-b <= c-d implies d-c <= b-a
proof
assume a-b <= c-d;
then a-b+d <= c by Lm17;
then a+d-b <= c;
then a+d <= c+b by Lm19;
hence thesis by Lm20;
end;
begin
theorem
a+b <= c iff a <= c-b by Lm16,Lm17;
theorem
a <= b+c iff a-b <= c by Lm18,Lm19;
theorem
a+b <= c+d iff a-c <= d-b
proof
thus a+b <= c+d implies a-c <= d-b by Lm20;
assume a-c <= d-b;
then a-c+b <= d-b+b by Lm5;
then a-c+b+c <= d+c by Lm5;
hence thesis;
end;
theorem
a+b <= c-d implies a+d <= c-b
proof
assume a+b <= c-d;
then a+b+d <= c-d+d by Lm5;
then a+b+d-b <= c-b by Th9;
hence thesis;
end;
theorem
a-b <= c+d implies a-d <= c+b
proof
assume c+d >= a-b;
then per cases; ::??? wyzej bylo to samo
suppose
c+d >= a-b;
then c+d+b >= a by Lm19;
then c+b+d >= a;
hence thesis by Lm18;
end;
suppose
d+c >= a-b;
then c+d+b >= a by Lm19;
then c+b+d >= a;
hence thesis by Lm18;
end;
end;
begin
theorem
a <= b iff -b <= -a by Lm14,Lm15;
Lm21: a < b implies 0 < b-a
proof
assume a < b;
then a + 0 < b;
hence thesis by Lm19;
end;
theorem Th25:
a <= -b implies b <= -a
proof
assume a <= -b;
then --b <= -a by Lm14;
hence thesis;
end;
theorem Th26:
-b <= a implies -a <= b
proof
assume -b <= a;
then -a <= --b by Lm14;
hence thesis;
end;
begin
theorem
0 <= a & 0 <= b & a+b = 0 implies a = 0;
theorem
a <= 0 & b <= 0 & a+b = 0 implies a = 0;
begin
theorem
0 < a implies b < b+a by Lm9;
theorem
a < 0 implies a+b < b
proof
assume a<0;
then b+a<0+b by Lm10;
hence thesis;
end;
Lm23: a < b implies a-b < 0
proof
assume
A1: a < b;
assume a-b>=0;
then a-b+b>=0+b by Lm5;
hence thesis by A1;
end;
theorem
0 <= a implies b <= a+b
proof
assume 0 <= a;
then 0+b <= a+b by Lm5;
hence thesis;
end;
theorem
a <= 0 implies a+b <= b
proof
assume a <= 0;
then a+b <= 0+b by Lm5;
hence thesis;
end;
begin
theorem
0 <= a & 0 <= b implies 0 <= a+b;
theorem
0 <= a & 0 < b implies 0 < a+b;
theorem Th35:
a <= 0 & c <= b implies c+a <= b
proof
assume a <= 0 & c <= b;
then a+c <= 0+b by Lm6;
hence thesis;
end;
theorem Th36:
a <= 0 & c < b implies c+a < b
proof
assume a <= 0 & c < b;
then a+c < 0+b by Lm8;
hence thesis;
end;
theorem Th37:
a < 0 & c <= b implies a+c < b
proof
assume a < 0 & c <= b;
then a+c < 0+b by Lm8;
hence thesis;
end;
theorem Th38:
0 <= a & b <= c implies b <= a+c
proof
assume 0 <= a & b <= c;
then 0+b <= a+c by Lm6;
hence thesis;
end;
theorem Th39:
0 < a & b <= c implies b < a+c
proof
assume 0 < a & b <= c;
then b+0 < a+c by Lm8;
hence thesis;
end;
theorem Th40:
0 <= a & b < c implies b < a+c
proof
assume 0 <= a & b < c;
then b+0 < a+c by Lm8;
hence thesis;
end;
Lm24: c < 0 & a < b implies b*c < a*c
proof
assume
A1: c < 0;
assume a<b;
then a*(-c) < b*(-c) by A1,Lm13;
then -(a*c) < -(b*c);
hence thesis by Lm14;
end;
Lm25: 0 <= c & b <= a implies b/c <= a/c
proof
assume that
A1: 0 <= c and
A2: b <= a;
per cases by A1;
suppose
c = 0;
then
A3: c" = 0;
then b*c" = 0;
then
A4: b/c = 0 by XCMPLX_0:def 9;
a*c" = 0 by A3;
hence thesis by A4,XCMPLX_0:def 9;
end;
suppose
A5: 0 < c;
assume a/c < b/c;
then a/c*c < b/c*c by A5,Lm13;
then a<b/c*c by A5,XCMPLX_1:87;
hence contradiction by A2,A5,XCMPLX_1:87;
end;
end;
Lm26: 0 < c & a < b implies a/c < b/c
proof
assume
A1: 0 < c;
assume a < b;
then a*c" < b*c" by A1,Lm13;
then a/c < b*c" by XCMPLX_0:def 9;
hence thesis by XCMPLX_0:def 9;
end;
Lm27: 0 < a implies a/2 < a
proof
assume 0 < a;
then 0+a/2 < a/2+a/2 by Lm10;
hence thesis;
end;
begin
theorem
(for a being Real st a > 0 holds c <= b+a) implies c <= b
proof
assume
A1: for a st a > 0 holds b+a >= c;
set d = c-b;
assume b < c;
then
A2: 0 < d by Lm21;
then b+d/2 < b+d by Lm10,Lm27;
hence contradiction by A1,A2;
end;
theorem
(for a being Real st a < 0 holds b+a <= c) implies b <= c
proof
assume
A1: for a st a < 0 holds b+a<=c;
set d = c-b;
assume c < b;
then
A2: 0 > c-b by Lm23;
then (-d)/2 < -d by Lm27;
then c+-d/2 < c+-d by Lm10;
then c-d/2 < c-d;
then c < b+d/2 by Lm16;
hence contradiction by A1,A2;
end;
begin
theorem
0 <= a implies b-a <= b
proof
0 <= a implies b - a <= b - 0 by Th13;
hence thesis;
end;
theorem Th44:
0 < a implies b-a < b
proof
assume 0 < a;
then b + -a < b + 0 by Lm10;
hence thesis;
end;
theorem
a <= 0 implies b <= b-a
proof
assume a <= 0;
then b+a <= 0+b by Lm6;
hence thesis by Lm16;
end;
theorem
a < 0 implies b < b-a
proof
assume a < 0;
then b+a < 0+b by Lm10;
hence thesis by Lm19;
end;
theorem
a <= b implies a-b <= 0
proof
assume a <= b;
then a-b <= b-b by Th9;
hence thesis;
end;
theorem Th48:
a <= b implies 0 <= b-a
proof
assume a <= b;
then a-a <= b-a by Lm7;
hence thesis;
end;
theorem
a < b implies a-b < 0 by Lm23;
theorem
a < b implies 0 < b-a by Lm21;
theorem
0 <= a & b < c implies b-a < c
proof
assume 0 <= a & b < c;
then 0+b < a+c by Th40;
hence thesis by Lm17;
end;
theorem
a <= 0 & b <= c implies b <= c-a
proof
assume a <= 0 & b <= c;
then b+a <= c by Th35;
hence thesis by Lm16;
end;
theorem
a <= 0 & b < c implies b < c-a
proof
assume that
A1: a <= 0 and
A2: b < c;
b+a < c by A1,A2,Th36;
hence thesis by Lm19;
end;
theorem
a < 0 & b <= c implies b < c-a
proof
assume that
A1: a < 0 and
A2: b <= c;
a+b < c by A1,A2,Th37;
hence thesis by Lm19;
end;
theorem
a <> b implies 0 < a-b or 0 < b-a
proof
assume a <> b;
then per cases by XXREAL_0:1;
suppose a < b;
then 0 + a < b;
hence thesis by Lm19;
end;
suppose b < a;
then 0 + b < a;
hence thesis by Lm19;
end;
end;
begin
theorem
(for a being Real st a < 0 holds c <= b-a) implies b >= c
proof
assume
A1: for a st a < 0 holds b-a >= c;
set d = b-c;
assume b < c;
then
A2: 0 > b-c by Lm23;
then (-d)/2 < -d by Lm27;
then b+-d/2 < b+-d by Lm10;
then b-d/2 < b-d;
hence contradiction by A1,A2;
end;
theorem
(for a being Real st a > 0 holds b-a <= c) implies b <= c
proof
assume
A1: for a st a > 0 holds b-a <= c;
set d = b-c;
assume b > c;
then
A2: 0 < d by Lm21;
then c+d/2 < c+d by Lm10,Lm27;
then c < b-d/2 by Lm19;
hence contradiction by A1,A2;
end;
begin
theorem
a < 0 iff 0 < -a;
theorem
a <= -b implies a+b <= 0
proof
assume a <= -b;
then a+b <= -b+b by Lm5;
hence thesis;
end;
theorem
-a <= b implies 0 <= a+b
proof
assume -a <= b;
then -a+a <= b+a by Lm5;
hence thesis;
end;
theorem
a < -b implies a+b < 0
proof
assume a < -b;
then a+b < -b+b by Lm10;
hence thesis;
end;
theorem
-b < a implies 0 < a+b
proof
assume -b < a;
then -b+b < a+b by Lm10;
hence thesis;
end;
Lm28: a <= b & c <= 0 implies b*c <= a*c
proof
assume a <= b & c <= 0;
then a*(-c) <= b*(-c) by Lm12;
then -(a*c) <= -(b*c);
hence thesis by Lm15;
end;
begin
theorem
0 <= a*a
proof
0 <= a or a < 0;
hence thesis;
end;
theorem
a <= b & 0 <= c implies a*c <= b*c by Lm12;
theorem
a <= b & c <= 0 implies b*c <= a*c by Lm28;
theorem Th66:
0 <= a & a <= b & 0 <= c & c <= d implies a*c <= b*d
proof
assume that
A1: 0 <= a and
A2: a <= b and
A3: 0 <= c and
A4: c <= d;
A5: a*c <= b*c by A2,A3,Lm12;
b*c <= b*d by A1,A2,A4,Lm12;
hence thesis by A5,XXREAL_0:2;
end;
theorem
a <= 0 & b <= a & c <= 0 & d <= c implies a*c <= b*d
proof
assume that
A1: 0 >= a and
A2: a >= b and
A3: 0 >= c and
A4: c >= d;
A5: -c <= -d by A4,Lm14;
-a <= -b by A2,Lm14;
then (-a)*(-c) <= (-b)*(-d) by A1,A3,A5,Th66;
hence thesis;
end;
theorem
0 < c & a < b implies a*c < b*c by Lm13;
theorem
c < 0 & a < b implies b*c < a*c by Lm24;
theorem
a < 0 & b <= a & c < 0 & d < c implies a*c < b*d
proof
assume that
A1: 0 > a and
A2: a >= b and
A3: 0 > c and
A4: c > d;
A5: a*c < a*d by A1,A4,Lm24;
a*d <= b*d by A2,A3,A4,Lm28;
hence thesis by A5,XXREAL_0:2;
end;
begin
theorem
0 <= a & 0 <= b & 0 <= c & 0 <= d & a*c+b*d = 0 implies a = 0 or c = 0;
Lm29: c < 0 & a < b implies b/c < a/c
proof
assume that
A1: c < 0 and
A2: a < b;
a/(-c)<b/(-c) by A1,A2,Lm26;
then -a/c < b/(-c) by XCMPLX_1:188;
then -a/c < -b/c by XCMPLX_1:188;
hence thesis by Lm14;
end;
Lm30: c <= 0 & b/c < a/c implies a < b
proof
assume that
A1: c <= 0 and
A2: b/c < a/c;
A3: now
assume c = 0;
then
A4: c" = 0;
a/c = a*c" by XCMPLX_0:def 9
.= b*c" by A4
.= b/c by XCMPLX_0:def 9;
hence contradiction by A2;
end;
then a/c*c < b/c*c by A1,A2,Lm24;
then a<b/c*c by A3,XCMPLX_1:87;
hence thesis by A3,XCMPLX_1:87;
end;
begin
theorem
0 <= c & b <= a implies b/c <= a/c by Lm25;
theorem
c <= 0 & a <= b implies b/c <= a/c by Lm30;
theorem
0 < c & a < b implies a/c < b/c by Lm26;
theorem
c < 0 & a < b implies b/c < a/c by Lm29;
theorem
0 < c & 0 < a & a < b implies c/b < c/a
proof
assume that
A1: 0 < c and
A2: 0 < a and
A3: a < b;
a*b" < b*b" by A2,A3,Lm13;
then a*b" < 1 by A2,A3,XCMPLX_0:def 7;
then a"*(a*b") < a"*1 by A2,Lm13;
then a"*a*b" < a";
then 1*b" < a" by A2,XCMPLX_0:def 7;
then c*b"<c*a" by A1,Lm13;
then c/b < c*a" by XCMPLX_0:def 9;
hence thesis by XCMPLX_0:def 9;
end;
Lm31: b < 0 & a < b implies b" < a"
proof
A1: a" = 1/a by XCMPLX_1:215;
assume that
A2: 0>b and
A3: a<b;
b*(a")<a*(a") by A2,A3,Lm24;
then b*(a")<1 by A1,A2,A3,XCMPLX_1:87;
then b"*(b*(a"))>1*(b") by A2,Lm24;
then b"*b*(a")>1*(b");
then 1*(a")>1*(b") by A2,XCMPLX_0:def 7;
hence thesis;
end;
begin
theorem Th77:
0 < b & a*b <= c implies a <= c/b
proof
assume
A1: b > 0;
assume a*b <= c;
then a*b/b <= c/b by A1,Lm25;
hence thesis by A1,XCMPLX_1:89;
end;
theorem Th78:
b < 0 & a*b <= c implies c/b <= a
proof
assume that
A1: b<0 and
A2: a*b<=c;
a*b/b>=c/b by A1,A2,Lm30;
hence thesis by A1,XCMPLX_1:89;
end;
theorem Th79:
0 < b & c <= a*b implies c/b <= a
proof
assume that
A1: b>0 and
A2: a*b>=c;
a*b/b>=c/b by A1,A2,Lm25;
hence thesis by A1,XCMPLX_1:89;
end;
theorem Th80:
b < 0 & c <= a*b implies a <= c/b
proof
assume that
A1: b<0 and
A2: a*b>=c;
a*b/b<=c/b by A1,A2,Lm30;
hence thesis by A1,XCMPLX_1:89;
end;
theorem Th81:
0 < b & a*b < c implies a < c/b
proof
assume that
A1: b>0 and
A2: a*b<c;
a*b/b<c/b by A1,A2,Lm26;
hence thesis by A1,XCMPLX_1:89;
end;
theorem Th82:
b < 0 & a*b < c implies c/b < a
proof
assume that
A1: b<0 and
A2: a*b<c;
a*b/b>c/b by A1,A2,Lm29;
hence thesis by A1,XCMPLX_1:89;
end;
theorem Th83:
0 < b & c < a*b implies c/b < a
proof
assume that
A1: b>0 and
A2: a*b>c;
a*b/b>c/b by A1,A2,Lm26;
hence thesis by A1,XCMPLX_1:89;
end;
theorem Th84:
b < 0 & c < a*b implies a < c/b
proof
assume that
A1: b<0 and
A2: a*b>c;
a*b/b<c/b by A1,A2,Lm29;
hence thesis by A1,XCMPLX_1:89;
end;
Lm32: 0 < a & a <= b implies b" <= a"
proof
assume that
A1: 0<a and
A2: a<=b;
a*(b")<=b*(b") by A1,A2,Lm12;
then a*(b")<=1 by A1,A2,XCMPLX_0:def 7;
then a"*(a*b")<=1*a" by A1,Lm12;
then a"*a*b"<=1*a";
then 1*b"<=1*a" by A1,XCMPLX_0:def 7;
hence thesis;
end;
Lm33: b < 0 & a <= b implies b" <= a"
proof
assume that
A1: 0>b and
A2: a<=b;
b*(a")<=a*(a") by A1,A2,Lm28;
then b*(a")<=1 by A1,A2,XCMPLX_0:def 7;
then b"*(b*(a"))>=1*(b") by A1,Lm28;
then b"*b*a">=1*b";
then 1*a">=1*b" by A1,XCMPLX_0:def 7;
hence thesis;
end;
begin
theorem
0 < a & a <= b implies b" <= a" by Lm32;
theorem
b < 0 & a <= b implies b" <= a" by Lm33;
theorem
b < 0 & a < b implies b" < a" by Lm31;
Lm34: 0 < a & a < b implies b" < a"
proof
A1: b" = 1/b by XCMPLX_1:215;
assume that
A2: 0<a and
A3: a<b;
a*(b")<b*(b") by A2,A3,Lm13;
then a*(b")<1 by A1,A2,A3,XCMPLX_1:87;
then a"*(a*(b"))<1*(a") by A2,Lm13;
then a"*a*b"<1*(a");
then 1*b"<1*(a") by A2,XCMPLX_0:def 7;
hence thesis;
end;
theorem
0 < a & a < b implies b" < a" by Lm34;
theorem
0 < b" & b" <= a" implies a <= b
proof
assume that
A1: b">0 and
A2: a">=b";
a""<=b"" by A1,A2,Lm32;
hence thesis;
end;
theorem
a" < 0 & b" <= a" implies a <= b
proof
assume that
A1: a"<0 and
A2: a">=b";
a""<=b"" by A1,A2,Lm33;
hence thesis;
end;
theorem
0 < b" & b" < a" implies a < b
proof
assume that
A1: b">0 and
A2: a">b";
a""<b"" by A1,A2,Lm34;
hence thesis;
end;
theorem
a" < 0 & b" < a" implies a < b
proof
assume that
A1: a"<0 and
A2: a">b";
a""<b"" by A1,A2,Lm31;
hence thesis;
end;
Lm35: for a being non negative non positive Real holds 0 = a*b;
begin
theorem
0 <= a & (b-a)*(b+a) <= 0 implies -a <= b & b <= a
proof
assume that
A1: a>=0 and
A2: (b-a)*(b+a)<=0;
b+0<=b+a by A1,Lm6;
then b+a>=0 by A1,A2;
then
A3: b>=0-a by Lm18;
b-a>=0 & b+a<=0 or b-a<=0 & b+a>=0 by A2;
then b<=a+0 by A1,Lm19;
hence thesis by A3;
end;
theorem
0 <= a & (b-a)*(b+a) < 0 implies -a < b & b < a
proof
assume that
A1: a>=0 and
A2: (b-a)*(b+a)<0;
A3: b-a>0 & b+a<0 or b-a<0 & b+a>0 by A2,Lm35;
then
A4: b<a+0 by A1,Lm16;
b+0<=b+a by A1,Lm6;
then b>0-a by A1,A3,Lm17;
hence thesis by A4;
end;
theorem
0 <= (b-a)*(b+a) implies b <= -a or a <= b
proof
assume (b-a)*(b+a)>=0;
then b-a>=0 & b+a>=0 or b-a<=0 & b+a<=0;
then b-a+a>=0+a or b+a<=0 by Lm6;
then b>=0+a or b+a-a<=0-a by Lm7;
hence thesis;
end;
theorem
0 <= a & 0 <= c & a < b & c < d implies a*c < b*d
proof
assume that
A1: 0<=a and
A2: 0<=c and
A3: a<b and
A4: c < d;
A5: a*c <= a*d by A1,A4,Lm12;
a*d<b*d by A2,A3,A4,Lm13;
hence thesis by A5,XXREAL_0:2;
end;
theorem
0 <= a & 0 < c & a < b & c <= d implies a*c < b*d
proof
assume that
A1: 0<=a and
A2: 0<c and
A3: a<b and
A4: c <=d;
A5: a*c <=a*d by A1,A4,Lm12;
a*d<b*d by A2,A3,A4,Lm13;
hence thesis by A5,XXREAL_0:2;
end;
theorem Th98:
0 < a & 0 < c & a <= b & c < d implies a*c < b*d
proof
assume that
A1: 0<a and
A2: 0<c and
A3: a<=b and
A4: c < d;
A5: a*c < a*d by A1,A4,Lm13;
a*d<=b*d by A2,A3,A4,Lm12;
hence thesis by A5,XXREAL_0:2;
end;
theorem
0 < c & b < 0 & a < b implies c/b < c/a
proof
assume that
A1: c>0 and
A2: b<0 and
A3: a<b;
a">b" by A2,A3,Lm31;
then a"*c>b"*c by A1,Lm13;
then c/a>b"*c by XCMPLX_0:def 9;
hence thesis by XCMPLX_0:def 9;
end;
theorem
c < 0 & 0 < a & a < b implies c/a < c/b
proof
assume that
A1: c < 0 and
A2: a>0 and
A3: a<b;
a">b" by A2,A3,Lm34;
then a"*c < b"*c by A1,Lm24;
then c/a<b"*c by XCMPLX_0:def 9;
hence thesis by XCMPLX_0:def 9;
end;
theorem
c < 0 & b < 0 & a < b implies c/a < c/b
proof
assume that
A1: c < 0 and
A2: b<0 and
A3: a<b;
a">b" by A2,A3,Lm31;
then a"*c < b"*c by A1,Lm24;
then c/a<b"*c by XCMPLX_0:def 9;
hence thesis by XCMPLX_0:def 9;
end;
theorem
0 < b & 0 < d & a*d <= c*b implies a/b <= c/d
proof
assume that
A1: b>0 and
A2: d>0 and
A3: a*d<=c*b;
a*d/b<=c by A1,A3,Th79;
then a/b*d<=c by XCMPLX_1:74;
hence thesis by A2,Th77;
end;
theorem
b < 0 & d < 0 & a*d <= c*b implies a/b <= c/d
proof
assume that
A1: b<0 and
A2: d<0 and
A3: a*d<=c*b;
a*d/b>=c by A1,A3,Th80;
then a/b*d>=c by XCMPLX_1:74;
hence thesis by A2,Th80;
end;
theorem
0 < b & d < 0 & a*d <= c*b implies c/d <= a/b
proof
assume that
A1: b>0 and
A2: d<0 and
A3: a*d<=c*b;
a*d/b<=c by A1,A3,Th79;
then a/b*d<=c by XCMPLX_1:74;
hence thesis by A2,Th78;
end;
theorem
b < 0 & 0 < d & a*d <= c*b implies c/d <= a/b
proof
assume that
A1: b<0 and
A2: d>0 and
A3: a*d<=c*b;
a*d/b>=c by A1,A3,Th80;
then a/b*d>=c by XCMPLX_1:74;
hence thesis by A2,Th79;
end;
theorem
0 < b & 0 < d & a*d < c*b implies a/b < c/d
proof
assume that
A1: b>0 and
A2: d>0 and
A3: a*d<c*b;
a*d/b<c by A1,A3,Th83;
then a/b*d<c by XCMPLX_1:74;
hence thesis by A2,Th81;
end;
theorem
b < 0 & d < 0 & a*d < c*b implies a/b < c/d
proof
assume that
A1: b<0 and
A2: d<0 and
A3: a*d<c*b;
a*d/b>c by A1,A3,Th84;
then a/b*d>c by XCMPLX_1:74;
hence thesis by A2,Th84;
end;
theorem
0 < b & d < 0 & a*d < c*b implies c/d < a/b
proof
assume that
A1: b>0 and
A2: d<0 and
A3: a*d<c*b;
a*d/b<c by A1,A3,Th83;
then a/b*d<c by XCMPLX_1:74;
hence thesis by A2,Th82;
end;
theorem
b < 0 & 0 < d & a*d < c*b implies c/d < a/b
proof
assume that
A1: b<0 and
A2: d>0 and
A3: a*d<c*b;
a*d/b>c by A1,A3,Th84;
then a/b*d>c by XCMPLX_1:74;
hence thesis by A2,Th83;
end;
theorem
b < 0 & d < 0 & a*b < c/d implies a*d < c/b
proof
assume that
A1: b<0 and
A2: d<0;
assume a*b<c/d;
then a*b*d>c by A2,Th78;
then a*d*b>c;
hence thesis by A1,Th84;
end;
theorem
0 < b & 0 < d & a*b < c/d implies a*d < c/b
proof
assume that
A1: b>0 and
A2: d>0;
assume a*b<c/d;
then a*b*d<c by A2,Th79;
then a*d*b<c;
hence thesis by A1,Th81;
end;
theorem
b < 0 & d < 0 & c/d < a*b implies c/b < a*d
proof
assume that
A1: b<0 and
A2: d<0;
assume a*b>c/d;
then a*b*d<c by A2,Th80;
then a*d*b<c;
hence thesis by A1,Th82;
end;
theorem
0 < b & 0 < d & c/d < a*b implies c/b < a*d
proof
assume that
A1: b>0 and
A2: d>0;
assume a*b>c/d;
then a*b*d>c by A2,Th77;
then a*d*b>c;
hence thesis by A1,Th83;
end;
theorem
b < 0 & 0 < d & a*b < c/d implies c/b < a*d
proof
assume that
A1: b<0 and
A2: d>0;
assume a*b<c/d;
then a*b*d<c by A2,Th79;
then a*d*b<c;
hence thesis by A1,Th82;
end;
theorem
0 < b & d < 0 & a*b < c/d implies c/b < a*d
proof
assume that
A1: b>0 and
A2: d<0;
assume a*b<c/d;
then a*b*d>c by A2,Th78;
then a*d*b>c;
hence thesis by A1,Th83;
end;
theorem
b < 0 & 0 < d & c/d < a*b implies a*d < c/b
proof
assume that
A1: b<0 and
A2: d>0;
assume a*b>c/d;
then a*b*d>c by A2,Th77;
then a*d*b>c;
hence thesis by A1,Th84;
end;
theorem
0 < b & d < 0 & c/d < a*b implies a*d < c/b
proof
assume that
A1: b>0 and
A2: d<0;
assume a*b>c/d;
then a*b*d<c by A2,Th80;
then a*d*b<c;
hence thesis by A1,Th81;
end;
theorem
0 < a & 0 <= c & a <= b implies c/b <= c/a
proof
assume that
A1: 0<a and
A2: 0<=c and
A3: a<=b;
a*b"<=b*b" by A1,A3,Lm12;
then a*b"<=1 by A1,A3,XCMPLX_0:def 7;
then a"*(a*b")<=a"*1 by A1,Lm12;
then a"*a*b"<=a";
then 1*b"<=a" by A1,XCMPLX_0:def 7;
then c*b"<=c*a" by A2,Lm12;
then c/b<=c*a" by XCMPLX_0:def 9;
hence thesis by XCMPLX_0:def 9;
end;
theorem
0 <= c & b < 0 & a <= b implies c/b <= c/a
proof
assume that
A1: c>=0 and
A2: b<0 and
A3: a<=b;
a">=b" by A2,A3,Lm33;
then a"*c>=b"*c by A1,Lm12;
then c/a>=b"*c by XCMPLX_0:def 9;
hence thesis by XCMPLX_0:def 9;
end;
theorem
c <= 0 & 0 < a & a <= b implies c/a <= c/b
proof
assume
A1: c <= 0;
assume that
A2: a>0 and
A3: a<=b;
a">=b" by A2,A3,Lm32;
then a"*c <= b"*c by A1,Lm28;
then c/a<=b"*c by XCMPLX_0:def 9;
hence thesis by XCMPLX_0:def 9;
end;
theorem
c <= 0 & b < 0 & a <= b implies c/a <= c/b
proof
assume that
A1: c <= 0 and
A2: b<0 and
A3: a<=b;
a">=b" by A2,A3,Lm33;
then a"*c <= b"*c by A1,Lm28;
then c/a<=b"*c by XCMPLX_0:def 9;
hence thesis by XCMPLX_0:def 9;
end;
theorem
0 < a iff 0 < a";
theorem
a < 0 iff a" < 0;
theorem Th124:
a < 0 & 0 < b implies a" < b"
proof
assume that
A1: a<0 and
A2: b>0;
a"<0 by A1;
hence thesis by A2;
end;
theorem
a" < 0 & 0 < b" implies a < b
proof
assume that
A1: a"<0 and
A2: b">0;
a""<b"" by A1,A2,Th124;
hence thesis;
end;
begin
theorem
a <= 0 & 0 <= a implies 0 = a*b by Lm35;
theorem
0 <= a & 0 <= b implies 0 <= a*b;
theorem
a <= 0 & b <= 0 implies 0 <= a*b;
theorem
0 < a & 0 < b implies 0 < a*b;
theorem
a < 0 & b < 0 implies 0 < a*b;
theorem
0 <= a & b <= 0 implies a*b <= 0;
theorem
0 < a & b < 0 implies a*b < 0;
theorem
a*b < 0 implies a > 0 & b < 0 or a < 0 & b > 0
proof
assume
A1: a*b<0;
then
A2: b <> 0;
a <> 0 by A1;
hence thesis by A1,A2;
end;
theorem
a*b > 0 implies a > 0 & b > 0 or a < 0 & b < 0
proof
assume
A1: a*b>0;
then
A2: b <> 0;
a <> 0 by A1;
hence thesis by A1,A2;
end;
theorem
a <= 0 & b <= 0 implies 0 <= a/b;
theorem
0 <= a & 0 <= b implies 0 <= a/b;
theorem
0 <= a & b <= 0 implies a/b <= 0;
theorem
a <= 0 & 0 <= b implies a/b <= 0;
theorem
0 < a & 0 < b implies 0 < a/b;
theorem
a < 0 & b < 0 implies 0 < a/b;
theorem
a < 0 & 0 < b implies a/b < 0;
theorem
a < 0 & 0 < b implies b/a < 0;
theorem
a/b < 0 implies b < 0 & a > 0 or b > 0 & a < 0
proof
assume
A1: a/b<0;
then
A2: a <> 0;
a/b = a*b" by XCMPLX_0:def 9;
then b" <> 0 by A1;
hence thesis by A1,A2;
end;
theorem
a/b > 0 implies b > 0 & a > 0 or b < 0 & a < 0
proof
assume
A1: a/b>0;
then
A2: a <> 0;
a/b = a*b" by XCMPLX_0:def 9;
then b" <> 0 by A1;
hence thesis by A1,A2;
end;
begin
theorem
a <= b implies a < b+1
proof
assume a<=b;
then
A1: a-1<=b-1 by Lm7;
b-1<b-1+1 by Lm9;
then a-1<b by A1,XXREAL_0:2;
then a-1+1<b+1 by Lm10;
hence thesis;
end;
theorem
a - 1 < a
proof
a+- 1 < a + 0 by Lm10;
hence thesis;
end;
theorem
a <= b implies a-1 < b
proof
assume a<=b;
then
A1: a-1<=b-1 by Lm7;
b-1<b-1+1 by Lm9;
hence thesis by A1,XXREAL_0:2;
end;
theorem
-1 < a implies 0 < 1+a
proof
assume -1<a;
then -1+1<a+1 by Lm8;
hence thesis;
end;
theorem
a < 1 implies 1-a > 0 by Lm21;
begin
theorem
a <= 1 & 0 <= b & b <= 1 & a*b = 1 implies a = 1
proof
assume that
A1: a<=1 and
A2: 0<=b and
A3: b<=1 and
A4: a*b=1;
now
per cases by A2;
case
b=0;
hence contradiction by A4;
end;
case
A5: b>0;
then a=b" by A4,XCMPLX_0:def 7;
then a>=1" by A3,A5,Lm32;
hence thesis by A1,XXREAL_0:1;
end;
end;
hence thesis;
end;
theorem
0 <= a & 1 <= b implies a <= a*b
proof
assume that
A1: a>=0 and
A2: b>=1;
a*b>=a*1 by A1,A2,Lm12;
hence thesis;
end;
theorem
a <= 0 & b <= 1 implies a <= a*b
proof
assume that
A1: a<=0 and
A2: b<=1;
a*b>=a*1 by A1,A2,Lm28;
hence thesis;
end;
theorem
0 <= a & b <= 1 implies a*b <= a
proof
assume that
A1: a>=0 and
A2: b<=1;
a*b<=a*1 by A1,A2,Lm12;
hence thesis;
end;
theorem
a <= 0 & 1 <= b implies a*b <= a
proof
assume that
A1: a<=0 and
A2: b>=1;
a*b<=a*1 by A1,A2,Lm28;
hence thesis;
end;
theorem Th155:
0 < a & 1 < b implies a < a*b
proof
assume that
A1: a>0 and
A2: b>1;
a*b>a*1 by A1,A2,Lm13;
hence thesis;
end;
theorem
a < 0 & b < 1 implies a < a*b
proof
assume that
A1: a<0 and
A2: b<1;
a*b>a*1 by A1,A2,Lm24;
hence thesis;
end;
theorem
0 < a & b < 1 implies a*b < a
proof
assume that
A1: a>0 and
A2: b<1;
a*b<a*1 by A1,A2,Lm13;
hence thesis;
end;
theorem
a < 0 & 1 < b implies a*b < a
proof
assume that
A1: a<0 and
A2: b>1;
a*b<a*1 by A1,A2,Lm24;
hence thesis;
end;
theorem
1 <= a & 1 <= b implies 1 <= a*b
proof
assume that
A1: a>=1 and
A2: b>=1;
a*b>=b*1 by A1,A2,Lm12;
hence thesis by A2,XXREAL_0:2;
end;
theorem
0 <= a & a <= 1 & b <= 1 implies a*b <= 1
proof
assume that
A1: 0<=a and
A2: a<=1 and
A3: b<=1;
a*b<=1*a by A1,A3,Lm12;
hence thesis by A2,XXREAL_0:2;
end;
theorem
1 < a & 1 <= b implies 1 < a*b
proof
assume that
A1: a>1 and
A2: b>=1;
a*b>b*1 by A1,A2,Lm13;
hence thesis by A2,XXREAL_0:2;
end;
theorem
0 <= a & a < 1 & b <= 1 implies a*b < 1
proof
assume that
A1: 0<=a and
A2: a<1 and
A3: b<=1;
a*b<=1*a by A1,A3,Lm12;
hence thesis by A2,XXREAL_0:2;
end;
theorem
a <= -1 & b <= -1 implies 1 <= a*b
proof
assume that
A1: a<=-1 and
A2: b<=-1;
A3: -b>=--1 by A2,Lm14;
a*b>=b*(-1) by A1,A2,Lm28;
hence thesis by A3,XXREAL_0:2;
end;
theorem
a < -1 & b <= -1 implies 1 < a*b
proof
assume that
A1: a<-1 and
A2: b<=-1;
A3: -b>=--1 by A2,Lm14;
a*b>b*(-1) by A1,A2,Lm24;
hence thesis by A3,XXREAL_0:2;
end;
theorem
a <= 0 & -1 <= a & -1 <= b implies a*b <= 1
proof
assume that
A1: 0>=a and
A2: a>=-1 and
A3: b>=-1;
A4: -a<=--1 by A2,Lm14;
a*b<=(-1)*a by A1,A3,Lm28;
hence thesis by A4,XXREAL_0:2;
end;
theorem
a <= 0 & -1 < a & -1 <= b implies a*b < 1
proof
assume that
A1: 0>=a and
A2: a>-1 and
A3: b>=-1;
A4: -a<--1 by A2,Lm15;
a*b<=(-1)*a by A1,A3,Lm28;
hence thesis by A4,XXREAL_0:2;
end;
begin
theorem Th167:
(for a st 1 < a holds c <= b*a) implies c <= b
proof
assume
A1: for a st a>1 holds b*a>=c;
assume
A2: not thesis;
A3: b>=0
proof
A4: c <= b*2 by A1;
assume b<0;
then
A5: b*2<0;
then c < 0 by A1;
then b/c>c/c by A2,Lm29;
then b/c>1 by A5,A4,XCMPLX_1:60;
then
A6: b*(b/c)>=c by A1;
b*(b/c)<c*(b/c) by A2,A5,A4,Lm13;
then b*(b/c)<b by A5,A4,XCMPLX_1:87;
hence contradiction by A2,A6,XXREAL_0:2;
end;
per cases by A3;
suppose
A7: b>0;
then b/b<c/b by A2,Lm26;
then 1<c/b by A7,XCMPLX_1:60;
then consider d being Real such that
A8: 1<d and
A9: d<c/b by Th5;
b*d<b*(c/b) by A7,A9,Lm13;
then b*d<c by A7,XCMPLX_1:87;
hence contradiction by A1,A8;
end;
suppose
A10: b=0;
b*2>=c by A1;
hence contradiction by A2,A10;
end;
end;
Lm36: 1 < a implies a" < 1
proof
assume
A1: 1<a;
then 1*a"<a*a" by Lm13;
hence thesis by A1,XCMPLX_0:def 7;
end;
theorem
(for a st 0 < a & a < 1 holds b*a <= c) implies b <= c
proof
assume
A1: for a st 0<a & a<1 holds b*a<=c;
now
let d;
assume
A2: d>1;
then b*(d")<=c by A1,Lm36;
then b/d<=c by XCMPLX_0:def 9;
hence b<=c*d by A2,Th81;
end;
hence thesis by Th167;
end;
Lm37: a <= b & 0 <= a implies a/b <= 1
proof
assume
A1: a <= b;
assume
A2: 0 <= a;
per cases by A2;
suppose
a = 0;
hence thesis;
end;
suppose
A3: a > 0;
then a/b<=b/b by A1,Lm25;
hence thesis by A1,A3,XCMPLX_1:60;
end;
end;
Lm38: b <= a & 0 <= a implies b/a <= 1
proof
assume
A1: b <= a;
assume
A2: a>=0;
per cases by A2;
suppose
a = 0;
then a" = 0;
then b*a" < 1;
hence thesis by XCMPLX_0:def 9;
end;
suppose
A3: a > 0;
assume b/a>1;
then b/a*a>1*a by A3,Lm13;
hence thesis by A1,A3,XCMPLX_1:87;
end;
end;
theorem
(for a st 0 < a & a < 1 holds b <= a*c) implies b <= 0
proof
assume that
A1: for a st 0 < a & a < 1 holds b <= a*c and
A2: b > 0;
A3: b*2 > b by A2,Th155;
then
A4: b > b/2 by Th83;
per cases;
suppose
c <= 0;
then 1/2*c <= 0;
hence contradiction by A1,A2;
end;
suppose that
A5: c <= b and
A6: c > 0;
set a = c/(2*b);
c/b*2 > c/b by A2,A6,Th155;
then c/b > c/b/2 by Th83;
then
A7: c/b > c/(b*2) by XCMPLX_1:78;
c/b <= 1 by A5,A6,Lm37;
then a < 1 by A7,XXREAL_0:2;
then
A8: a*c >= b by A1,A2,A6;
per cases;
suppose
c >= b;
then b = c by A5,XXREAL_0:1;
then a*c = b/2 by A6,XCMPLX_1:92;
hence contradiction by A2,A8,Th83,Th155;
end;
suppose
A9: c < b;
then a*c < c/(2*b)*b by A6,Th98;
then
A10: a*c < c/2 by A2,XCMPLX_1:92;
c/2 < b/2 by A9,Lm26;
then a*c < b/2 by A10,XXREAL_0:2;
hence contradiction by A4,A8,XXREAL_0:2;
end;
end;
suppose that
A11: b <= c and
A12: c > 0;
set a = b/(2*c);
b/c*2 > b/c by A2,A12,Th155;
then b/c > b/c/2 by Th83;
then
A13: b/c > b/(c*2) by XCMPLX_1:78;
b/c <= 1 by A11,A12,Lm38;
then a < 1 by A13,XXREAL_0:2;
then
A14: a*c >= b by A1,A2,A12;
a*c = b/2 by A12,XCMPLX_1:92;
hence contradiction by A3,A14,Th83;
end;
end;
theorem
0 <= d & d <= 1 & 0 <= a & 0 <= b & d*a+(1-d)*b = 0 implies d = 0 & b = 0 or
d = 1 & a = 0 or a = 0 & b = 0
proof
assume that
A1: 0<=d and
A2: d<=1 and
A3: a>=0 and
A4: b>=0 and
A5: d*a+(1-d)*b=0;
d-d<=1-d by A2,Lm7;
then 1-d=0 or b=0 by A1,A3,A4,A5;
hence thesis by A5;
end;
theorem
0 <= d & a <= b implies a <= (1-d)*a+d*b
proof
assume that
A1: 0<=d and
A2: a<=b;
d*a<=d*b by A1,A2,Lm12;
then (1-d)*a+d*a<=(1-d)*a+d*b by Lm6;
hence thesis;
end;
theorem
d <= 1 & a <= b implies (1-d)*a+d*b <= b
proof
assume that
A1: d<=1 and
A2: a<=b;
1-d>=0 by A1,Th48;
then (1-d)*a<=(1-d)*b by A2,Lm12;
then (1-d)*a+d*b<=(1-d)*b+d*b by Lm6;
hence thesis;
end;
theorem
0 <= d & d <= 1 & a <= b & a <= c implies a <= (1-d)*b+d*c
proof
assume that
A1: 0<=d and
A2: d<=1 and
A3: a<=b and
A4: a<=c;
1-d>=0 by A2,Th48;
then
A5: (1-d)*a<=(1-d)*b by A3,Lm12;
A6: (1-d)*a+d*a = a;
d*a<=d*c by A1,A4,Lm12;
hence thesis by A5,A6,Lm6;
end;
theorem
0 <= d & d <= 1 & b <= a & c <= a implies (1-d)*b+d*c <= a
proof
assume that
A1: 0<=d and
A2: d<=1 and
A3: a>=b and
A4: a>=c;
1-d>=0 by A2,Th48;
then
A5: (1-d)*a>=(1-d)*b by A3,Lm12;
A6: (1-d)*a+d*a = a;
d*a>=d*c by A1,A4,Lm12;
hence thesis by A5,A6,Lm6;
end;
theorem
0 <= d & d <= 1 & a < b & a < c implies a < (1-d)*b+d*c
proof
assume that
A1: 0 <= d and
A2: d <= 1 and
A3: a<b and
A4: a<c;
per cases;
suppose
d=0;
hence thesis by A3;
end;
suppose
d=1;
hence thesis by A4;
end;
suppose
A5: not(d=0 or d=1);
then d<1 by A2,XXREAL_0:1;
then 1-d>0 by Lm21;
then
A6: (1-d)*a<(1-d)*b by A3,Lm13;
A7: (1-d)*a+d*a=a;
d*a<d*c by A1,A4,A5,Lm13;
hence thesis by A6,A7,Lm8;
end;
end;
theorem
0 <= d & d <= 1 & b < a & c < a implies (1-d)*b+d*c < a
proof
assume that
A1: 0 <= d and
A2: d <= 1 and
A3: a>b and
A4: a>c;
per cases;
suppose
d=0;
hence thesis by A3;
end;
suppose
d=1;
hence thesis by A4;
end;
suppose
A5: not(d=0 or d=1);
then d<1 by A2,XXREAL_0:1;
then 1-d>0 by Lm21;
then
A6: (1-d)*a>(1-d)*b by A3,Lm13;
A7: (1-d)*a+d*a=a;
d*a>d*c by A1,A4,A5,Lm13;
hence thesis by A6,A7,Lm8;
end;
end;
theorem
0 < d & d < 1 & a <= b & a < c implies a < (1-d)*b+d*c
proof
assume that
A1: 0 < d and
A2: d < 1 and
A3: a <= b and
A4: a < c;
1-d > 0 by A2,Lm21;
then
A5: (1-d)*a <= (1-d)*b by A3,Lm12;
A6: (1-d)*a+d*a = a;
d*a < d*c by A1,A4,Lm13;
hence thesis by A5,A6,Lm8;
end;
theorem
0 < d & d < 1 & b < a & c <= a implies (1-d)*b+d*c < a
proof
assume that
A1: 0 < d and
A2: d < 1 and
A3: a > b and
A4: a >= c;
1-d > 0 by A2,Lm21;
then
A5: (1-d)*a > (1-d)*b by A3,Lm13;
A6: (1-d)*a+d*a = a;
d*a >= d*c by A1,A4,Lm12;
hence thesis by A5,A6,Lm8;
end;
theorem
0 <= d & d <= 1 & a <= (1-d)*a+d*b & b < (1-d)*a+d*b implies d = 0
proof
assume that
A1: d >= 0 and
A2: d <= 1 and
A3: a <= (1-d)*a + d*b and
A4: b < (1-d)*a + d*b;
set s = (1-d)*a + d*b;
assume d <> 0;
then
A5: d*b < d*s by A1,A4,Lm13;
1-d >= 0 by A2,Th48;
then
A6: (1-d)*a <= (1-d)*s by A3,Lm12;
1*s = (1-d)*s + d*s;
hence contradiction by A5,A6,Lm8;
end;
theorem
0 <= d & d <= 1 & (1-d)*a+d*b <= a & (1-d)*a+d*b < b implies d = 0
proof
assume that
A1: d >= 0 and
A2: d <= 1 and
A3: a >= (1-d)*a + d*b and
A4: b > (1-d)*a + d*b;
set s = (1-d)*a + d*b;
assume d <> 0;
then
A5: d*b > d*s by A1,A4,Lm13;
1-d >= 0 by A2,Th48;
then
A6: (1-d)*a >= (1-d)*s by A3,Lm12;
1*s = (1-d)*s + d*s;
hence contradiction by A5,A6,Lm8;
end;
begin
theorem
0 < a & a <= b implies 1 <= b/a
proof
assume that
A1: 0<a and
A2: a<=b;
b/a>=a/a by A1,A2,Lm25;
hence thesis by A1,XCMPLX_1:60;
end;
theorem
a < 0 & b <= a implies 1 <= b/a
proof
assume
A1: a < 0;
assume b <= a;
then b/a >= a/a by A1,Lm30;
hence thesis by A1,XCMPLX_1:60;
end;
theorem
0 <= a & a <= b implies a/b <= 1 by Lm37;
theorem
b <= a & a <= 0 implies a/b <= 1
proof
assume
A1: b <= a;
assume a <= 0;
then per cases;
suppose a = 0;
hence thesis;
end;
suppose
A3: a < 0;
then a/b <= b/b by A1,Lm30;
hence thesis by A1,A3,XCMPLX_1:60;
end;
end;
theorem
0 <= a & b <= a implies b/a <= 1 by Lm38;
theorem
a <= 0 & a <= b implies b/a <= 1
proof
assume a <= 0;
then per cases;
suppose a = 0;
then a" = 0;
then b*a" = 0;
hence thesis by XCMPLX_0:def 9;
end;
suppose
A2: a < 0;
assume
A3: a <= b;
assume b/a > 1;
then b/a*a < 1*a by A2,Lm24;
hence thesis by A2,A3,XCMPLX_1:87;
end;
end;
theorem
0 < a & a < b implies 1 < b/a
proof
assume
A1: a > 0;
assume
A2: a < b;
assume b/a <= 1;
then b/a*a <= 1*a by A1,Lm12;
hence thesis by A1,A2,XCMPLX_1:87;
end;
theorem
a < 0 & b < a implies 1 < b/a
proof
assume
A1: a < 0;
assume b < a;
then b/a > a/a by A1,Lm29;
hence thesis by A1,XCMPLX_1:60;
end;
theorem
0 <= a & a < b implies a/b < 1
proof
assume
A1: 0 <= a & a < b;
then a/b < b/b by Lm26;
hence thesis by A1,XCMPLX_1:60;
end;
theorem
a <= 0 & b < a implies a/b < 1
proof
assume
A1: a <= 0 & b < a;
then a/b < b/b by Lm29;
hence thesis by A1,XCMPLX_1:60;
end;
theorem
0 < a & b < a implies b/a < 1
proof
assume that
A1: a > 0 and
A2: b < a;
assume b/a >= 1;
then b/a*a >= 1*a by A1,Lm12;
hence thesis by A1,A2,XCMPLX_1:87;
end;
theorem
a < 0 & a < b implies b/a < 1
proof
assume that
A1: a < 0 and
A2: a < b;
assume b/a >= 1;
then b/a*a <= 1*a by A1,Lm28;
hence thesis by A1,A2,XCMPLX_1:87;
end;
begin
theorem
0 <= b & -b <= a implies -1 <= a/b
proof
assume b >= 0;
then per cases;
suppose b = 0;
then b" = 0;
then a*b" = 0;
hence thesis by XCMPLX_0:def 9;
end;
suppose
A2: b > 0;
assume
A3: -b <= a;
assume a/b < -1;
then a/b*b < (-1)*b by A2,Lm13;
hence thesis by A2,A3,XCMPLX_1:87;
end;
end;
theorem
0 <= b & -a <= b implies -1 <= a/b
proof
assume b >= 0;
then per cases;
suppose b = 0;
then b" = 0;
then a*b" = 0;
hence thesis by XCMPLX_0:def 9;
end;
suppose
A2: b > 0;
assume
A3: -a <= b;
assume a/b < -1;
then a/b*b < (-1)*b by A2,Lm13;
then a < -b by A2,XCMPLX_1:87;
hence thesis by A3,Th26;
end;
end;
theorem
b <= 0 & a <= -b implies -1 <= a/b
proof
assume b <= 0;
then per cases;
suppose b = 0;
then b" = 0;
then a*b" = 0;
hence thesis by XCMPLX_0:def 9;
end;
suppose
A2: b < 0;
assume
A3: a <= -b;
assume a/b < -1;
then a/b*b > (-1)*b by A2,Lm24;
hence thesis by A2,A3,XCMPLX_1:87;
end;
end;
theorem
b <= 0 & b <= -a implies -1 <= a/b
proof
assume b <= 0;
then per cases;
suppose b = 0;
then b" = 0;
then a*b" = 0;
hence thesis by XCMPLX_0:def 9;
end;
suppose
A2: b < 0;
assume
A3: b <= -a;
assume a/b < -1;
then a/b*b > (-1)*b by A2,Lm24;
then a > -b by A2,XCMPLX_1:87;
hence thesis by A3,Th25;
end;
end;
theorem
0 < b & -b < a implies -1 < a/b
proof
assume that
A1: b > 0 and
A2: -b < a;
assume a/b <= -1;
then a/b*b <= (-1)*b by A1,Lm12;
hence thesis by A1,A2,XCMPLX_1:87;
end;
theorem
0 < b & -a < b implies -1 < a/b
proof
assume that
A1: b > 0 and
A2: -a < b;
assume a/b <= -1;
then a/b*b <= (-1)*b by A1,Lm12;
then a <= -b by A1,XCMPLX_1:87;
hence thesis by A2,Th25;
end;
theorem
b < 0 & a < -b implies -1 < a/b
proof
assume that
A1: b < 0 and
A2: a < -b;
assume a/b <= -1;
then a/b*b >= (-1)*b by A1,Lm28;
hence thesis by A1,A2,XCMPLX_1:87;
end;
theorem
b < 0 & b < -a implies -1 < a/b
proof
assume that
A1: b < 0 and
A2: b < -a;
assume a/b <= -1;
then a/b*b >= (-1)*b by A1,Lm28;
then a >= -b by A1,XCMPLX_1:87;
hence thesis by A2,Th26;
end;
theorem
0 < b & a <= -b implies a/b <= -1
proof
assume that
A1: b > 0 and
A2: a <= -b;
assume a/b > -1;
then a/b*b > (-1)*b by A1,Lm13;
hence thesis by A1,A2,XCMPLX_1:87;
end;
theorem
0 < b & b <= -a implies a/b <= -1
proof
assume
A1: b>0;
assume
A2: b <= -a;
assume a/b>-1;
then a/b*b>(-1)*b by A1,Lm13;
then a>-b by A1,XCMPLX_1:87;
hence thesis by A2,Th25;
end;
theorem
b < 0 & -b <= a implies a/b <= -1
proof
assume that
A1: b < 0 and
A2: -b <= a;
assume a/b>-1;
then a/b*b < (-1)*b by A1,Lm24;
hence thesis by A1,A2,XCMPLX_1:87;
end;
theorem
b < 0 & -a <= b implies a/b <= -1
proof
assume that
A1: b < 0 and
A2: -a <= b;
assume a/b > -1;
then a/b*b < (-1)*b by A1,Lm24;
then a < -b by A1,XCMPLX_1:87;
hence thesis by A2,Th26;
end;
theorem
0 < b & a < -b implies a/b < -1
proof
assume that
A1: b > 0 and
A2: a < -b;
assume a/b >= -1;
then a/b*b >= (-1)*b by A1,Lm12;
hence thesis by A1,A2,XCMPLX_1:87;
end;
theorem
0 < b & b < -a implies a/b < -1
proof
assume
A1: b>0;
assume
A2: b < -a;
assume a/b >= -1;
then a/b*b >= (-1)*b by A1,Lm12;
then a >= -b by A1,XCMPLX_1:87;
hence thesis by A2,Th26;
end;
theorem
b < 0 & -b < a implies a/b < -1
proof
assume
A1: b < 0;
assume
A2: -b < a;
assume a/b >= -1;
then a/b*b <= (-1)*b by A1,Lm28;
hence thesis by A1,A2,XCMPLX_1:87;
end;
theorem
b < 0 & -a < b implies a/b < -1
proof
assume
A1: b < 0;
assume
A2: -a < b;
assume a/b >= -1;
then a/b*b <= (-1)*b by A1,Lm28;
then a <= -b by A1,XCMPLX_1:87;
hence thesis by A2,Th25;
end;
begin
theorem Th209:
(for a being Real st 0 < a & a < 1 holds c <= b/a) implies c <= b
proof
assume
A1: for a st a > 0 & a < 1 holds b/a >= c;
now
let d;
assume d > 1;
then
A2: b/(d") >= c by A1,Lm36;
d" = 1/d by XCMPLX_1:215;
then b*d/1 >= c by A2,XCMPLX_1:77;
hence b*d >= c;
end;
hence thesis by Th167;
end;
theorem
(for a being Real st 1 < a holds b/a <= c) implies b <= c
proof
assume
A1: for a st a > 1 holds b/a <= c;
now
let d;
A2: d" = 1/d by XCMPLX_1:215;
assume that
A3: 0 < d and
A4: d < 1;
d" > 1" by A3,A4,Lm34;
then b/(d") <= c by A1;
then b*d/1 <= c by A2,XCMPLX_1:77;
hence b <= c/d by A3,Th77;
end;
hence thesis by Th209;
end;
theorem
1 <= a implies a" <= 1
proof
1 <= a implies a" <= 1" by Lm32;
hence thesis;
end;
theorem
1 < a implies a" < 1 by Lm36;
theorem
a <= -1 implies -1 <= a"
proof
a <= -1 implies (-1)" <= a" by Lm33;
hence thesis;
end;
theorem
a < -1 implies -1 < a"
proof
a < -1 implies (-1)" < a" by Lm31;
hence thesis;
end;
begin
theorem
0 < a implies 0 < a/2;
theorem
0 < a implies a/2 < a by Lm27;
theorem
a <= 1/2 implies 2*a-1 <= 0
proof
assume a <= 1/2;
then 2 * a <= 2 * (1/2) by Lm12;
then 2 * a <= 1 + 0;
hence thesis by Lm18;
end;
theorem
a <= 1/2 implies 0 <= 1-2*a
proof
assume a <= 1/2;
then 2 * a <= 2 * (1/2) by Lm12;
then 2 * a + 0 <= 1;
hence thesis by Lm16;
end;
theorem
a >= 1/2 implies 2*a-1 >= 0
proof
assume a >= 1/2;
then 2 * a >= 2 * (1/2) by Lm12;
then 2 * a >= 1 + 0;
hence thesis by Lm16;
end;
theorem
a >= 1/2 implies 0 >= 1-2*a
proof
assume a >= 1/2;
then 2 * a >= 2 * (1/2) by Lm12;
then 2 * a + 0 >= 1;
hence thesis by Lm18;
end;
begin
theorem
0 < a implies a/3 < a
proof
assume
A1: 0 < a;
then
A2: a/3+a/3+0 < a/3+a/3+a/3 by Lm10;
0+a/3 < a/3+a/3 by A1,Lm10;
hence thesis by A2,XXREAL_0:2;
end;
theorem
0 < a implies 0 < a/3;
begin
theorem
0 < a implies a/4 < a
proof
assume
A1: 0 < a;
then
A2: 0+a/4 < a/4+a/4 by Lm10;
then a/4 < a/4+a/4+a/4 by A1,Lm10;
then a/4+a/4 < a/4+a/4+a/4+a/4 by Lm10;
hence thesis by A2,XXREAL_0:2;
end;
theorem
0 < a implies 0 < a/4;
theorem
for a,b st b <> 0 ex c st a = b/c
proof
let a,b;
assume
A1: b <> 0;
then consider c being Complex such that
A2: a = b/c by XCMPLX_1:232;
per cases;
suppose c = 0;
hence thesis by A2;
end;
suppose c <> 0;
then c = b/a by A1,A2,XCMPLX_1:54;
then reconsider c as Real;
take c;
thus thesis by A2;
end;
end;
begin :: Addenda
:: from TOPREAL3, 2006.07.15, A.T.
theorem
r < s implies r < (r+s)/2 & (r+s)/2 < s
proof
assume r < s;
then
A1: r/2 < s/2 by Lm26;
then r/2 + r/2 < r/2 + s/2 by Lm10;
hence r < (r+s)/2;
r/2 + s/2 < s/2 + s/2 by A1,Lm10;
hence thesis;
end;
:: missing, 2007.01.16, A.T.
registration
cluster -> ext-real for Element of REAL;
coherence;
end;
reserve p,q,r,s,t for ExtReal;
theorem Th227:
r < t implies ex s st r < s & s < t
proof
assume
A1: r < t;
then
A2: r <> +infty by XXREAL_0:3;
A3: t <> -infty by A1,XXREAL_0:5;
per cases by A2,A3,XXREAL_0:14;
suppose that
A4: r = -infty and
A5: t = +infty;
take 0;
thus thesis by A4,A5;
end;
suppose that
A6: r = -infty and
A7: t in REAL;
reconsider t as Real by A7;
consider s being Real such that
A8: s < t by Th2;
take s;
s in REAL by XREAL_0:def 1;
hence r < s by A6,XXREAL_0:12;
thus thesis by A8;
end;
suppose that
A9: r in REAL and
A10: t = +infty;
reconsider r9 = r as Real by A9;
consider s being Real such that
A11: r9 < s by Th1;
take s;
thus r < s by A11;
s in REAL by XREAL_0:def 1;
hence thesis by A10,XXREAL_0:9;
end;
suppose that
A12: r in REAL and
A13: t in REAL;
reconsider r,t as Real by A12,A13;
consider s being Real such that
A14: r < s & s < t by A1,Th5;
take s;
thus thesis by A14;
end;
end;
theorem
r < s & (for q st r < q & q < s holds t <= q) implies t <= r
proof
assume that
A1: r < s and
A2: for q st r < q & q < s holds t <= q;
for q st r < q holds t <= q
proof
let q such that
A3: r < q;
per cases;
suppose q < s;
hence thesis by A2,A3;
end;
suppose
A4: s <= q;
consider p such that
A5: r < p and
A6: p < s by A1,Th227;
t <= p by A2,A5,A6;
then t <= s by A6,XXREAL_0:2;
hence thesis by A4,XXREAL_0:2;
end;
end;
hence thesis by Th227;
end;
theorem
r < s & (for q st r < q & q < s holds q <= t) implies s <= t
proof
assume that
A1: r < s and
A2: for q st r < q & q < s holds q <= t;
for q st t < q holds s <= q
proof
let q such that
A3: t < q and
A4: q < s;
per cases;
suppose r < q;
hence thesis by A2,A3,A4;
end;
suppose
A5: q <= r;
consider p such that
A6: r < p and
A7: p < s by A1,Th227;
p <= t by A2,A6,A7;
then r <= t by A6,XXREAL_0:2;
hence thesis by A3,A5,XXREAL_0:2;
end;
end;
hence thesis by Th227;
end;
:: missing, 2008.08.13, A.T.
theorem
0 <= a & b <= c implies b-a <= c
proof
assume 0 <= a & b <= c;
then b+0 <= a+c by Th38;
hence thesis by Lm18;
end;
theorem
0 < a & b <= c implies b-a < c
proof
assume 0 < a & b <= c;
then b+0 < a+c by Th39;
hence thesis by Lm17;
end;
begin
theorem
a -' a = 0
proof
a-a = 0;
hence thesis by XREAL_0:def 2;
end;
theorem Th233:
b <= a implies a -' b = a - b by Th48,XREAL_0:def 2;
theorem
c <= a & c <= b & a -' c = b -' c implies a = b
proof
assume that
A1: a >= c and
A2: b >= c and
A3: a -' c = b -' c;
a - c >= 0 by A1,Th48;
then
A4: a -' c = a - c by XREAL_0:def 2;
b - c >= 0 by A2,Th48;
then a + (-c) = b + (-c) by A3,A4,XREAL_0:def 2;
hence thesis;
end;
theorem
a >= b implies a -' b + b = a
proof
assume a >= b;
then a - b = a -' b by Th48,XREAL_0:def 2;
hence thesis;
end;
:: from LEXBFS, 2008.08.23, A.T.
theorem
a <= b & c < a implies b -' a < b -' c
proof
assume that
A1: a <= b and
A2: c < a;
A3: b - a < b - c by A2,Th15;
b -' c = b - c by A1,A2,Th233,XXREAL_0:2;
hence thesis by A1,A3,Th48,XREAL_0:def 2;
end;
:: missing, 2010.05.18, A.T.
theorem
1 <= a implies a -' 1 < a
proof
assume 1 <= a;
then a -' 1 = a - 1 by Th48,XREAL_0:def 2;
hence a -' 1 < a by Th44;
end;