let a, b, c, d be positive Real; sqrt ((a + b) * (c + d)) >= (sqrt (a * c)) + (sqrt (b * d))
A1:
sqrt ((a + b) * (c + d)) > 0
by SQUARE_1:25;
A2:
sqrt (b * d) > 0
by SQUARE_1:25;
(a * d) + (b * c) >= 2 * (sqrt ((a * d) * (b * c)))
by SIN_COS2:1;
then
((a * d) + (b * c)) + ((a * c) + (b * d)) >= (2 * (sqrt ((a * d) * (b * c)))) + ((a * c) + (b * d))
by XREAL_1:7;
then
(a + b) * (c + d) >= ((2 * (sqrt ((a * d) * (b * c)))) + (a * c)) + (b * d)
;
then
(a + b) * (c + d) >= ((2 * (sqrt ((a * d) * (b * c)))) + ((sqrt (a * c)) ^2)) + (b * d)
by SQUARE_1:def 2;
then
(a + b) * (c + d) >= ((2 * (sqrt ((a * d) * (b * c)))) + ((sqrt (a * c)) ^2)) + ((sqrt (b * d)) ^2)
by SQUARE_1:def 2;
then
(sqrt ((a + b) * (c + d))) ^2 >= ((2 * (sqrt ((a * c) * (b * d)))) + ((sqrt (a * c)) ^2)) + ((sqrt (b * d)) ^2)
by SQUARE_1:def 2;
then A3:
(sqrt ((a + b) * (c + d))) ^2 >= (((sqrt (a * c)) ^2) + (2 * ((sqrt (a * c)) * (sqrt (b * d))))) + ((sqrt (b * d)) ^2)
by SQUARE_1:29;
((sqrt (a * c)) + (sqrt (b * d))) ^2 >= 0
by XREAL_1:63;
then A4:
sqrt ((sqrt ((a + b) * (c + d))) ^2) >= sqrt (((sqrt (a * c)) + (sqrt (b * d))) ^2)
by A3, SQUARE_1:26;
sqrt (a * c) > 0
by SQUARE_1:25;
then
sqrt ((sqrt ((a + b) * (c + d))) ^2) >= (sqrt (a * c)) + (sqrt (b * d))
by A4, A2, SQUARE_1:22;
hence
sqrt ((a + b) * (c + d)) >= (sqrt (a * c)) + (sqrt (b * d))
by A1, SQUARE_1:22; verum