let a, b, c, d be real number ; ( 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:129;
then A1:
0 + 0 <= (a * c) + (d * b)
by XREAL_1:9;
( 0 <= d ^2 & 0 <= c ^2 )
by XREAL_1:65;
then A2:
0 + 0 <= (c ^2 ) + (d ^2 )
by XREAL_1:9;
then A3:
0 <= sqrt ((c ^2 ) + (d ^2 ))
by SQUARE_1:def 4;
0 <= ((a * d) - (c * b)) ^2
by XREAL_1:65;
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:21;
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:8;
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:8;
( 0 <= a ^2 & 0 <= b ^2 )
by XREAL_1:65;
then A5:
0 + 0 <= (a ^2 ) + (b ^2 )
by XREAL_1:9;
then
0 <= sqrt ((a ^2 ) + (b ^2 ))
by SQUARE_1:def 4;
then A6:
0 + 0 <= (sqrt ((a ^2 ) + (b ^2 ))) + (sqrt ((c ^2 ) + (d ^2 )))
by A3, XREAL_1:9;
0 <= ((a * c) + (d * b)) ^2
by XREAL_1:65;
then
sqrt (((a * c) + (d * b)) ^2 ) <= sqrt (((a ^2 ) + (b ^2 )) * ((c ^2 ) + (d ^2 )))
by A4, SQUARE_1:94;
then
2 * (sqrt (((a * c) + (d * b)) ^2 )) <= 2 * (sqrt (((a ^2 ) + (b ^2 )) * ((c ^2 ) + (d ^2 ))))
by XREAL_1:66;
then
2 * (sqrt (((a * c) + (d * b)) ^2 )) <= 2 * ((sqrt ((a ^2 ) + (b ^2 ))) * (sqrt ((c ^2 ) + (d ^2 ))))
by A5, A2, SQUARE_1:97;
then
2 * ((a * c) + (d * b)) <= 2 * ((sqrt ((a ^2 ) + (b ^2 ))) * (sqrt ((d ^2 ) + (c ^2 ))))
by A1, SQUARE_1:89;
then
(b ^2 ) + (2 * ((a * c) + (d * b))) <= (2 * ((sqrt ((a ^2 ) + (b ^2 ))) * (sqrt ((d ^2 ) + (c ^2 ))))) + (b ^2 )
by XREAL_1:8;
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:8;
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:8;
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:8;
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 4;
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 4;
( 0 <= (a + c) ^2 & 0 <= (d + b) ^2 )
by XREAL_1:65;
then
0 + 0 <= ((a + c) ^2 ) + ((d + b) ^2 )
by XREAL_1:9;
then
sqrt (((a + c) ^2 ) + ((d + b) ^2 )) <= sqrt (((sqrt ((a ^2 ) + (b ^2 ))) + (sqrt ((c ^2 ) + (d ^2 )))) ^2 )
by A7, SQUARE_1:94;
hence
sqrt (((a + c) ^2 ) + ((b + d) ^2 )) <= (sqrt ((a ^2 ) + (b ^2 ))) + (sqrt ((c ^2 ) + (d ^2 )))
by A6, SQUARE_1:89; verum