let a, b be positive Real; (a + b) * ((1 / a) + (1 / b)) >= 4
(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 * (sqrt (((a / b) * b) / a))
by XCMPLX_1:83;
then
(a / b) + (b / a) >= 2 * (sqrt (a / a))
by XCMPLX_1:87;
then
(a / b) + (b / a) >= 2 * 1
by SQUARE_1:18, XCMPLX_1:60;
then
((a / b) + (b / a)) + 2 >= 2 + 2
by XREAL_1:7;
then
(((a / b) + (b / a)) + 1) + 1 >= 4
;
then
(((a * (1 / b)) + (b / a)) + 1) + 1 >= 4
by XCMPLX_1:99;
then
(((a * (1 / b)) + (b * (1 / a))) + 1) + 1 >= 4
by XCMPLX_1:99;
then
(((a * (1 / b)) + (b * (1 / a))) + (a * (1 / a))) + 1 >= 4
by XCMPLX_1:106;
then
(((a * (1 / b)) + (b * (1 / a))) + (a * (1 / a))) + (b * (1 / b)) >= 4
by XCMPLX_1:106;
hence
(a + b) * ((1 / a) + (1 / b)) >= 4
; verum