let x, y be real number ; (abs (x + y)) / (1 + (abs (x + y))) <= ((abs x) / (1 + (abs x))) + ((abs y) / (1 + (abs y)))
per cases
( abs (x + y) = 0 or abs (x + y) > 0 )
;
suppose A1:
abs (x + y) > 0
;
(abs (x + y)) / (1 + (abs (x + y))) <= ((abs x) / (1 + (abs x))) + ((abs y) / (1 + (abs y)))
1
+ (abs y) >= 1
by XREAL_1:33;
then
(1 + (abs y)) + (abs x) >= 1
+ (abs x)
by XREAL_1:8;
then A2:
(abs x) / ((1 + (abs x)) + (abs y)) <= (abs x) / (1 + (abs x))
by XREAL_1:120;
1
+ (abs x) >= 1
by XREAL_1:33;
then
(1 + (abs x)) + (abs y) >= 1
+ (abs y)
by XREAL_1:8;
then
(abs y) / ((1 + (abs x)) + (abs y)) <= (abs y) / (1 + (abs y))
by XREAL_1:120;
then A3:
((abs x) / ((1 + (abs x)) + (abs y))) + ((abs y) / ((1 + (abs x)) + (abs y))) <= ((abs x) / (1 + (abs x))) + ((abs y) / (1 + (abs y)))
by A2, XREAL_1:9;
1
/ ((abs x) + (abs y)) <= 1
/ (abs (x + y))
by A1, COMPLEX1:142, XREAL_1:120;
then
(1 / ((abs x) + (abs y))) + 1
<= (1 / (abs (x + y))) + 1
by XREAL_1:9;
then A4:
1
/ ((1 / (abs (x + y))) + 1) <= 1
/ ((1 / ((abs x) + (abs y))) + 1)
by XREAL_1:120;
A5:
0 < (abs x) + (abs y)
by A1, COMPLEX1:142;
then A6: 1
/ ((1 / ((abs x) + (abs y))) + 1) =
(1 * ((abs x) + (abs y))) / (((1 / ((abs x) + (abs y))) + 1) * ((abs x) + (abs y)))
by XCMPLX_1:92
.=
((abs x) + (abs y)) / (((1 / ((abs x) + (abs y))) * ((abs x) + (abs y))) + ((abs x) + (abs y)))
.=
((abs x) + (abs y)) / (1 + ((abs x) + (abs y)))
by A5, XCMPLX_1:88
.=
((abs x) / ((1 + (abs x)) + (abs y))) + ((abs y) / ((1 + (abs x)) + (abs y)))
by XCMPLX_1:63
;
(abs (x + y)) / (1 + (abs (x + y))) =
((abs (x + y)) / (abs (x + y))) / ((1 + (abs (x + y))) / (abs (x + y)))
by A1, XCMPLX_1:55
.=
1
/ ((1 + (abs (x + y))) / (abs (x + y)))
by A1, XCMPLX_1:60
.=
1
/ ((1 / (abs (x + y))) + ((abs (x + y)) / (abs (x + y))))
by XCMPLX_1:63
.=
1
/ ((1 / (abs (x + y))) + 1)
by A1, XCMPLX_1:60
;
hence
(abs (x + y)) / (1 + (abs (x + y))) <= ((abs x) / (1 + (abs x))) + ((abs y) / (1 + (abs y)))
by A4, A6, A3, XXREAL_0:2;
verum