let x, y be real number ; :: thesis: (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 abs (x + y) = 0 ; :: thesis: (abs (x + y)) / (1 + (abs (x + y))) <= ((abs x) / (1 + (abs x))) + ((abs y) / (1 + (abs y)))

hence (abs (x + y)) / (1 + (abs (x + y))) <= ((abs x) / (1 + (abs x))) + ((abs y) / (1 + (abs y))) ; :: thesis: verum

end;

suppose A1: abs (x + y) > 0 ; :: thesis: (abs (x + y)) / (1 + (abs (x + y))) <= ((abs x) / (1 + (abs x))) + ((abs y) / (1 + (abs y)))

then 1 / ((abs x) + (abs y)) <= 1 / (abs (x + y)) by COMPLEX1:142, XREAL_1:120;
then (1 / ((abs x) + (abs y))) + 1 <= (1 / (abs (x + y))) + 1 by XREAL_1:9;
then A2: 1 / ((1 / (abs (x + y))) + 1) <= 1 / ((1 / ((abs x) + (abs y))) + 1) by XREAL_1:120;
A3: 0 < (abs x) + (abs y) by A1, COMPLEX1:142;
then A4: 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 A3, XCMPLX_1:88
.= ((abs x) / ((1 + (abs x)) + (abs y))) + ((abs y) / ((1 + (abs x)) + (abs y))) by XCMPLX_1:63 ;
( 1 + (abs x) >= 1 & 1 + (abs y) >= 1 ) by XREAL_1:33;
then ( (1 + (abs x)) + (abs y) >= 1 + (abs y) & (1 + (abs y)) + (abs x) >= 1 + (abs x) ) by XREAL_1:8;
then ( (abs x) / ((1 + (abs x)) + (abs y)) <= (abs x) / (1 + (abs x)) & (abs y) / ((1 + (abs x)) + (abs y)) <= (abs y) / (1 + (abs y)) ) by XREAL_1:120;
then A5: ((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 XREAL_1:9;
(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 A2, A4, A5, XXREAL_0:2; :: thesis: verum

end;

end;