let r, s, t be real number ; :: thesis: ( r <= s implies r + t <= s + t )
reconsider x1 = r, y1 = s, z1 = t as Element of REAL by Def1;
A1: for x' being Element of REAL
for r being real number st x' = r holds
+ x',z1 = r + t

proof

let x' be Element of REAL ; :: thesis: for r being real number st x' = r holds
+ x',z1 = r + t
let r be real number ; :: thesis: ( x' = r implies + x',z1 = r + t )
assume A2: x' = r ; :: thesis: + x',z1 = r + t
consider x1, x2, y1, y2 being Element of REAL such that
A3: ( r = [*x1,x2*] & t = [*y1,y2*] ) and
A4: r + t = [*(+ x1,y1),(+ x2,y2)*] by XCMPLX_0:def 4;
( x2 = 0 & y2 = 0 ) by A3, Lm1;
then A5: + x2,y2 = 0 by ARYTM_0:13;
( r = x1 & t = y1 ) by A3, Lm1;
hence + x',z1 = r + t by A2, A4, A5, ARYTM_0:def 7; :: thesis: verum

end;

then A6: + y1,z1 = s + t ;
A7: + x1,z1 = r + t by A1;
assume A8: r <= s ; :: thesis: r + t <= s + t

per cases ( ( r in REAL+ & s in REAL+ & t in REAL+ ) or ( r in [:{0 },REAL+ :] & s in REAL+ & t in REAL+ ) or ( r in [:{0 },REAL+ :] & s in [:{0 },REAL+ :] & t in REAL+ ) or ( r in REAL+ & s in REAL+ & t in [:{0 },REAL+ :] ) or ( r in [:{0 },REAL+ :] & s in REAL+ & t in [:{0 },REAL+ :] ) or ( r in [:{0 },REAL+ :] & s in [:{0 },REAL+ :] & t in [:{0 },REAL+ :] ) ) by A8, XXREAL_0:def 5;

suppose that A9: r in REAL+ and
A10: s in REAL+ and
A11: t in REAL+ ; :: thesis: r + t <= s + t

