let a, b be positive Real; (a + (1 / a)) * (b + (1 / b)) >= ((sqrt (a * b)) + (1 / (sqrt (a * b)))) ^2
A1:
sqrt (a * b) > 0
by SQUARE_1:25;
A2: (a + (1 / a)) * (b + (1 / b)) =
(((a * b) + (a * (1 / b))) + ((1 / a) * b)) + ((1 / a) * (1 / b))
.=
(((a * b) + ((a * 1) / b)) + ((1 / a) * b)) + ((1 / a) * (1 / b))
by XCMPLX_1:74
.=
(((a * b) + ((a * 1) / b)) + ((b * 1) / a)) + ((1 / a) * (1 / b))
by XCMPLX_1:74
.=
(((a * b) + ((a * 1) / b)) + ((b * 1) / a)) + ((1 * 1) / (a * b))
by XCMPLX_1:76
.=
(((a * b) + (a / b)) + (b / a)) + (1 / (a * b))
;
(a / b) + (b / a) >= 2 * (sqrt ((a / b) * (b / a)))
by SIN_COS2:1;
then
(a / b) + (b / a) >= 2 * (sqrt ((a * b) / (b * a)))
by XCMPLX_1:76;
then
(a / b) + (b / a) >= 2 * 1
by SQUARE_1:18, XCMPLX_1:60;
then A3:
((a / b) + (b / a)) + ((a * b) + (1 / (a * b))) >= 2 + ((a * b) + (1 / (a * b)))
by XREAL_1:6;
((sqrt (a * b)) + (1 / (sqrt (a * b)))) ^2 =
(((sqrt (a * b)) ^2) + ((2 * (sqrt (a * b))) * (1 / (sqrt (a * b))))) + ((1 / (sqrt (a * b))) ^2)
.=
((a * b) + ((2 * (sqrt (a * b))) * (1 / (sqrt (a * b))))) + ((1 / (sqrt (a * b))) ^2)
by SQUARE_1:def 2
.=
((a * b) + ((2 * (sqrt (a * b))) * (1 / (sqrt (a * b))))) + ((1 ^2) / ((sqrt (a * b)) ^2))
by XCMPLX_1:76
.=
((a * b) + (2 * ((sqrt (a * b)) * (1 / (sqrt (a * b)))))) + (1 / (a * b))
by SQUARE_1:def 2
.=
((a * b) + (2 * (((sqrt (a * b)) * 1) / (sqrt (a * b))))) + (1 / (a * b))
by XCMPLX_1:74
.=
((a * b) + (2 * 1)) + (1 / (a * b))
by A1, XCMPLX_1:60
.=
((a * b) + 2) + (1 / (a * b))
;
hence
(a + (1 / a)) * (b + (1 / b)) >= ((sqrt (a * b)) + (1 / (sqrt (a * b)))) ^2
by A2, A3; verum