let a, b be real positive number ; ( 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:12;
then
(1 - (a * b)) ^2 >= (3 / 4) ^2
by SQUARE_1:77;
then
1 + ((1 - (a * b)) ^2 ) >= 1 + (9 / 16)
by XREAL_1:8;
then A3:
4 * (1 + ((1 - (a * b)) ^2 )) >= 4 * (25 / 16)
by XREAL_1:66;
(1 - (a * b)) ^2 >= 0
by XREAL_1:65;
then A4:
(1 + ((1 - (a * b)) ^2 )) / (a * b) >= (1 + ((1 - (a * b)) ^2 )) / (1 / 4)
by A2, XREAL_1:120;
(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:63;
(a + (1 / a)) * (b + (1 / b)) =
((1 + (a ^2 )) / a) * (b + (1 / b))
by XCMPLX_1:114
.=
((1 + (a ^2 )) / a) * ((1 + (b ^2 )) / b)
by XCMPLX_1:114
.=
((1 + (a ^2 )) * (1 + (b ^2 ))) / (a * b)
by XCMPLX_1:77
.=
(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