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