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

let r be Real; :: thesis: ( x9 = r implies + (x9,z1) = r + t )
assume A2: x9 = r ; :: thesis: + (x9,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 ;
then A5: + (x2,y2) = 0 by ARYTM_0:11;
( r = x1 & t = y1 ) by ;
hence + (x9,z1) = r + t by ; :: 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 & s in REAL+ & t in REAL+ ) or ( r in & s in & t in REAL+ ) or ( r in REAL+ & s in REAL+ & t in ) or ( r in & s in REAL+ & t in ) or ( r in & s in & t in ) ) by ;
suppose that A9: r in REAL+ and
A10: s in REAL+ and
A11: t in REAL+ ; :: thesis: r + t <= s + t
consider s9, t99 being Element of REAL+ such that
A12: ( s = s9 & t = t99 ) and
A13: + (y1,z1) = s9 + t99 by ;
consider x9, t9 being Element of REAL+ such that
A14: ( r = x9 & t = t9 ) and
A15: + (x1,z1) = x9 + t9 by ;
ex x99, s99 being Element of REAL+ st
( r = x99 & s = s99 & x99 <=' s99 ) by ;
then x9 + t9 <=' s9 + t99 by ;
hence r + t <= s + t by A6, A7, A15, A13, Lm2; :: thesis: verum
end;
suppose that A16: r in and
A17: s in REAL+ and
A18: t in REAL+ ; :: thesis: r + t <= s + t
consider s9, t99 being Element of REAL+ such that
s = s9 and
A19: t = t99 and
A20: + (y1,z1) = s9 + t99 by ;
consider x9, t9 being Element of REAL+ such that
r = [0,x9] and
A21: t = t9 and
A22: + (x1,z1) = t9 - x9 by ;
now :: thesis: r + t <= s + t
per cases ( x9 <=' t9 or not x9 <=' t9 ) ;
suppose A23: x9 <=' t9 ; :: thesis: r + t <= s + t
( t9 -' x9 <=' t9 & t9 <=' s9 + t99 ) by ;
then A24: t9 -' x9 <=' s9 + t99 by ARYTM_1:3;
t9 - x9 = t9 -' x9 by ;
hence r + t <= s + t by A6, A7, A22, A20, A24, Lm2; :: thesis: verum
end;
suppose not x9 <=' t9 ; :: thesis: r + t <= s + t
then t9 - x9 = [0,(x9 -' t9)] by ARYTM_1:def 2;
then t9 - x9 in by ;
then A25: not r + t in REAL+ by ;
not s + t in by ;
hence r + t <= s + t by ; :: thesis: verum
end;
end;
end;
hence r + t <= s + t ; :: thesis: verum
end;
suppose that A26: r in and
A27: s in and
A28: t in REAL+ ; :: thesis: r + t <= s + t
consider s9, t99 being Element of REAL+ such that
A29: s = [0,s9] and
A30: t = t99 and
A31: + (y1,z1) = t99 - s9 by ;
consider x99, s99 being Element of REAL+ such that
A32: r = [0,x99] and
A33: s = [0,s99] and
A34: s99 <=' x99 by ;
consider x9, t9 being Element of REAL+ such that
A35: r = [0,x9] and
A36: t = t9 and
A37: + (x1,z1) = t9 - x9 by ;
A38: x9 = x99 by ;
A39: s9 = s99 by ;
now :: thesis: r + t <= s + t
per cases ( x9 <=' t9 or not x9 <=' t9 ) ;
suppose A40: x9 <=' t9 ; :: thesis: r + t <= s + t
then s9 <=' t9 by ;
then A41: t9 - s9 = t9 -' s9 by ARYTM_1:def 2;
A42: t9 - x9 = t9 -' x9 by ;
t9 -' x9 <=' t99 -' s9 by ;
hence r + t <= s + t by A6, A7, A36, A37, A30, A31, A42, A41, Lm2; :: thesis: verum
end;
suppose not x9 <=' t9 ; :: thesis: r + t <= s + t
then A43: + (x1,z1) = [0,(x9 -' t9)] by ;
then A44: + (x1,z1) in by ;
now :: thesis: r + t <= s + t
per cases ( s9 <=' t9 or not s9 <=' t9 ) ;
suppose s9 <=' t9 ; :: thesis: r + t <= s + t
then t9 - s9 = t9 -' s9 by ARYTM_1:def 2;
then A45: not + (y1,z1) in by ;
not + (x1,z1) in REAL+ by ;
hence r + t <= s + t by ; :: thesis: verum
end;
suppose A46: not s9 <=' t9 ; :: thesis: r + t <= s + t
A47: s9 -' t9 <=' x9 -' t9 by ;
A48: + (y1,z1) = [0,(s9 -' t9)] by ;
then + (y1,z1) in by ;
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 ; :: thesis: r + t <= s + t
consider s9, t99 being Element of REAL+ such that
A52: s = s9 and
A53: t = [0,t99] and
A54: + (y1,z1) = s9 - t99 by ;
consider x9, t9 being Element of REAL+ such that
A55: r = x9 and
A56: t = [0,t9] and
A57: + (x1,z1) = x9 - t9 by ;
A58: t9 = t99 by ;
A59: ex x99, s99 being Element of REAL+ st
( r = x99 & s = s99 & x99 <=' s99 ) by ;
now :: thesis: r + t <= s + t
per cases ( t9 <=' x9 or not t9 <=' x9 ) ;
suppose A60: t9 <=' x9 ; :: thesis: r + t <= s + t
then t9 <=' s9 by ;
then A61: s9 - t9 = s9 -' t9 by ARYTM_1:def 2;
A62: x9 - t9 = x9 -' t9 by ;
x9 -' t9 <=' s9 -' t99 by ;
hence r + t <= s + t by A6, A7, A57, A54, A58, A62, A61, Lm2; :: thesis: verum
end;
suppose not t9 <=' x9 ; :: thesis: r + t <= s + t
then A63: + (x1,z1) = [0,(t9 -' x9)] by ;
then A64: + (x1,z1) in by ;
now :: thesis: r + t <= s + t
per cases ( t9 <=' s9 or not t9 <=' s9 ) ;
suppose t9 <=' s9 ; :: thesis: r + t <= s + t
then s9 - t9 = s9 -' t9 by ARYTM_1:def 2;
then A65: not + (y1,z1) in by ;
not + (x1,z1) in REAL+ by ;
hence r + t <= s + t by ; :: thesis: verum
end;
suppose A66: not t9 <=' s9 ; :: thesis: r + t <= s + t
A67: t9 -' s9 <=' t9 -' x9 by ;
A68: + (y1,z1) = [0,(t9 -' s9)] by ;
then + (y1,z1) in by ;
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 and
A70: s in REAL+ and
A71: t in ; :: thesis: r + t <= s + t
( not r in REAL+ & not t in REAL+ ) by ;
then consider x9, t9 being Element of REAL+ such that
r = [0,x9] and
A72: t = [0,t9] and
A73: + (x1,z1) = [0,(x9 + t9)] by ARYTM_0:def 1;
A74: + (x1,z1) in by ;
consider s9, t99 being Element of REAL+ such that
s = s9 and
A75: t = [0,t99] and
A76: + (y1,z1) = s9 - t99 by ;
A77: t9 = t99 by ;
now :: thesis: r + t <= s + t
per cases ( t9 <=' s9 or not t9 <=' s9 ) ;
suppose t9 <=' s9 ; :: thesis: r + t <= s + t
then s9 - t99 = s9 -' t99 by ;
then A78: not + (y1,z1) in by ;
not + (x1,z1) in REAL+ by ;
hence r + t <= s + t by ; :: thesis: verum
end;
suppose A79: not t9 <=' s9 ; :: thesis: r + t <= s + t
( t9 -' s9 <=' t9 & t9 <=' t9 + x9 ) by ;
then A80: t9 -' s9 <=' t9 + x9 by ARYTM_1:3;
A81: + (y1,z1) = [0,(t9 -' s9)] by ;
then + (y1,z1) in by ;
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 and
A83: s in and
A84: t in ; :: thesis: r + t <= s + t
( not s in REAL+ & not t in REAL+ ) by ;
then consider s9, t99 being Element of REAL+ such that
A85: s = [0,s9] and
A86: t = [0,t99] and
A87: + (y1,z1) = [0,(s9 + t99)] by ARYTM_0:def 1;
A88: + (y1,z1) in by ;
( not r in REAL+ & not t in REAL+ ) by ;
then consider x9, t9 being Element of REAL+ such that
A89: r = [0,x9] and
A90: t = [0,t9] and
A91: + (x1,z1) = [0,(x9 + t9)] by ARYTM_0:def 1;
A92: + (x1,z1) in by ;
A93: t9 = t99 by ;
consider x99, s99 being Element of REAL+ such that
A94: r = [0,x99] and
A95: s = [0,s99] and
A96: s99 <=' x99 by ;
A97: s9 = s99 by ;
x9 = x99 by ;
then s9 + t9 <=' x9 + t99 by ;
hence r + t <= s + t by A6, A7, A91, A87, A93, A92, A88, Lm2; :: thesis: verum
end;
end;