let a, b, c, d be Real; ( 0 <= a & 0 <= b & 0 <= c & 0 <= d implies sqrt (((a + c) ^2) + ((b + d) ^2)) <= (sqrt ((a ^2) + (b ^2))) + (sqrt ((c ^2) + (d ^2))) )
assume
( 0 <= a & 0 <= b & 0 <= c & 0 <= d )
; sqrt (((a + c) ^2) + ((b + d) ^2)) <= (sqrt ((a ^2) + (b ^2))) + (sqrt ((c ^2) + (d ^2)))
then
( 0 <= a * c & 0 <= d * b )
by XREAL_1:127;
then A1:
0 + 0 <= (a * c) + (d * b)
by XREAL_1:7;
( 0 <= d ^2 & 0 <= c ^2 )
by XREAL_1:63;
then A2:
0 + 0 <= (c ^2) + (d ^2)
by XREAL_1:7;
then A3:
0 <= sqrt ((c ^2) + (d ^2))
by SQUARE_1:def 2;
0 <= ((a * d) - (c * b)) ^2
by XREAL_1:63;
then
0 <= (((a ^2) * (d ^2)) + ((c ^2) * (b ^2))) - ((2 * (a * d)) * (c * b))
;
then
0 + ((2 * (a * d)) * (c * b)) <= ((a ^2) * (d ^2)) + ((c ^2) * (b ^2))
by XREAL_1:19;
then
((b ^2) * (d ^2)) + ((2 * (a * d)) * (c * b)) <= (((a ^2) * (d ^2)) + ((c ^2) * (b ^2))) + ((b ^2) * (d ^2))
by XREAL_1:6;
then A4:
((a ^2) * (c ^2)) + (((b ^2) * (d ^2)) + ((2 * (a * d)) * (c * b))) <= ((a ^2) * (c ^2)) + (((b ^2) * (d ^2)) + (((a ^2) * (d ^2)) + ((c ^2) * (b ^2))))
by XREAL_1:6;
( 0 <= a ^2 & 0 <= b ^2 )
by XREAL_1:63;
then A5:
0 + 0 <= (a ^2) + (b ^2)
by XREAL_1:7;
then
0 <= sqrt ((a ^2) + (b ^2))
by SQUARE_1:def 2;
then A6:
0 + 0 <= (sqrt ((a ^2) + (b ^2))) + (sqrt ((c ^2) + (d ^2)))
by A3, XREAL_1:7;
0 <= ((a * c) + (d * b)) ^2
by XREAL_1:63;
then
sqrt (((a * c) + (d * b)) ^2) <= sqrt (((a ^2) + (b ^2)) * ((c ^2) + (d ^2)))
by A4, SQUARE_1:26;
then
2 * (sqrt (((a * c) + (d * b)) ^2)) <= 2 * (sqrt (((a ^2) + (b ^2)) * ((c ^2) + (d ^2))))
by XREAL_1:64;
then
2 * (sqrt (((a * c) + (d * b)) ^2)) <= 2 * ((sqrt ((a ^2) + (b ^2))) * (sqrt ((c ^2) + (d ^2))))
by A5, A2, SQUARE_1:29;
then
2 * ((a * c) + (d * b)) <= 2 * ((sqrt ((a ^2) + (b ^2))) * (sqrt ((d ^2) + (c ^2))))
by A1, SQUARE_1:22;
then
(b ^2) + (2 * ((a * c) + (d * b))) <= (2 * ((sqrt ((a ^2) + (b ^2))) * (sqrt ((d ^2) + (c ^2))))) + (b ^2)
by XREAL_1:6;
then
(d ^2) + ((b ^2) + (2 * ((a * c) + (d * b)))) <= (d ^2) + ((b ^2) + (2 * ((sqrt ((a ^2) + (b ^2))) * (sqrt ((d ^2) + (c ^2))))))
by XREAL_1:6;
then
(c ^2) + ((d ^2) + ((b ^2) + (2 * ((a * c) + (d * b))))) <= ((d ^2) + ((b ^2) + (2 * ((sqrt ((a ^2) + (b ^2))) * (sqrt ((d ^2) + (c ^2))))))) + (c ^2)
by XREAL_1:6;
then
(a ^2) + ((c ^2) + ((d ^2) + (((b ^2) + (2 * (d * b))) + (2 * (a * c))))) <= (a ^2) + ((c ^2) + ((d ^2) + ((b ^2) + (2 * ((sqrt ((a ^2) + (b ^2))) * (sqrt ((d ^2) + (c ^2))))))))
by XREAL_1:6;
then
((a + c) ^2) + ((d + b) ^2) <= (((a ^2) + (b ^2)) + (2 * ((sqrt ((a ^2) + (b ^2))) * (sqrt ((c ^2) + (d ^2)))))) + ((c ^2) + (d ^2))
;
then
((a + c) ^2) + ((d + b) ^2) <= (((sqrt ((a ^2) + (b ^2))) ^2) + (2 * ((sqrt ((a ^2) + (b ^2))) * (sqrt ((c ^2) + (d ^2)))))) + ((c ^2) + (d ^2))
by A5, SQUARE_1:def 2;
then A7:
((a + c) ^2) + ((d + b) ^2) <= (((sqrt ((a ^2) + (b ^2))) ^2) + ((2 * (sqrt ((a ^2) + (b ^2)))) * (sqrt ((c ^2) + (d ^2))))) + ((sqrt ((c ^2) + (d ^2))) ^2)
by A2, SQUARE_1:def 2;
( 0 <= (a + c) ^2 & 0 <= (d + b) ^2 )
by XREAL_1:63;
then
0 + 0 <= ((a + c) ^2) + ((d + b) ^2)
by XREAL_1:7;
then
sqrt (((a + c) ^2) + ((d + b) ^2)) <= sqrt (((sqrt ((a ^2) + (b ^2))) + (sqrt ((c ^2) + (d ^2)))) ^2)
by A7, SQUARE_1:26;
hence
sqrt (((a + c) ^2) + ((b + d) ^2)) <= (sqrt ((a ^2) + (b ^2))) + (sqrt ((c ^2) + (d ^2)))
by A6, SQUARE_1:22; verum