let a, b, c, d be Real; ((a + b) ^2) + ((c + d) ^2) <= ((sqrt ((a ^2) + (c ^2))) + (sqrt ((b ^2) + (d ^2)))) ^2
set A = (a ^2) + (c ^2);
set B = (b ^2) + (d ^2);
set C1 = sqrt ((a ^2) + (c ^2));
set C2 = sqrt ((b ^2) + (d ^2));
A1:
( 0 <= sqrt ((a ^2) + (c ^2)) & 0 <= sqrt ((b ^2) + (d ^2)) )
by SQUARE_1:def 2;
A2:
( (sqrt ((a ^2) + (c ^2))) ^2 = (a ^2) + (c ^2) & (sqrt ((b ^2) + (d ^2))) ^2 = (b ^2) + (d ^2) )
by SQUARE_1:def 2;
A3:
(((a ^2) + ((2 * a) * b)) + (b ^2)) + (((c ^2) + ((2 * c) * d)) + (d ^2)) = ((((a ^2) + (c ^2)) + (b ^2)) + (d ^2)) + (((2 * a) * b) + ((2 * c) * d))
;
A4:
(((a ^2) + (c ^2)) + ((2 * (sqrt ((a ^2) + (c ^2)))) * (sqrt ((b ^2) + (d ^2))))) + ((b ^2) + (d ^2)) = (((a ^2) + (c ^2)) + ((b ^2) + (d ^2))) + ((2 * (sqrt ((a ^2) + (c ^2)))) * (sqrt ((b ^2) + (d ^2))))
;
A5:
((2 * a) * b) + ((2 * c) * d) = 2 * ((a * b) + (c * d))
;
A6:
2 * ((sqrt ((a ^2) + (c ^2))) * (sqrt ((b ^2) + (d ^2)))) = (2 * (sqrt ((a ^2) + (c ^2)))) * (sqrt ((b ^2) + (d ^2)))
;
((a * d) - (c * b)) ^2 = (((a * d) ^2) + ((c * b) ^2)) - ((2 * (a * d)) * (c * b))
;
then A7:
0 + ((2 * (a * d)) * (c * b)) <= ((((a * d) ^2) + ((c * b) ^2)) - ((2 * (a * d)) * (c * b))) + ((2 * (a * d)) * (c * b))
by XREAL_1:6;
A8:
((a ^2) + (c ^2)) * ((b ^2) + (d ^2)) = (sqrt (((a ^2) + (c ^2)) * ((b ^2) + (d ^2)))) ^2
by SQUARE_1:def 2;
(((a ^2) * (b ^2)) + ((c ^2) * (d ^2))) + ((((2 * a) * b) * c) * d) <= (((a ^2) * (b ^2)) + ((c ^2) * (d ^2))) + (((c ^2) * (b ^2)) + ((a ^2) * (d ^2)))
by A7, XREAL_1:6;
then A9:
((a * b) + (c * d)) ^2 <= ((a ^2) + (c ^2)) * ((b ^2) + (d ^2))
;
(sqrt ((a ^2) + (c ^2))) * (sqrt ((b ^2) + (d ^2))) = sqrt (((a ^2) + (c ^2)) * ((b ^2) + (d ^2)))
by SQUARE_1:29;
then
(a * b) + (c * d) <= (sqrt ((a ^2) + (c ^2))) * (sqrt ((b ^2) + (d ^2)))
by A1, A8, A9, SQUARE_1:16;
then
((2 * a) * b) + ((2 * c) * d) <= (2 * (sqrt ((a ^2) + (c ^2)))) * (sqrt ((b ^2) + (d ^2)))
by A5, A6, XREAL_1:64;
hence
((a + b) ^2) + ((c + d) ^2) <= ((sqrt ((a ^2) + (c ^2))) + (sqrt ((b ^2) + (d ^2)))) ^2
by A2, A3, A4, XREAL_1:6; verum