let a, b be positive Real; ( a + b = 1 implies (a + (1 / a)) * (b + (1 / b)) >= 25 / 4 )
assume A1:
a + b = 1
; (a + (1 / a)) * (b + (1 / b)) >= 25 / 4
then A2:
a * b <= (1 / 2) ^2
by Th4;
then
1 - (a * b) >= 1 - (1 / 4)
by XREAL_1:10;
then
(1 - (a * b)) ^2 >= (3 / 4) ^2
by SQUARE_1:15;
then
1 + ((1 - (a * b)) ^2) >= 1 + (9 / 16)
by XREAL_1:6;
then A3:
4 * (1 + ((1 - (a * b)) ^2)) >= 4 * (25 / 16)
by XREAL_1:64;
(1 - (a * b)) ^2 >= 0
by XREAL_1:63;
then A4:
(1 + ((1 - (a * b)) ^2)) / (a * b) >= (1 + ((1 - (a * b)) ^2)) / (1 / 4)
by A2, XREAL_1:118;
(a ^2) + (b ^2) = (((a ^2) + ((2 * a) * b)) + (b ^2)) - ((2 * a) * b)
;
then A5:
(a ^2) + (b ^2) = (1 ^2) - ((2 * a) * b)
by A1, SQUARE_1:4;
(a + (1 / a)) * (b + (1 / b)) =
((1 + (a ^2)) / a) * (b + (1 / b))
by XCMPLX_1:113
.=
((1 + (a ^2)) / a) * ((1 + (b ^2)) / b)
by XCMPLX_1:113
.=
((1 + (a ^2)) * (1 + (b ^2))) / (a * b)
by XCMPLX_1:76
.=
(1 + (((1 ^2) - (2 * (a * b))) + ((a ^2) * (b ^2)))) / (a * b)
by A5
.=
(1 + ((1 - (a * b)) ^2)) / (a * b)
;
hence
(a + (1 / a)) * (b + (1 / b)) >= 25 / 4
by A4, A3, XXREAL_0:2; verum