let x, y be real number ; :: thesis: (abs (x + y)) / (1 + (abs (x + y))) <= ((abs x) / (1 + (abs x))) + ((abs y) / (1 + (abs y)))
set a = abs x;
set b = abs y;
set c = abs (x + y);
A1: 0 <= abs x by COMPLEX1:132;
A2: 0 <= abs y by COMPLEX1:132;
then A3: 0 + 0 <= (abs x) + (abs y) by A1;
then A4: 0 + 0 < 1 + ((abs x) + (abs y)) ;
A5: 0 < 1 + ((abs x) + (abs y)) by A3;
A6: 0 + 0 < 1 + (abs (x + y)) by COMPLEX1:132, XREAL_1:10;
A7: 0 + 0 < 1 + (abs x) by COMPLEX1:132, XREAL_1:10;
A8: 0 + 0 < 1 + (abs y) by COMPLEX1:132, XREAL_1:10;
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
A9: s <= t and
A10: 0 < 1 + s and
A11: 0 < 1 + t ; :: thesis: s / (1 + s) <= t / (1 + t)
A12: (s * 1) + (s * t) <= t + (s * t) by A9, XREAL_1:8;
A13: 0 < (1 + s) " by A10;
A14: 0 < (1 + t) " by A11;
(s * (1 + t)) * ((1 + s) " ) <= (t * (1 + s)) * ((1 + s) " ) by A12, A13, XREAL_1:66;
then (s * (1 + t)) * ((1 + s) " ) <= t * ((1 + s) * ((1 + s) " )) ;
then (s * (1 + t)) * ((1 + s) " ) <= t * 1 by A10, XCMPLX_0:def 7;
then ((s * ((1 + s) " )) * (1 + t)) * ((1 + t) " ) <= t * ((1 + t) " ) by A14, XREAL_1:66;
then (s * ((1 + s) " )) * ((1 + t) * ((1 + t) " )) <= t * ((1 + t) " ) ;
then (s * ((1 + s) " )) * 1 <= t * ((1 + t) " ) by A11, 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;

then A15: (abs (x + y)) / (1 + (abs (x + y))) <= ((abs x) + (abs y)) / (1 + ((abs x) + (abs y))) by A5, A6, COMPLEX1:142;
((abs x) + (abs y)) / ((1 + (abs x)) + (abs y)) <= ((abs x) / (1 + (abs x))) + ((abs y) / (1 + (abs y)))

proof

A16: ((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;
A17: ( 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
A18: 0 < 1 + (abs x) and
A19: 0 < (1 + (abs x)) + (abs y) ; :: thesis: (abs x) / ((1 + (abs x)) + (abs y)) <= (abs x) / (1 + (abs x))
0 * (abs y) <= (abs x) * (abs y) by A1, A2;
then 0 + (abs x) <= ((abs x) * (abs y)) + (abs x) by XREAL_1:8;
then A20: ((abs x) * 1) + ((abs x) * (abs x)) <= ((abs x) * (1 + (abs y))) + ((abs x) * (abs x)) by XREAL_1:8;
A21: 0 <= (1 + (abs x)) " by A18;
A22: 0 <= ((1 + (abs x)) + (abs y)) " by A19;
((abs x) * (1 + (abs x))) * ((1 + (abs x)) " ) <= ((abs x) * ((1 + (abs x)) + (abs y))) * ((1 + (abs x)) " ) by A20, A21, 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 A22, 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 A4, 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;

( 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
A23: 0 < 1 + (abs y) and
A24: 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) by A1, A2;
then 0 + (abs y) <= ((abs x) * (abs y)) + (abs y) by XREAL_1:8;
then A25: ((abs y) * 1) + ((abs y) * (abs y)) <= ((1 + (abs x)) * (abs y)) + ((abs y) * (abs y)) by XREAL_1:8;
A26: 0 <= (1 + (abs y)) " by A23;
A27: 0 <= ((1 + (abs x)) + (abs y)) " by A24;
((abs y) * (1 + (abs y))) * ((1 + (abs y)) " ) <= ((abs y) * ((1 + (abs x)) + (abs y))) * ((1 + (abs y)) " ) by A25, A26, 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 A8, 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 A27, 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 A4, 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;

hence ((abs x) + (abs y)) / ((1 + (abs x)) + (abs y)) <= ((abs x) / (1 + (abs x))) + ((abs y) / (1 + (abs y))) by A2, A7, A16, A17, XREAL_1:9; :: thesis: verum

end;

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