xreal_1.miz

begin

 reserve a,b,c,d for Real;

 reserve r,s for Real;



 Lm1: (r in REAL+ & s in REAL+ & ex x9,y9 be Element of REAL+ st r = x9 & s = y9 & x9 <=' y9) or (r in [: { 0 }, REAL+ :] & s in [: { 0 }, REAL+ :] & ex x9,y9 be 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 be Element of REAL+ st r = x9 & s = y9 & x9 <=' y9) or (r in [: { 0 }, REAL+ :] & s in [: { 0 }, REAL+ :] & ex x9,y9 be 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 be Element of REAL st a = [*x1, x2*] holds x2 = 0 & a = x1

 proof

 let x1,x2 be Element of REAL ;

 assume

 A1: a = [*x1, x2*];



 A2: a in REAL by XREAL_0:def 1;

 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 be 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 be 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 be 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 be 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 be 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 be 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 be 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 be 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 be 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 be 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 be 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 be 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 be 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 be 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 be 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 be 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 be 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 be 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 + 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 < a;

 then (b + 0 ) < (b + a) by Lm8;

 hence thesis;

 end;

 theorem :: XREAL_1:1



 Th1: ex b st a < b

 proof

 take (a + 1);

 (a + 0 ) < (a + 1) by Lm8;

 hence thesis;

 end;

 theorem :: XREAL_1:2



 Th2: ex b st b < a

 proof

 take (a - 1);

 (a + ( - 1)) < (a + ( - 0 )) by Lm8;

 hence thesis;

 end;

 theorem :: XREAL_1:3

 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 :: XREAL_1:4

 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 be 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 be 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, ARYTM_0: 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 be 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 be 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 be 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 be 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 be 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 be 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 be 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 be 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 * 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 :: XREAL_1:5



 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 :: XREAL_1:6

 a <= b iff (a + c) <= (b + c) by Lm5, Lm10;

 theorem :: XREAL_1:7

 a <= b & c <= d implies (a + c) <= (b + d) by Lm6;

 theorem :: XREAL_1:8

 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 :: XREAL_1:9



 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 :: XREAL_1:10

 a <= b iff (c - b) <= (c - a)

 proof

 hereby

 assume

 A1: a <= b;

 assume (c - a) < (c - b);

 then ( - (c - b)) < ( - (c - a)) by Lm15;

 then (b - c) < (a - c);

 hence contradiction by A1, Lm7;

 end;

 assume (c - 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 :: XREAL_1:11

 a <= (b - c) implies c <= (b - a)

 proof

 assume a <= (b - c);

 then (a + c) <= b by Lm17;

 hence thesis by Lm16;

 end;

 theorem :: XREAL_1:12

 (a - b) <= c implies (a - c) <= b

 proof

 assume c >= (a - b);

 then (c + b) >= a by Lm19;

 hence thesis by Lm18;

 end;

 theorem :: XREAL_1:13



 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 :: XREAL_1:14



 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 :: XREAL_1:15



 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 :: XREAL_1:16

 (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 :: XREAL_1:17

 (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 :: XREAL_1:18

 (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 :: XREAL_1:19

 (a + b) <= c iff a <= (c - b) by Lm16, Lm17;

 theorem :: XREAL_1:20

 a <= (b + c) iff (a - b) <= c by Lm18, Lm19;

 theorem :: XREAL_1:21

 (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);

 then d < ((b + a) - c) by Lm19;

 then d < (b + (a - c));

 hence thesis by A1, Lm17;

 end;

 theorem :: XREAL_1:22

 (a + b) <= (c - d) implies (a + d) <= (c - b)

 proof

 assume

 A1: (a + b) <= (c - d);

 per cases by A1;

 suppose (a + b) <= (c - d);

 then ((a + b) + d) <= c by Lm17;

 then ((a + d) + b) <= c;

 hence thesis by Lm16;

 end;

 suppose (b + a) <= (c - d);

 then ((a + b) + d) <= c by Lm17;

 then ((a + d) + b) <= c;

 hence thesis by Lm16;

 end;

 end;

 theorem :: XREAL_1:23

 (a - b) <= (c + d) implies (a - d) <= (c + b)

 proof

 assume

 A1: (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 :: XREAL_1:24

 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 :: XREAL_1:25



 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 :: XREAL_1:26



 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 :: XREAL_1:27

 0 <= a & 0 <= b & (a + b) = 0 implies a = 0 ;

 theorem :: XREAL_1:28

 a <= 0 & b <= 0 & (a + b) = 0 implies a = 0 ;

 begin

 theorem :: XREAL_1:29

 0 < a implies b < (b + a) by Lm9;

 theorem :: XREAL_1:30

 a < 0 implies (a + b) < b

 proof

 assume a < 0 ;

 then (b + a) < ( 0 + b) by Lm10;

 hence thesis;

 end;



 Lm23: a = 0 ;

 then ((a - b) + b) >= ( 0 + b) by Lm5;

 hence thesis by A1;

 end;

 theorem :: XREAL_1:31

 0 <= a implies b <= (a + b)

 proof

 assume

 A1: 0 <= a;

 assume

 A2: (a + b) < b;

 per cases by A2;

 suppose (a + b) < b;

 then ((a + b) - b) < 0 by Lm23;

 hence thesis by A1;

 end;

 suppose (b - a) > b;

 then ((b + ( - a)) - b) > 0 by Lm21;

 hence thesis by A1;

 end;

 end;

 theorem :: XREAL_1:32

 a <= 0 implies (a + b) <= b

 proof

 assume a <= 0 ;

 then (b + a) <= ( 0 + b) by Lm6;

 hence thesis;

 end;

 begin

 theorem :: XREAL_1:33

 0 <= a & 0 <= b implies 0 <= (a + b);

 theorem :: XREAL_1:34

 0 <= a & 0 < b implies 0 < (a + b);

 theorem :: XREAL_1:35



 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 :: XREAL_1:36



 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 :: XREAL_1:37



 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 :: XREAL_1:38



 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 :: XREAL_1:39



 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 :: XREAL_1:40



 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 < 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;

 a < b implies (a / c) < (b / c)

 proof

 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;

 hence thesis;

 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 :: XREAL_1:41

 (for a be 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 :: XREAL_1:42

 (for a be 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 :: XREAL_1:43

 0 <= a implies (b - a) <= b

 proof

 0 <= a implies (b - a) <= (b - 0 ) by Th13;

 hence thesis;

 end;

 theorem :: XREAL_1:44



 Th44: 0 < a implies (b - a) < b

 proof

 assume 0 < a;

 then (b + ( - a)) < (b + 0 ) by Lm10;

 hence thesis;

 end;

 theorem :: XREAL_1:45

 a <= 0 implies b <= (b - a)

 proof

 assume a <= 0 ;

 then (b + a) <= ( 0 + b) by Lm6;

 hence thesis by Lm16;

 end;

 theorem :: XREAL_1:46

 a < 0 implies b < (b - a)

 proof

 assume a < 0 ;

 then (b + a) < ( 0 + b) by Lm10;

 hence thesis by Lm19;

 end;

 theorem :: XREAL_1:47

 a <= b implies (a - b) <= 0

 proof

 assume

 A1: a <= b;

 assume (a - b) > 0 ;

 then ((a - b) + b) > ( 0 + b) by Lm10;

 hence thesis by A1;

 end;

 theorem :: XREAL_1:48



 Th48: a <= b implies 0 <= (b - a)

 proof

 assume a <= b;

 then (a - a) <= (b - a) by Lm7;

 hence thesis;

 end;

 theorem :: XREAL_1:49

 a < b implies (a - b) < 0 by Lm23;

 theorem :: XREAL_1:50

 a < b implies 0 < (b - a) by Lm21;

 theorem :: XREAL_1:51

 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 :: XREAL_1:52

 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 :: XREAL_1:53

 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 :: XREAL_1:54

 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 :: XREAL_1:55

 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 :: XREAL_1:56

 (for a be 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 :: XREAL_1:57

 (for a be 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 :: XREAL_1:58

 a < 0 iff 0 < ( - a);

 theorem :: XREAL_1:59

 a <= ( - b) implies (a + b) <= 0

 proof

 assume a <= ( - b);

 then (a + b) <= (( - b) + b) by Lm5;

 hence thesis;

 end;

 theorem :: XREAL_1:60

 ( - a) <= b implies 0 <= (a + b)

 proof

 assume b >= ( - a);

 then (b + a) >= (( - a) + a) by Lm5;

 hence thesis;

 end;

 theorem :: XREAL_1:61

 a < ( - b) implies (a + b) < 0

 proof

 assume a < ( - b);

 then (a + b) < (( - b) + b) by Lm10;

 hence thesis;

 end;

 theorem :: XREAL_1:62

 ( - 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 :: XREAL_1:63

 0 <= (a * a)

 proof

 per cases ;

 suppose 0 <= a;

 hence thesis;

 end;

 suppose not 0 <= a;

 hence thesis;

 end;

 end;

 theorem :: XREAL_1:64

 a <= b & 0 <= c implies (a * c) <= (b * c) by Lm12;

 theorem :: XREAL_1:65

 a <= b & c <= 0 implies (b * c) <= (a * c) by Lm28;

 theorem :: XREAL_1:66



 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 :: XREAL_1:67

 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 :: XREAL_1:68

 0 < c & a < b implies (a * c) < (b * c) by Lm13;

 theorem :: XREAL_1:69

 c < 0 & a 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 :: XREAL_1:71

 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 :: XREAL_1:72

 0 <= c & b <= a implies (b / c) <= (a / c) by Lm25;

 theorem :: XREAL_1:73

 c <= 0 & a <= b implies (b / c) <= (a / c) by Lm30;

 theorem :: XREAL_1:74

 0 < c & a < b implies (a / c) < (b / c) by Lm26;

 theorem :: XREAL_1:75

 c < 0 & a < b implies (b / c) < (a / c) by Lm29;

 theorem :: XREAL_1:76

 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 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 :: XREAL_1:77



 Th77: 0 0 and

 A2: (a * b) <= c;

 ((a * b) / b) <= (c / b) by A1, A2, Lm25;

 hence thesis by A1, XCMPLX_1: 89;

 end;

 theorem :: XREAL_1:78



 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 :: XREAL_1:79



 Th79: 0 0 and

 A2: (a * b) >= c;

 ((a * b) / b) >= (c / b) by A1, A2, Lm25;

 hence thesis by A1, XCMPLX_1: 89;

 end;

 theorem :: XREAL_1:80



 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 :: XREAL_1:81



 Th81: 0 0 and

 A2: (a * b) < c;

 ((a * b) / b) < (c / b) by A1, A2, Lm26;

 hence thesis by A1, XCMPLX_1: 89;

 end;

 theorem :: XREAL_1:82



 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 :: XREAL_1:83



 Th83: 0 0 and

 A2: (a * b) > c;

 ((a * b) / b) > (c / b) by A1, A2, Lm26;

 hence thesis by A1, XCMPLX_1: 89;

 end;

 theorem :: XREAL_1:84



 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 :: XREAL_1:85

 0 < a & a <= b implies (b " ) <= (a " ) by Lm32;

 theorem :: XREAL_1:86

 b < 0 & a <= b implies (b " ) <= (a " ) by Lm33;

 theorem :: XREAL_1:87

 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 :: XREAL_1:88

 0 < a & a 0 and

 A2: (a " ) >= (b " );

 ((a " ) " ) <= ((b " ) " ) by A1, A2, Lm32;

 hence thesis;

 end;

 theorem :: XREAL_1:90

 (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 :: XREAL_1:91

 0 < (b " ) & (b " ) < (a " ) implies a 0 and

 A2: (a " ) > (b " );

 ((a " ) " ) < ((b " ) " ) by A1, A2, Lm34;

 hence thesis;

 end;

 theorem :: XREAL_1:92

 (a " ) < 0 & (b " ) < (a " ) implies a (b " );

 ((a " ) " ) < ((b " ) " ) by A1, A2, Lm31;

 hence thesis;

 end;



 Lm35: for a be non negative non positive Real holds 0 = (a * b);

 begin

 theorem :: XREAL_1:93

 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 :: XREAL_1:94

 0 <= a & ((b - a) * (b + a)) < 0 implies ( - 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 :: XREAL_1:95

 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 :: XREAL_1:96

 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 :: XREAL_1:97

 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 :: XREAL_1:98



 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 :: XREAL_1:99

 0 < c & b < 0 & a 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 :: XREAL_1:100

 c < 0 & 0 < a & 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 :: XREAL_1:101

 c < 0 & b < 0 & 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 :: XREAL_1:102

 0 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 :: XREAL_1:103

 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 :: XREAL_1:104

 0 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 :: XREAL_1:105

 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 :: XREAL_1:106

 0 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 :: XREAL_1:107

 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 :: XREAL_1:108

 0 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 :: XREAL_1:109

 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 :: XREAL_1:110

 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 :: XREAL_1:111

 0 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 :: XREAL_1:112

 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 :: XREAL_1:113

 0 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 :: XREAL_1:114

 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 :: XREAL_1:115

 0 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 :: XREAL_1:116

 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 :: XREAL_1:117

 0 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 :: XREAL_1:118

 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 :: XREAL_1:119

 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 :: XREAL_1:120

 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 :: XREAL_1:121

 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 :: XREAL_1:122

 0 < a iff 0 < (a " );

 theorem :: XREAL_1:123

 a < 0 iff (a " ) < 0 ;

 theorem :: XREAL_1:124



 Th124: a < 0 & 0 0 ;

 (a " ) < 0 by A1;

 hence thesis by A2;

 end;

 theorem :: XREAL_1:125

 (a " ) < 0 & 0 < (b " ) implies a 0 ;

 ((a " ) " ) < ((b " ) " ) by A1, A2, Th124;

 hence thesis;

 end;

 begin

 theorem :: XREAL_1:126

 a <= 0 & 0 <= a implies 0 = (a * b) by Lm35;

 theorem :: XREAL_1:127

 0 <= a & 0 <= b implies 0 <= (a * b);

 theorem :: XREAL_1:128

 a <= 0 & b <= 0 implies 0 <= (a * b);

 theorem :: XREAL_1:129

 0 < a & 0 < b implies 0 < (a * b);

 theorem :: XREAL_1:130

 a < 0 & b < 0 implies 0 < (a * b);

 theorem :: XREAL_1:131

 0 <= a & b <= 0 implies (a * b) <= 0 ;

 theorem :: XREAL_1:132

 0 < a & b < 0 implies (a * b) < 0 ;

 theorem :: XREAL_1:133

 (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 :: XREAL_1:134

 (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 :: XREAL_1:135

 a <= 0 & b <= 0 implies 0 <= (a / b);

 theorem :: XREAL_1:136

 0 <= a & 0 <= b implies 0 <= (a / b);

 theorem :: XREAL_1:137

 0 <= a & b <= 0 implies (a / b) <= 0 ;

 theorem :: XREAL_1:138

 a <= 0 & 0 <= b implies (a / b) <= 0 ;

 theorem :: XREAL_1:139

 0 < a & 0 < b implies 0 < (a / b);

 theorem :: XREAL_1:140

 a < 0 & b < 0 implies 0 < (a / b);

 theorem :: XREAL_1:141

 a < 0 & 0 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 :: XREAL_1:144

 (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 :: XREAL_1:145

 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 :: XREAL_1:146

 (a - 1) < a

 proof

 (a + ( - 1)) < (a + 0 ) by Lm10;

 hence thesis;

 end;

 theorem :: XREAL_1:147

 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 :: XREAL_1:148

 ( - 1) < a implies 0 < (1 + a)

 proof

 assume ( - 1) < a;

 then (( - 1) + 1) < (a + 1) by Lm8;

 hence thesis;

 end;

 theorem :: XREAL_1:149

 a < 1 implies (1 - a) > 0 by Lm21;

 begin

 theorem :: XREAL_1:150

 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 :: XREAL_1:151

 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 :: XREAL_1:152

 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 :: XREAL_1:153

 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 :: XREAL_1:154

 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 :: XREAL_1:155



 Th155: 0 < a & 1 0 and

 A2: b > 1;

 (a * b) > (a * 1) by A1, A2, Lm13;

 hence thesis;

 end;

 theorem :: XREAL_1:156

 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 :: XREAL_1:157

 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 :: XREAL_1:158

 a < 0 & 1 1;

 (a * b) < (a * 1) by A1, A2, Lm24;

 hence thesis;

 end;

 theorem :: XREAL_1:159

 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 :: XREAL_1:160

 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 :: XREAL_1:161

 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 :: XREAL_1:162

 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 :: XREAL_1:163

 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 :: XREAL_1:164

 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 :: XREAL_1:165

 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 :: XREAL_1:166

 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 :: XREAL_1:167



 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)) 0 ;

 then (b / b) < (c / b) by A2, Lm26;

 then 1 < (c / b) by A7, XCMPLX_1: 60;

 then

 consider d be 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 :: XREAL_1:168

 (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 :: XREAL_1:169

 (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 :: XREAL_1:170

 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 :: XREAL_1:171

 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 :: XREAL_1:172

 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 :: XREAL_1:173

 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 :: XREAL_1:174

 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 :: XREAL_1:175

 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 :: XREAL_1:176

 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 :: XREAL_1:177

 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 :: XREAL_1:178

 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 :: XREAL_1:179

 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 :: XREAL_1:180

 0 <= d & d <= 1 & (((1 - d) * a) + (d * b)) <= a & (((1 - d) * a) + (d * b)) = 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 :: XREAL_1:181

 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 :: XREAL_1:182

 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 :: XREAL_1:183

 0 <= a & a <= b implies (a / b) <= 1 by Lm37;

 theorem :: XREAL_1:184

 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 :: XREAL_1:185

 0 <= a & b <= a implies (b / a) <= 1 by Lm38;

 theorem :: XREAL_1:186

 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 :: XREAL_1:187

 0 < a & 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 :: XREAL_1:188

 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, Lm29;

 hence thesis by A1, XCMPLX_1: 60;

 end;

 theorem :: XREAL_1:189

 0 <= a & a < b implies (a / b) < 1

 proof

 assume that

 A1: 0 <= a and

 A2: a < b;

 (a / b) < (b / b) by A1, A2, Lm26;

 hence thesis by A1, A2, XCMPLX_1: 60;

 end;

 theorem :: XREAL_1:190

 a <= 0 & b < a implies (a / b) < 1

 proof

 assume that

 A1: a <= 0 and

 A2: b < a;

 (a / b) < (b / b) by A1, A2, Lm29;

 hence thesis by A1, A2, XCMPLX_1: 60;

 end;

 theorem :: XREAL_1:191

 0 < a & b < a implies (b / a) < 1

 proof

 assume

 A1: a > 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 :: XREAL_1:192

 a < 0 & a = 1;

 then ((b / a) * a) <= (1 * a) by A1, Lm28;

 hence thesis by A1, A2, XCMPLX_1: 87;

 end;

 begin

 theorem :: XREAL_1:193

 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 :: XREAL_1:194

 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 :: XREAL_1:195

 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 :: XREAL_1:196

 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 :: XREAL_1:197

 0 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 :: XREAL_1:198

 0 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 :: XREAL_1:199

 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 :: XREAL_1:200

 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 :: XREAL_1:201

 0 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 :: XREAL_1:202

 0 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 :: XREAL_1:203

 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 :: XREAL_1:204

 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 :: XREAL_1:205

 0 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 :: XREAL_1:206

 0 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 :: XREAL_1:207

 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 :: XREAL_1:208

 b < 0 & ( - a) = ( - 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 :: XREAL_1:209



 Th209: (for a be 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 :: XREAL_1:210

 (for a be 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: 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;

 hence thesis;

 end;

 theorem :: XREAL_1:211

 1 <= a implies (a " ) <= 1

 proof

 1 <= a implies (a " ) <= (1 " ) by Lm32;

 hence thesis;

 end;

 theorem :: XREAL_1:212

 1 < a implies (a " ) < 1 by Lm36;

 theorem :: XREAL_1:213

 a <= ( - 1) implies ( - 1) <= (a " )

 proof

 a <= ( - 1) implies (( - 1) " ) <= (a " ) by Lm33;

 hence thesis;

 end;

 theorem :: XREAL_1:214

 a < ( - 1) implies ( - 1) < (a " )

 proof

 a < ( - 1) implies (( - 1) " ) < (a " ) by Lm31;

 hence thesis;

 end;

 begin

 theorem :: XREAL_1:215

 0 < a implies 0 < (a / 2);

 theorem :: XREAL_1:216

 0 < a implies (a / 2) < a by Lm27;

 theorem :: XREAL_1:217

 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 :: XREAL_1:218

 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 :: XREAL_1:219

 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 :: XREAL_1:220

 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 :: XREAL_1:221

 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 :: XREAL_1:222

 0 < a implies 0 < (a / 3);

 begin

 theorem :: XREAL_1:223

 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 :: XREAL_1:224

 0 < a implies 0 < (a / 4);

 theorem :: XREAL_1:225

 for a, b st b <> 0 holds ex c st a = (b / c)

 proof

 let a, b;

 assume

 A1: b <> 0 ;

 then

 consider c be 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

 theorem :: XREAL_1:226

 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;

 registration

 cluster -> ext-real for Element of REAL ;

 coherence ;

 end

 reserve p,q,r,s,t for ExtReal;

 theorem :: XREAL_1:227



 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 be 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 be 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 be Real such that

 A14: r < s and

 A15: s < t by A1, Th5;

 take s;

 thus thesis by A14, A15;

 end;

 end;

 theorem :: XREAL_1:228

 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 :: XREAL_1:229

 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;

 theorem :: XREAL_1:230

 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 :: XREAL_1:231

 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 :: XREAL_1:232

 (a -' a) = 0

 proof

 (a - a) = 0 ;

 hence thesis by XREAL_0:def 2;

 end;

 theorem :: XREAL_1:233



 Th233: b <= a implies (a -' b) = (a - b) by Th48, XREAL_0:def 2;

 theorem :: XREAL_1:234

 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 :: XREAL_1:235

 a >= b implies ((a -' b) + b) = a

 proof

 assume a >= b;

 then (a - b) = (a -' b) by Th233;

 hence thesis;

 end;

 theorem :: XREAL_1:236

 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;

 theorem :: XREAL_1:237

 1 <= a implies (a -' 1) < a

 proof

 assume 1 <= a;

 then (a -' 1) = (a - 1) by Th233;

 hence (a -' 1) < a by Th44;

 end;