let x, y be real number ; :: thesis: (abs (x + y)) / (1 + (abs (x + y))) <= ((abs x) / (1 + (abs x))) + ((abs y) / (1 + (abs y)))
A1: for s, t being real number st s <= t & 0 < 1 + s & 0 < 1 + t holds
s / (1 + s) <= t / (1 + t)

proof

let s, t be real number ; :: thesis: ( s <= t & 0 < 1 + s & 0 < 1 + t implies s / (1 + s) <= t / (1 + t) )
assume that
A2: s <= t and
A3: 0 < 1 + s and
A4: 0 < 1 + t ; :: thesis: s / (1 + s) <= t / (1 + t)
(s * 1) + (s * t) <= t + (s * t) by A2, XREAL_1:8;
then (s * (1 + t)) * ((1 + s) " ) <= (t * (1 + s)) * ((1 + s) " ) by A3, XREAL_1:66;
then (s * (1 + t)) * ((1 + s) " ) <= t * ((1 + s) * ((1 + s) " )) ;
then (s * (1 + t)) * ((1 + s) " ) <= t * 1 by A3, XCMPLX_0:def 7;
then ((s * ((1 + s) " )) * (1 + t)) * ((1 + t) " ) <= t * ((1 + t) " ) by A4, XREAL_1:66;
then (s * ((1 + s) " )) * ((1 + t) * ((1 + t) " )) <= t * ((1 + t) " ) ;
then (s * ((1 + s) " )) * 1 <= t * ((1 + t) " ) by A4, XCMPLX_0:def 7;
then s / (1 + s) <= t * ((1 + t) " ) by XCMPLX_0:def 9;
hence s / (1 + s) <= t / (1 + t) by XCMPLX_0:def 9; :: thesis: verum

end;

set a = abs x;
set b = abs y;
set c = abs (x + y);
A5: 0 <= abs x by COMPLEX1:132;
A6: 0 <= abs y by COMPLEX1:132;
A7: 0 + 0 < 1 + (abs x) by COMPLEX1:132, XREAL_1:10;
A8: ( 0 < 1 + (abs x) & 0 < (1 + (abs x)) + (abs y) implies (abs x) / ((1 + (abs x)) + (abs y)) <= (abs x) / (1 + (abs x)) )

proof

assume that
A9: 0 < 1 + (abs x) and
A10: 0 < (1 + (abs x)) + (abs y) ; :: thesis: (abs x) / ((1 + (abs x)) + (abs y)) <= (abs x) / (1 + (abs x))
0 + (abs x) <= ((abs x) * (abs y)) + (abs x) by A5, A6, XREAL_1:8;
then ((abs x) * 1) + ((abs x) * (abs x)) <= ((abs x) * (1 + (abs y))) + ((abs x) * (abs x)) by XREAL_1:8;
then ((abs x) * (1 + (abs x))) * ((1 + (abs x)) " ) <= ((abs x) * ((1 + (abs x)) + (abs y))) * ((1 + (abs x)) " ) by A9, XREAL_1:66;
then (abs x) * ((1 + (abs x)) * ((1 + (abs x)) " )) <= ((abs x) * ((1 + (abs x)) + (abs y))) * ((1 + (abs x)) " ) ;
then (abs x) * 1 <= ((abs x) * ((1 + (abs x)) + (abs y))) * ((1 + (abs x)) " ) by A7, XCMPLX_0:def 7;
then (abs x) * (((1 + (abs x)) + (abs y)) " ) <= (((abs x) * ((1 + (abs x)) " )) * ((1 + (abs x)) + (abs y))) * (((1 + (abs x)) + (abs y)) " ) by A10, XREAL_1:66;
then (abs x) * (((1 + (abs x)) + (abs y)) " ) <= ((abs x) * ((1 + (abs x)) " )) * (((1 + (abs x)) + (abs y)) * (((1 + (abs x)) + (abs y)) " )) ;
then (abs x) * (((1 + (abs x)) + (abs y)) " ) <= ((abs x) * ((1 + (abs x)) " )) * 1 by A5, A6, XCMPLX_0:def 7;
then (abs x) / ((1 + (abs x)) + (abs y)) <= (abs x) * ((1 + (abs x)) " ) by XCMPLX_0:def 9;
hence (abs x) / ((1 + (abs x)) + (abs y)) <= (abs x) / (1 + (abs x)) by XCMPLX_0:def 9; :: thesis: verum

end;

A11: 0 + 0 < 1 + (abs y) by COMPLEX1:132, XREAL_1:10;
A12: ( 0 < 1 + (abs y) & 0 < (1 + (abs x)) + (abs y) implies (abs y) / ((1 + (abs x)) + (abs y)) <= (abs y) / (1 + (abs y)) )

proof

assume that
A13: 0 < 1 + (abs y) and
A14: 0 < (1 + (abs x)) + (abs y) ; :: thesis: (abs y) / ((1 + (abs x)) + (abs y)) <= (abs y) / (1 + (abs y))
0 + (abs y) <= ((abs x) * (abs y)) + (abs y) by A5, A6, XREAL_1:8;
then ((abs y) * 1) + ((abs y) * (abs y)) <= ((1 + (abs x)) * (abs y)) + ((abs y) * (abs y)) by XREAL_1:8;
then ((abs y) * (1 + (abs y))) * ((1 + (abs y)) " ) <= ((abs y) * ((1 + (abs x)) + (abs y))) * ((1 + (abs y)) " ) by A13, XREAL_1:66;
then (abs y) * ((1 + (abs y)) * ((1 + (abs y)) " )) <= ((abs y) * ((1 + (abs x)) + (abs y))) * ((1 + (abs y)) " ) ;
then (abs y) * 1 <= ((abs y) * ((1 + (abs x)) + (abs y))) * ((1 + (abs y)) " ) by A11, XCMPLX_0:def 7;
then (abs y) * (((1 + (abs x)) + (abs y)) " ) <= (((abs y) * ((1 + (abs y)) " )) * ((1 + (abs x)) + (abs y))) * (((1 + (abs x)) + (abs y)) " ) by A14, XREAL_1:66;
then (abs y) * (((1 + (abs x)) + (abs y)) " ) <= ((abs y) * ((1 + (abs y)) " )) * (((1 + (abs x)) + (abs y)) * (((1 + (abs x)) + (abs y)) " )) ;
then (abs y) * (((1 + (abs x)) + (abs y)) " ) <= ((abs y) * ((1 + (abs y)) " )) * 1 by A5, A6, XCMPLX_0:def 7;
then (abs y) / ((1 + (abs x)) + (abs y)) <= (abs y) * ((1 + (abs y)) " ) by XCMPLX_0:def 9;
hence (abs y) / ((1 + (abs x)) + (abs y)) <= (abs y) / (1 + (abs y)) by XCMPLX_0:def 9; :: thesis: verum

end;

0 + 0 < 1 + (abs (x + y)) by COMPLEX1:132, XREAL_1:10;
then A15: (abs (x + y)) / (1 + (abs (x + y))) <= ((abs x) + (abs y)) / (1 + ((abs x) + (abs y))) by A5, A6, A1, COMPLEX1:142;
((abs x) + (abs y)) / ((1 + (abs x)) + (abs y)) = ((abs x) / ((1 + (abs x)) + (abs y))) + ((abs y) / ((1 + (abs x)) + (abs y))) by XCMPLX_1:63;
then ((abs x) + (abs y)) / ((1 + (abs x)) + (abs y)) <= ((abs x) / (1 + (abs x))) + ((abs y) / (1 + (abs y))) by A6, A7, A8, A12, XREAL_1:9;
hence (abs (x + y)) / (1 + (abs (x + y))) <= ((abs x) / (1 + (abs x))) + ((abs y) / (1 + (abs y))) by A15, XXREAL_0:2; :: thesis: verum