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

proof

let s, t be Real; :: 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:6;
then (s * (1 + t)) * ((1 + s) ") <= (t * (1 + s)) * ((1 + s) ") by A3, XREAL_1:64;
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:64;
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 = |.x.|;
set b = |.y.|;
set c = |.(x + y).|;
A5: 0 <= |.x.| by COMPLEX1:46;
A6: 0 <= |.y.| by COMPLEX1:46;
A7: 0 + 0 < 1 + |.x.| by COMPLEX1:46, XREAL_1:8;
A8: ( 0 < 1 + |.x.| & 0 < (1 + |.x.|) + |.y.| implies |.x.| / ((1 + |.x.|) + |.y.|) <= |.x.| / (1 + |.x.|) )

proof

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

end;

A11: 0 + 0 < 1 + |.y.| by COMPLEX1:46, XREAL_1:8;
A12: ( 0 < 1 + |.y.| & 0 < (1 + |.x.|) + |.y.| implies |.y.| / ((1 + |.x.|) + |.y.|) <= |.y.| / (1 + |.y.|) )

proof

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

end;

0 + 0 < 1 + |.(x + y).| by COMPLEX1:46, XREAL_1:8;
then A15: |.(x + y).| / (1 + |.(x + y).|) <= (|.x.| + |.y.|) / (1 + (|.x.| + |.y.|)) by A5, A6, A1, COMPLEX1:56;
(|.x.| + |.y.|) / ((1 + |.x.|) + |.y.|) = (|.x.| / ((1 + |.x.|) + |.y.|)) + (|.y.| / ((1 + |.x.|) + |.y.|)) by XCMPLX_1:62;
then (|.x.| + |.y.|) / ((1 + |.x.|) + |.y.|) <= (|.x.| / (1 + |.x.|)) + (|.y.| / (1 + |.y.|)) by A6, A7, A8, A12, XREAL_1:7;
hence |.(x + y).| / (1 + |.(x + y).|) <= (|.x.| / (1 + |.x.|)) + (|.y.| / (1 + |.y.|)) by A15, XXREAL_0:2; :: thesis: verum