let x, y be Real; |.(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)
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.|) )
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.|) )
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; verum