:: Real Numbers - Basic Theorems
:: by Library Committee
::
:: Received February 9, 2005
:: Copyright (c) 2005-2021 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+d
proof
a+c <= d+a by A4,Lm5;
then
A6: a+c-d<=a+d-d by Lm7;
assume a+c = b+d;
hence contradiction by A3,A6;
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 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 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****=c-b;
then -(c-a)<=-(c-b) by Lm14;
then a-c <= b-c;
hence thesis by Th9;
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 <= c;
then a <= c - -b by Lm16;
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 that
A1: a <= b and
A2: c <= d;
-d <= -c by A2,Lm14;
then a+ -d <= b+ -c by A1,Lm6;
hence thesis;
end;
theorem Th14:
a < b & c <= d implies a-d < b-c
proof
assume that
A1: a < b and
A2: c <= d;
- d <= - c by A2,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 that
A1: a <= b and
A2: c < d;
c-b < d-a by A1,A2,Th14;
then -(d-a) < -(c-b) by Lm15;
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
a-b <= c-d implies a-c <= b-d
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;
theorem
a-b <= c-d implies d-b <= c-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;
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
A1: a-c <= d-b;
assume c+d=a-b;
per cases by A1;
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 a+b<=-b+b by Lm5;
then b--a<=0;
hence thesis by Lm21;
end;
Lm22: a <= b implies 0 <= b-a
proof
assume a <= b;
then a - a <= b - a by Lm7;
hence thesis;
end;
theorem Th26:
-b<=a implies -a<=b
proof
assume
A1: -b<=a;
assume b<-a;
then b+a<-a+a by Lm10;
then a--b<0;
hence thesis by A1,Lm22;
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
A1: 0 <= a;
assume
A2: a+b****b;
then b+-a-b>0 by Lm21;
hence thesis by A1;
end;
end;
theorem
a <= 0 implies a+b <= b
proof
assume a<=0;
then b+a<=0+b by Lm6;
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 that
A1: a <= 0 and
A2: c <= b;
a+c <= 0+b by A1,A2,Lm6;
hence thesis;
end;
theorem Th36:
a <= 0 & c < b implies c+a < b
proof
assume that
A1: a <= 0 and
A2: c < b;
a+c < 0+b by A1,A2,Lm8;
hence thesis;
end;
theorem Th37:
a < 0 & c <= b implies c+a < b
proof
assume that
A1: a < 0 and
A2: c <= b;
a+c < 0+b by A1,A2,Lm8;
hence thesis;
end;
theorem Th38:
0 <= a & b <= c implies b <= a+c
proof
assume that
A1: 0 <= a and
A2: b <= c;
b+0 <= a+c by A1,A2,Lm6;
hence thesis;
end;
theorem Th39:
0 < a & b <= c implies b < a+c
proof
assume that
A1: 0 < a and
A2: b <= c;
b+0 < a+c by A1,A2,Lm8;
hence thesis;
end;
theorem Th40:
0 <= a & b < c implies b < a+c
proof
assume that
A1: 0 <= a and
A2: b < c;
b+0 < a+c by A1,A2,Lm8;
hence thesis;
end;
Lm24: c < 0 & a < b implies b*c < a*c
proof
assume
A1: c < 0;
assume 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 bc-b by Lm23;
then (-d)/2<-d by Lm27;
then c+-d/20;
then a-b+b>0+b by Lm10;
hence thesis by A1;
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 that
A1: 0 <= a and
A2: b < c;
b+0 < a+c by A1,A2,Th40;
hence thesis by Lm17;
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,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
A1: a <> b;
per cases by A1,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 bb-c by Lm23;
then (-d)/2<-d by Lm27;
then b+-d/2****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=-a;
then b+a>=-a+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 a>-b;
then a+b>-b+b by Lm10;
hence thesis;
end;
Lm28: a <= b & c <= 0 implies b*c <= a*c
proof
assume
A1: a<=b;
assume c <= 0;
then a*(-c)<=b*(-c) by A1,Lm12;
then -(a*c)<=-(b*c);
hence thesis by Lm15;
end;
begin
theorem
0 <= a*a
proof
per cases;
suppose
0 <= a;
hence thesis;
end;
suppose
not 0 <= a;
hence thesis;
end;
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 and
A3: 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 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 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*bc/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/bb 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: 00 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";
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: b0-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****0 and
A2: b<0 and
A3: 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" by A2,A3,Lm34;
then a"*c < b"*c by A1,Lm24;
then c/a****b" by A2,A3,Lm31;
then a"*c < b"*c by A1,Lm24;
then c/a****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*dc 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*d0 and
A3: a*dc 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*bc 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*bc/d;
then a*b*d0 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*b0 and
A2: d<0;
assume a*bc 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=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""****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-10 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*b1;
a*b=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)0;
then b/b=c by A1;
hence contradiction by A2,A10;
end;
end;
Lm36: 1 < a implies a" < 1
proof
assume
A1: 11;
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****0 by Lm21;
then
A6: (1-d)*a<(1-d)*b by A3,Lm13;
A7: (1-d)*a+d*a=a;
d*ab 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/a by A1,A2,Lm25;
hence thesis by A1,XCMPLX_1:60;
end;
theorem
a < 0 & b <= a implies 1 <= b/a
proof
assume that
A1: a < 0 and
A2: b<=a;
b/a>=a/a by A1,A2,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
A2: a <= 0;
per cases by A2;
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
A1: a<=0;
per cases by A1;
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 that
A1: a < 0 and
A2: ba/a by A1,A2,Lm29;
hence thesis by A1,XCMPLX_1:60;
end;
theorem
0 <= a & a < b implies a/b < 1
proof
assume that
A1: 0 <= a and
A2: a < b;
a/b**** 0;
assume
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
A1: a<0;
assume
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
A1: b>=0;
per cases by A1;
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
A1: b >= 0;
per cases by A1;
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
A1: b<=0;
per cases by A1;
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
A1: b<=0;
per cases by A1;
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
A1: b>0;
assume
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
A1: b>0;
assume
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
A1: b<0;
assume
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
A1: b<0;
assume
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
A1: b>0;
assume
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
A1: b<0;
assume
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
A1: b<0;
assume
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
A1: b>0;
assume
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
(for a st a>1 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: 01" 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;
hence thesis;
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: 00 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**~~ 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 and
A15: s < t by A1,Th5;
take s;
thus thesis by A14,A15;
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 that
A1: 0 <= a and
A2: b <= c;
b+0 <= a+c by A1,A2,Th38;
hence thesis by Lm18;
end;
theorem
0 < a & b <= c implies b-a < c
proof
assume that
A1: 0 < a and
A2: b <= c;
b+0 < a+c by A1,A2,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 Th233;
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,Th233;
end;
:: missing, 2010.05.18, A.T.
theorem
1 <= a implies a -' 1 < a
proof
assume 1 <= a;
then a -' 1 = a - 1 by Th233;
hence a -' 1 < a by Th44;
end;
~~