let a, b be real positive number ; ( a + b = 1 implies ((1 / (a ^2 )) - 1) * ((1 / (b ^2 )) - 1) >= 9 )
assume A1:
a + b = 1
; ((1 / (a ^2 )) - 1) * ((1 / (b ^2 )) - 1) >= 9
sqrt (a * b) > 0
by SQUARE_1:93;
then
1 ^2 >= (2 * (sqrt (a * b))) ^2
by A1, SIN_COS2:1, SQUARE_1:77;
then
1 >= (2 * 2) * ((sqrt (a * b)) ^2 )
;
then
1 >= 4 * (a * b)
by SQUARE_1:def 4;
then
8 / 1 <= 8 / ((4 * a) * b)
by XREAL_1:120;
then
8 <= 8 / (4 * (a * b))
;
then
8 <= (8 / 4) / (a * b)
by XCMPLX_1:79;
then A2:
8 + 1 <= (2 / (a * b)) + 1
by XREAL_1:9;
((1 / (a ^2 )) - 1) * ((1 / (b ^2 )) - 1) =
((1 - (1 * (a ^2 ))) / (a ^2 )) * ((1 / (b ^2 )) - 1)
by XCMPLX_1:127
.=
((1 - (1 * (a ^2 ))) / (a ^2 )) * ((1 - (1 * (b ^2 ))) / (b ^2 ))
by XCMPLX_1:127
.=
(((1 - a) * (1 + a)) * ((1 - b) * (1 + b))) / ((a ^2 ) * (b ^2 ))
by XCMPLX_1:77
;
then ((1 / (a ^2 )) - 1) * ((1 / (b ^2 )) - 1) =
((a * b) * ((1 + a) * (1 + b))) / ((a * b) * (a * b))
by A1
.=
((a * b) / (a * b)) * (((1 + a) * (1 + b)) / (a * b))
by XCMPLX_1:77
.=
1 * (((1 + a) * (1 + b)) / (a * b))
by XCMPLX_1:60
.=
((1 + (a + b)) + (a * b)) / (a * b)
.=
(2 / (a * b)) + ((a * b) / (a * b))
by A1, XCMPLX_1:63
.=
(2 / (a * b)) + 1
by XCMPLX_1:60
;
hence
((1 / (a ^2 )) - 1) * ((1 / (b ^2 )) - 1) >= 9
by A2; verum