consider s', t'' being Element of REAL+ such that
A12: ( s = s' & t = t'' ) and
A13: + y1,z1 = s' + t'' by A10, A11, ARYTM_0:def 2;
consider x', t' being Element of REAL+ such that
A14: ( r = x' & t = t' ) and
A15: + x1,z1 = x' + t' by A9, A11, ARYTM_0:def 2;
ex x'', s'' being Element of REAL+ st
( r = x'' & s = s'' & x'' <=' s'' ) by A8, A9, A10, XXREAL_0:def 5;
then x' + t' <=' s' + t'' by A14, A12, ARYTM_1:7;
hence r + t <= s + t by A6, A7, A15, A13, Lm2; :: thesis: verum

end;

suppose that A16: r in [:{0 },REAL+ :] and
A17: s in REAL+ and
A18: t in REAL+ ; :: thesis: r + t <= s + t

consider s', t'' being Element of REAL+ such that
s = s' and
A19: t = t'' and
A20: + y1,z1 = s' + t'' by A17, A18, ARYTM_0:def 2;
consider x', t' being Element of REAL+ such that
r = [0 ,x'] and
A21: t = t' and
A22: + x1,z1 = t' - x' by A16, A18, ARYTM_0:def 2;

now

per cases ( x' <=' t' or not x' <=' t' ) ;

suppose A23: x' <=' t' ; :: thesis: r + t <= s + t

( t' -' x' <=' t' & t' <=' s' + t'' ) by A21, A19, ARYTM_1:11, ARYTM_2:20;
then A24: t' -' x' <=' s' + t'' by ARYTM_1:3;
t' - x' = t' -' x' by A23, ARYTM_1:def 2;
hence r + t <= s + t by A6, A7, A22, A20, A24, Lm2; :: thesis: verum

end;

suppose not x' <=' t' ; :: thesis: r + t <= s + t

then t' - x' = [0 ,(x' -' t')] by ARYTM_1:def 2;
then t' - x' in [:{0 },REAL+ :] by Lm3, ZFMISC_1:106;
then A25: not r + t in REAL+ by A7, A22, ARYTM_0:5, XBOOLE_0:3;
not s + t in [:{0 },REAL+ :] by A6, A20, ARYTM_0:5, XBOOLE_0:3;
hence r + t <= s + t by A25, XXREAL_0:def 5; :: thesis: verum

end;

end;

end;

hence r + t <= s + t ; :: thesis: verum

end;

suppose that A26: r in [:{0 },REAL+ :] and
A27: s in [:{0 },REAL+ :] and
A28: t in REAL+ ; :: thesis: r + t <= s + t

consider s', t'' being Element of REAL+ such that
A29: s = [0 ,s'] and
A30: t = t'' and
A31: + y1,z1 = t'' - s' by A27, A28, ARYTM_0:def 2;
consider x'', s'' being Element of REAL+ such that
A32: r = [0 ,x''] and
A33: s = [0 ,s''] and
A34: s'' <=' x'' by A8, A26, A27, XXREAL_0:def 5;
consider x', t' being Element of REAL+ such that
A35: r = [0 ,x'] and
A36: t = t' and
A37: + x1,z1 = t' - x' by A26, A28, ARYTM_0:def 2;
A38: x' = x'' by A32, A35, ZFMISC_1:33;
A39: s' = s'' by A33, A29, ZFMISC_1:33;

now

per cases ( x' <=' t' or not x' <=' t' ) ;

suppose A40: x' <=' t' ; :: thesis: r + t <= s + t

then s' <=' t' by A34, A38, A39, ARYTM_1:3;
then A41: t' - s' = t' -' s' by ARYTM_1:def 2;
A42: t' - x' = t' -' x' by A40, ARYTM_1:def 2;
t' -' x' <=' t'' -' s' by A34, A36, A30, A38, A39, ARYTM_1:16;
hence r + t <= s + t by A6, A7, A36, A37, A30, A31, A42, A41, Lm2; :: thesis: verum

end;

suppose not x' <=' t' ; :: thesis: r + t <= s + t

then A43: + x1,z1 = [0 ,(x' -' t')] by A37, ARYTM_1:def 2;
then A44: + x1,z1 in [:{0 },REAL+ :] by Lm3, ZFMISC_1:106;

now

per cases ( s' <=' t' or not s' <=' t' ) ;

suppose s' <=' t' ; :: thesis: r + t <= s + t

then t' - s' = t' -' s' by ARYTM_1:def 2;
then A45: not + y1,z1 in [:{0 },REAL+ :] by A36, A30, A31, ARYTM_0:5, XBOOLE_0:3;
not + x1,z1 in REAL+ by A44, ARYTM_0:5, XBOOLE_0:3;
hence r + t <= s + t by A6, A7, A45, XXREAL_0:def 5; :: thesis: verum

end;

suppose A46: not s' <=' t' ; :: thesis: r + t <= s + t

A47: s' -' t' <=' x' -' t' by A34, A38, A39, ARYTM_1:17;
A48: + y1,z1 = [0 ,(s' -' t')] by A36, A30, A31, A46, ARYTM_1:def 2;
then + y1,z1 in [:{0 },REAL+ :] by Lm3, ZFMISC_1:106;
hence r + t <= s + t by A6, A7, A43, A44, A48, A47, Lm2; :: thesis: verum

end;

end;

end;

hence r + t <= s + t ; :: thesis: verum

end;

end;

end;

hence r + t <= s + t ; :: thesis: verum

end;

suppose that A49: r in REAL+ and
A50: s in REAL+ and
A51: t in [:{0 },REAL+ :] ; :: thesis: r + t <= s + t

consider s', t'' being Element of REAL+ such that
A52: s = s' and
A53: t = [0 ,t''] and
A54: + y1,z1 = s' - t'' by A50, A51, ARYTM_0:def 2;
consider x', t' being Element of REAL+ such that
A55: r = x' and
A56: t = [0 ,t'] and
A57: + x1,z1 = x' - t' by A49, A51, ARYTM_0:def 2;
A58: t' = t'' by A56, A53, ZFMISC_1:33;
A59: ex x'', s'' being Element of REAL+ st
( r = x'' & s = s'' & x'' <=' s'' ) by A8, A49, A50, XXREAL_0:def 5;

now

per cases ( t' <=' x' or not t' <=' x' ) ;

suppose A60: t' <=' x' ; :: thesis: r + t <= s + t

then t' <=' s' by A59, A55, A52, ARYTM_1:3;
then A61: s' - t' = s' -' t' by ARYTM_1:def 2;
A62: x' - t' = x' -' t' by A60, ARYTM_1:def 2;
x' -' t' <=' s' -' t'' by A59, A55, A52, A58, ARYTM_1:17;
hence r + t <= s + t by A6, A7, A57, A54, A58, A62, A61, Lm2; :: thesis: verum

end;

suppose not t' <=' x' ; :: thesis: r + t <= s + t

then A63: + x1,z1 = [0 ,(t' -' x')] by A57, ARYTM_1:def 2;
then A64: + x1,z1 in [:{0 },REAL+ :] by Lm3, ZFMISC_1:106;

now

per cases ( t' <=' s' or not t' <=' s' ) ;

suppose t' <=' s' ; :: thesis: r + t <= s + t

then s' - t' = s' -' t' by ARYTM_1:def 2;
then A65: not + y1,z1 in [:{0 },REAL+ :] by A54, A58, ARYTM_0:5, XBOOLE_0:3;
not + x1,z1 in REAL+ by A64, ARYTM_0:5, XBOOLE_0:3;
hence r + t <= s + t by A6, A7, A65, XXREAL_0:def 5; :: thesis: verum

end;

suppose A66: not t' <=' s' ; :: thesis: r + t <= s + t

A67: t' -' s' <=' t' -' x' by A59, A55, A52, ARYTM_1:16;
A68: + y1,z1 = [0 ,(t' -' s')] by A54, A58, A66, ARYTM_1:def 2;
then + y1,z1 in [:{0 },REAL+ :] by Lm3, ZFMISC_1:106;
hence r + t <= s + t by A6, A7, A63, A64, A68, A67, Lm2; :: thesis: verum

end;

end;

end;

hence r + t <= s + t ; :: thesis: verum

end;

end;

end;

hence r + t <= s + t ; :: thesis: verum

end;

suppose that A69: r in [:{0 },REAL+ :] and
A70: s in REAL+ and
A71: t in [:{0 },REAL+ :] ; :: thesis: r + t <= s + t

( not r in REAL+ & not t in REAL+ ) by A69, A71, ARYTM_0:5, XBOOLE_0:3;
then consider x', t' being Element of REAL+ such that
r = [0 ,x'] and
A72: t = [0 ,t'] and
A73: + x1,z1 = [0 ,(x' + t')] by ARYTM_0:def 2;
A74: + x1,z1 in [:{0 },REAL+ :] by A73, Lm3, ZFMISC_1:106;
consider s', t'' being Element of REAL+ such that
s = s' and
A75: t = [0 ,t''] and
A76: + y1,z1 = s' - t'' by A70, A71, ARYTM_0:def 2;
A77: t' = t'' by A72, A75, ZFMISC_1:33;

now

per cases ( t' <=' s' or not t' <=' s' ) ;

suppose t' <=' s' ; :: thesis: r + t <= s + t

then s' - t'' = s' -' t'' by A77, ARYTM_1:def 2;
then A78: not + y1,z1 in [:{0 },REAL+ :] by A76, ARYTM_0:5, XBOOLE_0:3;
not + x1,z1 in REAL+ by A74, ARYTM_0:5, XBOOLE_0:3;
hence r + t <= s + t by A6, A7, A78, XXREAL_0:def 5; :: thesis: verum

end;

suppose A79: not t' <=' s' ; :: thesis: r + t <= s + t

( t' -' s' <=' t' & t' <=' t' + x' ) by ARYTM_1:11, ARYTM_2:20;
then A80: t' -' s' <=' t' + x' by ARYTM_1:3;
A81: + y1,z1 = [0 ,(t' -' s')] by A76, A77, A79, ARYTM_1:def 2;
then + y1,z1 in [:{0 },REAL+ :] by Lm3, ZFMISC_1:106;
hence r + t <= s + t by A6, A7, A73, A74, A81, A80, Lm2; :: thesis: verum

end;

end;

end;

hence r + t <= s + t ; :: thesis: verum

end;

suppose that A82: r in [:{0 },REAL+ :] and
A83: s in [:{0 },REAL+ :] and
A84: t in [:{0 },REAL+ :] ; :: thesis: r + t <= s + t

( not s in REAL+ & not t in REAL+ ) by A83, A84, ARYTM_0:5, XBOOLE_0:3;
then consider s', t'' being Element of REAL+ such that
A85: s = [0 ,s'] and
A86: t = [0 ,t''] and
A87: + y1,z1 = [0 ,(s' + t'')] by ARYTM_0:def 2;
A88: + y1,z1 in [:{0 },REAL+ :] by A87, Lm3, ZFMISC_1:106;
( not r in REAL+ & not t in REAL+ ) by A82, A84, ARYTM_0:5, XBOOLE_0:3;
then consider x', t' being Element of REAL+ such that
A89: r = [0 ,x'] and
A90: t = [0 ,t'] and
A91: + x1,z1 = [0 ,(x' + t')] by ARYTM_0:def 2;
A92: + x1,z1 in [:{0 },REAL+ :] by A91, Lm3, ZFMISC_1:106;
A93: t' = t'' by A90, A86, ZFMISC_1:33;
consider x'', s'' being Element of REAL+ such that
A94: r = [0 ,x''] and
A95: s = [0 ,s''] and
A96: s'' <=' x'' by A8, A82, A83, XXREAL_0:def 5;
A97: s' = s'' by A95, A85, ZFMISC_1:33;
x' = x'' by A94, A89, ZFMISC_1:33;
then s' + t' <=' x' + t'' by A96, A97, A93, ARYTM_1:7;
hence r + t <= s + t by A6, A7, A91, A87, A93, A92, A88, Lm2; :: thesis: verum

end;

end;