let a, b, c be Real; :: thesis: ( a <= b implies a + c <= b + c )
reconsider x1 = a, y1 = b, z1 = c as Element of REAL by XREAL_0:def 1;
A1: + (y1,z1) = b + c by Lm3;
A2: + (x1,z1) = a + c by Lm3;
assume A3: a <= b ; :: thesis: a + c <= b + c
per cases ( ( a in REAL+ & b in REAL+ & c in REAL+ ) or ( a in [:{0},REAL+:] & b in REAL+ & c in REAL+ ) or ( a in [:{0},REAL+:] & b in [:{0},REAL+:] & c in REAL+ ) or ( a in REAL+ & b in REAL+ & c in [:{0},REAL+:] ) or ( a in [:{0},REAL+:] & b in REAL+ & c in [:{0},REAL+:] ) or ( a in [:{0},REAL+:] & b in [:{0},REAL+:] & c in [:{0},REAL+:] ) ) by A3, XXREAL_0:def 5;
suppose that A4: a in REAL+ and
A5: b in REAL+ and
A6: c in REAL+ ; :: thesis: a + c <= b + c
consider b9, c99 being Element of REAL+ such that
A7: b = b9 and
A8: c = c99 and
A9: + (y1,z1) = b9 + c99 by A5, A6, ARYTM_0:def 1;
consider a9, c9 being Element of REAL+ such that
A10: a = a9 and
A11: c = c9 and
A12: + (x1,z1) = a9 + c9 by A4, A6, ARYTM_0:def 1;
ex a99, b99 being Element of REAL+ st
( a = a99 & b = b99 & a99 <=' b99 ) by A3, A4, A5, XXREAL_0:def 5;
then a9 + c9 <=' b9 + c99 by A10, A11, A7, A8, ARYTM_1:7;
hence a + c <= b + c by A1, A2, A12, A9, Lm1; :: thesis: verum
end;
suppose that A13: a in [:{0},REAL+:] and
A14: b in REAL+ and
A15: c in REAL+ ; :: thesis: a + c <= b + c
consider b9, c99 being Element of REAL+ such that
b = b9 and
A16: c = c99 and
A17: + (y1,z1) = b9 + c99 by A14, A15, ARYTM_0:def 1;
consider a9, c9 being Element of REAL+ such that
a = [0,a9] and
A18: c = c9 and
A19: + (x1,z1) = c9 - a9 by A13, A15, ARYTM_0:def 1;
hence a + c <= b + c ; :: thesis: verum
end;
suppose that A24: a in [:{0},REAL+:] and
A25: b in [:{0},REAL+:] and
A26: c in REAL+ ; :: thesis: a + c <= b + c
consider b9, c99 being Element of REAL+ such that
A27: b = [0,b9] and
A28: c = c99 and
A29: + (y1,z1) = c99 - b9 by A25, A26, ARYTM_0:def 1;
consider a99, b99 being Element of REAL+ such that
A30: a = [0,a99] and
A31: b = [0,b99] and
A32: b99 <=' a99 by A3, A24, A25, XXREAL_0:def 5;
consider a9, c9 being Element of REAL+ such that
A33: a = [0,a9] and
A34: c = c9 and
A35: + (x1,z1) = c9 - a9 by A24, A26, ARYTM_0:def 1;
A36: a9 = a99 by A30, A33, XTUPLE_0:1;
A37: b9 = b99 by A31, A27, XTUPLE_0:1;
now :: thesis: a + c <= b + c
per cases ( a9 <=' c9 or not a9 <=' c9 ) ;
suppose A38: a9 <=' c9 ; :: thesis: a + c <= b + c
then b9 <=' c9 by A32, A36, A37, ARYTM_1:3;
then A39: c9 - b9 = c9 -' b9 by ARYTM_1:def 2;
A40: c9 - a9 = c9 -' a9 by A38, ARYTM_1:def 2;
c9 -' a9 <=' c99 -' b9 by A32, A34, A28, A36, A37, ARYTM_1:16;
hence a + c <= b + c by A1, A2, A34, A35, A28, A29, A40, A39, Lm1; :: thesis: verum
end;
suppose not a9 <=' c9 ; :: thesis: a + c <= b + c
then A41: + (x1,z1) = [0,(a9 -' c9)] by A35, ARYTM_1:def 2;
then A42: + (x1,z1) in [:{0},REAL+:] by Lm4, ZFMISC_1:87;
now :: thesis: a + c <= b + c
per cases ( b9 <=' c9 or not b9 <=' c9 ) ;
suppose A44: not b9 <=' c9 ; :: thesis: a + c <= b + c
A45: b9 -' c9 <=' a9 -' c9 by A32, A36, A37, ARYTM_1:17;
A46: + (y1,z1) = [0,(b9 -' c9)] by A34, A28, A29, A44, ARYTM_1:def 2;
then + (y1,z1) in [:{0},REAL+:] by Lm4, ZFMISC_1:87;
hence a + c <= b + c by A1, A2, A41, A42, A46, A45, Lm1; :: thesis: verum
end;
end;
end;
hence a + c <= b + c ; :: thesis: verum
end;
end;
end;
hence a + c <= b + c ; :: thesis: verum
end;
suppose that A47: a in REAL+ and
A48: b in REAL+ and
A49: c in [:{0},REAL+:] ; :: thesis: a + c <= b + c
consider b9, c99 being Element of REAL+ such that
A50: b = b9 and
A51: c = [0,c99] and
A52: + (y1,z1) = b9 - c99 by A48, A49, ARYTM_0:def 1;
consider a9, c9 being Element of REAL+ such that
A53: a = a9 and
A54: c = [0,c9] and
A55: + (x1,z1) = a9 - c9 by A47, A49, ARYTM_0:def 1;
A56: c9 = c99 by A54, A51, XTUPLE_0:1;
A57: ex a99, b99 being Element of REAL+ st
( a = a99 & b = b99 & a99 <=' b99 ) by A3, A47, A48, XXREAL_0:def 5;
now :: thesis: a + c <= b + c
per cases ( c9 <=' a9 or not c9 <=' a9 ) ;
suppose A58: c9 <=' a9 ; :: thesis: a + c <= b + c
then c9 <=' b9 by A57, A53, A50, ARYTM_1:3;
then A59: b9 - c9 = b9 -' c9 by ARYTM_1:def 2;
A60: a9 - c9 = a9 -' c9 by A58, ARYTM_1:def 2;
a9 -' c9 <=' b9 -' c99 by A57, A53, A50, A56, ARYTM_1:17;
hence a + c <= b + c by A1, A2, A55, A52, A56, A60, A59, Lm1; :: thesis: verum
end;
suppose not c9 <=' a9 ; :: thesis: a + c <= b + c
then A61: + (x1,z1) = [0,(c9 -' a9)] by A55, ARYTM_1:def 2;
then A62: + (x1,z1) in [:{0},REAL+:] by Lm4, ZFMISC_1:87;
now :: thesis: a + c <= b + c
per cases ( c9 <=' b9 or not c9 <=' b9 ) ;
suppose A64: not c9 <=' b9 ; :: thesis: a + c <= b + c
A65: c9 -' b9 <=' c9 -' a9 by A57, A53, A50, ARYTM_1:16;
A66: + (y1,z1) = [0,(c9 -' b9)] by A52, A56, A64, ARYTM_1:def 2;
then + (y1,z1) in [:{0},REAL+:] by Lm4, ZFMISC_1:87;
hence a + c <= b + c by A1, A2, A61, A62, A66, A65, Lm1; :: thesis: verum
end;
end;
end;
hence a + c <= b + c ; :: thesis: verum
end;
end;
end;
hence a + c <= b + c ; :: thesis: verum
end;
suppose that A67: a in [:{0},REAL+:] and
A68: b in REAL+ and
A69: c in [:{0},REAL+:] ; :: thesis: a + c <= b + c
A70: not c in REAL+ by A69, ARYTM_0:5, XBOOLE_0:3;
not a in REAL+ by A67, ARYTM_0:5, XBOOLE_0:3;
then consider a9, c9 being Element of REAL+ such that
a = [0,a9] and
A71: c = [0,c9] and
A72: + (x1,z1) = [0,(a9 + c9)] by A70, ARYTM_0:def 1;
A73: + (x1,z1) in [:{0},REAL+:] by A72, Lm4, ZFMISC_1:87;
consider b9, c99 being Element of REAL+ such that
b = b9 and
A74: c = [0,c99] and
A75: + (y1,z1) = b9 - c99 by A68, A69, ARYTM_0:def 1;
A76: c9 = c99 by A71, A74, XTUPLE_0:1;
hence a + c <= b + c ; :: thesis: verum
end;
suppose that A82: a in [:{0},REAL+:] and
A83: b in [:{0},REAL+:] and
A84: c in [:{0},REAL+:] ; :: thesis: a + c <= b + c
A85: not c in REAL+ by A84, ARYTM_0:5, XBOOLE_0:3;
A86: not c in REAL+ by A84, ARYTM_0:5, XBOOLE_0:3;
not a in REAL+ by A82, ARYTM_0:5, XBOOLE_0:3;
then consider a9, c9 being Element of REAL+ such that
A87: a = [0,a9] and
A88: c = [0,c9] and
A89: + (x1,z1) = [0,(a9 + c9)] by A86, ARYTM_0:def 1;
A90: + (x1,z1) in [:{0},REAL+:] by A89, Lm4, ZFMISC_1:87;
not b in REAL+ by A83, ARYTM_0:5, XBOOLE_0:3;
then consider b9, c99 being Element of REAL+ such that
A91: b = [0,b9] and
A92: c = [0,c99] and
A93: + (y1,z1) = [0,(b9 + c99)] by A85, ARYTM_0:def 1;
A94: + (y1,z1) in [:{0},REAL+:] by A93, Lm4, ZFMISC_1:87;
A95: c9 = c99 by A88, A92, XTUPLE_0:1;
consider a99, b99 being Element of REAL+ such that
A96: a = [0,a99] and
A97: b = [0,b99] and
A98: b99 <=' a99 by A3, A82, A83, XXREAL_0:def 5;
A99: b9 = b99 by A97, A91, XTUPLE_0:1;
a9 = a99 by A96, A87, XTUPLE_0:1;
then b9 + c9 <=' a9 + c99 by A98, A99, A95, ARYTM_1:7;
hence a + c <= b + c by A1, A2, A89, A93, A95, A90, A94, Lm1; :: thesis: verum
end;
end;