:: XREAL_1 semantic presentation

begin

      Lm1:  for r, s being real number st ( ( 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+:] ) ) holds
r <= s
proof
let r, s be real number ; ::_thesis: ( ( ( 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 )
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+:] ) ) ; ::_thesis: r <= s
percases ( ( r in REAL+ & s in REAL+ ) or ( r in [:{0},REAL+:] & s in [:{0},REAL+:] ) or ( ( not r in REAL+ or not s in REAL+ ) & ( not r in [:{0},REAL+:] or not s in [:{0},REAL+:] ) ) ) ;
:: according to XXREAL_0:def_5
case ( r in REAL+ & s in REAL+ ) ; ::_thesis: ex b1, b2 being Element of REAL+ st
( r = b1 & s = b2 & b1 <=' b2 )
hence  ex b1, b2 being Element of REAL+ st
( r = b1 & s = b2 & b1 <=' b2 ) by A1, ARYTM_0:5, XBOOLE_0:3; ::_thesis: verum
end;
case ( r in [:{0},REAL+:] & s in [:{0},REAL+:] ) ; ::_thesis: ex b1, b2 being Element of REAL+ st
( r = [0,b1] & s = [0,b2] & b2 <=' b1 )
hence  ex b1, b2 being Element of REAL+ st
( r = [0,b1] & s = [0,b2] & b2 <=' b1 ) by A1, ARYTM_0:5, XBOOLE_0:3; ::_thesis: verum
end;
case ( ( not r in REAL+ or not s in REAL+ ) & ( not r in [:{0},REAL+:] or not s in [:{0},REAL+:] ) ) ; ::_thesis: ( ( s in REAL+ & r in [:{0},REAL+:] ) or r = -infty or s = +infty )
hence  ( ( s in REAL+ & r in [:{0},REAL+:] ) or r = -infty or s = +infty ) by A1; ::_thesis: verum
end;
end;
end;

Lm2:  for a being real number
for x1, x2 being Element of REAL st a = [*x1,x2*] holds
( x2 = 0 & a = x1 )
proof
let a be real number ; ::_thesis: for x1, x2 being Element of REAL st a = [*x1,x2*] holds
( x2 = 0 & a = x1 )
let x1, x2 be Element of REAL ; ::_thesis: ( a = [*x1,x2*] implies ( x2 = 0 & a = x1 ) )
assume A1: a = [*x1,x2*] ; ::_thesis: ( x2 = 0 & a = x1 )
A2: a in REAL by XREAL_0:def_1;
hereby  ::_thesis: a = x1
assume  x2 <> 0 ; ::_thesis: contradiction
then  a = (0,1) --> (x1,x2) by A1, ARYTM_0:def_5;
hence  contradiction by A2, ARYTM_0:8; ::_thesis: verum
end;
hence  a = x1 by A1, ARYTM_0:def_5; ::_thesis: verum
end;

Lm3:  for a9, b9 being Element of REAL
for a, b being real number st a9 = a & b9 = b holds
+ (a9,b9) = a + b
proof
let a9, b9 be Element of REAL ; ::_thesis: for a, b being real number st a9 = a & b9 = b holds
+ (a9,b9) = a + b
let a, b be real number ; ::_thesis: ( a9 = a & b9 = b implies + (a9,b9) = a + b )
assume that
A1: a9 = a and
A2: b9 = b ; ::_thesis: + (a9,b9) = a + 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  + (a9,b9) = a + b by A1, A2, A5, A8, A7, ARYTM_0:def_5; ::_thesis: verum
end;

Lm4:  {} in {{}}
by TARSKI:def_1;

Lm5:  for a, b, c being real number st a <= b holds
a + c <= b + c
proof
let a, b, c be real number ; ::_thesis: ( a <= b implies a + c <= b + c )
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 ; ::_thesis: a + c <= b + c
percases ( ( a in REAL+ & b in REAL+ & c in REAL+ ) or ( a in [:{0},REAL+:] & b in REAL+ & c in REAL+ ) or ( a in [:{0},REAL+:] & b in [:{0},REAL+:] & c in REAL+ ) or ( a in REAL+ & b in REAL+ & c in [:{0},REAL+:] ) or ( a in [:{0},REAL+:] & b in REAL+ & c in [:{0},REAL+:] ) or ( a in [:{0},REAL+:] & b in [:{0},REAL+:] & c in [:{0},REAL+:] ) ) by A3, XXREAL_0:def_5;
supposethat A4: a in REAL+ and
A5: b in REAL+ and
A6: c in REAL+ ; ::_thesis: a + c <= b + c
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  a + c <= b + c by A1, A2, A12, A9, Lm1; ::_thesis: verum
end;
supposethat A13: a in [:{0},REAL+:] and
A14: b in REAL+ and
A15: c in REAL+ ; ::_thesis: a + c <= b + c
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__::_thesis:_a_+_c_<=_b_+_c
percases ( a9 <=' c9 or not a9 <=' c9 ) ;
supposeA20: a9 <=' c9 ; ::_thesis: a + c <= b + c
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  a + c <= b + c by A1, A2, A19, A17, A22, Lm1; ::_thesis: verum
end;
suppose not a9 <=' c9 ; ::_thesis: a + c <= b + c
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  a + c <= b + c by A23, XXREAL_0:def_5; ::_thesis: verum
end;
end;
end;
hence  a + c <= b + c ; ::_thesis: verum
end;
supposethat A24: a in [:{0},REAL+:] and
A25: b in [:{0},REAL+:] and
A26: c in REAL+ ; ::_thesis: a + c <= b + c
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__::_thesis:_a_+_c_<=_b_+_c
percases ( a9 <=' c9 or not a9 <=' c9 ) ;
supposeA38: a9 <=' c9 ; ::_thesis: a + c <= b + c
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  a + c <= b + c by A1, A2, A34, A35, A28, A29, A40, A39, Lm1; ::_thesis: verum
end;
suppose not a9 <=' c9 ; ::_thesis: a + c <= b + c
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__::_thesis:_a_+_c_<=_b_+_c
percases ( b9 <=' c9 or not b9 <=' c9 ) ;
suppose b9 <=' c9 ; ::_thesis: a + c <= b + c
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  a + c <= b + c by A1, A2, A43, XXREAL_0:def_5; ::_thesis: verum
end;
supposeA44: not b9 <=' c9 ; ::_thesis: a + c <= b + c
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  a + c <= b + c by A1, A2, A41, A42, A46, A45, Lm1; ::_thesis: verum
end;
end;
end;
hence  a + c <= b + c ; ::_thesis: verum
end;
end;
end;
hence  a + c <= b + c ; ::_thesis: verum
end;
supposethat A47: a in REAL+ and
A48: b in REAL+ and
A49: c in [:{0},REAL+:] ; ::_thesis: a + c <= b + c
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__::_thesis:_a_+_c_<=_b_+_c
percases ( c9 <=' a9 or not c9 <=' a9 ) ;
supposeA58: c9 <=' a9 ; ::_thesis: a + c <= b + c
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  a + c <= b + c by A1, A2, A55, A52, A56, A60, A59, Lm1; ::_thesis: verum
end;
suppose not c9 <=' a9 ; ::_thesis: a + c <= b + c
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__::_thesis:_a_+_c_<=_b_+_c
percases ( c9 <=' b9 or not c9 <=' b9 ) ;
suppose c9 <=' b9 ; ::_thesis: a + c <= b + c
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  a + c <= b + c by A1, A2, A63, XXREAL_0:def_5; ::_thesis: verum
end;
supposeA64: not c9 <=' b9 ; ::_thesis: a + c <= b + c
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  a + c <= b + c by A1, A2, A61, A62, A66, A65, Lm1; ::_thesis: verum
end;
end;
end;
hence  a + c <= b + c ; ::_thesis: verum
end;
end;
end;
hence  a + c <= b + c ; ::_thesis: verum
end;
supposethat A67: a in [:{0},REAL+:] and
A68: b in REAL+ and
A69: c in [:{0},REAL+:] ; ::_thesis: a + c <= b + c
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__::_thesis:_a_+_c_<=_b_+_c
percases ( c9 <=' b9 or not c9 <=' b9 ) ;
suppose c9 <=' b9 ; ::_thesis: a + c <= b + c
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  a + c <= b + c by A1, A2, A77, XXREAL_0:def_5; ::_thesis: verum
end;
supposeA78: not c9 <=' b9 ; ::_thesis: a + c <= b + c
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  a + c <= b + c by A1, A2, A72, A73, A81, A80, Lm1; ::_thesis: verum
end;
end;
end;
hence  a + c <= b + c ; ::_thesis: verum
end;
supposethat A82: a in [:{0},REAL+:] and
A83: b in [:{0},REAL+:] and
A84: c in [:{0},REAL+:] ; ::_thesis: a + c <= b + c
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  a + c <= b + c by A1, A2, A89, A93, A95, A90, A94, Lm1; ::_thesis: verum
end;
end;
end;

Lm6:  for a, b, c, d being real number st a <= b & c <= d holds
a + c <= b + d
proof
let a, b, c, d be real number ; ::_thesis: ( a <= b & c <= d implies a + c <= b + d )
assume  a <= b ; ::_thesis: ( not c <= d or a + c <= b + d )
then A1: a + c <= b + c by Lm5;
assume  c <= d ; ::_thesis: a + c <= b + d
then  b + c <= b + d by Lm5;
hence  a + c <= b + d by A1, XXREAL_0:2; ::_thesis: verum
end;

Lm7:  for a, b, c being real number st a <= b holds
a - c <= b - c
proof
let a, b, c be real number ; ::_thesis: ( a <= b implies a - c <= b - c )
 ( a <= b implies a + (- c) <= b + (- c) ) by Lm5;
hence  ( a <= b implies a - c <= b - c ) ; ::_thesis: verum
end;

Lm8:  for a, b, c, d being real number st a < b & c <= d holds
a + c < b + d
proof
let a, b, c, d be real number ; ::_thesis: ( a < b & c <= d implies a + c < b + d )
assume that
A1: a < b and
A2: c <= d ; ::_thesis: a + c < b + d
 for a, b, c, d being real number st a < b & c <= d holds
a + c < b + d
proof
let a, b, c, d be real number ; ::_thesis: ( a < b & c <= d implies a + c < b + d )
assume A3: a < b ; ::_thesis: ( not c <= d or a + c < b + d )
assume A4: c <= d ; ::_thesis: a + c < b + d
A5: a + c <> 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 ; ::_thesis: contradiction
hence  contradiction by A3, A6; ::_thesis: verum
end;
 a + c <= b + d by A3, A4, Lm6;
hence  a + c < b + d by A5, XXREAL_0:1; ::_thesis: verum
end;
hence  a + c < b + d by A1, A2; ::_thesis: verum
end;

Lm9:  for a, b being real number st 0 < a holds
b < b + a
proof
let a, b be real number ; ::_thesis: ( 0 < a implies b < b + a )
assume  0 < a ; ::_thesis: b < b + a
then  b + 0 < b + a by Lm8;
hence  b < b + a ; ::_thesis: verum
end;

theorem Th1: :: XREAL_1:1
for a being real number ex b being real number st a < b
proof
let a be real number ; ::_thesis: ex b being real number st a < b
take  a + 1 ; ::_thesis: a < a + 1
 a + 0 < a + 1 by Lm8;
hence  a < a + 1 ; ::_thesis: verum
end;

theorem Th2: :: XREAL_1:2
for a being real number ex b being real number st b < a
proof
let a be real number ; ::_thesis: ex b being real number st b < a
take  a - 1 ; ::_thesis: a - 1 < a
 a + (- 1) < a + (- 0) by Lm8;
hence  a - 1 < a ; ::_thesis: verum
end;

theorem :: XREAL_1:3
for a, b being real number ex c being real number st
( a < c & b < c )
proof
let a, b be real number ; ::_thesis: ex c being real number st
( a < c & b < c )
percases ( a <= b or b <= a ) ;
supposeA1: a <= b ; ::_thesis: ex c being real number st
( a < c & b < c )
take z = b + 1; ::_thesis: ( a < z & b < z )
 b < z by Lm9;
hence  ( a < z & b < z ) by A1, XXREAL_0:2; ::_thesis: verum
end;
supposeA2: b <= a ; ::_thesis: ex c being real number st
( a < c & b < c )
take z = a + 1; ::_thesis: ( a < z & b < z )
 a < z by Lm9;
hence  ( a < z & b < z ) by A2, XXREAL_0:2; ::_thesis: verum
end;
end;
end;

Lm10:  for a, c, b being real number st a + c <= b + c holds
a <= b
proof
let a, c, b be real number ; ::_thesis: ( a + c <= b + c implies a <= b )
assume  a + c <= b + c ; ::_thesis: a <= b
then  (a + c) + (- c) <= (b + c) + (- c) by Lm5;
hence  a <= b ; ::_thesis: verum
end;

theorem :: XREAL_1:4
for a, b being real number ex c being real number st
( c < a & c < b )
proof
let a, b be real number ; ::_thesis: ex c being real number st
( c < a & c < b )
percases ( a <= b or b <= a ) ;
supposeA1: a <= b ; ::_thesis: ex c being real number st
( c < a & c < b )
take z = a + (- 1); ::_thesis: ( z < a & z < b )
 z < a + 0 by Lm10;
hence  ( z < a & z < b ) by A1, XXREAL_0:2; ::_thesis: verum
end;
supposeA2: b <= a ; ::_thesis: ex c being real number st
( c < a & c < b )
take z = b + (- 1); ::_thesis: ( z < a & z < b )
 z < b + 0 by Lm10;
hence  ( z < a & z < b ) by A2, XXREAL_0:2; ::_thesis: verum
end;
end;
end;

Lm11:  for a9, b9 being Element of REAL
for a, b being real number st a9 = a & b9 = b holds
* (a9,b9) = a * b
proof
let a9, b9 be Element of REAL ; ::_thesis: for a, b being real number st a9 = a & b9 = b holds
* (a9,b9) = a * b
let a, b be real number ; ::_thesis: ( a9 = a & b9 = b implies * (a9,b9) = a * b )
assume that
A1: a9 = a and
A2: b9 = b ; ::_thesis: * (a9,b9) = a * b
consider x1, x2, y1, y2 being Element of REAL  such that
A3: a = [*x1,x2*] and
A4: b = [*y1,y2*] and
A5: a * b = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] by XCMPLX_0:def_5;
A6: b = y1 by A4, Lm2;
 x2 = 0 by A3, Lm2;
then A7: * (x2,y1) = 0 by ARYTM_0:12;
A8: y2 = 0 by A4, Lm2;
then  * (x1,y2) = 0 by ARYTM_0:12;
then A9: + ((* (x1,y2)),(* (x2,y1))) = 0 by A7, ARYTM_0:11;
 a = x1 by A3, Lm2;
hence  * (a9,b9) = + ((* (x1,y1)),(* ((opp x2),y2))) by A1, A2, A6, A8, ARYTM_0:11, ARYTM_0:12
.= + ((* (x1,y1)),(opp (* (x2,y2)))) by ARYTM_0:15
.= a * b by A5, A9, ARYTM_0:def_5 ;
::_thesis: verum
end;

reconsider o = 0 as Element of REAL+ by ARYTM_2:20;

Lm12:  for a, b, c being real number st a <= b & 0 <= c holds
a * c <= b * c
proof
let a, b, c be real number ; ::_thesis: ( a <= b & 0 <= c implies a * c <= b * c )
assume that
A1: a <= b and
A2: 0 <= c ; ::_thesis: a * c <= b * c
 not o 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 a * c <= b * c ; ::_thesis: contradiction
then A7: c <> 0 ;
percases ( ( a in REAL+ & b in REAL+ ) or ( a in [:{0},REAL+:] & b in REAL+ ) or ( a in [:{0},REAL+:] & b in [:{0},REAL+:] ) ) by A1, XXREAL_0:def_5;
supposethat A8: a in REAL+ and
A9: b in REAL+ ; ::_thesis: contradiction
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; ::_thesis: verum
end;
supposethat A16: a in [:{0},REAL+:] and
A17: b in REAL+ ; ::_thesis: contradiction
 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; ::_thesis: verum
end;
supposethat A19: a in [:{0},REAL+:] and
A20: b in [:{0},REAL+:] ; ::_thesis: contradiction
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; ::_thesis: verum
end;
end;
end;

Lm13:  for c, a, b being real number st 0 < c & a < b holds
a * c < b * c
proof
let c, a, b be real number ; ::_thesis: ( 0 < c & a < b implies a * c < b * c )
assume A1: 0 < c ; ::_thesis: ( not a < b or a * c < b * c )
assume A2: a < b ; ::_thesis: a * c < b * c
A3: a * c <> b * c
proof
assume  a * c = b * c ; ::_thesis: contradiction
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; ::_thesis: verum
end;
 a * c <= b * c by A1, A2, Lm12;
hence  a * c < b * c by A3, XXREAL_0:1; ::_thesis: verum
end;

theorem Th5: :: XREAL_1:5
for a, b being real number st a < b holds
ex c being real number st
( a < c & c < b )
proof
let a, b be real number ; ::_thesis: ( a < b implies ex c being real number st
( a < c & c < b ) )
assume A1: a < b ; ::_thesis: ex c being real number st
( a < c & c < b )
take z = (a + b) / 2; ::_thesis: ( a < z & z < b )
 (1 * a) + a < a + b by A1, Lm10;
then  (2 ") * (2 * a) < (2 ") * (a + b) by Lm13;
hence  a < z ; ::_thesis: z < b
 a + b < (1 * b) + b by A1, Lm10;
then  (2 ") * (a + b) < (2 ") * (2 * b) by Lm13;
hence  z < b ; ::_thesis: verum
end;

begin

theorem :: XREAL_1:6
for a, b, c being real number holds
( a <= b iff a + c <= b + c ) by Lm5, Lm10;

theorem :: XREAL_1:7
for a, b, c, d being real number st a <= b & c <= d holds
a + c <= b + d by Lm6;

theorem :: XREAL_1:8
for a, b, c, d being real number st a < b & c <= d holds
a + c < b + d by Lm8;

Lm14:  for a, b being real number st a <= b holds
- b <= - a
proof
let a, b be real number ; ::_thesis: ( a <= b implies - b <= - a )
assume  a <= b ; ::_thesis: - b <= - a
then  a - b <= b - b by Lm7;
then  (a - b) - a <= 0 - a by Lm7;
hence  - b <= - a ; ::_thesis: verum
end;

Lm15:  for b, a being real number st - b <= - a holds
a <= b
proof
let b, a be real number ; ::_thesis: ( - b <= - a implies a <= b )
assume  - b <= - a ; ::_thesis: a <= b
then  - (- a) <= - (- b) by Lm14;
hence  a <= b ; ::_thesis: verum
end;

begin

theorem Th9: :: XREAL_1:9
for a, b, c being real number holds
( a <= b iff a - c <= b - c )
proof
let a, b, c be real number ; ::_thesis: ( a <= b iff a - c <= b - c )
thus  ( a <= b implies a - c <= b - c ) by Lm7; ::_thesis: ( a - c <= b - c implies a <= b )
assume  a - c <= b - c ; ::_thesis: a <= b
then  (a + (- c)) + c <= (b + (- c)) + c by Lm5;
hence  a <= b ; ::_thesis: verum
end;

theorem :: XREAL_1:10
for a, b, c being real number holds
( a <= b iff c - b <= c - a )
proof
let a, b, c be real number ; ::_thesis: ( a <= b iff c - b <= c - a )
hereby  ::_thesis: ( c - b <= c - a implies a <= b )
assume A1: a <= b ; ::_thesis: not c - a < c - b
assume  c - a < c - b ; ::_thesis: contradiction
then  - (c - b) < - (c - a) by Lm15;
then  b - c < a - c ;
hence  contradiction by A1, Lm7; ::_thesis: verum
end;
assume  c - a >= c - b ; ::_thesis: a <= b
then  - (c - a) <= - (c - b) by Lm14;
then  a - c <= b - c ;
hence  a <= b by Th9; ::_thesis: verum
end;

Lm16:  for a, b, c being real number st a + b <= c holds
a <= c - b
proof
let a, b, c be real number ; ::_thesis: ( a + b <= c implies a <= c - b )
assume  a + b <= c ; ::_thesis: a <= c - b
then  (a + b) - b <= c - b by Lm7;
hence  a <= c - b ; ::_thesis: verum
end;

Lm17:  for a, b, c being real number st a <= b - c holds
a + c <= b
proof
let a, b, c be real number ; ::_thesis: ( a <= b - c implies a + c <= b )
assume  a <= b - c ; ::_thesis: a + c <= b
then  a + c <= (b - c) + c by Lm5;
hence  a + c <= b ; ::_thesis: verum
end;

Lm18:  for a, b, c being real number st a <= b + c holds
a - b <= c
proof
let a, b, c be real number ; ::_thesis: ( a <= b + c implies a - b <= c )
assume  a <= b + c ; ::_thesis: a - b <= c
then  a - b <= (c + b) - b by Lm7;
hence  a - b <= c ; ::_thesis: verum
end;

Lm19:  for a, b, c being real number st a - b <= c holds
a <= b + c
proof
let a, b, c be real number ; ::_thesis: ( a - b <= c implies a <= b + c )
assume  a - b <= c ; ::_thesis: a <= b + c
then  a + (- b) <= c ;
then  a <= c - (- b) by Lm16;
hence  a <= b + c ; ::_thesis: verum
end;

theorem :: XREAL_1:11
for a, b, c being real number st a <= b - c holds
c <= b - a
proof
let a, b, c be real number ; ::_thesis: ( a <= b - c implies c <= b - a )
assume  a <= b - c ; ::_thesis: c <= b - a
then  a + c <= b by Lm17;
hence  c <= b - a by Lm16; ::_thesis: verum
end;

theorem :: XREAL_1:12
for a, b, c being real number st a - b <= c holds
a - c <= b
proof
let a, b, c be real number ; ::_thesis: ( a - b <= c implies a - c <= b )
assume  c >= a - b ; ::_thesis: a - c <= b
then  c + b >= a by Lm19;
hence  a - c <= b by Lm18; ::_thesis: verum
end;

theorem Th13: :: XREAL_1:13
for a, b, c, d being real number st a <= b & c <= d holds
a - d <= b - c
proof
let a, b, c, d be real number ; ::_thesis: ( a <= b & c <= d implies a - d <= b - c )
assume that
A1: a <= b and
A2: c <= d ; ::_thesis: a - d <= b - c
 - d <= - c by A2, Lm14;
then  a + (- d) <= b + (- c) by A1, Lm6;
hence  a - d <= b - c ; ::_thesis: verum
end;

theorem Th14: :: XREAL_1:14
for a, b, c, d being real number st a < b & c <= d holds
a - d < b - c
proof
let a, b, c, d be real number ; ::_thesis: ( a < b & c <= d implies a - d < b - c )
assume that
A1: a < b and
A2: c <= d ; ::_thesis: a - d < b - c
 - d <= - c by A2, Lm14;
then  a + (- d) < b + (- c) by A1, Lm8;
hence  a - d < b - c ; ::_thesis: verum
end;

theorem Th15: :: XREAL_1:15
for a, b, c, d being real number st a <= b & c < d holds
a - d < b - c
proof
let a, b, c, d be real number ; ::_thesis: ( a <= b & c < d implies a - d < b - c )
assume that
A1: a <= b and
A2: c < d ; ::_thesis: a - d < b - c
 c - b < d - a by A1, A2, Th14;
then  - (d - a) < - (c - b) by Lm15;
hence  a - d < b - c ; ::_thesis: verum
end;

Lm20:  for a, b, c, d being real number st a + b <= c + d holds
a - c <= d - b
proof
let a, b, c, d be real number ; ::_thesis: ( a + b <= c + d implies a - c <= d - b )
assume  a + b <= c + d ; ::_thesis: a - c <= d - b
then  a <= (c + d) - b by Lm16;
then  a <= c + (d - b) ;
hence  a - c <= d - b by Lm18; ::_thesis: verum
end;

theorem :: XREAL_1:16
for a, b, c, d being real number st a - b <= c - d holds
a - c <= b - d
proof
let a, b, c, d be real number ; ::_thesis: ( a - b <= c - d implies a - c <= b - d )
assume  a - b <= c - d ; ::_thesis: a - c <= b - d
then  (a - b) + d <= c by Lm17;
then  (a + d) - b <= c ;
then  a + d <= c + b by Lm19;
hence  a - c <= b - d by Lm20; ::_thesis: verum
end;

theorem :: XREAL_1:17
for a, b, c, d being real number st a - b <= c - d holds
d - b <= c - a
proof
let a, b, c, d be real number ; ::_thesis: ( a - b <= c - d implies d - b <= c - a )
assume  a - b <= c - d ; ::_thesis: d - b <= c - a
then  (a - b) + d <= c by Lm17;
then  (a + d) - b <= c ;
then  a + d <= c + b by Lm19;
hence  d - b <= c - a by Lm20; ::_thesis: verum
end;

theorem :: XREAL_1:18
for a, b, c, d being real number st a - b <= c - d holds
d - c <= b - a
proof
let a, b, c, d be real number ; ::_thesis: ( a - b <= c - d implies d - c <= b - a )
assume  a - b <= c - d ; ::_thesis: d - c <= b - a
then  (a - b) + d <= c by Lm17;
then  (a + d) - b <= c ;
then  a + d <= c + b by Lm19;
hence  d - c <= b - a by Lm20; ::_thesis: verum
end;

begin

theorem :: XREAL_1:19
for a, b, c being real number holds
( a + b <= c iff a <= c - b ) by Lm16, Lm17;

theorem :: XREAL_1:20
for a, b, c being real number holds
( a <= b + c iff a - b <= c ) by Lm18, Lm19;

theorem :: XREAL_1:21
for a, b, c, d being real number holds
( a + b <= c + d iff a - c <= d - b )
proof
let a, b, c, d be real number ; ::_thesis: ( a + b <= c + d iff a - c <= d - b )
thus  ( a + b <= c + d implies a - c <= d - b ) by Lm20; ::_thesis: ( a - c <= d - b implies a + b <= c + d )
assume A1: a - c <= d - b ; ::_thesis: a + b <= c + d
assume  c + d < a + b ; ::_thesis: contradiction
then  d < (b + a) - c by Lm19;
then  d < b + (a - c) ;
hence  contradiction by A1, Lm17; ::_thesis: verum
end;

theorem :: XREAL_1:22
for a, b, c, d being real number st a + b <= c - d holds
a + d <= c - b
proof
let a, b, c, d be real number ; ::_thesis: ( a + b <= c - d implies a + d <= c - b )
assume A1: a + b <= c - d ; ::_thesis: a + d <= c - b
percases ( a + b <= c - d or b + a <= c - d ) by A1;
suppose a + b <= c - d ; ::_thesis: a + d <= c - b
then  (a + b) + d <= c by Lm17;
then  (a + d) + b <= c ;
hence  a + d <= c - b by Lm16; ::_thesis: verum
end;
suppose b + a <= c - d ; ::_thesis: a + d <= c - b
then  (a + b) + d <= c by Lm17;
then  (a + d) + b <= c ;
hence  a + d <= c - b by Lm16; ::_thesis: verum
end;
end;
end;

theorem :: XREAL_1:23
for a, b, c, d being real number st a - b <= c + d holds
a - d <= c + b
proof
let a, b, c, d be real number ; ::_thesis: ( a - b <= c + d implies a - d <= c + b )
assume A1: c + d >= a - b ; ::_thesis: a - d <= c + b
percases ( c + d >= a - b or d + c >= a - b ) by A1;
suppose c + d >= a - b ; ::_thesis: a - d <= c + b
then  (c + d) + b >= a by Lm19;
then  (c + b) + d >= a ;
hence  a - d <= c + b by Lm18; ::_thesis: verum
end;
suppose d + c >= a - b ; ::_thesis: a - d <= c + b
then  (c + d) + b >= a by Lm19;
then  (c + b) + d >= a ;
hence  a - d <= c + b by Lm18; ::_thesis: verum
end;
end;
end;

begin

theorem :: XREAL_1:24
for a, b being real number holds
( a <= b iff - b <= - a ) by Lm14, Lm15;

Lm21:  for a, b being real number st a < b holds
0 < b - a
proof
let a, b be real number ; ::_thesis: ( a < b implies 0 < b - a )
assume  a < b ; ::_thesis: 0 < b - a
then  a + 0 < b ;
hence  0 < b - a by Lm19; ::_thesis: verum
end;

theorem Th25: :: XREAL_1:25
for a, b being real number st a <= - b holds
b <= - a
proof
let a, b be real number ; ::_thesis: ( a <= - b implies b <= - a )
assume  a <= - b ; ::_thesis: b <= - a
then  a + b <= (- b) + b by Lm5;
then  b - (- a) <= 0 ;
hence  b <= - a by Lm21; ::_thesis: verum
end;

Lm22:  for a, b being real number st a <= b holds
0 <= b - a
proof
let a, b be real number ; ::_thesis: ( a <= b implies 0 <= b - a )
assume  a <= b ; ::_thesis: 0 <= b - a
then  a - a <= b - a by Lm7;
hence  0 <= b - a ; ::_thesis: verum
end;

theorem Th26: :: XREAL_1:26
for b, a being real number st - b <= a holds
- a <= b
proof
let b, a be real number ; ::_thesis: ( - b <= a implies - a <= b )
assume A1: - b <= a ; ::_thesis: - a <= b
assume  b < - a ; ::_thesis: contradiction
then  b + a < (- a) + a by Lm10;
then  a - (- b) < 0 ;
hence  contradiction by A1, Lm22; ::_thesis: verum
end;

begin

theorem :: XREAL_1:27
for a, b being real number st 0 <= a & 0 <= b & a + b = 0 holds
a = 0 ;

theorem :: XREAL_1:28
for a, b being real number st a <= 0 & b <= 0 & a + b = 0 holds
a = 0 ;

begin

theorem :: XREAL_1:29
for a, b being real number st 0 < a holds
b < b + a by Lm9;

theorem :: XREAL_1:30
for a, b being real number st a < 0 holds
a + b < b
proof
let a, b be real number ; ::_thesis: ( a < 0 implies a + b < b )
assume  a < 0 ; ::_thesis: a + b < b
then  b + a < 0 + b by Lm10;
hence  a + b < b ; ::_thesis: verum
end;

Lm23:  for a, b being real number st a < b holds
a - b < 0
proof
let a, b be real number ; ::_thesis: ( a < b implies a - b < 0 )
assume A1: a < b ; ::_thesis: a - b < 0
assume  a - b >= 0 ; ::_thesis: contradiction
then  (a - b) + b >= 0 + b by Lm5;
hence  contradiction by A1; ::_thesis: verum
end;

theorem :: XREAL_1:31
for a, b being real number st 0 <= a holds
b <= a + b
proof
let a, b be real number ; ::_thesis: ( 0 <= a implies b <= a + b )
assume A1: 0 <= a ; ::_thesis: b <= a + b
assume A2: a + b < b ; ::_thesis: contradiction
percases ( a + b < b or b - a > b ) by A2;
suppose a + b < b ; ::_thesis: contradiction
then  (a + b) - b < 0 by Lm23;
hence  contradiction by A1; ::_thesis: verum
end;
suppose b - a > b ; ::_thesis: contradiction
then  (b + (- a)) - b > 0 by Lm21;
hence  contradiction by A1; ::_thesis: verum
end;
end;
end;

theorem :: XREAL_1:32
for a, b being real number st a <= 0 holds
a + b <= b
proof
let a, b be real number ; ::_thesis: ( a <= 0 implies a + b <= b )
assume  a <= 0 ; ::_thesis: a + b <= b
then  b + a <= 0 + b by Lm6;
hence  a + b <= b ; ::_thesis: verum
end;

begin

theorem :: XREAL_1:33
for a, b being real number st 0 <= a & 0 <= b holds
0 <= a + b ;

theorem :: XREAL_1:34
for a, b being real number st 0 <= a & 0 < b holds
0 < a + b ;

theorem Th35: :: XREAL_1:35
for a, c, b being real number st a <= 0 & c <= b holds
c + a <= b
proof
let a, c, b be real number ; ::_thesis: ( a <= 0 & c <= b implies c + a <= b )
assume that
A1: a <= 0 and
A2: c <= b ; ::_thesis: c + a <= b
 a + c <= 0 + b by A1, A2, Lm6;
hence  c + a <= b ; ::_thesis: verum
end;

theorem Th36: :: XREAL_1:36
for a, c, b being real number st a <= 0 & c < b holds
c + a < b
proof
let a, c, b be real number ; ::_thesis: ( a <= 0 & c < b implies c + a < b )
assume that
A1: a <= 0 and
A2: c < b ; ::_thesis: c + a < b
 a + c < 0 + b by A1, A2, Lm8;
hence  c + a < b ; ::_thesis: verum
end;

theorem Th37: :: XREAL_1:37
for a, c, b being real number st a < 0 & c <= b holds
c + a < b
proof
let a, c, b be real number ; ::_thesis: ( a < 0 & c <= b implies c + a < b )
assume that
A1: a < 0 and
A2: c <= b ; ::_thesis: c + a < b
 a + c < 0 + b by A1, A2, Lm8;
hence  c + a < b ; ::_thesis: verum
end;

theorem Th38: :: XREAL_1:38
for a, b, c being real number st 0 <= a & b <= c holds
b <= a + c
proof
let a, b, c be real number ; ::_thesis: ( 0 <= a & b <= c implies b <= a + c )
assume that
A1: 0 <= a and
A2: b <= c ; ::_thesis: b <= a + c
 b + 0 <= a + c by A1, A2, Lm6;
hence  b <= a + c ; ::_thesis: verum
end;

theorem Th39: :: XREAL_1:39
for a, b, c being real number st 0 < a & b <= c holds
b < a + c
proof
let a, b, c be real number ; ::_thesis: ( 0 < a & b <= c implies b < a + c )
assume that
A1: 0 < a and
A2: b <= c ; ::_thesis: b < a + c
 b + 0 < a + c by A1, A2, Lm8;
hence  b < a + c ; ::_thesis: verum
end;

theorem Th40: :: XREAL_1:40
for a, b, c being real number st 0 <= a & b < c holds
b < a + c
proof
let a, b, c be real number ; ::_thesis: ( 0 <= a & b < c implies b < a + c )
assume that
A1: 0 <= a and
A2: b < c ; ::_thesis: b < a + c
 b + 0 < a + c by A1, A2, Lm8;
hence  b < a + c ; ::_thesis: verum
end;

Lm24:  for c, a, b being real number st c < 0 & a < b holds
b * c < a * c
proof
let c, a, b be real number ; ::_thesis: ( c < 0 & a < b implies b * c < a * c )
assume A1: c < 0 ; ::_thesis: ( not a < b or b * c < a * c )
assume  a < b ; ::_thesis: b * c < a * c
then  a * (- c) < b * (- c) by A1, Lm13;
then  - (a * c) < - (b * c) ;
hence  b * c < a * c by Lm14; ::_thesis: verum
end;

Lm25:  for c, b, a being real number st 0 <= c & b <= a holds
b / c <= a / c
proof
let c, b, a be real number ; ::_thesis: ( 0 <= c & b <= a implies b / c <= a / c )
assume that
A1: 0 <= c and
A2: b <= a ; ::_thesis: b / c <= a / c
percases ( c = 0 or 0 < c ) by A1;
suppose c = 0 ; ::_thesis: b / c <= a / c
then A3: c " = 0 ;
then  b * (c ") = 0 ;
then A4: b / c = 0 by XCMPLX_0:def_9;
 a * (c ") = 0 by A3;
hence  b / c <= a / c by A4, XCMPLX_0:def_9; ::_thesis: verum
end;
supposeA5: 0 < c ; ::_thesis: b / c <= a / c
assume  a / c < b / c ; ::_thesis: contradiction
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; ::_thesis: verum
end;
end;
end;

Lm26:  for c, a, b being real number st 0 < c & a < b holds
a / c < b / c
proof
let c, a, b be real number ; ::_thesis: ( 0 < c & a < b implies a / c < b / c )
assume A1: 0 < c ; ::_thesis: ( not a < b or a / c < b / c )
 ( a < b implies a / c < b / c )
proof
assume  a < b ; ::_thesis: a / c < b / c
then  a * (c ") < b * (c ") by A1, Lm13;
then  a / c < b * (c ") by XCMPLX_0:def_9;
hence  a / c < b / c by XCMPLX_0:def_9; ::_thesis: verum
end;
hence  ( not a < b or a / c < b / c ) ; ::_thesis: verum
end;

Lm27:  for a being real number st 0 < a holds
a / 2 < a
proof
let a be real number ; ::_thesis: ( 0 < a implies a / 2 < a )
assume  0 < a ; ::_thesis: a / 2 < a
then  0 + (a / 2) < (a / 2) + (a / 2) by Lm10;
hence  a / 2 < a ; ::_thesis: verum
end;

begin

theorem :: XREAL_1:41
for c, b being real number st ( for a being real number st a > 0 holds
c <= b + a ) holds
c <= b
proof
let c, b be real number ; ::_thesis: ( ( for a being real number st a > 0 holds
c <= b + a ) implies c <= b )
assume A1: for a being real number st a > 0 holds
b + a >= c ; ::_thesis: c <= b
set d = c - b;
assume  b < c ; ::_thesis: contradiction
then A2: 0 < c - b by Lm21;
then  b + ((c - b) / 2) < b + (c - b) by Lm10, Lm27;
hence  contradiction by A1, A2; ::_thesis: verum
end;

theorem :: XREAL_1:42
for b, c being real number st ( for a being real number st a < 0 holds
b + a <= c ) holds
b <= c
proof
let b, c be real number ; ::_thesis: ( ( for a being real number st a < 0 holds
b + a <= c ) implies b <= c )
assume A1: for a being real number st a < 0 holds
b + a <= c ; ::_thesis: b <= c
set d = c - b;
assume  c < b ; ::_thesis: contradiction
then A2: 0 > c - b by Lm23;
then  (- (c - b)) / 2 < - (c - b) by Lm27;
then  c + (- ((c - b) / 2)) < c + (- (c - b)) by Lm10;
then  c - ((c - b) / 2) < c - (c - b) ;
then  c < b + ((c - b) / 2) by Lm16;
hence  contradiction by A1, A2; ::_thesis: verum
end;

begin

theorem :: XREAL_1:43
for a, b being real number st 0 <= a holds
b - a <= b
proof
let a, b be real number ; ::_thesis: ( 0 <= a implies b - a <= b )
 ( 0 <= a implies b - a <= b - 0 ) by Th13;
hence  ( 0 <= a implies b - a <= b ) ; ::_thesis: verum
end;

theorem Th44: :: XREAL_1:44
for a, b being real number st 0 < a holds
b - a < b
proof
let a, b be real number ; ::_thesis: ( 0 < a implies b - a < b )
assume  0 < a ; ::_thesis: b - a < b
then  b + (- a) < b + 0 by Lm10;
hence  b - a < b ; ::_thesis: verum
end;

theorem :: XREAL_1:45
for a, b being real number st a <= 0 holds
b <= b - a
proof
let a, b be real number ; ::_thesis: ( a <= 0 implies b <= b - a )
assume  a <= 0 ; ::_thesis: b <= b - a
then  b + a <= 0 + b by Lm6;
hence  b <= b - a by Lm16; ::_thesis: verum
end;

theorem :: XREAL_1:46
for a, b being real number st a < 0 holds
b < b - a
proof
let a, b be real number ; ::_thesis: ( a < 0 implies b < b - a )
assume  a < 0 ; ::_thesis: b < b - a
then  b + a < 0 + b by Lm10;
hence  b < b - a by Lm19; ::_thesis: verum
end;

theorem :: XREAL_1:47
for a, b being real number st a <= b holds
a - b <= 0
proof
let a, b be real number ; ::_thesis: ( a <= b implies a - b <= 0 )
assume A1: a <= b ; ::_thesis: a - b <= 0
assume  a - b > 0 ; ::_thesis: contradiction
then  (a - b) + b > 0 + b by Lm10;
hence  contradiction by A1; ::_thesis: verum
end;

theorem Th48: :: XREAL_1:48
for a, b being real number st a <= b holds
0 <= b - a
proof
let a, b be real number ; ::_thesis: ( a <= b implies 0 <= b - a )
assume  a <= b ; ::_thesis: 0 <= b - a
then  a - a <= b - a by Lm7;
hence  0 <= b - a ; ::_thesis: verum
end;

theorem :: XREAL_1:49
for a, b being real number st a < b holds
a - b < 0 by Lm23;

theorem :: XREAL_1:50
for a, b being real number st a < b holds
0 < b - a by Lm21;

theorem :: XREAL_1:51
for a, b, c being real number st 0 <= a & b < c holds
b - a < c
proof
let a, b, c be real number ; ::_thesis: ( 0 <= a & b < c implies b - a < c )
assume that
A1: 0 <= a and
A2: b < c ; ::_thesis: b - a < c
 b + 0 < a + c by A1, A2, Th40;
hence  b - a < c by Lm17; ::_thesis: verum
end;

theorem :: XREAL_1:52
for a, b, c being real number st a <= 0 & b <= c holds
b <= c - a
proof
let a, b, c be real number ; ::_thesis: ( a <= 0 & b <= c implies b <= c - a )
assume that
A1: a <= 0 and
A2: b <= c ; ::_thesis: b <= c - a
 b + a <= c by A1, A2, Th35;
hence  b <= c - a by Lm16; ::_thesis: verum
end;

theorem :: XREAL_1:53
for a, b, c being real number st a <= 0 & b < c holds
b < c - a
proof
let a, b, c be real number ; ::_thesis: ( a <= 0 & b < c implies b < c - a )
assume that
A1: a <= 0 and
A2: b < c ; ::_thesis: b < c - a
 b + a < c by A1, A2, Th36;
hence  b < c - a by Lm19; ::_thesis: verum
end;

theorem :: XREAL_1:54
for a, b, c being real number st a < 0 & b <= c holds
b < c - a
proof
let a, b, c be real number ; ::_thesis: ( a < 0 & b <= c implies b < c - a )
assume that
A1: a < 0 and
A2: b <= c ; ::_thesis: b < c - a
 a + b < c by A1, A2, Th37;
hence  b < c - a by Lm19; ::_thesis: verum
end;

theorem :: XREAL_1:55
for a, b being real number holds
( not a <> b or 0 < a - b or 0 < b - a )
proof
let a, b be real number ; ::_thesis: ( not a <> b or 0 < a - b or 0 < b - a )
assume A1: a <> b ; ::_thesis: ( 0 < a - b or 0 < b - a )
percases ( a < b or b < a ) by A1, XXREAL_0:1;
suppose a < b ; ::_thesis: ( 0 < a - b or 0 < b - a )
then  0 + a < b ;
hence  ( 0 < a - b or 0 < b - a ) by Lm19; ::_thesis: verum
end;
suppose b < a ; ::_thesis: ( 0 < a - b or 0 < b - a )
then  0 + b < a ;
hence  ( 0 < a - b or 0 < b - a ) by Lm19; ::_thesis: verum
end;
end;
end;

begin

theorem :: XREAL_1:56
for c, b being real number st ( for a being real number st a < 0 holds
c <= b - a ) holds
b >= c
proof
let c, b be real number ; ::_thesis: ( ( for a being real number st a < 0 holds
c <= b - a ) implies b >= c )
assume A1: for a being real number st a < 0 holds
b - a >= c ; ::_thesis: b >= c
set d = b - c;
assume  b < c ; ::_thesis: contradiction
then A2: 0 > b - c by Lm23;
then  (- (b - c)) / 2 < - (b - c) by Lm27;
then  b + (- ((b - c) / 2)) < b + (- (b - c)) by Lm10;
then  b - ((b - c) / 2) < b - (b - c) ;
hence  contradiction by A1, A2; ::_thesis: verum
end;

theorem :: XREAL_1:57
for b, c being real number st ( for a being real number st a > 0 holds
b - a <= c ) holds
b <= c
proof
let b, c be real number ; ::_thesis: ( ( for a being real number st a > 0 holds
b - a <= c ) implies b <= c )
assume A1: for a being real number st a > 0 holds
b - a <= c ; ::_thesis: b <= c
set d = b - c;
assume  b > c ; ::_thesis: contradiction
then A2: 0 < b - c by Lm21;
then  c + ((b - c) / 2) < c + (b - c) by Lm10, Lm27;
then  c < b - ((b - c) / 2) by Lm19;
hence  contradiction by A1, A2; ::_thesis: verum
end;

begin

theorem :: XREAL_1:58
for a being real number holds
( a < 0 iff 0 < - a ) ;

theorem :: XREAL_1:59
for a, b being real number st a <= - b holds
a + b <= 0
proof
let a, b be real number ; ::_thesis: ( a <= - b implies a + b <= 0 )
assume  a <= - b ; ::_thesis: a + b <= 0
then  a + b <= (- b) + b by Lm5;
hence  a + b <= 0 ; ::_thesis: verum
end;

theorem :: XREAL_1:60
for a, b being real number st - a <= b holds
0 <= a + b
proof
let a, b be real number ; ::_thesis: ( - a <= b implies 0 <= a + b )
assume  b >= - a ; ::_thesis: 0 <= a + b
then  b + a >= (- a) + a by Lm5;
hence  0 <= a + b ; ::_thesis: verum
end;

theorem :: XREAL_1:61
for a, b being real number st a < - b holds
a + b < 0
proof
let a, b be real number ; ::_thesis: ( a < - b implies a + b < 0 )
assume  a < - b ; ::_thesis: a + b < 0
then  a + b < (- b) + b by Lm10;
hence  a + b < 0 ; ::_thesis: verum
end;

theorem :: XREAL_1:62
for b, a being real number st - b < a holds
0 < a + b
proof
let b, a be real number ; ::_thesis: ( - b < a implies 0 < a + b )
assume  a > - b ; ::_thesis: 0 < a + b
then  a + b > (- b) + b by Lm10;
hence  0 < a + b ; ::_thesis: verum
end;

Lm28:  for a, b, c being real number st a <= b & c <= 0 holds
b * c <= a * c
proof
let a, b, c be real number ; ::_thesis: ( a <= b & c <= 0 implies b * c <= a * c )
assume A1: a <= b ; ::_thesis: ( not c <= 0 or b * c <= a * c )
assume  c <= 0 ; ::_thesis: b * c <= a * c
then  a * (- c) <= b * (- c) by A1, Lm12;
then  - (a * c) <= - (b * c) ;
hence  b * c <= a * c by Lm15; ::_thesis: verum
end;

begin

theorem :: XREAL_1:63
for a being real number holds 0 <= a * a
proof
let a be real number ; ::_thesis: 0 <= a * a
percases ( 0 <= a or not 0 <= a ) ;
suppose 0 <= a ; ::_thesis: 0 <= a * a
hence  0 <= a * a ; ::_thesis: verum
end;
suppose not 0 <= a ; ::_thesis: 0 <= a * a
hence  0 <= a * a ; ::_thesis: verum
end;
end;
end;

theorem :: XREAL_1:64
for a, b, c being real number st a <= b & 0 <= c holds
a * c <= b * c by Lm12;

theorem :: XREAL_1:65
for a, b, c being real number st a <= b & c <= 0 holds
b * c <= a * c by Lm28;

theorem Th66: :: XREAL_1:66
for a, b, c, d being real number st 0 <= a & a <= b & 0 <= c & c <= d holds
a * c <= b * d
proof
let a, b, c, d be real number ; ::_thesis: ( 0 <= a & a <= b & 0 <= c & c <= d implies a * c <= b * d )
assume that
A1: 0 <= a and
A2: a <= b and
A3: 0 <= c and
A4: c <= d ; ::_thesis: a * c <= b * d
A5: a * c <= b * c by A2, A3, Lm12;
 b * c <= b * d by A1, A2, A4, Lm12;
hence  a * c <= b * d by A5, XXREAL_0:2; ::_thesis: verum
end;

theorem :: XREAL_1:67
for a, b, c, d being real number st a <= 0 & b <= a & c <= 0 & d <= c holds
a * c <= b * d
proof
let a, b, c, d be real number ; ::_thesis: ( a <= 0 & b <= a & c <= 0 & d <= c implies a * c <= b * d )
assume that
A1: 0 >= a and
A2: a >= b and
A3: 0 >= c and
A4: c >= d ; ::_thesis: a * c <= b * d
A5: - c <= - d by A4, Lm14;
 - a <= - b by A2, Lm14;
then  (- a) * (- c) <= (- b) * (- d) by A1, A3, A5, Th66;
hence  a * c <= b * d ; ::_thesis: verum
end;

theorem :: XREAL_1:68
for c, a, b being real number st 0 < c & a < b holds
a * c < b * c by Lm13;

theorem :: XREAL_1:69
for c, a, b being real number st c < 0 & a < b holds
b * c < a * c by Lm24;

theorem :: XREAL_1:70
for a, b, c, d being real number st a < 0 & b <= a & c < 0 & d < c holds
a * c < b * d
proof
let a, b, c, d be real number ; ::_thesis: ( a < 0 & b <= a & c < 0 & d < c implies a * c < b * d )
assume that
A1: 0 > a and
A2: a >= b and
A3: 0 > c and
A4: c > d ; ::_thesis: a * c < b * d
A5: a * c < a * d by A1, A4, Lm24;
 a * d <= b * d by A2, A3, A4, Lm28;
hence  a * c < b * d by A5, XXREAL_0:2; ::_thesis: verum
end;

begin

theorem :: XREAL_1:71
for a, b, c, d being real number st 0 <= a & 0 <= b & 0 <= c & 0 <= d & (a * c) + (b * d) = 0 & not a = 0 holds
c = 0 ;

Lm29:  for c, a, b being real number st c < 0 & a < b holds
b / c < a / c
proof
let c, a, b be real number ; ::_thesis: ( c < 0 & a < b implies b / c < a / c )
assume that
A1: c < 0 and
A2: a < b ; ::_thesis: b / c < a / c
 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  b / c < a / c by Lm14; ::_thesis: verum
end;

Lm30:  for c, b, a being real number st c <= 0 & b / c < a / c holds
a < b
proof
let c, b, a be real number ; ::_thesis: ( c <= 0 & b / c < a / c implies a < b )
assume that
A1: c <= 0 and
A2: b / c < a / c ; ::_thesis: a < b
A3: now__::_thesis:_not_c_=_0
assume  c = 0 ; ::_thesis: contradiction
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; ::_thesis: verum
end;
then  (a / c) * c < (b / c) * c by A1, A2, Lm24;
then  a < (b / c) * c by A3, XCMPLX_1:87;
hence  a < b by A3, XCMPLX_1:87; ::_thesis: verum
end;

begin

theorem :: XREAL_1:72
for c, b, a being real number st 0 <= c & b <= a holds
b / c <= a / c by Lm25;

theorem :: XREAL_1:73
for c, a, b being real number st c <= 0 & a <= b holds
b / c <= a / c by Lm30;

theorem :: XREAL_1:74
for c, a, b being real number st 0 < c & a < b holds
a / c < b / c by Lm26;

theorem :: XREAL_1:75
for c, a, b being real number st c < 0 & a < b holds
b / c < a / c by Lm29;

theorem :: XREAL_1:76
for c, a, b being real number st 0 < c & 0 < a & a < b holds
c / b < c / a
proof
let c, a, b be real number ; ::_thesis: ( 0 < c & 0 < a & a < b implies c / b < c / a )
assume that
A1: 0 < c and
A2: 0 < a and
A3: a < b ; ::_thesis: c / b < c / a
 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  c / b < c / a by XCMPLX_0:def_9; ::_thesis: verum
end;

Lm31:  for b, a being real number st b < 0 & a < b holds
b " < a "
proof
let b, a be real number ; ::_thesis: ( b < 0 & a < b implies b " < a " )
A1: a " = 1 / a by XCMPLX_1:215;
assume that
A2: 0 > b and
A3: a < b ; ::_thesis: b " < a "
 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  b " < a " ; ::_thesis: verum
end;

begin

theorem Th77: :: XREAL_1:77
for b, a, c being real number st 0 < b & a * b <= c holds
a <= c / b
proof
let b, a, c be real number ; ::_thesis: ( 0 < b & a * b <= c implies a <= c / b )
assume that
A1: b > 0 and
A2: a * b <= c ; ::_thesis: a <= c / b
 (a * b) / b <= c / b by A1, A2, Lm25;
hence  a <= c / b by A1, XCMPLX_1:89; ::_thesis: verum
end;

theorem Th78: :: XREAL_1:78
for b, a, c being real number st b < 0 & a * b <= c holds
c / b <= a
proof
let b, a, c be real number ; ::_thesis: ( b < 0 & a * b <= c implies c / b <= a )
assume that
A1: b < 0 and
A2: a * b <= c ; ::_thesis: c / b <= a
 (a * b) / b >= c / b by A1, A2, Lm30;
hence  c / b <= a by A1, XCMPLX_1:89; ::_thesis: verum
end;

theorem Th79: :: XREAL_1:79
for b, c, a being real number st 0 < b & c <= a * b holds
c / b <= a
proof
let b, c, a be real number ; ::_thesis: ( 0 < b & c <= a * b implies c / b <= a )
assume that
A1: b > 0 and
A2: a * b >= c ; ::_thesis: c / b <= a
 (a * b) / b >= c / b by A1, A2, Lm25;
hence  c / b <= a by A1, XCMPLX_1:89; ::_thesis: verum
end;

theorem Th80: :: XREAL_1:80
for b, c, a being real number st b < 0 & c <= a * b holds
a <= c / b
proof
let b, c, a be real number ; ::_thesis: ( b < 0 & c <= a * b implies a <= c / b )
assume that
A1: b < 0 and
A2: a * b >= c ; ::_thesis: a <= c / b
 (a * b) / b <= c / b by A1, A2, Lm30;
hence  a <= c / b by A1, XCMPLX_1:89; ::_thesis: verum
end;

theorem Th81: :: XREAL_1:81
for b, a, c being real number st 0 < b & a * b < c holds
a < c / b
proof
let b, a, c be real number ; ::_thesis: ( 0 < b & a * b < c implies a < c / b )
assume that
A1: b > 0 and
A2: a * b < c ; ::_thesis: a < c / b
 (a * b) / b < c / b by A1, A2, Lm26;
hence  a < c / b by A1, XCMPLX_1:89; ::_thesis: verum
end;

theorem Th82: :: XREAL_1:82
for b, a, c being real number st b < 0 & a * b < c holds
c / b < a
proof
let b, a, c be real number ; ::_thesis: ( b < 0 & a * b < c implies c / b < a )
assume that
A1: b < 0 and
A2: a * b < c ; ::_thesis: c / b < a
 (a * b) / b > c / b by A1, A2, Lm29;
hence  c / b < a by A1, XCMPLX_1:89; ::_thesis: verum
end;

theorem Th83: :: XREAL_1:83
for b, c, a being real number st 0 < b & c < a * b holds
c / b < a
proof
let b, c, a be real number ; ::_thesis: ( 0 < b & c < a * b implies c / b < a )
assume that
A1: b > 0 and
A2: a * b > c ; ::_thesis: c / b < a
 (a * b) / b > c / b by A1, A2, Lm26;
hence  c / b < a by A1, XCMPLX_1:89; ::_thesis: verum
end;

theorem Th84: :: XREAL_1:84
for b, c, a being real number st b < 0 & c < a * b holds
a < c / b
proof
let b, c, a be real number ; ::_thesis: ( b < 0 & c < a * b implies a < c / b )
assume that
A1: b < 0 and
A2: a * b > c ; ::_thesis: a < c / b
 (a * b) / b < c / b by A1, A2, Lm29;
hence  a < c / b by A1, XCMPLX_1:89; ::_thesis: verum
end;

Lm32:  for a, b being real number st 0 < a & a <= b holds
b " <= a "
proof
let a, b be real number ; ::_thesis: ( 0 < a & a <= b implies b " <= a " )
assume that
A1: 0 < a and
A2: a <= b ; ::_thesis: b " <= a "
 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  b " <= a " ; ::_thesis: verum
end;

Lm33:  for b, a being real number st b < 0 & a <= b holds
b " <= a "
proof
let b, a be real number ; ::_thesis: ( b < 0 & a <= b implies b " <= a " )
assume that
A1: 0 > b and
A2: a <= b ; ::_thesis: b " <= a "
 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  b " <= a " ; ::_thesis: verum
end;

begin

theorem :: XREAL_1:85
for a, b being real number st 0 < a & a <= b holds
b " <= a " by Lm32;

theorem :: XREAL_1:86
for b, a being real number st b < 0 & a <= b holds
b " <= a " by Lm33;

theorem :: XREAL_1:87
for b, a being real number st b < 0 & a < b holds
b " < a " by Lm31;

Lm34:  for a, b being real number st 0 < a & a < b holds
b " < a "
proof
let a, b be real number ; ::_thesis: ( 0 < a & a < b implies b " < a " )
A1: b " = 1 / b by XCMPLX_1:215;
assume that
A2: 0 < a and
A3: a < b ; ::_thesis: b " < a "
 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  b " < a " ; ::_thesis: verum
end;

theorem :: XREAL_1:88
for a, b being real number st 0 < a & a < b holds
b " < a " by Lm34;

theorem :: XREAL_1:89
for b, a being real number st 0 < b " & b " <= a " holds
a <= b
proof
let b, a be real number ; ::_thesis: ( 0 < b " & b " <= a " implies a <= b )
assume that
A1: b " > 0 and
A2: a " >= b " ; ::_thesis: a <= b
 (a ") " <= (b ") " by A1, A2, Lm32;
hence  a <= b ; ::_thesis: verum
end;

theorem :: XREAL_1:90
for a, b being real number st a " < 0 & b " <= a " holds
a <= b
proof
let a, b be real number ; ::_thesis: ( a " < 0 & b " <= a " implies a <= b )
assume that
A1: a " < 0 and
A2: a " >= b " ; ::_thesis: a <= b
 (a ") " <= (b ") " by A1, A2, Lm33;
hence  a <= b ; ::_thesis: verum
end;

theorem :: XREAL_1:91
for b, a being real number st 0 < b " & b " < a " holds
a < b
proof
let b, a be real number ; ::_thesis: ( 0 < b " & b " < a " implies a < b )
assume that
A1: b " > 0 and
A2: a " > b " ; ::_thesis: a < b
 (a ") " < (b ") " by A1, A2, Lm34;
hence  a < b ; ::_thesis: verum
end;

theorem :: XREAL_1:92
for a, b being real number st a " < 0 & b " < a " holds
a < b
proof
let a, b be real number ; ::_thesis: ( a " < 0 & b " < a " implies a < b )
assume that
A1: a " < 0 and
A2: a " > b " ; ::_thesis: a < b
 (a ") " < (b ") " by A1, A2, Lm31;
hence  a < b ; ::_thesis: verum
end;

Lm35:  for b being real number
for a being non positive non negative real number holds 0 = a * b
;

begin

theorem :: XREAL_1:93
for a, b being real number st 0 <= a & (b - a) * (b + a) <= 0 holds
( - a <= b & b <= a )
proof
let a, b be real number ; ::_thesis: ( 0 <= a & (b - a) * (b + a) <= 0 implies ( - a <= b & b <= a ) )
assume that
A1: a >= 0 and
A2: (b - a) * (b + a) <= 0 ; ::_thesis: ( - a <= b & b <= a )
 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  ( - a <= b & b <= a ) by A3; ::_thesis: verum
end;

theorem :: XREAL_1:94
for a, b being real number st 0 <= a & (b - a) * (b + a) < 0 holds
( - a < b & b < a )
proof
let a, b be real number ; ::_thesis: ( 0 <= a & (b - a) * (b + a) < 0 implies ( - a < b & b < a ) )
assume that
A1: a >= 0 and
A2: (b - a) * (b + a) < 0 ; ::_thesis: ( - a < b & b < a )
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  ( - a < b & b < a ) by A4; ::_thesis: verum
end;

theorem :: XREAL_1:95
for b, a being real number holds
( not 0 <= (b - a) * (b + a) or b <= - a or a <= b )
proof
let b, a be real number ; ::_thesis: ( not 0 <= (b - a) * (b + a) or b <= - a or a <= b )
assume  (b - a) * (b + a) >= 0 ; ::_thesis: ( b <= - a or a <= b )
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  ( b <= - a or a <= b ) ; ::_thesis: verum
end;

theorem :: XREAL_1:96
for a, c, b, d being real number st 0 <= a & 0 <= c & a < b & c < d holds
a * c < b * d
proof
let a, c, b, d be real number ; ::_thesis: ( 0 <= a & 0 <= c & a < b & c < d implies a * c < b * d )
assume that
A1: 0 <= a and
A2: 0 <= c and
A3: a < b and
A4: c < d ; ::_thesis: a * c < b * d
A5: a * c <= a * d by A1, A4, Lm12;
 a * d < b * d by A2, A3, A4, Lm13;
hence  a * c < b * d by A5, XXREAL_0:2; ::_thesis: verum
end;

theorem :: XREAL_1:97
for a, c, b, d being real number st 0 <= a & 0 < c & a < b & c <= d holds
a * c < b * d
proof
let a, c, b, d be real number ; ::_thesis: ( 0 <= a & 0 < c & a < b & c <= d implies a * c < b * d )
assume that
A1: 0 <= a and
A2: 0 < c and
A3: a < b and
A4: c <= d ; ::_thesis: a * c < b * d
A5: a * c <= a * d by A1, A4, Lm12;
 a * d < b * d by A2, A3, A4, Lm13;
hence  a * c < b * d by A5, XXREAL_0:2; ::_thesis: verum
end;

theorem Th98: :: XREAL_1:98
for a, c, b, d being real number st 0 < a & 0 < c & a <= b & c < d holds
a * c < b * d
proof
let a, c, b, d be real number ; ::_thesis: ( 0 < a & 0 < c & a <= b & c < d implies a * c < b * d )
assume that
A1: 0 < a and
A2: 0 < c and
A3: a <= b and
A4: c < d ; ::_thesis: a * c < b * d
A5: a * c < a * d by A1, A4, Lm13;
 a * d <= b * d by A2, A3, A4, Lm12;
hence  a * c < b * d by A5, XXREAL_0:2; ::_thesis: verum
end;

theorem :: XREAL_1:99
for c, b, a being real number st 0 < c & b < 0 & a < b holds
c / b < c / a
proof
let c, b, a be real number ; ::_thesis: ( 0 < c & b < 0 & a < b implies c / b < c / a )
assume that
A1: c > 0 and
A2: b < 0 and
A3: a < b ; ::_thesis: c / b < c / a
 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  c / b < c / a by XCMPLX_0:def_9; ::_thesis: verum
end;

theorem :: XREAL_1:100
for c, a, b being real number st c < 0 & 0 < a & a < b holds
c / a < c / b
proof
let c, a, b be real number ; ::_thesis: ( c < 0 & 0 < a & a < b implies c / a < c / b )
assume that
A1: c < 0 and
A2: a > 0 and
A3: a < b ; ::_thesis: c / a < c / 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  c / a < c / b by XCMPLX_0:def_9; ::_thesis: verum
end;

theorem :: XREAL_1:101
for c, b, a being real number st c < 0 & b < 0 & a < b holds
c / a < c / b
proof
let c, b, a be real number ; ::_thesis: ( c < 0 & b < 0 & a < b implies c / a < c / b )
assume that
A1: c < 0 and
A2: b < 0 and
A3: a < b ; ::_thesis: c / a < c / b
 a " > b " by A2, A3, Lm31;
then  (a ") * c < (b ") * c by A1, Lm24;
then  c / a < (b ") * c by XCMPLX_0:def_9;
hence  c / a < c / b by XCMPLX_0:def_9; ::_thesis: verum
end;

theorem :: XREAL_1:102
for b, d, a, c being real number st 0 < b & 0 < d & a * d <= c * b holds
a / b <= c / d
proof
let b, d, a, c be real number ; ::_thesis: ( 0 < b & 0 < d & a * d <= c * b implies a / b <= c / d )
assume that
A1: b > 0 and
A2: d > 0 and
A3: a * d <= c * b ; ::_thesis: a / b <= c / d
 (a * d) / b <= c by A1, A3, Th79;
then  (a / b) * d <= c by XCMPLX_1:74;
hence  a / b <= c / d by A2, Th77; ::_thesis: verum
end;

theorem :: XREAL_1:103
for b, d, a, c being real number st b < 0 & d < 0 & a * d <= c * b holds
a / b <= c / d
proof
let b, d, a, c be real number ; ::_thesis: ( b < 0 & d < 0 & a * d <= c * b implies a / b <= c / d )
assume that
A1: b < 0 and
A2: d < 0 and
A3: a * d <= c * b ; ::_thesis: a / b <= c / d
 (a * d) / b >= c by A1, A3, Th80;
then  (a / b) * d >= c by XCMPLX_1:74;
hence  a / b <= c / d by A2, Th80; ::_thesis: verum
end;

theorem :: XREAL_1:104
for b, d, a, c being real number st 0 < b & d < 0 & a * d <= c * b holds
c / d <= a / b
proof
let b, d, a, c be real number ; ::_thesis: ( 0 < b & d < 0 & a * d <= c * b implies c / d <= a / b )
assume that
A1: b > 0 and
A2: d < 0 and
A3: a * d <= c * b ; ::_thesis: c / d <= a / b
 (a * d) / b <= c by A1, A3, Th79;
then  (a / b) * d <= c by XCMPLX_1:74;
hence  c / d <= a / b by A2, Th78; ::_thesis: verum
end;

theorem :: XREAL_1:105
for b, d, a, c being real number st b < 0 & 0 < d & a * d <= c * b holds
c / d <= a / b
proof
let b, d, a, c be real number ; ::_thesis: ( b < 0 & 0 < d & a * d <= c * b implies c / d <= a / b )
assume that
A1: b < 0 and
A2: d > 0 and
A3: a * d <= c * b ; ::_thesis: c / d <= a / b
 (a * d) / b >= c by A1, A3, Th80;
then  (a / b) * d >= c by XCMPLX_1:74;
hence  c / d <= a / b by A2, Th79; ::_thesis: verum
end;

theorem :: XREAL_1:106
for b, d, a, c being real number st 0 < b & 0 < d & a * d < c * b holds
a / b < c / d
proof
let b, d, a, c be real number ; ::_thesis: ( 0 < b & 0 < d & a * d < c * b implies a / b < c / d )
assume that
A1: b > 0 and
A2: d > 0 and
A3: a * d < c * b ; ::_thesis: a / b < c / d
 (a * d) / b < c by A1, A3, Th83;
then  (a / b) * d < c by XCMPLX_1:74;
hence  a / b < c / d by A2, Th81; ::_thesis: verum
end;

theorem :: XREAL_1:107
for b, d, a, c being real number st b < 0 & d < 0 & a * d < c * b holds
a / b < c / d
proof
let b, d, a, c be real number ; ::_thesis: ( b < 0 & d < 0 & a * d < c * b implies a / b < c / d )
assume that
A1: b < 0 and
A2: d < 0 and
A3: a * d < c * b ; ::_thesis: a / b < c / d
 (a * d) / b > c by A1, A3, Th84;
then  (a / b) * d > c by XCMPLX_1:74;
hence  a / b < c / d by A2, Th84; ::_thesis: verum
end;

theorem :: XREAL_1:108
for b, d, a, c being real number st 0 < b & d < 0 & a * d < c * b holds
c / d < a / b
proof
let b, d, a, c be real number ; ::_thesis: ( 0 < b & d < 0 & a * d < c * b implies c / d < a / b )
assume that
A1: b > 0 and
A2: d < 0 and
A3: a * d < c * b ; ::_thesis: c / d < a / b
 (a * d) / b < c by A1, A3, Th83;
then  (a / b) * d < c by XCMPLX_1:74;
hence  c / d < a / b by A2, Th82; ::_thesis: verum
end;

theorem :: XREAL_1:109
for b, d, a, c being real number st b < 0 & 0 < d & a * d < c * b holds
c / d < a / b
proof
let b, d, a, c be real number ; ::_thesis: ( b < 0 & 0 < d & a * d < c * b implies c / d < a / b )
assume that
A1: b < 0 and
A2: d > 0 and
A3: a * d < c * b ; ::_thesis: c / d < a / b
 (a * d) / b > c by A1, A3, Th84;
then  (a / b) * d > c by XCMPLX_1:74;
hence  c / d < a / b by A2, Th83; ::_thesis: verum
end;

theorem :: XREAL_1:110
for b, d, a, c being real number st b < 0 & d < 0 & a * b < c / d holds
a * d < c / b
proof
let b, d, a, c be real number ; ::_thesis: ( b < 0 & d < 0 & a * b < c / d implies a * d < c / b )
assume that
A1: b < 0 and
A2: d < 0 ; ::_thesis: ( not a * b < c / d or a * d < c / b )
assume  a * b < c / d ; ::_thesis: a * d < c / b
then  (a * b) * d > c by A2, Th78;
then  (a * d) * b > c ;
hence  a * d < c / b by A1, Th84; ::_thesis: verum
end;

theorem :: XREAL_1:111
for b, d, a, c being real number st 0 < b & 0 < d & a * b < c / d holds
a * d < c / b
proof
let b, d, a, c be real number ; ::_thesis: ( 0 < b & 0 < d & a * b < c / d implies a * d < c / b )
assume that
A1: b > 0 and
A2: d > 0 ; ::_thesis: ( not a * b < c / d or a * d < c / b )
assume  a * b < c / d ; ::_thesis: a * d < c / b
then  (a * b) * d < c by A2, Th79;
then  (a * d) * b < c ;
hence  a * d < c / b by A1, Th81; ::_thesis: verum
end;

theorem :: XREAL_1:112
for b, d, c, a being real number st b < 0 & d < 0 & c / d < a * b holds
c / b < a * d
proof
let b, d, c, a be real number ; ::_thesis: ( b < 0 & d < 0 & c / d < a * b implies c / b < a * d )
assume that
A1: b < 0 and
A2: d < 0 ; ::_thesis: ( not c / d < a * b or c / b < a * d )
assume  a * b > c / d ; ::_thesis: c / b < a * d
then  (a * b) * d < c by A2, Th80;
then  (a * d) * b < c ;
hence  c / b < a * d by A1, Th82; ::_thesis: verum
end;

theorem :: XREAL_1:113
for b, d, c, a being real number st 0 < b & 0 < d & c / d < a * b holds
c / b < a * d
proof
let b, d, c, a be real number ; ::_thesis: ( 0 < b & 0 < d & c / d < a * b implies c / b < a * d )
assume that
A1: b > 0 and
A2: d > 0 ; ::_thesis: ( not c / d < a * b or c / b < a * d )
assume  a * b > c / d ; ::_thesis: c / b < a * d
then  (a * b) * d > c by A2, Th77;
then  (a * d) * b > c ;
hence  c / b < a * d by A1, Th83; ::_thesis: verum
end;

theorem :: XREAL_1:114
for b, d, a, c being real number st b < 0 & 0 < d & a * b < c / d holds
c / b < a * d
proof
let b, d, a, c be real number ; ::_thesis: ( b < 0 & 0 < d & a * b < c / d implies c / b < a * d )
assume that
A1: b < 0 and
A2: d > 0 ; ::_thesis: ( not a * b < c / d or c / b < a * d )
assume  a * b < c / d ; ::_thesis: c / b < a * d
then  (a * b) * d < c by A2, Th79;
then  (a * d) * b < c ;
hence  c / b < a * d by A1, Th82; ::_thesis: verum
end;

theorem :: XREAL_1:115
for b, d, a, c being real number st 0 < b & d < 0 & a * b < c / d holds
c / b < a * d
proof
let b, d, a, c be real number ; ::_thesis: ( 0 < b & d < 0 & a * b < c / d implies c / b < a * d )
assume that
A1: b > 0 and
A2: d < 0 ; ::_thesis: ( not a * b < c / d or c / b < a * d )
assume  a * b < c / d ; ::_thesis: c / b < a * d
then  (a * b) * d > c by A2, Th78;
then  (a * d) * b > c ;
hence  c / b < a * d by A1, Th83; ::_thesis: verum
end;

theorem :: XREAL_1:116
for b, d, c, a being real number st b < 0 & 0 < d & c / d < a * b holds
a * d < c / b
proof
let b, d, c, a be real number ; ::_thesis: ( b < 0 & 0 < d & c / d < a * b implies a * d < c / b )
assume that
A1: b < 0 and
A2: d > 0 ; ::_thesis: ( not c / d < a * b or a * d < c / b )
assume  a * b > c / d ; ::_thesis: a * d < c / b
then  (a * b) * d > c by A2, Th77;
then  (a * d) * b > c ;
hence  a * d < c / b by A1, Th84; ::_thesis: verum
end;

theorem :: XREAL_1:117
for b, d, c, a being real number st 0 < b & d < 0 & c / d < a * b holds
a * d < c / b
proof
let b, d, c, a be real number ; ::_thesis: ( 0 < b & d < 0 & c / d < a * b implies a * d < c / b )
assume that
A1: b > 0 and
A2: d < 0 ; ::_thesis: ( not c / d < a * b or a * d < c / b )
assume  a * b > c / d ; ::_thesis: a * d < c / b
then  (a * b) * d < c by A2, Th80;
then  (a * d) * b < c ;
hence  a * d < c / b by A1, Th81; ::_thesis: verum
end;

theorem :: XREAL_1:118
for a, c, b being real number st 0 < a & 0 <= c & a <= b holds
c / b <= c / a
proof
let a, c, b be real number ; ::_thesis: ( 0 < a & 0 <= c & a <= b implies c / b <= c / a )
assume that
A1: 0 < a and
A2: 0 <= c and
A3: a <= b ; ::_thesis: c / b <= c / a
 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  c / b <= c / a by XCMPLX_0:def_9; ::_thesis: verum
end;

theorem :: XREAL_1:119
for c, b, a being real number st 0 <= c & b < 0 & a <= b holds
c / b <= c / a
proof
let c, b, a be real number ; ::_thesis: ( 0 <= c & b < 0 & a <= b implies c / b <= c / a )
assume that
A1: c >= 0 and
A2: b < 0 and
A3: a <= b ; ::_thesis: c / b <= c / a
 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  c / b <= c / a by XCMPLX_0:def_9; ::_thesis: verum
end;

theorem :: XREAL_1:120
for c, a, b being real number st c <= 0 & 0 < a & a <= b holds
c / a <= c / b
proof
let c, a, b be real number ; ::_thesis: ( c <= 0 & 0 < a & a <= b implies c / a <= c / b )
assume A1: c <= 0 ; ::_thesis: ( not 0 < a or not a <= b or c / a <= c / b )
assume that
A2: a > 0 and
A3: a <= b ; ::_thesis: c / a <= c / 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  c / a <= c / b by XCMPLX_0:def_9; ::_thesis: verum
end;

theorem :: XREAL_1:121
for c, b, a being real number st c <= 0 & b < 0 & a <= b holds
c / a <= c / b
proof
let c, b, a be real number ; ::_thesis: ( c <= 0 & b < 0 & a <= b implies c / a <= c / b )
assume that
A1: c <= 0 and
A2: b < 0 and
A3: a <= b ; ::_thesis: c / a <= c / 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  c / a <= c / b by XCMPLX_0:def_9; ::_thesis: verum
end;

theorem :: XREAL_1:122
for a being real number holds
( 0 < a iff 0 < a " ) ;

theorem :: XREAL_1:123
for a being real number holds
( a < 0 iff a " < 0 ) ;

theorem Th124: :: XREAL_1:124
for a, b being real number st a < 0 & 0 < b holds
a " < b "
proof
let a, b be real number ; ::_thesis: ( a < 0 & 0 < b implies a " < b " )
assume that
A1: a < 0 and
A2: b > 0 ; ::_thesis: a " < b "
 a " < 0 by A1;
hence  a " < b " by A2; ::_thesis: verum
end;

theorem :: XREAL_1:125
for a, b being real number st a " < 0 & 0 < b " holds
a < b
proof
let a, b be real number ; ::_thesis: ( a " < 0 & 0 < b " implies a < b )
assume that
A1: a " < 0 and
A2: b " > 0 ; ::_thesis: a < b
 (a ") " < (b ") " by A1, A2, Th124;
hence  a < b ; ::_thesis: verum
end;

begin

theorem :: XREAL_1:126
for a, b being real number st a <= 0 & 0 <= a holds
0 = a * b by Lm35;

theorem :: XREAL_1:127
for a, b being real number st 0 <= a & 0 <= b holds
0 <= a * b ;

theorem :: XREAL_1:128
for a, b being real number st a <= 0 & b <= 0 holds
0 <= a * b ;

theorem :: XREAL_1:129
for a, b being real number st 0 < a & 0 < b holds
0 < a * b ;

theorem :: XREAL_1:130
for a, b being real number st a < 0 & b < 0 holds
0 < a * b ;

theorem :: XREAL_1:131
for a, b being real number st 0 <= a & b <= 0 holds
a * b <= 0 ;

theorem :: XREAL_1:132
for a, b being real number st 0 < a & b < 0 holds
a * b < 0 ;

theorem :: XREAL_1:133
for a, b being real number holds
( not a * b < 0 or ( a > 0 & b < 0 ) or ( a < 0 & b > 0 ) )
proof
let a, b be real number ; ::_thesis: ( not a * b < 0 or ( a > 0 & b < 0 ) or ( a < 0 & b > 0 ) )
assume A1: a * b < 0 ; ::_thesis: ( ( a > 0 & b < 0 ) or ( a < 0 & b > 0 ) )
then A2: b <> 0 ;
 a <> 0 by A1;
hence  ( ( a > 0 & b < 0 ) or ( a < 0 & b > 0 ) ) by A1, A2; ::_thesis: verum
end;

theorem :: XREAL_1:134
for a, b being real number holds
( not a * b > 0 or ( a > 0 & b > 0 ) or ( a < 0 & b < 0 ) )
proof
let a, b be real number ; ::_thesis: ( not a * b > 0 or ( a > 0 & b > 0 ) or ( a < 0 & b < 0 ) )
assume A1: a * b > 0 ; ::_thesis: ( ( a > 0 & b > 0 ) or ( a < 0 & b < 0 ) )
then A2: b <> 0 ;
 a <> 0 by A1;
hence  ( ( a > 0 & b > 0 ) or ( a < 0 & b < 0 ) ) by A1, A2; ::_thesis: verum
end;

theorem :: XREAL_1:135
for a, b being real number st a <= 0 & b <= 0 holds
0 <= a / b ;

theorem :: XREAL_1:136
for a, b being real number st 0 <= a & 0 <= b holds
0 <= a / b ;

theorem :: XREAL_1:137
for a, b being real number st 0 <= a & b <= 0 holds
a / b <= 0 ;

theorem :: XREAL_1:138
for a, b being real number st a <= 0 & 0 <= b holds
a / b <= 0 ;

theorem :: XREAL_1:139
for a, b being real number st 0 < a & 0 < b holds
0 < a / b ;

theorem :: XREAL_1:140
for a, b being real number st a < 0 & b < 0 holds
0 < a / b ;

theorem :: XREAL_1:141
for a, b being real number st a < 0 & 0 < b holds
a / b < 0 ;

theorem :: XREAL_1:142
for a, b being real number st a < 0 & 0 < b holds
b / a < 0 ;

theorem :: XREAL_1:143
for a, b being real number holds
( not a / b < 0 or ( b < 0 & a > 0 ) or ( b > 0 & a < 0 ) )
proof
let a, b be real number ; ::_thesis: ( not a / b < 0 or ( b < 0 & a > 0 ) or ( b > 0 & a < 0 ) )
assume A1: a / b < 0 ; ::_thesis: ( ( b < 0 & a > 0 ) or ( b > 0 & a < 0 ) )
then A2: a <> 0 ;
 a / b = a * (b ") by XCMPLX_0:def_9;
then  b " <> 0 by A1;
hence  ( ( b < 0 & a > 0 ) or ( b > 0 & a < 0 ) ) by A1, A2; ::_thesis: verum
end;

theorem :: XREAL_1:144
for a, b being real number holds
( not a / b > 0 or ( b > 0 & a > 0 ) or ( b < 0 & a < 0 ) )
proof
let a, b be real number ; ::_thesis: ( not a / b > 0 or ( b > 0 & a > 0 ) or ( b < 0 & a < 0 ) )
assume A1: a / b > 0 ; ::_thesis: ( ( b > 0 & a > 0 ) or ( b < 0 & a < 0 ) )
then A2: a <> 0 ;
 a / b = a * (b ") by XCMPLX_0:def_9;
then  b " <> 0 by A1;
hence  ( ( b > 0 & a > 0 ) or ( b < 0 & a < 0 ) ) by A1, A2; ::_thesis: verum
end;

begin

theorem :: XREAL_1:145
for a, b being real number st a <= b holds
a < b + 1
proof
let a, b be real number ; ::_thesis: ( a <= b implies a < b + 1 )
assume  a <= b ; ::_thesis: a < b + 1
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  a < b + 1 ; ::_thesis: verum
end;

theorem :: XREAL_1:146
for a being real number holds a - 1 < a
proof
let a be real number ; ::_thesis: a - 1 < a
 a + (- 1) < a + 0 by Lm10;
hence  a - 1 < a ; ::_thesis: verum
end;

theorem :: XREAL_1:147
for a, b being real number st a <= b holds
a - 1 < b
proof
let a, b be real number ; ::_thesis: ( a <= b implies a - 1 < b )
assume  a <= b ; ::_thesis: a - 1 < b
then A1: a - 1 <= b - 1 by Lm7;
 b - 1 < (b - 1) + 1 by Lm9;
hence  a - 1 < b by A1, XXREAL_0:2; ::_thesis: verum
end;

theorem :: XREAL_1:148
for a being real number st - 1 < a holds
0 < 1 + a
proof
let a be real number ; ::_thesis: ( - 1 < a implies 0 < 1 + a )
assume  - 1 < a ; ::_thesis: 0 < 1 + a
then  (- 1) + 1 < a + 1 by Lm8;
hence  0 < 1 + a ; ::_thesis: verum
end;

theorem :: XREAL_1:149
for a being real number st a < 1 holds
1 - a > 0 by Lm21;

begin

theorem :: XREAL_1:150
for a, b being real number st a <= 1 & 0 <= b & b <= 1 & a * b = 1 holds
a = 1
proof
let a, b be real number ; ::_thesis: ( a <= 1 & 0 <= b & b <= 1 & a * b = 1 implies a = 1 )
assume that
A1: a <= 1 and
A2: 0 <= b and
A3: b <= 1 and
A4: a * b = 1 ; ::_thesis: a = 1
now__::_thesis:_(_(_b_=_0_&_contradiction_)_or_(_b_>_0_&_a_=_1_)_)
percases ( b = 0 or b > 0 ) by A2;
case b = 0 ; ::_thesis: contradiction
hence  contradiction by A4; ::_thesis: verum
end;
caseA5: b > 0 ; ::_thesis: a = 1
then  a = b " by A4, XCMPLX_0:def_7;
then  a >= 1 " by A3, A5, Lm32;
hence  a = 1 by A1, XXREAL_0:1; ::_thesis: verum
end;
end;
end;
hence  a = 1 ; ::_thesis: verum
end;

theorem :: XREAL_1:151
for a, b being real number st 0 <= a & 1 <= b holds
a <= a * b
proof
let a, b be real number ; ::_thesis: ( 0 <= a & 1 <= b implies a <= a * b )
assume that
A1: a >= 0 and
A2: b >= 1 ; ::_thesis: a <= a * b
 a * b >= a * 1 by A1, A2, Lm12;
hence  a <= a * b ; ::_thesis: verum
end;

theorem :: XREAL_1:152
for a, b being real number st a <= 0 & b <= 1 holds
a <= a * b
proof
let a, b be real number ; ::_thesis: ( a <= 0 & b <= 1 implies a <= a * b )
assume that
A1: a <= 0 and
A2: b <= 1 ; ::_thesis: a <= a * b
 a * b >= a * 1 by A1, A2, Lm28;
hence  a <= a * b ; ::_thesis: verum
end;

theorem :: XREAL_1:153
for a, b being real number st 0 <= a & b <= 1 holds
a * b <= a
proof
let a, b be real number ; ::_thesis: ( 0 <= a & b <= 1 implies a * b <= a )
assume that
A1: a >= 0 and
A2: b <= 1 ; ::_thesis: a * b <= a
 a * b <= a * 1 by A1, A2, Lm12;
hence  a * b <= a ; ::_thesis: verum
end;

theorem :: XREAL_1:154
for a, b being real number st a <= 0 & 1 <= b holds
a * b <= a
proof
let a, b be real number ; ::_thesis: ( a <= 0 & 1 <= b implies a * b <= a )
assume that
A1: a <= 0 and
A2: b >= 1 ; ::_thesis: a * b <= a
 a * b <= a * 1 by A1, A2, Lm28;
hence  a * b <= a ; ::_thesis: verum
end;

theorem Th155: :: XREAL_1:155
for a, b being real number st 0 < a & 1 < b holds
a < a * b
proof
let a, b be real number ; ::_thesis: ( 0 < a & 1 < b implies a < a * b )
assume that
A1: a > 0 and
A2: b > 1 ; ::_thesis: a < a * b
 a * b > a * 1 by A1, A2, Lm13;
hence  a < a * b ; ::_thesis: verum
end;

theorem :: XREAL_1:156
for a, b being real number st a < 0 & b < 1 holds
a < a * b
proof
let a, b be real number ; ::_thesis: ( a < 0 & b < 1 implies a < a * b )
assume that
A1: a < 0 and
A2: b < 1 ; ::_thesis: a < a * b
 a * b > a * 1 by A1, A2, Lm24;
hence  a < a * b ; ::_thesis: verum
end;

theorem :: XREAL_1:157
for a, b being real number st 0 < a & b < 1 holds
a * b < a
proof
let a, b be real number ; ::_thesis: ( 0 < a & b < 1 implies a * b < a )
assume that
A1: a > 0 and
A2: b < 1 ; ::_thesis: a * b < a
 a * b < a * 1 by A1, A2, Lm13;
hence  a * b < a ; ::_thesis: verum
end;

theorem :: XREAL_1:158
for a, b being real number st a < 0 & 1 < b holds
a * b < a
proof
let a, b be real number ; ::_thesis: ( a < 0 & 1 < b implies a * b < a )
assume that
A1: a < 0 and
A2: b > 1 ; ::_thesis: a * b < a
 a * b < a * 1 by A1, A2, Lm24;
hence  a * b < a ; ::_thesis: verum
end;

theorem :: XREAL_1:159
for a, b being real number st 1 <= a & 1 <= b holds
1 <= a * b
proof
let a, b be real number ; ::_thesis: ( 1 <= a & 1 <= b implies 1 <= a * b )
assume that
A1: a >= 1 and
A2: b >= 1 ; ::_thesis: 1 <= a * b
 a * b >= b * 1 by A1, A2, Lm12;
hence  1 <= a * b by A2, XXREAL_0:2; ::_thesis: verum
end;

theorem :: XREAL_1:160
for a, b being real number st 0 <= a & a <= 1 & b <= 1 holds
a * b <= 1
proof
let a, b be real number ; ::_thesis: ( 0 <= a & a <= 1 & b <= 1 implies a * b <= 1 )
assume that
A1: 0 <= a and
A2: a <= 1 and
A3: b <= 1 ; ::_thesis: a * b <= 1
 a * b <= 1 * a by A1, A3, Lm12;
hence  a * b <= 1 by A2, XXREAL_0:2; ::_thesis: verum
end;

theorem :: XREAL_1:161
for a, b being real number st 1 < a & 1 <= b holds
1 < a * b
proof
let a, b be real number ; ::_thesis: ( 1 < a & 1 <= b implies 1 < a * b )
assume that
A1: a > 1 and
A2: b >= 1 ; ::_thesis: 1 < a * b
 a * b > b * 1 by A1, A2, Lm13;
hence  1 < a * b by A2, XXREAL_0:2; ::_thesis: verum
end;

theorem :: XREAL_1:162
for a, b being real number st 0 <= a & a < 1 & b <= 1 holds
a * b < 1
proof
let a, b be real number ; ::_thesis: ( 0 <= a & a < 1 & b <= 1 implies a * b < 1 )
assume that
A1: 0 <= a and
A2: a < 1 and
A3: b <= 1 ; ::_thesis: a * b < 1
 a * b <= 1 * a by A1, A3, Lm12;
hence  a * b < 1 by A2, XXREAL_0:2; ::_thesis: verum
end;

theorem :: XREAL_1:163
for a, b being real number st a <= - 1 & b <= - 1 holds
1 <= a * b
proof
let a, b be real number ; ::_thesis: ( a <= - 1 & b <= - 1 implies 1 <= a * b )
assume that
A1: a <= - 1 and
A2: b <= - 1 ; ::_thesis: 1 <= a * b
A3: - b >= - (- 1) by A2, Lm14;
 a * b >= b * (- 1) by A1, A2, Lm28;
hence  1 <= a * b by A3, XXREAL_0:2; ::_thesis: verum
end;

theorem :: XREAL_1:164
for a, b being real number st a < - 1 & b <= - 1 holds
1 < a * b
proof
let a, b be real number ; ::_thesis: ( a < - 1 & b <= - 1 implies 1 < a * b )
assume that
A1: a < - 1 and
A2: b <= - 1 ; ::_thesis: 1 < a * b
A3: - b >= - (- 1) by A2, Lm14;
 a * b > b * (- 1) by A1, A2, Lm24;
hence  1 < a * b by A3, XXREAL_0:2; ::_thesis: verum
end;

theorem :: XREAL_1:165
for a, b being real number st a <= 0 & - 1 <= a & - 1 <= b holds
a * b <= 1
proof
let a, b be real number ; ::_thesis: ( a <= 0 & - 1 <= a & - 1 <= b implies a * b <= 1 )
assume that
A1: 0 >= a and
A2: a >= - 1 and
A3: b >= - 1 ; ::_thesis: a * b <= 1
A4: - a <= - (- 1) by A2, Lm14;
 a * b <= (- 1) * a by A1, A3, Lm28;
hence  a * b <= 1 by A4, XXREAL_0:2; ::_thesis: verum
end;

theorem :: XREAL_1:166
for a, b being real number st a <= 0 & - 1 < a & - 1 <= b holds
a * b < 1
proof
let a, b be real number ; ::_thesis: ( a <= 0 & - 1 < a & - 1 <= b implies a * b < 1 )
assume that
A1: 0 >= a and
A2: a > - 1 and
A3: b >= - 1 ; ::_thesis: a * b < 1
A4: - a < - (- 1) by A2, Lm15;
 a * b <= (- 1) * a by A1, A3, Lm28;
hence  a * b < 1 by A4, XXREAL_0:2; ::_thesis: verum
end;

begin

theorem Th167: :: XREAL_1:167
for c, b being real number st ( for a being real number st 1 < a holds
c <= b * a ) holds
c <= b
proof
let c, b be real number ; ::_thesis: ( ( for a being real number st 1 < a holds
c <= b * a ) implies c <= b )
assume A1: for a being real number st a > 1 holds
b * a >= c ; ::_thesis: c <= b
assume A2: not c <= b ; ::_thesis: contradiction
A3: b >= 0
proof
A4: c <= b * 2 by A1;
assume  b < 0 ; ::_thesis: contradiction
then A5: b * 2 < 0 ;
then  c < 0 by A1;
then  b / c > c / c by A2, Lm29;
then  b / c > 1 by A5, A4, XCMPLX_1:60;
then A6: b * (b / c) >= c by A1;
 b * (b / c) < c * (b / c) by A2, A5, A4, Lm13;
then  b * (b / c) < b by A5, A4, XCMPLX_1:87;
hence  contradiction by A2, A6, XXREAL_0:2; ::_thesis: verum
end;
percases ( b > 0 or b = 0 ) by A3;
supposeA7: b > 0 ; ::_thesis: contradiction
then  b / b < c / b by A2, Lm26;
then  1 < c / b by A7, XCMPLX_1:60;
then consider d being real number  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; ::_thesis: verum
end;
supposeA10: b = 0 ; ::_thesis: contradiction
 b * 2 >= c by A1;
hence  contradiction by A2, A10; ::_thesis: verum
end;
end;
end;

Lm36:  for a being real number st 1 < a holds
a " < 1
proof
let a be real number ; ::_thesis: ( 1 < a implies a " < 1 )
assume A1: 1 < a ; ::_thesis: a " < 1
then  1 * (a ") < a * (a ") by Lm13;
hence  a " < 1 by A1, XCMPLX_0:def_7; ::_thesis: verum
end;

theorem :: XREAL_1:168
for b, c being real number st ( for a being real number st 0 < a & a < 1 holds
b * a <= c ) holds
b <= c
proof
let b, c be real number ; ::_thesis: ( ( for a being real number st 0 < a & a < 1 holds
b * a <= c ) implies b <= c )
assume A1: for a being real number st 0 < a & a < 1 holds
b * a <= c ; ::_thesis: b <= c
now__::_thesis:_for_d_being_real_number_st_d_>_1_holds_
b_<=_c_*_d
let d be real number ; ::_thesis: ( d > 1 implies b <= c * d )
assume A2: d > 1 ; ::_thesis: b <= c * d
then  b * (d ") <= c by A1, Lm36;
then  b / d <= c by XCMPLX_0:def_9;
hence  b <= c * d by A2, Th81; ::_thesis: verum
end;
hence  b <= c by Th167; ::_thesis: verum
end;

Lm37:  for a, b being real number st a <= b & 0 <= a holds
a / b <= 1
proof
let a, b be real number ; ::_thesis: ( a <= b & 0 <= a implies a / b <= 1 )
assume A1: a <= b ; ::_thesis: ( not 0 <= a or a / b <= 1 )
assume A2: 0 <= a ; ::_thesis: a / b <= 1
percases ( a = 0 or a > 0 ) by A2;
suppose a = 0 ; ::_thesis: a / b <= 1
hence  a / b <= 1 ; ::_thesis: verum
end;
supposeA3: a > 0 ; ::_thesis: a / b <= 1
then  a / b <= b / b by A1, Lm25;
hence  a / b <= 1 by A1, A3, XCMPLX_1:60; ::_thesis: verum
end;
end;
end;

Lm38:  for b, a being real number st b <= a & 0 <= a holds
b / a <= 1
proof
let b, a be real number ; ::_thesis: ( b <= a & 0 <= a implies b / a <= 1 )
assume A1: b <= a ; ::_thesis: ( not 0 <= a or b / a <= 1 )
assume A2: a >= 0 ; ::_thesis: b / a <= 1
percases ( a = 0 or a > 0 ) by A2;
suppose a = 0 ; ::_thesis: b / a <= 1
then  a " = 0 ;
then  b * (a ") < 1 ;
hence  b / a <= 1 by XCMPLX_0:def_9; ::_thesis: verum
end;
supposeA3: a > 0 ; ::_thesis: b / a <= 1
assume  b / a > 1 ; ::_thesis: contradiction
then  (b / a) * a > 1 * a by A3, Lm13;
hence  contradiction by A1, A3, XCMPLX_1:87; ::_thesis: verum
end;
end;
end;

theorem :: XREAL_1:169
for b, c being real number st ( for a being real number st 0 < a & a < 1 holds
b <= a * c ) holds
b <= 0
proof
let b, c be real number ; ::_thesis: ( ( for a being real number st 0 < a & a < 1 holds
b <= a * c ) implies b <= 0 )
assume that
A1: for a being real number st 0 < a & a < 1 holds
b <= a * c and
A2: b > 0 ; ::_thesis: contradiction
A3: b * 2 > b by A2, Th155;
then A4: b > b / 2 by Th83;
percases ( c <= 0 or ( c <= b & c > 0 ) or ( b <= c & c > 0 ) ) ;
suppose c <= 0 ; ::_thesis: contradiction
then  (1 / 2) * c <= 0 ;
hence  contradiction by A1, A2; ::_thesis: verum
end;
supposethat A5: c <= b and
A6: c > 0 ; ::_thesis: contradiction
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  c / (2 * b) < 1 by A7, XXREAL_0:2;
then A8: (c / (2 * b)) * c >= b by A1, A2, A6;
percases ( c >= b or c < b ) ;
suppose c >= b ; ::_thesis: contradiction
then  b = c by A5, XXREAL_0:1;
then  (c / (2 * b)) * c = b / 2 by A6, XCMPLX_1:92;
hence  contradiction by A2, A8, Th83, Th155; ::_thesis: verum
end;
supposeA9: c < b ; ::_thesis: contradiction
then  (c / (2 * b)) * c < (c / (2 * b)) * b by A6, Th98;
then A10: (c / (2 * b)) * c < c / 2 by A2, XCMPLX_1:92;
 c / 2 < b / 2 by A9, Lm26;
then  (c / (2 * b)) * c < b / 2 by A10, XXREAL_0:2;
hence  contradiction by A4, A8, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
supposethat A11: b <= c and
A12: c > 0 ; ::_thesis: contradiction
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  b / (2 * c) < 1 by A13, XXREAL_0:2;
then A14: (b / (2 * c)) * c >= b by A1, A2, A12;
 (b / (2 * c)) * c = b / 2 by A12, XCMPLX_1:92;
hence  contradiction by A3, A14, Th83; ::_thesis: verum
end;
end;
end;

theorem :: XREAL_1:170
for d, a, b being real number st 0 <= d & d <= 1 & 0 <= a & 0 <= b & (d * a) + ((1 - d) * b) = 0 & not ( d = 0 & b = 0 ) & not ( d = 1 & a = 0 ) holds
( a = 0 & b = 0 )
proof
let d, a, b be real number ; ::_thesis: ( 0 <= d & d <= 1 & 0 <= a & 0 <= b & (d * a) + ((1 - d) * b) = 0 & not ( d = 0 & b = 0 ) & not ( d = 1 & a = 0 ) implies ( a = 0 & b = 0 ) )
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 ; ::_thesis: ( ( d = 0 & b = 0 ) or ( d = 1 & a = 0 ) or ( a = 0 & b = 0 ) )
 d - d <= 1 - d by A2, Lm7;
then  ( 1 - d = 0 or b = 0 ) by A1, A3, A4, A5;
hence  ( ( d = 0 & b = 0 ) or ( d = 1 & a = 0 ) or ( a = 0 & b = 0 ) ) by A5; ::_thesis: verum
end;

theorem :: XREAL_1:171
for d, a, b being real number st 0 <= d & a <= b holds
a <= ((1 - d) * a) + (d * b)
proof
let d, a, b be real number ; ::_thesis: ( 0 <= d & a <= b implies a <= ((1 - d) * a) + (d * b) )
assume that
A1: 0 <= d and
A2: a <= b ; ::_thesis: a <= ((1 - d) * a) + (d * b)
 d * a <= d * b by A1, A2, Lm12;
then  ((1 - d) * a) + (d * a) <= ((1 - d) * a) + (d * b) by Lm6;
hence  a <= ((1 - d) * a) + (d * b) ; ::_thesis: verum
end;

theorem :: XREAL_1:172
for d, a, b being real number st d <= 1 & a <= b holds
((1 - d) * a) + (d * b) <= b
proof
let d, a, b be real number ; ::_thesis: ( d <= 1 & a <= b implies ((1 - d) * a) + (d * b) <= b )
assume that
A1: d <= 1 and
A2: a <= b ; ::_thesis: ((1 - d) * a) + (d * b) <= 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  ((1 - d) * a) + (d * b) <= b ; ::_thesis: verum
end;

theorem :: XREAL_1:173
for d, a, b, c being real number st 0 <= d & d <= 1 & a <= b & a <= c holds
a <= ((1 - d) * b) + (d * c)
proof
let d, a, b, c be real number ; ::_thesis: ( 0 <= d & d <= 1 & a <= b & a <= c implies a <= ((1 - d) * b) + (d * c) )
assume that
A1: 0 <= d and
A2: d <= 1 and
A3: a <= b and
A4: a <= c ; ::_thesis: a <= ((1 - d) * b) + (d * 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  a <= ((1 - d) * b) + (d * c) by A5, A6, Lm6; ::_thesis: verum
end;

theorem :: XREAL_1:174
for d, b, a, c being real number st 0 <= d & d <= 1 & b <= a & c <= a holds
((1 - d) * b) + (d * c) <= a
proof
let d, b, a, c be real number ; ::_thesis: ( 0 <= d & d <= 1 & b <= a & c <= a implies ((1 - d) * b) + (d * c) <= a )
assume that
A1: 0 <= d and
A2: d <= 1 and
A3: a >= b and
A4: a >= c ; ::_thesis: ((1 - d) * b) + (d * c) <= a
 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  ((1 - d) * b) + (d * c) <= a by A5, A6, Lm6; ::_thesis: verum
end;

theorem :: XREAL_1:175
for d, a, b, c being real number st 0 <= d & d <= 1 & a < b & a < c holds
a < ((1 - d) * b) + (d * c)
proof
let d, a, b, c be real number ; ::_thesis: ( 0 <= d & d <= 1 & a < b & a < c implies a < ((1 - d) * b) + (d * c) )
assume that
A1: 0 <= d and
A2: d <= 1 and
A3: a < b and
A4: a < c ; ::_thesis: a < ((1 - d) * b) + (d * c)
percases ( d = 0 or d = 1 or ( not d = 0 & not d = 1 ) ) ;
suppose d = 0 ; ::_thesis: a < ((1 - d) * b) + (d * c)
hence  a < ((1 - d) * b) + (d * c) by A3; ::_thesis: verum
end;
suppose d = 1 ; ::_thesis: a < ((1 - d) * b) + (d * c)
hence  a < ((1 - d) * b) + (d * c) by A4; ::_thesis: verum
end;
supposeA5: ( not d = 0 & not d = 1 ) ; ::_thesis: a < ((1 - d) * b) + (d * c)
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  a < ((1 - d) * b) + (d * c) by A6, A7, Lm8; ::_thesis: verum
end;
end;
end;

theorem :: XREAL_1:176
for d, b, a, c being real number st 0 <= d & d <= 1 & b < a & c < a holds
((1 - d) * b) + (d * c) < a
proof
let d, b, a, c be real number ; ::_thesis: ( 0 <= d & d <= 1 & b < a & c < a implies ((1 - d) * b) + (d * c) < a )
assume that
A1: 0 <= d and
A2: d <= 1 and
A3: a > b and
A4: a > c ; ::_thesis: ((1 - d) * b) + (d * c) < a
percases ( d = 0 or d = 1 or ( not d = 0 & not d = 1 ) ) ;
suppose d = 0 ; ::_thesis: ((1 - d) * b) + (d * c) < a
hence  ((1 - d) * b) + (d * c) < a by A3; ::_thesis: verum
end;
suppose d = 1 ; ::_thesis: ((1 - d) * b) + (d * c) < a
hence  ((1 - d) * b) + (d * c) < a by A4; ::_thesis: verum
end;
supposeA5: ( not d = 0 & not d = 1 ) ; ::_thesis: ((1 - d) * b) + (d * c) < a
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  ((1 - d) * b) + (d * c) < a by A6, A7, Lm8; ::_thesis: verum
end;
end;
end;

theorem :: XREAL_1:177
for d, a, b, c being real number st 0 < d & d < 1 & a <= b & a < c holds
a < ((1 - d) * b) + (d * c)
proof
let d, a, b, c be real number ; ::_thesis: ( 0 < d & d < 1 & a <= b & a < c implies a < ((1 - d) * b) + (d * c) )
assume that
A1: 0 < d and
A2: d < 1 and
A3: a <= b and
A4: a < c ; ::_thesis: a < ((1 - d) * b) + (d * 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  a < ((1 - d) * b) + (d * c) by A5, A6, Lm8; ::_thesis: verum
end;

theorem :: XREAL_1:178
for d, b, a, c being real number st 0 < d & d < 1 & b < a & c <= a holds
((1 - d) * b) + (d * c) < a
proof
let d, b, a, c be real number ; ::_thesis: ( 0 < d & d < 1 & b < a & c <= a implies ((1 - d) * b) + (d * c) < a )
assume that
A1: 0 < d and
A2: d < 1 and
A3: a > b and
A4: a >= c ; ::_thesis: ((1 - d) * b) + (d * c) < a
 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  ((1 - d) * b) + (d * c) < a by A5, A6, Lm8; ::_thesis: verum
end;

theorem :: XREAL_1:179
for d, a, b being real number st 0 <= d & d <= 1 & a <= ((1 - d) * a) + (d * b) & b < ((1 - d) * a) + (d * b) holds
d = 0
proof
let d, a, b be real number ; ::_thesis: ( 0 <= d & d <= 1 & a <= ((1 - d) * a) + (d * b) & b < ((1 - d) * a) + (d * b) implies d = 0 )
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) ; ::_thesis: d = 0
set s = ((1 - d) * a) + (d * b);
assume  d <> 0 ; ::_thesis: contradiction
then A5: d * b < d * (((1 - d) * a) + (d * b)) by A1, A4, Lm13;
 1 - d >= 0 by A2, Th48;
then A6: (1 - d) * a <= (1 - d) * (((1 - d) * a) + (d * b)) by A3, Lm12;
 1 * (((1 - d) * a) + (d * b)) = ((1 - d) * (((1 - d) * a) + (d * b))) + (d * (((1 - d) * a) + (d * b))) ;
hence  contradiction by A5, A6, Lm8; ::_thesis: verum
end;

theorem :: XREAL_1:180
for d, a, b being real number st 0 <= d & d <= 1 & ((1 - d) * a) + (d * b) <= a & ((1 - d) * a) + (d * b) < b holds
d = 0
proof
let d, a, b be real number ; ::_thesis: ( 0 <= d & d <= 1 & ((1 - d) * a) + (d * b) <= a & ((1 - d) * a) + (d * b) < b implies d = 0 )
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) ; ::_thesis: d = 0
set s = ((1 - d) * a) + (d * b);
assume  d <> 0 ; ::_thesis: contradiction
then A5: d * b > d * (((1 - d) * a) + (d * b)) by A1, A4, Lm13;
 1 - d >= 0 by A2, Th48;
then A6: (1 - d) * a >= (1 - d) * (((1 - d) * a) + (d * b)) by A3, Lm12;
 1 * (((1 - d) * a) + (d * b)) = ((1 - d) * (((1 - d) * a) + (d * b))) + (d * (((1 - d) * a) + (d * b))) ;
hence  contradiction by A5, A6, Lm8; ::_thesis: verum
end;

begin

theorem :: XREAL_1:181
for a, b being real number st 0 < a & a <= b holds
1 <= b / a
proof
let a, b be real number ; ::_thesis: ( 0 < a & a <= b implies 1 <= b / a )
assume that
A1: 0 < a and
A2: a <= b ; ::_thesis: 1 <= b / a
 b / a >= a / a by A1, A2, Lm25;
hence  1 <= b / a by A1, XCMPLX_1:60; ::_thesis: verum
end;

theorem :: XREAL_1:182
for a, b being real number st a < 0 & b <= a holds
1 <= b / a
proof
let a, b be real number ; ::_thesis: ( a < 0 & b <= a implies 1 <= b / a )
assume that
A1: a < 0 and
A2: b <= a ; ::_thesis: 1 <= b / a
 b / a >= a / a by A1, A2, Lm30;
hence  1 <= b / a by A1, XCMPLX_1:60; ::_thesis: verum
end;

theorem :: XREAL_1:183
for a, b being real number st 0 <= a & a <= b holds
a / b <= 1 by Lm37;

theorem :: XREAL_1:184
for b, a being real number st b <= a & a <= 0 holds
a / b <= 1
proof
let b, a be real number ; ::_thesis: ( b <= a & a <= 0 implies a / b <= 1 )
assume A1: b <= a ; ::_thesis: ( not a <= 0 or a / b <= 1 )
assume A2: a <= 0 ; ::_thesis: a / b <= 1
percases ( a = 0 or a < 0 ) by A2;
suppose a = 0 ; ::_thesis: a / b <= 1
hence  a / b <= 1 ; ::_thesis: verum
end;
supposeA3: a < 0 ; ::_thesis: a / b <= 1
then  a / b <= b / b by A1, Lm30;
hence  a / b <= 1 by A1, A3, XCMPLX_1:60; ::_thesis: verum
end;
end;
end;

theorem :: XREAL_1:185
for a, b being real number st 0 <= a & b <= a holds
b / a <= 1 by Lm38;

theorem :: XREAL_1:186
for a, b being real number st a <= 0 & a <= b holds
b / a <= 1
proof
let a, b be real number ; ::_thesis: ( a <= 0 & a <= b implies b / a <= 1 )
assume A1: a <= 0 ; ::_thesis: ( not a <= b or b / a <= 1 )
percases ( a = 0 or a < 0 ) by A1;
suppose a = 0 ; ::_thesis: ( not a <= b or b / a <= 1 )
then  a " = 0 ;
then  b * (a ") = 0 ;
hence  ( not a <= b or b / a <= 1 ) by XCMPLX_0:def_9; ::_thesis: verum
end;
supposeA2: a < 0 ; ::_thesis: ( not a <= b or b / a <= 1 )
assume A3: a <= b ; ::_thesis: b / a <= 1
assume  b / a > 1 ; ::_thesis: contradiction
then  (b / a) * a < 1 * a by A2, Lm24;
hence  contradiction by A2, A3, XCMPLX_1:87; ::_thesis: verum
end;
end;
end;

theorem :: XREAL_1:187
for a, b being real number st 0 < a & a < b holds
1 < b / a
proof
let a, b be real number ; ::_thesis: ( 0 < a & a < b implies 1 < b / a )
assume A1: a > 0 ; ::_thesis: ( not a < b or 1 < b / a )
assume A2: a < b ; ::_thesis: 1 < b / a
assume  b / a <= 1 ; ::_thesis: contradiction
then  (b / a) * a <= 1 * a by A1, Lm12;
hence  contradiction by A1, A2, XCMPLX_1:87; ::_thesis: verum
end;

theorem :: XREAL_1:188
for a, b being real number st a < 0 & b < a holds
1 < b / a
proof
let a, b be real number ; ::_thesis: ( a < 0 & b < a implies 1 < b / a )
assume that
A1: a < 0 and
A2: b < a ; ::_thesis: 1 < b / a
 b / a > a / a by A1, A2, Lm29;
hence  1 < b / a by A1, XCMPLX_1:60; ::_thesis: verum
end;

theorem :: XREAL_1:189
for a, b being real number st 0 <= a & a < b holds
a / b < 1
proof
let a, b be real number ; ::_thesis: ( 0 <= a & a < b implies a / b < 1 )
assume that
A1: 0 <= a and
A2: a < b ; ::_thesis: a / b < 1
 a / b < b / b by A1, A2, Lm26;
hence  a / b < 1 by A1, A2, XCMPLX_1:60; ::_thesis: verum
end;

theorem :: XREAL_1:190
for a, b being real number st a <= 0 & b < a holds
a / b < 1
proof
let a, b be real number ; ::_thesis: ( a <= 0 & b < a implies a / b < 1 )
assume that
A1: a <= 0 and
A2: b < a ; ::_thesis: a / b < 1
 a / b < b / b by A1, A2, Lm29;
hence  a / b < 1 by A1, A2, XCMPLX_1:60; ::_thesis: verum
end;

theorem :: XREAL_1:191
for a, b being real number st 0 < a & b < a holds
b / a < 1
proof
let a, b be real number ; ::_thesis: ( 0 < a & b < a implies b / a < 1 )
assume A1: a > 0 ; ::_thesis: ( not b < a or b / a < 1 )
assume A2: b < a ; ::_thesis: b / a < 1
assume  b / a >= 1 ; ::_thesis: contradiction
then  (b / a) * a >= 1 * a by A1, Lm12;
hence  contradiction by A1, A2, XCMPLX_1:87; ::_thesis: verum
end;

theorem :: XREAL_1:192
for a, b being real number st a < 0 & a < b holds
b / a < 1
proof
let a, b be real number ; ::_thesis: ( a < 0 & a < b implies b / a < 1 )
assume A1: a < 0 ; ::_thesis: ( not a < b or b / a < 1 )
assume A2: a < b ; ::_thesis: b / a < 1
assume  b / a >= 1 ; ::_thesis: contradiction
then  (b / a) * a <= 1 * a by A1, Lm28;
hence  contradiction by A1, A2, XCMPLX_1:87; ::_thesis: verum
end;

begin

theorem :: XREAL_1:193
for b, a being real number st 0 <= b & - b <= a holds
- 1 <= a / b
proof
let b, a be real number ; ::_thesis: ( 0 <= b & - b <= a implies - 1 <= a / b )
assume A1: b >= 0 ; ::_thesis: ( not - b <= a or - 1 <= a / b )
percases ( b = 0 or b > 0 ) by A1;
suppose b = 0 ; ::_thesis: ( not - b <= a or - 1 <= a / b )
then  b " = 0 ;
then  a * (b ") = 0 ;
hence  ( not - b <= a or - 1 <= a / b ) by XCMPLX_0:def_9; ::_thesis: verum
end;
supposeA2: b > 0 ; ::_thesis: ( not - b <= a or - 1 <= a / b )
assume A3: - b <= a ; ::_thesis: - 1 <= a / b
assume  a / b < - 1 ; ::_thesis: contradiction
then  (a / b) * b < (- 1) * b by A2, Lm13;
hence  contradiction by A2, A3, XCMPLX_1:87; ::_thesis: verum
end;
end;
end;

theorem :: XREAL_1:194
for b, a being real number st 0 <= b & - a <= b holds
- 1 <= a / b
proof
let b, a be real number ; ::_thesis: ( 0 <= b & - a <= b implies - 1 <= a / b )
assume A1: b >= 0 ; ::_thesis: ( not - a <= b or - 1 <= a / b )
percases ( b = 0 or b > 0 ) by A1;
suppose b = 0 ; ::_thesis: ( not - a <= b or - 1 <= a / b )
then  b " = 0 ;
then  a * (b ") = 0 ;
hence  ( not - a <= b or - 1 <= a / b ) by XCMPLX_0:def_9; ::_thesis: verum
end;
supposeA2: b > 0 ; ::_thesis: ( not - a <= b or - 1 <= a / b )
assume A3: - a <= b ; ::_thesis: - 1 <= a / b
assume  a / b < - 1 ; ::_thesis: contradiction
then  (a / b) * b < (- 1) * b by A2, Lm13;
then  a < - b by A2, XCMPLX_1:87;
hence  contradiction by A3, Th26; ::_thesis: verum
end;
end;
end;

theorem :: XREAL_1:195
for b, a being real number st b <= 0 & a <= - b holds
- 1 <= a / b
proof
let b, a be real number ; ::_thesis: ( b <= 0 & a <= - b implies - 1 <= a / b )
assume A1: b <= 0 ; ::_thesis: ( not a <= - b or - 1 <= a / b )
percases ( b = 0 or b < 0 ) by A1;
suppose b = 0 ; ::_thesis: ( not a <= - b or - 1 <= a / b )
then  b " = 0 ;
then  a * (b ") = 0 ;
hence  ( not a <= - b or - 1 <= a / b ) by XCMPLX_0:def_9; ::_thesis: verum
end;
supposeA2: b < 0 ; ::_thesis: ( not a <= - b or - 1 <= a / b )
assume A3: a <= - b ; ::_thesis: - 1 <= a / b
assume  a / b < - 1 ; ::_thesis: contradiction
then  (a / b) * b > (- 1) * b by A2, Lm24;
hence  contradiction by A2, A3, XCMPLX_1:87; ::_thesis: verum
end;
end;
end;

theorem :: XREAL_1:196
for b, a being real number st b <= 0 & b <= - a holds
- 1 <= a / b
proof
let b, a be real number ; ::_thesis: ( b <= 0 & b <= - a implies - 1 <= a / b )
assume A1: b <= 0 ; ::_thesis: ( not b <= - a or - 1 <= a / b )
percases ( b = 0 or b < 0 ) by A1;
suppose b = 0 ; ::_thesis: ( not b <= - a or - 1 <= a / b )
then  b " = 0 ;
then  a * (b ") = 0 ;
hence  ( not b <= - a or - 1 <= a / b ) by XCMPLX_0:def_9; ::_thesis: verum
end;
supposeA2: b < 0 ; ::_thesis: ( not b <= - a or - 1 <= a / b )
assume A3: b <= - a ; ::_thesis: - 1 <= a / b
assume  a / b < - 1 ; ::_thesis: contradiction
then  (a / b) * b > (- 1) * b by A2, Lm24;
then  a > - b by A2, XCMPLX_1:87;
hence  contradiction by A3, Th25; ::_thesis: verum
end;
end;
end;

theorem :: XREAL_1:197
for b, a being real number st 0 < b & - b < a holds
- 1 < a / b
proof
let b, a be real number ; ::_thesis: ( 0 < b & - b < a implies - 1 < a / b )
assume A1: b > 0 ; ::_thesis: ( not - b < a or - 1 < a / b )
assume A2: - b < a ; ::_thesis: - 1 < a / b
assume  a / b <= - 1 ; ::_thesis: contradiction
then  (a / b) * b <= (- 1) * b by A1, Lm12;
hence  contradiction by A1, A2, XCMPLX_1:87; ::_thesis: verum
end;

theorem :: XREAL_1:198
for b, a being real number st 0 < b & - a < b holds
- 1 < a / b
proof
let b, a be real number ; ::_thesis: ( 0 < b & - a < b implies - 1 < a / b )
assume A1: b > 0 ; ::_thesis: ( not - a < b or - 1 < a / b )
assume A2: - a < b ; ::_thesis: - 1 < a / b
assume  a / b <= - 1 ; ::_thesis: contradiction
then  (a / b) * b <= (- 1) * b by A1, Lm12;
then  a <= - b by A1, XCMPLX_1:87;
hence  contradiction by A2, Th25; ::_thesis: verum
end;

theorem :: XREAL_1:199
for b, a being real number st b < 0 & a < - b holds
- 1 < a / b
proof
let b, a be real number ; ::_thesis: ( b < 0 & a < - b implies - 1 < a / b )
assume A1: b < 0 ; ::_thesis: ( not a < - b or - 1 < a / b )
assume A2: a < - b ; ::_thesis: - 1 < a / b
assume  a / b <= - 1 ; ::_thesis: contradiction
then  (a / b) * b >= (- 1) * b by A1, Lm28;
hence  contradiction by A1, A2, XCMPLX_1:87; ::_thesis: verum
end;

theorem :: XREAL_1:200
for b, a being real number st b < 0 & b < - a holds
- 1 < a / b
proof
let b, a be real number ; ::_thesis: ( b < 0 & b < - a implies - 1 < a / b )
assume A1: b < 0 ; ::_thesis: ( not b < - a or - 1 < a / b )
assume A2: b < - a ; ::_thesis: - 1 < a / b
assume  a / b <= - 1 ; ::_thesis: contradiction
then  (a / b) * b >= (- 1) * b by A1, Lm28;
then  a >= - b by A1, XCMPLX_1:87;
hence  contradiction by A2, Th26; ::_thesis: verum
end;

theorem :: XREAL_1:201
for b, a being real number st 0 < b & a <= - b holds
a / b <= - 1
proof
let b, a be real number ; ::_thesis: ( 0 < b & a <= - b implies a / b <= - 1 )
assume A1: b > 0 ; ::_thesis: ( not a <= - b or a / b <= - 1 )
assume A2: a <= - b ; ::_thesis: a / b <= - 1
assume  a / b > - 1 ; ::_thesis: contradiction
then  (a / b) * b > (- 1) * b by A1, Lm13;
hence  contradiction by A1, A2, XCMPLX_1:87; ::_thesis: verum
end;

theorem :: XREAL_1:202
for b, a being real number st 0 < b & b <= - a holds
a / b <= - 1
proof
let b, a be real number ; ::_thesis: ( 0 < b & b <= - a implies a / b <= - 1 )
assume A1: b > 0 ; ::_thesis: ( not b <= - a or a / b <= - 1 )
assume A2: b <= - a ; ::_thesis: a / b <= - 1
assume  a / b > - 1 ; ::_thesis: contradiction
then  (a / b) * b > (- 1) * b by A1, Lm13;
then  a > - b by A1, XCMPLX_1:87;
hence  contradiction by A2, Th25; ::_thesis: verum
end;

theorem :: XREAL_1:203
for b, a being real number st b < 0 & - b <= a holds
a / b <= - 1
proof
let b, a be real number ; ::_thesis: ( b < 0 & - b <= a implies a / b <= - 1 )
assume A1: b < 0 ; ::_thesis: ( not - b <= a or a / b <= - 1 )
assume A2: - b <= a ; ::_thesis: a / b <= - 1
assume  a / b > - 1 ; ::_thesis: contradiction
then  (a / b) * b < (- 1) * b by A1, Lm24;
hence  contradiction by A1, A2, XCMPLX_1:87; ::_thesis: verum
end;

theorem :: XREAL_1:204
for b, a being real number st b < 0 & - a <= b holds
a / b <= - 1
proof
let b, a be real number ; ::_thesis: ( b < 0 & - a <= b implies a / b <= - 1 )
assume A1: b < 0 ; ::_thesis: ( not - a <= b or a / b <= - 1 )
assume A2: - a <= b ; ::_thesis: a / b <= - 1
assume  a / b > - 1 ; ::_thesis: contradiction
then  (a / b) * b < (- 1) * b by A1, Lm24;
then  a < - b by A1, XCMPLX_1:87;
hence  contradiction by A2, Th26; ::_thesis: verum
end;

theorem :: XREAL_1:205
for b, a being real number st 0 < b & a < - b holds
a / b < - 1
proof
let b, a be real number ; ::_thesis: ( 0 < b & a < - b implies a / b < - 1 )
assume A1: b > 0 ; ::_thesis: ( not a < - b or a / b < - 1 )
assume A2: a < - b ; ::_thesis: a / b < - 1
assume  a / b >= - 1 ; ::_thesis: contradiction
then  (a / b) * b >= (- 1) * b by A1, Lm12;
hence  contradiction by A1, A2, XCMPLX_1:87; ::_thesis: verum
end;

theorem :: XREAL_1:206
for b, a being real number st 0 < b & b < - a holds
a / b < - 1
proof
let b, a be real number ; ::_thesis: ( 0 < b & b < - a implies a / b < - 1 )
assume A1: b > 0 ; ::_thesis: ( not b < - a or a / b < - 1 )
assume A2: b < - a ; ::_thesis: a / b < - 1
assume  a / b >= - 1 ; ::_thesis: contradiction
then  (a / b) * b >= (- 1) * b by A1, Lm12;
then  a >= - b by A1, XCMPLX_1:87;
hence  contradiction by A2, Th26; ::_thesis: verum
end;

theorem :: XREAL_1:207
for b, a being real number st b < 0 & - b < a holds
a / b < - 1
proof
let b, a be real number ; ::_thesis: ( b < 0 & - b < a implies a / b < - 1 )
assume A1: b < 0 ; ::_thesis: ( not - b < a or a / b < - 1 )
assume A2: - b < a ; ::_thesis: a / b < - 1
assume  a / b >= - 1 ; ::_thesis: contradiction
then  (a / b) * b <= (- 1) * b by A1, Lm28;
hence  contradiction by A1, A2, XCMPLX_1:87; ::_thesis: verum
end;

theorem :: XREAL_1:208
for b, a being real number st b < 0 & - a < b holds
a / b < - 1
proof
let b, a be real number ; ::_thesis: ( b < 0 & - a < b implies a / b < - 1 )
assume A1: b < 0 ; ::_thesis: ( not - a < b or a / b < - 1 )
assume A2: - a < b ; ::_thesis: a / b < - 1
assume  a / b >= - 1 ; ::_thesis: contradiction
then  (a / b) * b <= (- 1) * b by A1, Lm28;
then  a <= - b by A1, XCMPLX_1:87;
hence  contradiction by A2, Th25; ::_thesis: verum
end;

begin

theorem Th209: :: XREAL_1:209
for c, b being real number st ( for a being real number st 0 < a & a < 1 holds
c <= b / a ) holds
c <= b
proof
let c, b be real number ; ::_thesis: ( ( for a being real number st 0 < a & a < 1 holds
c <= b / a ) implies c <= b )
assume A1: for a being real number st a > 0 & a < 1 holds
b / a >= c ; ::_thesis: c <= b
now__::_thesis:_for_d_being_real_number_st_d_>_1_holds_
b_*_d_>=_c
let d be real number ; ::_thesis: ( d > 1 implies b * d >= c )
assume  d > 1 ; ::_thesis: b * d >= c
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 ; ::_thesis: verum
end;
hence  c <= b by Th167; ::_thesis: verum
end;

theorem :: XREAL_1:210
for b, c being real number st ( for a being real number st 1 < a holds
b / a <= c ) holds
b <= c
proof
let b, c be real number ; ::_thesis: ( ( for a being real number st 1 < a holds
b / a <= c ) implies b <= c )
 ( ( for a being real number st a > 1 holds
b / a <= c ) implies b <= c )
proof
assume A1: for a being real number st a > 1 holds
b / a <= c ; ::_thesis: b <= c
now__::_thesis:_for_d_being_real_number_st_0_<_d_&_d_<_1_holds_
b_<=_c_/_d
let d be real number ; ::_thesis: ( 0 < d & d < 1 implies b <= c / d )
A2: d " = 1 / d by XCMPLX_1:215;
assume that
A3: 0 < d and
A4: d < 1 ; ::_thesis: b <= c / d
 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; ::_thesis: verum
end;
hence  b <= c by Th209; ::_thesis: verum
end;
hence  ( ( for a being real number st 1 < a holds
b / a <= c ) implies b <= c ) ; ::_thesis: verum
end;

theorem :: XREAL_1:211
for a being real number st 1 <= a holds
a " <= 1
proof
let a be real number ; ::_thesis: ( 1 <= a implies a " <= 1 )
 ( 1 <= a implies a " <= 1 " ) by Lm32;
hence  ( 1 <= a implies a " <= 1 ) ; ::_thesis: verum
end;

theorem :: XREAL_1:212
for a being real number st 1 < a holds
a " < 1 by Lm36;

theorem :: XREAL_1:213
for a being real number st a <= - 1 holds
- 1 <= a "
proof
let a be real number ; ::_thesis: ( a <= - 1 implies - 1 <= a " )
 ( a <= - 1 implies (- 1) " <= a " ) by Lm33;
hence  ( a <= - 1 implies - 1 <= a " ) ; ::_thesis: verum
end;

theorem :: XREAL_1:214
for a being real number st a < - 1 holds
- 1 < a "
proof
let a be real number ; ::_thesis: ( a < - 1 implies - 1 < a " )
 ( a < - 1 implies (- 1) " < a " ) by Lm31;
hence  ( a < - 1 implies - 1 < a " ) ; ::_thesis: verum
end;

begin

theorem :: XREAL_1:215
for a being real number st 0 < a holds
0 < a / 2 ;

theorem :: XREAL_1:216
for a being real number st 0 < a holds
a / 2 < a by Lm27;

theorem :: XREAL_1:217
for a being real number st a <= 1 / 2 holds
(2 * a) - 1 <= 0
proof
let a be real number ; ::_thesis: ( a <= 1 / 2 implies (2 * a) - 1 <= 0 )
assume  a <= 1 / 2 ; ::_thesis: (2 * a) - 1 <= 0
then  2 * a <= 2 * (1 / 2) by Lm12;
then  2 * a <= 1 + 0 ;
hence  (2 * a) - 1 <= 0 by Lm18; ::_thesis: verum
end;

theorem :: XREAL_1:218
for a being real number st a <= 1 / 2 holds
0 <= 1 - (2 * a)
proof
let a be real number ; ::_thesis: ( a <= 1 / 2 implies 0 <= 1 - (2 * a) )
assume  a <= 1 / 2 ; ::_thesis: 0 <= 1 - (2 * a)
then  2 * a <= 2 * (1 / 2) by Lm12;
then  (2 * a) + 0 <= 1 ;
hence  0 <= 1 - (2 * a) by Lm16; ::_thesis: verum
end;

theorem :: XREAL_1:219
for a being real number st a >= 1 / 2 holds
(2 * a) - 1 >= 0
proof
let a be real number ; ::_thesis: ( a >= 1 / 2 implies (2 * a) - 1 >= 0 )
assume  a >= 1 / 2 ; ::_thesis: (2 * a) - 1 >= 0
then  2 * a >= 2 * (1 / 2) by Lm12;
then  2 * a >= 1 + 0 ;
hence  (2 * a) - 1 >= 0 by Lm16; ::_thesis: verum
end;

theorem :: XREAL_1:220
for a being real number st a >= 1 / 2 holds
0 >= 1 - (2 * a)
proof
let a be real number ; ::_thesis: ( a >= 1 / 2 implies 0 >= 1 - (2 * a) )
assume  a >= 1 / 2 ; ::_thesis: 0 >= 1 - (2 * a)
then  2 * a >= 2 * (1 / 2) by Lm12;
then  (2 * a) + 0 >= 1 ;
hence  0 >= 1 - (2 * a) by Lm18; ::_thesis: verum
end;

begin

theorem :: XREAL_1:221
for a being real number st 0 < a holds
a / 3 < a
proof
let a be real number ; ::_thesis: ( 0 < a implies a / 3 < a )
assume A1: 0 < a ; ::_thesis: a / 3 < 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  a / 3 < a by A2, XXREAL_0:2; ::_thesis: verum
end;

theorem :: XREAL_1:222
for a being real number st 0 < a holds
0 < a / 3 ;

begin

theorem :: XREAL_1:223
for a being real number st 0 < a holds
a / 4 < a
proof
let a be real number ; ::_thesis: ( 0 < a implies a / 4 < a )
assume A1: 0 < a ; ::_thesis: a / 4 < 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  a / 4 < a by A2, XXREAL_0:2; ::_thesis: verum
end;

theorem :: XREAL_1:224
for a being real number st 0 < a holds
0 < a / 4 ;

theorem :: XREAL_1:225
for a, b being real number st b <> 0 holds
ex c being real number st a = b / c
proof
let a, b be real number ; ::_thesis: ( b <> 0 implies ex c being real number st a = b / c )
assume A1: b <> 0 ; ::_thesis: ex c being real number st a = b / c
then consider c being complex number  such that
A2: a = b / c by XCMPLX_1:232;
percases ( c = 0 or c <> 0 ) ;
suppose c = 0 ; ::_thesis: ex c being real number st a = b / c
hence  ex c being real number st a = b / c by A2; ::_thesis: verum
end;
suppose c <> 0 ; ::_thesis: ex c being real number st a = b / c
then  c = b / a by A1, A2, XCMPLX_1:54;
then reconsider c = c as real number ;
take  c ; ::_thesis: a = b / c
thus  a = b / c by A2; ::_thesis: verum
end;
end;
end;

begin

theorem :: XREAL_1:226
for r, s being real number st r < s holds
( r < (r + s) / 2 & (r + s) / 2 < s )
proof
let r, s be real number ; ::_thesis: ( r < s implies ( r < (r + s) / 2 & (r + s) / 2 < s ) )
assume  r < s ; ::_thesis: ( r < (r + s) / 2 & (r + s) / 2 < 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 ; ::_thesis: (r + s) / 2 < s
 (r / 2) + (s / 2) < (s / 2) + (s / 2) by A1, Lm10;
hence  (r + s) / 2 < s ; ::_thesis: verum
end;

registration
cluster  ->  ext-real for Element of REAL ;
coherence
 for b1 being Element of REAL holds b1 is ext-real ;
end;


theorem Th227: :: XREAL_1:227
for r, t being ext-real number st r < t holds
ex s being ext-real number st
( r < s & s < t )
proof
let r, t be ext-real number ; ::_thesis: ( r < t implies ex s being ext-real number st
( r < s & s < t ) )
assume A1: r < t ; ::_thesis: ex s being ext-real number st
( r < s & s < t )
then A2: r <> +infty by XXREAL_0:3;
A3: t <> -infty by A1, XXREAL_0:5;
percases ( ( r = -infty & t = +infty ) or ( r = -infty & t in REAL ) or ( r in REAL & t = +infty ) or ( r in REAL & t in REAL ) ) by A2, A3, XXREAL_0:14;
supposethat A4: r = -infty and
A5: t = +infty ; ::_thesis: ex s being ext-real number st
( r < s & s < t )
take  0 ; ::_thesis: ( r < 0 & 0 < t )
thus  ( r < 0 & 0 < t ) by A4, A5; ::_thesis: verum
end;
supposethat A6: r = -infty and
A7: t in REAL ; ::_thesis: ex s being ext-real number st
( r < s & s < t )
reconsider t = t as real number by A7;
consider s being real number  such that
A8: s < t by Th2;
take  s ; ::_thesis: ( r < s & s < t )
 s in REAL by XREAL_0:def_1;
hence  r < s by A6, XXREAL_0:12; ::_thesis: s < t
thus  s < t by A8; ::_thesis: verum
end;
supposethat A9: r in REAL and
A10: t = +infty ; ::_thesis: ex s being ext-real number st
( r < s & s < t )
reconsider r9 = r as real number by A9;
consider s being real number  such that
A11: r9 < s by Th1;
take  s ; ::_thesis: ( r < s & s < t )
thus  r < s by A11; ::_thesis: s < t
 s in REAL by XREAL_0:def_1;
hence  s < t by A10, XXREAL_0:9; ::_thesis: verum
end;
supposethat A12: r in REAL and
A13: t in REAL ; ::_thesis: ex s being ext-real number st
( r < s & s < t )
reconsider r = r, t = t as real number by A12, A13;
consider s being real number  such that
A14: r < s and
A15: s < t by A1, Th5;
take  s ; ::_thesis: ( r < s & s < t )
thus  ( r < s & s < t ) by A14, A15; ::_thesis: verum
end;
end;
end;

theorem :: XREAL_1:228
for r, s, t being ext-real number st r < s & ( for q being ext-real number st r < q & q < s holds
t <= q ) holds
t <= r
proof
let r, s, t be ext-real number ; ::_thesis: ( r < s & ( for q being ext-real number st r < q & q < s holds
t <= q ) implies t <= r )
assume that
A1: r < s and
A2: for q being ext-real number st r < q & q < s holds
t <= q ; ::_thesis: t <= r
 for q being ext-real number st r < q holds
t <= q
proof
let q be ext-real number ; ::_thesis: ( r < q implies t <= q )
assume A3: r < q ; ::_thesis: t <= q
percases ( q < s or s <= q ) ;
suppose q < s ; ::_thesis: t <= q
hence  t <= q by A2, A3; ::_thesis: verum
end;
supposeA4: s <= q ; ::_thesis: t <= q
consider p being ext-real number  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  t <= q by A4, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence  t <= r by Th227; ::_thesis: verum
end;

theorem :: XREAL_1:229
for r, s, t being ext-real number st r < s & ( for q being ext-real number st r < q & q < s holds
q <= t ) holds
s <= t
proof
let r, s, t be ext-real number ; ::_thesis: ( r < s & ( for q being ext-real number st r < q & q < s holds
q <= t ) implies s <= t )
assume that
A1: r < s and
A2: for q being ext-real number st r < q & q < s holds
q <= t ; ::_thesis: s <= t
 for q being ext-real number st t < q holds
s <= q
proof
let q be ext-real number ; ::_thesis: ( t < q implies s <= q )
assume that
A3: t < q and
A4: q < s ; ::_thesis: contradiction
percases ( r < q or q <= r ) ;
suppose r < q ; ::_thesis: contradiction
hence  contradiction by A2, A3, A4; ::_thesis: verum
end;
supposeA5: q <= r ; ::_thesis: contradiction
consider p being ext-real number  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  contradiction by A3, A5, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
hence  s <= t by Th227; ::_thesis: verum
end;

theorem :: XREAL_1:230
for a, b, c being real number st 0 <= a & b <= c holds
b - a <= c
proof
let a, b, c be real number ; ::_thesis: ( 0 <= a & b <= c implies b - a <= c )
assume that
A1: 0 <= a and
A2: b <= c ; ::_thesis: b - a <= c
 b + 0 <= a + c by A1, A2, Th38;
hence  b - a <= c by Lm18; ::_thesis: verum
end;

theorem :: XREAL_1:231
for a, b, c being real number st 0 < a & b <= c holds
b - a < c
proof
let a, b, c be real number ; ::_thesis: ( 0 < a & b <= c implies b - a < c )
assume that
A1: 0 < a and
A2: b <= c ; ::_thesis: b - a < c
 b + 0 < a + c by A1, A2, Th39;
hence  b - a < c by Lm17; ::_thesis: verum
end;

begin

theorem :: XREAL_1:232
for a being real number holds a -' a = 0
proof
let a be real number ; ::_thesis: a -' a = 0
 a - a = 0 ;
hence  a -' a = 0 by XREAL_0:def_2; ::_thesis: verum
end;

theorem Th233: :: XREAL_1:233
for b, a being real number st b <= a holds
a -' b = a - b
proof
let b, a be real number ; ::_thesis: ( b <= a implies a -' b = a - b )
assume  a >= b ; ::_thesis: a -' b = a - b
then  a - b >= 0 by Th48;
hence  a -' b = a - b by XREAL_0:def_2; ::_thesis: verum
end;

theorem :: XREAL_1:234
for c, a, b being real number st c <= a & c <= b & a -' c = b -' c holds
a = b
proof
let c, a, b be real number ; ::_thesis: ( c <= a & c <= b & a -' c = b -' c implies a = b )
assume that
A1: a >= c and
A2: b >= c and
A3: a -' c = b -' c ; ::_thesis: a = b
 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  a = b ; ::_thesis: verum
end;

theorem :: XREAL_1:235
for a, b being real number st a >= b holds
(a -' b) + b = a
proof
let a, b be real number ; ::_thesis: ( a >= b implies (a -' b) + b = a )
assume  a >= b ; ::_thesis: (a -' b) + b = a
then  a - b = a -' b by Th233;
hence  (a -' b) + b = a ; ::_thesis: verum
end;

theorem :: XREAL_1:236
for a, b, c being real number st a <= b & c < a holds
b -' a < b -' c
proof
let a, b, c be real number ; ::_thesis: ( a <= b & c < a implies b -' a < b -' c )
assume that
A1: a <= b and
A2: c < a ; ::_thesis: b -' a < b -' c
A3: b - a < b - c by A2, Th15;
 b -' c = b - c by A1, A2, Th233, XXREAL_0:2;
hence  b -' a < b -' c by A1, A3, Th233; ::_thesis: verum
end;

theorem :: XREAL_1:237
for a being real number st 1 <= a holds
a -' 1 < a
proof
let a be real number ; ::_thesis: ( 1 <= a implies a -' 1 < a )
assume  1 <= a ; ::_thesis: a -' 1 < a
then  a -' 1 = a - 1 by Th233;
hence  a -' 1 < a by Th44; ::_thesis: verum
end;