let r, s, t be real number ; :: thesis: ( r <= s implies r + t <= s + t )
assume A1: r <= s ; :: thesis: r + t <= s + t
reconsider x1 = r, y1 = s, z1 = t as Element of REAL by Def1;
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*] and
A4: t = [*y1,y2*] and
A5: r + t = [*(+ x1,y1),(+ x2,y2)*] by XCMPLX_0:def 4;
A6: ( r = x1 & t = y1 ) by A3, A4, Lm1;
( x2 = 0 & y2 = 0 ) by A3, A4, Lm1;
then + x2,y2 = 0 by ARYTM_0:13;
hence + x',z1 = r + t by A2, A5, A6, ARYTM_0:def 7; :: thesis: verum
end;
then A7: ( + y1,z1 = s + t & + x1,z1 = r + 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 A1, XXREAL_0:def 5;
suppose that A8: r in REAL+ and
A9: s in REAL+ and
A10: t in REAL+ ; :: thesis: r + t <= s + t
consider x'', s'' being Element of REAL+ such that
A11: r = x'' and
A12: s = s'' and
A13: x'' <=' s'' by A1, A8, A9, XXREAL_0:def 5;
consider x', t' being Element of REAL+ such that
A14: r = x' and
A15: t = t' and
A16: + x1,z1 = x' + t' by A8, A10, ARYTM_0:def 2;
consider s', t'' being Element of REAL+ such that
A17: s = s' and
A18: t = t'' and
A19: + y1,z1 = s' + t'' by A9, A10, ARYTM_0:def 2;
x' + t' <=' s' + t'' by A11, A12, A13, A14, A15, A17, A18, ARYTM_1:7;
hence r + t <= s + t by A7, A16, A19, Lm2; :: thesis: verum
end;
suppose that A20: r in [:{0 },REAL+ :] and
A21: s in REAL+ and
A22: t in REAL+ ; :: thesis: r + t <= s + t
consider x', t' being Element of REAL+ such that
r = [0 ,x'] and
A23: t = t' and
A24: + x1,z1 = t' - x' by A20, A22, ARYTM_0:def 2;
consider s', t'' being Element of REAL+ such that
s = s' and
A25: t = t'' and
A26: + y1,z1 = s' + t'' by A21, A22, ARYTM_0:def 2;
hence r + t <= s + t ; :: thesis: verum
end;
suppose that A29: r in [:{0 },REAL+ :] and
A30: s in [:{0 },REAL+ :] and
A31: t in REAL+ ; :: thesis: r + t <= s + t
consider x'', s'' being Element of REAL+ such that
A32: r = [0 ,x''] and
A33: s = [0 ,s''] and
A34: s'' <=' x'' by A1, A29, A30, 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 A29, A31, ARYTM_0:def 2;
consider s', t'' being Element of REAL+ such that
A38: s = [0 ,s'] and
A39: t = t'' and
A40: + y1,z1 = t'' - s' by A30, A31, ARYTM_0:def 2;
A41: x' = x'' by A32, A35, ZFMISC_1:33;
A42: s' = s'' by A33, A38, ZFMISC_1:33;
now
per cases ( x' <=' t' or not x' <=' t' ) ;
suppose A43: x' <=' t' ; :: thesis: r + t <= s + t
then A44: t' - x' = t' -' x' by ARYTM_1:def 2;
s' <=' t' by A34, A41, A42, A43, ARYTM_1:3;
then A45: t' - s' = t' -' s' by ARYTM_1:def 2;
t' -' x' <=' t'' -' s' by A34, A36, A39, A41, A42, ARYTM_1:16;
hence r + t <= s + t by A7, A36, A37, A39, A40, A44, A45, Lm2; :: thesis: verum
end;
suppose not x' <=' t' ; :: thesis: r + t <= s + t
then A46: + x1,z1 = [0 ,(x' -' t')] by A37, ARYTM_1:def 2;
then A47: + 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 ( not + x1,z1 in REAL+ & not + y1,z1 in [:{0 },REAL+ :] ) by A36, A39, A40, A47, ARYTM_0:5, XBOOLE_0:3;
hence r + t <= s + t by A7, XXREAL_0:def 5; :: thesis: verum
end;
suppose not s' <=' t' ; :: thesis: r + t <= s + t
then A48: + y1,z1 = [0 ,(s' -' t')] by A36, A39, A40, ARYTM_1:def 2;
then A49: + y1,z1 in [:{0 },REAL+ :] by Lm3, ZFMISC_1:106;
s' -' t' <=' x' -' t' by A34, A41, A42, ARYTM_1:17;
hence r + t <= s + t by A7, A46, A47, A48, A49, 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 A50: r in REAL+ and
A51: s in REAL+ and
A52: t in [:{0 },REAL+ :] ; :: thesis: r + t <= s + t
consider x'', s'' being Element of REAL+ such that
A53: r = x'' and
A54: s = s'' and
A55: x'' <=' s'' by A1, A50, A51, XXREAL_0:def 5;
consider x', t' being Element of REAL+ such that
A56: r = x' and
A57: t = [0 ,t'] and
A58: + x1,z1 = x' - t' by A50, A52, ARYTM_0:def 2;
consider s', t'' being Element of REAL+ such that
A59: s = s' and
A60: t = [0 ,t''] and
A61: + y1,z1 = s' - t'' by A51, A52, ARYTM_0:def 2;
A62: t' = t'' by A57, A60, ZFMISC_1:33;
now
per cases ( t' <=' x' or not t' <=' x' ) ;
suppose A63: t' <=' x' ; :: thesis: r + t <= s + t
then A64: x' - t' = x' -' t' by ARYTM_1:def 2;
t' <=' s' by A53, A54, A55, A56, A59, A63, ARYTM_1:3;
then A65: s' - t' = s' -' t' by ARYTM_1:def 2;
x' -' t' <=' s' -' t'' by A53, A54, A55, A56, A59, A62, ARYTM_1:17;
hence r + t <= s + t by A7, A58, A61, A62, A64, A65, Lm2; :: thesis: verum
end;
suppose not t' <=' x' ; :: thesis: r + t <= s + t
then A66: + x1,z1 = [0 ,(t' -' x')] by A58, ARYTM_1:def 2;
then A67: + 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 ( not + x1,z1 in REAL+ & not + y1,z1 in [:{0 },REAL+ :] ) by A61, A62, A67, ARYTM_0:5, XBOOLE_0:3;
hence r + t <= s + t by A7, XXREAL_0:def 5; :: thesis: verum
end;
suppose not t' <=' s' ; :: thesis: r + t <= s + t
then A68: + y1,z1 = [0 ,(t' -' s')] by A61, A62, ARYTM_1:def 2;
then A69: + y1,z1 in [:{0 },REAL+ :] by Lm3, ZFMISC_1:106;
t' -' s' <=' t' -' x' by A53, A54, A55, A56, A59, ARYTM_1:16;
hence r + t <= s + t by A7, A66, A67, A68, A69, 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 A70: r in [:{0 },REAL+ :] and
A71: s in REAL+ and
A72: t in [:{0 },REAL+ :] ; :: thesis: r + t <= s + t
( not r in REAL+ & not t in REAL+ ) by A70, A72, ARYTM_0:5, XBOOLE_0:3;
then consider x', t' being Element of REAL+ such that
r = [0 ,x'] and
A73: t = [0 ,t'] and
A74: + x1,z1 = [0 ,(x' + t')] by ARYTM_0:def 2;
consider s', t'' being Element of REAL+ such that
s = s' and
A75: t = [0 ,t''] and
A76: + y1,z1 = s' - t'' by A71, A72, ARYTM_0:def 2;
A77: t' = t'' by A73, A75, ZFMISC_1:33;
A78: + x1,z1 in [:{0 },REAL+ :] by A74, 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 A77, ARYTM_1:def 2;
then ( not + x1,z1 in REAL+ & not + y1,z1 in [:{0 },REAL+ :] ) by A76, A78, ARYTM_0:5, XBOOLE_0:3;
hence r + t <= s + t by A7, XXREAL_0:def 5; :: 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
consider x'', s'' being Element of REAL+ such that
A85: r = [0 ,x''] and
A86: s = [0 ,s''] and
A87: s'' <=' x'' by A1, A82, A83, XXREAL_0:def 5;
( 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
A88: r = [0 ,x'] and
A89: t = [0 ,t'] and
A90: + x1,z1 = [0 ,(x' + t')] by ARYTM_0:def 2;
( 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
A91: s = [0 ,s'] and
A92: t = [0 ,t''] and
A93: + y1,z1 = [0 ,(s' + t'')] by ARYTM_0:def 2;
A94: x' = x'' by A85, A88, ZFMISC_1:33;
A95: s' = s'' by A86, A91, ZFMISC_1:33;
A96: t' = t'' by A89, A92, ZFMISC_1:33;
then A97: s' + t' <=' x' + t'' by A87, A94, A95, ARYTM_1:7;
A98: + x1,z1 in [:{0 },REAL+ :] by A90, Lm3, ZFMISC_1:106;
+ y1,z1 in [:{0 },REAL+ :] by A93, Lm3, ZFMISC_1:106;
hence r + t <= s + t by A7, A90, A93, A96, A97, A98, Lm2; :: thesis: verum
end;
end;