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

A7: + (x1,z1) = r + t by A1;

assume A8: r <= s ; :: thesis: 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

then A6:
+ (y1,z1) = s + t
;
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 A3, Lm1;

then A5: + (x2,y2) = 0 by ARYTM_0:11;

( r = x1 & t = y1 ) by A3, Lm1;

hence + (x9,z1) = r + t by A2, A4, A5, ARYTM_0:def 5; :: thesis: verum

end;+ (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 A3, Lm1;

then A5: + (x2,y2) = 0 by ARYTM_0:11;

( r = x1 & t = y1 ) by A3, Lm1;

hence + (x9,z1) = r + t by A2, A4, A5, ARYTM_0:def 5; :: thesis: verum

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;

end;

suppose that A9:
r in REAL+
and

A10: s in REAL+ and

A11: t in REAL+ ; :: thesis: r + t <= s + t

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 A10, A11, ARYTM_0:def 1;

consider x9, t9 being Element of REAL+ such that

A14: ( r = x9 & t = t9 ) and

A15: + (x1,z1) = x9 + t9 by A9, A11, ARYTM_0:def 1;

ex x99, s99 being Element of REAL+ st

( r = x99 & s = s99 & x99 <=' s99 ) by A8, A9, A10, XXREAL_0:def 5;

then x9 + t9 <=' s9 + t99 by A14, A12, ARYTM_1:7;

hence r + t <= s + t by A6, A7, A15, A13, Lm2; :: thesis: verum

end;A12: ( s = s9 & t = t99 ) and

A13: + (y1,z1) = s9 + t99 by A10, A11, ARYTM_0:def 1;

consider x9, t9 being Element of REAL+ such that

A14: ( r = x9 & t = t9 ) and

A15: + (x1,z1) = x9 + t9 by A9, A11, ARYTM_0:def 1;

ex x99, s99 being Element of REAL+ st

( r = x99 & s = s99 & x99 <=' s99 ) by A8, A9, A10, XXREAL_0:def 5;

then x9 + t9 <=' s9 + t99 by A14, A12, ARYTM_1:7;

hence r + t <= s + t by A6, A7, A15, A13, Lm2; :: thesis: verum

suppose that A16:
r in [:{0},REAL+:]
and

A17: s in REAL+ and

A18: t in REAL+ ; :: thesis: r + t <= s + t

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 A17, A18, ARYTM_0:def 1;

consider x9, t9 being Element of REAL+ such that

r = [0,x9] and

A21: t = t9 and

A22: + (x1,z1) = t9 - x9 by A16, A18, ARYTM_0:def 1;

end;s = s9 and

A19: t = t99 and

A20: + (y1,z1) = s9 + t99 by A17, A18, ARYTM_0:def 1;

consider x9, t9 being Element of REAL+ such that

r = [0,x9] and

A21: t = t9 and

A22: + (x1,z1) = t9 - x9 by A16, A18, ARYTM_0:def 1;

now :: thesis: r + t <= s + tend;

hence
r + t <= s + t
; :: thesis: verumper cases
( x9 <=' t9 or not x9 <=' t9 )
;

end;

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

( t9 -' x9 <=' t9 & t9 <=' s9 + t99 )
by A21, A19, ARYTM_1:11, ARYTM_2:19;

then A24: t9 -' x9 <=' s9 + t99 by ARYTM_1:3;

t9 - x9 = t9 -' x9 by A23, ARYTM_1:def 2;

hence r + t <= s + t by A6, A7, A22, A20, A24, Lm2; :: thesis: verum

end;then A24: t9 -' x9 <=' s9 + t99 by ARYTM_1:3;

t9 - x9 = t9 -' x9 by A23, ARYTM_1:def 2;

hence r + t <= s + t by A6, A7, A22, A20, A24, Lm2; :: thesis: verum

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

then
t9 - x9 = [0,(x9 -' t9)]
by ARYTM_1:def 2;

then t9 - x9 in [:{0},REAL+:] by Lm3, ZFMISC_1:87;

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;then t9 - x9 in [:{0},REAL+:] by Lm3, ZFMISC_1:87;

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

suppose that A26:
r in [:{0},REAL+:]
and

A27: s in [:{0},REAL+:] and

A28: t in REAL+ ; :: thesis: r + t <= s + t

A27: s in [:{0},REAL+:] 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 A27, A28, ARYTM_0:def 1;

consider x99, s99 being Element of REAL+ such that

A32: r = [0,x99] and

A33: s = [0,s99] and

A34: s99 <=' x99 by A8, A26, A27, XXREAL_0:def 5;

consider x9, t9 being Element of REAL+ such that

A35: r = [0,x9] and

A36: t = t9 and

A37: + (x1,z1) = t9 - x9 by A26, A28, ARYTM_0:def 1;

A38: x9 = x99 by A32, A35, XTUPLE_0:1;

A39: s9 = s99 by A33, A29, XTUPLE_0:1;

end;A29: s = [0,s9] and

A30: t = t99 and

A31: + (y1,z1) = t99 - s9 by A27, A28, ARYTM_0:def 1;

consider x99, s99 being Element of REAL+ such that

A32: r = [0,x99] and

A33: s = [0,s99] and

A34: s99 <=' x99 by A8, A26, A27, XXREAL_0:def 5;

consider x9, t9 being Element of REAL+ such that

A35: r = [0,x9] and

A36: t = t9 and

A37: + (x1,z1) = t9 - x9 by A26, A28, ARYTM_0:def 1;

A38: x9 = x99 by A32, A35, XTUPLE_0:1;

A39: s9 = s99 by A33, A29, XTUPLE_0:1;

now :: thesis: r + t <= s + tend;

hence
r + t <= s + t
; :: thesis: verumper cases
( x9 <=' t9 or not x9 <=' t9 )
;

end;

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

then
s9 <=' t9
by A34, A38, A39, ARYTM_1:3;

then A41: t9 - s9 = t9 -' s9 by ARYTM_1:def 2;

A42: t9 - x9 = t9 -' x9 by A40, ARYTM_1:def 2;

t9 -' x9 <=' t99 -' s9 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;then A41: t9 - s9 = t9 -' s9 by ARYTM_1:def 2;

A42: t9 - x9 = t9 -' x9 by A40, ARYTM_1:def 2;

t9 -' x9 <=' t99 -' s9 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

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

then A43:
+ (x1,z1) = [0,(x9 -' t9)]
by A37, ARYTM_1:def 2;

then A44: + (x1,z1) in [:{0},REAL+:] by Lm3, ZFMISC_1:87;

end;then A44: + (x1,z1) in [:{0},REAL+:] by Lm3, ZFMISC_1:87;

now :: thesis: r + t <= s + tend;

hence
r + t <= s + t
; :: thesis: verumper cases
( s9 <=' t9 or not s9 <=' t9 )
;

end;

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

then
t9 - s9 = t9 -' s9
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;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

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

A47:
s9 -' t9 <=' x9 -' t9
by A34, A38, A39, ARYTM_1:17;

A48: + (y1,z1) = [0,(s9 -' t9)] by A36, A30, A31, A46, ARYTM_1:def 2;

then + (y1,z1) in [:{0},REAL+:] by Lm3, ZFMISC_1:87;

hence r + t <= s + t by A6, A7, A43, A44, A48, A47, Lm2; :: thesis: verum

end;A48: + (y1,z1) = [0,(s9 -' t9)] by A36, A30, A31, A46, ARYTM_1:def 2;

then + (y1,z1) in [:{0},REAL+:] by Lm3, ZFMISC_1:87;

hence r + t <= s + t by A6, A7, A43, A44, A48, A47, Lm2; :: thesis: verum

suppose that A49:
r in REAL+
and

A50: s in REAL+ and

A51: t in [:{0},REAL+:] ; :: thesis: r + t <= s + t

A50: s in REAL+ and

A51: t in [:{0},REAL+:] ; :: 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 A50, A51, ARYTM_0:def 1;

consider x9, t9 being Element of REAL+ such that

A55: r = x9 and

A56: t = [0,t9] and

A57: + (x1,z1) = x9 - t9 by A49, A51, ARYTM_0:def 1;

A58: t9 = t99 by A56, A53, XTUPLE_0:1;

A59: ex x99, s99 being Element of REAL+ st

( r = x99 & s = s99 & x99 <=' s99 ) by A8, A49, A50, XXREAL_0:def 5;

end;A52: s = s9 and

A53: t = [0,t99] and

A54: + (y1,z1) = s9 - t99 by A50, A51, ARYTM_0:def 1;

consider x9, t9 being Element of REAL+ such that

A55: r = x9 and

A56: t = [0,t9] and

A57: + (x1,z1) = x9 - t9 by A49, A51, ARYTM_0:def 1;

A58: t9 = t99 by A56, A53, XTUPLE_0:1;

A59: ex x99, s99 being Element of REAL+ st

( r = x99 & s = s99 & x99 <=' s99 ) by A8, A49, A50, XXREAL_0:def 5;

now :: thesis: r + t <= s + tend;

hence
r + t <= s + t
; :: thesis: verumper cases
( t9 <=' x9 or not t9 <=' x9 )
;

end;

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

then
t9 <=' s9
by A59, A55, A52, ARYTM_1:3;

then A61: s9 - t9 = s9 -' t9 by ARYTM_1:def 2;

A62: x9 - t9 = x9 -' t9 by A60, ARYTM_1:def 2;

x9 -' t9 <=' s9 -' t99 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;then A61: s9 - t9 = s9 -' t9 by ARYTM_1:def 2;

A62: x9 - t9 = x9 -' t9 by A60, ARYTM_1:def 2;

x9 -' t9 <=' s9 -' t99 by A59, A55, A52, A58, ARYTM_1:17;

hence r + t <= s + t by A6, A7, A57, A54, A58, A62, A61, Lm2; :: thesis: verum

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

then A63:
+ (x1,z1) = [0,(t9 -' x9)]
by A57, ARYTM_1:def 2;

then A64: + (x1,z1) in [:{0},REAL+:] by Lm3, ZFMISC_1:87;

end;then A64: + (x1,z1) in [:{0},REAL+:] by Lm3, ZFMISC_1:87;

now :: thesis: r + t <= s + tend;

hence
r + t <= s + t
; :: thesis: verumper cases
( t9 <=' s9 or not t9 <=' s9 )
;

end;

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

then
s9 - t9 = s9 -' t9
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;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

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

A67:
t9 -' s9 <=' t9 -' x9
by A59, A55, A52, ARYTM_1:16;

A68: + (y1,z1) = [0,(t9 -' s9)] by A54, A58, A66, ARYTM_1:def 2;

then + (y1,z1) in [:{0},REAL+:] by Lm3, ZFMISC_1:87;

hence r + t <= s + t by A6, A7, A63, A64, A68, A67, Lm2; :: thesis: verum

end;A68: + (y1,z1) = [0,(t9 -' s9)] by A54, A58, A66, ARYTM_1:def 2;

then + (y1,z1) in [:{0},REAL+:] by Lm3, ZFMISC_1:87;

hence r + t <= s + t by A6, A7, A63, A64, A68, A67, Lm2; :: thesis: verum

suppose that A69:
r in [:{0},REAL+:]
and

A70: s in REAL+ and

A71: t in [:{0},REAL+:] ; :: thesis: r + t <= s + t

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 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 [:{0},REAL+:] by A73, Lm3, ZFMISC_1:87;

consider s9, t99 being Element of REAL+ such that

s = s9 and

A75: t = [0,t99] and

A76: + (y1,z1) = s9 - t99 by A70, A71, ARYTM_0:def 1;

A77: t9 = t99 by A72, A75, XTUPLE_0:1;

end;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 [:{0},REAL+:] by A73, Lm3, ZFMISC_1:87;

consider s9, t99 being Element of REAL+ such that

s = s9 and

A75: t = [0,t99] and

A76: + (y1,z1) = s9 - t99 by A70, A71, ARYTM_0:def 1;

A77: t9 = t99 by A72, A75, XTUPLE_0:1;

now :: thesis: r + t <= s + tend;

hence
r + t <= s + t
; :: thesis: verumper cases
( t9 <=' s9 or not t9 <=' s9 )
;

end;

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

then
s9 - t99 = s9 -' t99
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;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

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

( t9 -' s9 <=' t9 & t9 <=' t9 + x9 )
by ARYTM_1:11, ARYTM_2:19;

then A80: t9 -' s9 <=' t9 + x9 by ARYTM_1:3;

A81: + (y1,z1) = [0,(t9 -' s9)] by A76, A77, A79, ARYTM_1:def 2;

then + (y1,z1) in [:{0},REAL+:] by Lm3, ZFMISC_1:87;

hence r + t <= s + t by A6, A7, A73, A74, A81, A80, Lm2; :: thesis: verum

end;then A80: t9 -' s9 <=' t9 + x9 by ARYTM_1:3;

A81: + (y1,z1) = [0,(t9 -' s9)] by A76, A77, A79, ARYTM_1:def 2;

then + (y1,z1) in [:{0},REAL+:] by Lm3, ZFMISC_1:87;

hence r + t <= s + t by A6, A7, A73, A74, A81, A80, Lm2; :: thesis: verum

suppose that A82:
r in [:{0},REAL+:]
and

A83: s in [:{0},REAL+:] and

A84: t in [:{0},REAL+:] ; :: thesis: r + t <= s + t

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 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 [:{0},REAL+:] by A87, Lm3, ZFMISC_1:87;

( not r in REAL+ & not t in REAL+ ) by A82, A84, ARYTM_0:5, XBOOLE_0:3;

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 [:{0},REAL+:] by A91, Lm3, ZFMISC_1:87;

A93: t9 = t99 by A90, A86, XTUPLE_0:1;

consider x99, s99 being Element of REAL+ such that

A94: r = [0,x99] and

A95: s = [0,s99] and

A96: s99 <=' x99 by A8, A82, A83, XXREAL_0:def 5;

A97: s9 = s99 by A95, A85, XTUPLE_0:1;

x9 = x99 by A94, A89, XTUPLE_0:1;

then s9 + t9 <=' x9 + t99 by A96, A97, A93, ARYTM_1:7;

hence r + t <= s + t by A6, A7, A91, A87, A93, A92, A88, Lm2; :: thesis: verum

end;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 [:{0},REAL+:] by A87, Lm3, ZFMISC_1:87;

( not r in REAL+ & not t in REAL+ ) by A82, A84, ARYTM_0:5, XBOOLE_0:3;

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 [:{0},REAL+:] by A91, Lm3, ZFMISC_1:87;

A93: t9 = t99 by A90, A86, XTUPLE_0:1;

consider x99, s99 being Element of REAL+ such that

A94: r = [0,x99] and

A95: s = [0,s99] and

A96: s99 <=' x99 by A8, A82, A83, XXREAL_0:def 5;

A97: s9 = s99 by A95, A85, XTUPLE_0:1;

x9 = x99 by A94, A89, XTUPLE_0:1;

then s9 + t9 <=' x9 + t99 by A96, A97, A93, ARYTM_1:7;

hence r + t <= s + t by A6, A7, A91, A87, A93, A92, A88, Lm2; :: thesis: verum