let x, y be Real; |.(x + y).| / (1 + |.(x + y).|) <= (|.x.| / (1 + |.x.|)) + (|.y.| / (1 + |.y.|))
per cases
( |.(x + y).| = 0 or |.(x + y).| > 0 )
;
suppose A1:
|.(x + y).| > 0
;
|.(x + y).| / (1 + |.(x + y).|) <= (|.x.| / (1 + |.x.|)) + (|.y.| / (1 + |.y.|))
1
+ |.y.| >= 1
by XREAL_1:31;
then
(1 + |.y.|) + |.x.| >= 1
+ |.x.|
by XREAL_1:6;
then A2:
|.x.| / ((1 + |.x.|) + |.y.|) <= |.x.| / (1 + |.x.|)
by XREAL_1:118;
1
+ |.x.| >= 1
by XREAL_1:31;
then
(1 + |.x.|) + |.y.| >= 1
+ |.y.|
by XREAL_1:6;
then
|.y.| / ((1 + |.x.|) + |.y.|) <= |.y.| / (1 + |.y.|)
by XREAL_1:118;
then A3:
(|.x.| / ((1 + |.x.|) + |.y.|)) + (|.y.| / ((1 + |.x.|) + |.y.|)) <= (|.x.| / (1 + |.x.|)) + (|.y.| / (1 + |.y.|))
by A2, XREAL_1:7;
1
/ (|.x.| + |.y.|) <= 1
/ |.(x + y).|
by A1, COMPLEX1:56, XREAL_1:118;
then
(1 / (|.x.| + |.y.|)) + 1
<= (1 / |.(x + y).|) + 1
by XREAL_1:7;
then A4:
1
/ ((1 / |.(x + y).|) + 1) <= 1
/ ((1 / (|.x.| + |.y.|)) + 1)
by XREAL_1:118;
A5:
0 < |.x.| + |.y.|
by A1, COMPLEX1:56;
then A6: 1
/ ((1 / (|.x.| + |.y.|)) + 1) =
(1 * (|.x.| + |.y.|)) / (((1 / (|.x.| + |.y.|)) + 1) * (|.x.| + |.y.|))
by XCMPLX_1:91
.=
(|.x.| + |.y.|) / (((1 / (|.x.| + |.y.|)) * (|.x.| + |.y.|)) + (|.x.| + |.y.|))
.=
(|.x.| + |.y.|) / (1 + (|.x.| + |.y.|))
by A5, XCMPLX_1:87
.=
(|.x.| / ((1 + |.x.|) + |.y.|)) + (|.y.| / ((1 + |.x.|) + |.y.|))
by XCMPLX_1:62
;
|.(x + y).| / (1 + |.(x + y).|) =
(|.(x + y).| / |.(x + y).|) / ((1 + |.(x + y).|) / |.(x + y).|)
by A1, XCMPLX_1:55
.=
1
/ ((1 + |.(x + y).|) / |.(x + y).|)
by A1, XCMPLX_1:60
.=
1
/ ((1 / |.(x + y).|) + (|.(x + y).| / |.(x + y).|))
by XCMPLX_1:62
.=
1
/ ((1 / |.(x + y).|) + 1)
by A1, XCMPLX_1:60
;
hence
|.(x + y).| / (1 + |.(x + y).|) <= (|.x.| / (1 + |.x.|)) + (|.y.| / (1 + |.y.|))
by A4, A6, A3, XXREAL_0:2;
verum