let a, b be real positive number ; :: thesis: ( a + b = 1 implies (a + (1 / a)) * (b + (1 / b)) >= 25 / 4 )
assume A1: a + b = 1 ; :: thesis: (a + (1 / a)) * (b + (1 / b)) >= 25 / 4
(a ^2 ) + (b ^2 ) = (((a ^2 ) + ((2 * a) * b)) + (b ^2 )) - ((2 * a) * b) ;
then A2: (a ^2 ) + (b ^2 ) = (1 ^2 ) - ((2 * a) * b) by A1, SQUARE_1:63;
A3: (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 A2
.= (1 + ((1 - (a * b)) ^2 )) / (a * b) ;
(1 - (a * b)) ^2 >= 0 by XREAL_1:65;
then A4: 1 + ((1 - (a * b)) ^2 ) >= 1 + 0 by XREAL_1:8;
A5: a * b <= (1 / 2) ^2 by A1, Th4;
then A6: (1 + ((1 - (a * b)) ^2 )) / (a * b) >= (1 + ((1 - (a * b)) ^2 )) / (1 / 4) by A4, XREAL_1:120;
1 - (a * b) >= 1 - (1 / 4) by A5, 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 4 * (1 + ((1 - (a * b)) ^2 )) >= 4 * (25 / 16) by XREAL_1:66;
hence (a + (1 / a)) * (b + (1 / b)) >= 25 / 4 by A3, A6, XXREAL_0:2; :: thesis: verum