:: REAL semantic presentation

begin

   Lm1:  for x, y being real number st x <= y & y <= x holds
x = y
proof
let x, y be real number ; ::_thesis: ( x <= y & y <= x implies x = y )
assume that
A1: x <= y and
A2: y <= x ; ::_thesis: x = y
A3: ( x in REAL & y in REAL ) by XREAL_0:def_1;
percases ( ( x in REAL+ & y in REAL+ ) or ( x in REAL+ & y in [:{0},REAL+:] ) or ( y in REAL+ & x in [:{0},REAL+:] ) or ( x in [:{0},REAL+:] & y in [:{0},REAL+:] ) ) by A3, NUMBERS:def_1, XBOOLE_0:def_3;
suppose ( x in REAL+ & y in REAL+ ) ; ::_thesis: x = y
then  ( ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & x9 <=' y9 ) & ex y99, x99 being Element of REAL+ st
( y = y99 & x = x99 & y99 <=' x99 ) ) by A1, A2, XXREAL_0:def_5;
hence  x = y by ARYTM_1:4; ::_thesis: verum
end;
supposeA4: ( x in REAL+ & y in [:{0},REAL+:] ) ; ::_thesis: x = y
then  ( ( not x in REAL+ or not y in REAL+ ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) ) by ARYTM_0:5, XBOOLE_0:3;
hence  x = y by A1, A4, XXREAL_0:def_5; ::_thesis: verum
end;
supposeA5: ( y in REAL+ & x in [:{0},REAL+:] ) ; ::_thesis: x = y
then  ( ( not x in REAL+ or not y in REAL+ ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) ) by ARYTM_0:5, XBOOLE_0:3;
hence  x = y by A2, A5, XXREAL_0:def_5; ::_thesis: verum
end;
supposeA6: ( x in [:{0},REAL+:] & y in [:{0},REAL+:] ) ; ::_thesis: x = y
consider x9, y9 being Element of REAL+  such that
A7: ( x = [0,x9] & y = [0,y9] ) and
A8: y9 <=' x9 by A1, A6, XXREAL_0:def_5;
consider y99, x99 being Element of REAL+  such that
A9: ( y = [0,y99] & x = [0,x99] ) and
A10: x99 <=' y99 by A2, A6, XXREAL_0:def_5;
 ( x9 = x99 & y9 = y99 ) by A7, A9, XTUPLE_0:1;
hence  x = y by A8, A9, A10, ARYTM_1:4; ::_thesis: verum
end;
end;
end;

Lm2:  for x, y, z being real number st x <= y & y <= z holds
x <= z
proof
let x, y, z be real number ; ::_thesis: ( x <= y & y <= z implies x <= z )
assume that
A1: x <= y and
A2: y <= z ; ::_thesis: x <= z
A3: ( x in REAL & y in REAL ) by XREAL_0:def_1;
A4: z in REAL by XREAL_0:def_1;
percases ( ( x in REAL+ & y in REAL+ & z in REAL+ ) or ( x in REAL+ & y in [:{0},REAL+:] ) or ( y in REAL+ & z in [:{0},REAL+:] ) or ( x in [:{0},REAL+:] & z in REAL+ ) or ( x in [:{0},REAL+:] & y in [:{0},REAL+:] & z in [:{0},REAL+:] ) ) by A3, A4, NUMBERS:def_1, XBOOLE_0:def_3;
supposethat A5: x in REAL+ and
A6: y in REAL+ and
A7: z in REAL+ ; ::_thesis: x <= z
consider y99, z9 being Element of REAL+  such that
A8: y = y99 and
A9: z = z9 and
A10: y99 <=' z9 by A2, A6, A7, XXREAL_0:def_5;
consider x9, y9 being Element of REAL+  such that
A11: x = x9 and
A12: ( y = y9 & x9 <=' y9 ) by A1, A5, A6, XXREAL_0:def_5;
 x9 <=' z9 by A12, A8, A10, ARYTM_1:3;
hence  x <= z by A11, A9, XXREAL_0:def_5; ::_thesis: verum
end;
supposeA13: ( x in REAL+ & y in [:{0},REAL+:] ) ; ::_thesis: x <= z
then  ( ( not x in REAL+ or not y in REAL+ ) & ( not x in [:{0},REAL+:] or not y in [:{0},REAL+:] ) ) by ARYTM_0:5, XBOOLE_0:3;
hence  x <= z by A1, A13, XXREAL_0:def_5; ::_thesis: verum
end;
supposeA14: ( y in REAL+ & z in [:{0},REAL+:] ) ; ::_thesis: x <= z
then  ( ( not z in REAL+ or not y in REAL+ ) & ( not z in [:{0},REAL+:] or not y in [:{0},REAL+:] ) ) by ARYTM_0:5, XBOOLE_0:3;
hence  x <= z by A2, A14, XXREAL_0:def_5; ::_thesis: verum
end;
supposethat A15: x in [:{0},REAL+:] and
A16: z in REAL+ ; ::_thesis: x <= z
 ( ( not x in REAL+ or not z in REAL+ ) & ( not x in [:{0},REAL+:] or not z in [:{0},REAL+:] ) ) by A15, A16, ARYTM_0:5, XBOOLE_0:3;
hence  x <= z by A16, XXREAL_0:def_5; ::_thesis: verum
end;
supposethat A17: x in [:{0},REAL+:] and
A18: y in [:{0},REAL+:] and
A19: z in [:{0},REAL+:] ; ::_thesis: x <= z
consider y99, z9 being Element of REAL+  such that
A20: y = [0,y99] and
A21: z = [0,z9] and
A22: z9 <=' y99 by A2, A18, A19, XXREAL_0:def_5;
consider x9, y9 being Element of REAL+  such that
A23: x = [0,x9] and
A24: y = [0,y9] and
A25: y9 <=' x9 by A1, A17, A18, XXREAL_0:def_5;
 y9 = y99 by A24, A20, XTUPLE_0:1;
then  z9 <=' x9 by A25, A22, ARYTM_1:3;
hence  x <= z by A17, A19, A23, A21, XXREAL_0:def_5; ::_thesis: verum
end;
end;
end;

theorem :: REAL:1
for x, y being real number st x <= y & x is positive holds
y is positive
proof
let x, y be real number ; ::_thesis: ( x <= y & x is positive implies y is positive )
assume that
A1: x <= y and
A2: x is positive ; ::_thesis: y is positive
 x > 0 by A2, XXREAL_0:def_6;
then  y > 0 by A1, Lm2;
hence  y is positive by XXREAL_0:def_6; ::_thesis: verum
end;

theorem :: REAL:2
for x, y being real number st x <= y & y is negative holds
x is negative
proof
let x, y be real number ; ::_thesis: ( x <= y & y is negative implies x is negative )
assume that
A1: x <= y and
A2: y is negative ; ::_thesis: x is negative
 y < 0 by A2, XXREAL_0:def_7;
then  x < 0 by A1, Lm2;
hence  x is negative by XXREAL_0:def_7; ::_thesis: verum
end;

theorem :: REAL:3
for x, y being real number st x <= y & not x is negative holds
not y is negative
proof
let x, y be real number ; ::_thesis: ( x <= y & not x is negative implies not y is negative )
assume that
A1: x <= y and
A2: not x is negative and
A3: y is negative ; ::_thesis: contradiction
 y < 0 by A3, XXREAL_0:def_7;
then  x < 0 by A1, Lm2;
hence  contradiction by A2, XXREAL_0:def_7; ::_thesis: verum
end;

theorem :: REAL:4
for x, y being real number st x <= y & not y is positive holds
not x is positive
proof
let x, y be real number ; ::_thesis: ( x <= y & not y is positive implies not x is positive )
assume that
A1: x <= y and
A2: not y is positive and
A3: x is positive ; ::_thesis: contradiction
 x > 0 by A3, XXREAL_0:def_6;
then  y > 0 by A1, Lm2;
hence  contradiction by A2, XXREAL_0:def_6; ::_thesis: verum
end;

theorem :: REAL:5
for x, y being real number st x <= y & not y is zero & not x is negative holds
y is positive
proof
let x, y be real number ; ::_thesis: ( x <= y & not y is zero & not x is negative implies y is positive )
assume that
A1: x <= y and
A2: not y is zero and
A3: not x is negative and
A4: not y is positive ; ::_thesis: contradiction
 y <= 0 by A4, XXREAL_0:def_6;
then A5: y < 0 by A2, Lm1;
 x >= 0 by A3, XXREAL_0:def_7;
hence  contradiction by A1, A5, Lm2; ::_thesis: verum
end;

theorem :: REAL:6
for x, y being real number st x <= y & not x is zero & not y is positive holds
x is negative
proof
let x, y be real number ; ::_thesis: ( x <= y & not x is zero & not y is positive implies x is negative )
assume that
A1: x <= y and
A2: not x is zero and
A3: not y is positive and
A4: not x is negative ; ::_thesis: contradiction
 x >= 0 by A4, XXREAL_0:def_7;
then A5: x > 0 by A2, Lm1;
 y <= 0 by A3, XXREAL_0:def_6;
hence  contradiction by A1, A5, Lm2; ::_thesis: verum
end;

theorem :: REAL:7
for x, y being real number st not x <= y & not x is positive holds
y is negative
proof
let x, y be real number ; ::_thesis: ( not x <= y & not x is positive implies y is negative )
assume that
A1: x > y and
A2: ( not x is positive & not y is negative ) ; ::_thesis: contradiction
 ( x <= 0 & y >= 0 ) by A2, XXREAL_0:def_6, XXREAL_0:def_7;
hence  contradiction by A1, Lm2; ::_thesis: verum
end;

theorem :: REAL:8
for x, y being real number st not x <= y & not y is negative holds
x is positive
proof
let x, y be real number ; ::_thesis: ( not x <= y & not y is negative implies x is positive )
assume that
A1: x > y and
A2: ( not y is negative & not x is positive ) ; ::_thesis: contradiction
 ( x <= 0 & y >= 0 ) by A2, XXREAL_0:def_6, XXREAL_0:def_7;
hence  contradiction by A1, Lm2; ::_thesis: verum
end;