let a, b be positive Real; ( a + b = 1 implies (a * b) + (1 / (a * b)) >= 17 / 4 )
A1:
sqrt (a * b) > 0
by SQUARE_1:25;
assume
a + b = 1
; (a * b) + (1 / (a * b)) >= 17 / 4
then
1 ^2 >= (2 * (sqrt (a * b))) ^2
by A1, SIN_COS2:1, SQUARE_1:15;
then
1 >= (2 * 2) * ((sqrt (a * b)) ^2)
;
then
1 >= 4 * (a * b)
by SQUARE_1:def 2;
then A2:
1 / 4 >= ((a * b) * 4) / 4
by XREAL_1:72;
then
(1 / 4) * (- 1) <= (a * b) * (- 1)
by XREAL_1:65;
then
(- (1 / 4)) + 1 <= (- (a * b)) + 1
by XREAL_1:7;
then
(3 / 4) ^2 <= (1 - (a * b)) ^2
by SQUARE_1:15;
then
(9 / (4 ^2)) / (1 / 4) <= ((1 - (a * b)) ^2) / (1 / 4)
by XREAL_1:72;
then A3:
(9 / 4) + (8 / 4) <= (((1 - (a * b)) ^2) * 4) + 2
by XREAL_1:7;
(1 - (a * b)) ^2 >= 0
by XREAL_1:63;
then
((1 - (a * b)) ^2) / (1 / 4) <= ((1 - (a * b)) ^2) / (a * b)
by A2, XREAL_1:118;
then A4:
(((1 - (a * b)) ^2) * 4) + 2 <= (((1 - (a * b)) ^2) / (a * b)) + 2
by XREAL_1:7;
(1 / (a * b)) + (a * b) =
(1 + ((a * b) * (a * b))) / (a * b)
by XCMPLX_1:113
.=
((((1 ^2) - ((2 * 1) * (a * b))) + ((a * b) ^2)) + (2 * (a * b))) / (a * b)
.=
(((1 - (a * b)) ^2) / (a * b)) + ((2 * (a * b)) / (a * b))
by XCMPLX_1:62
.=
(((1 - (a * b)) ^2) / (a * b)) + (2 * ((a * b) / (a * b)))
by XCMPLX_1:74
.=
(((1 - (a * b)) ^2) / (a * b)) + (2 * 1)
by XCMPLX_1:60
.=
(((1 - (a * b)) ^2) / (a * b)) + 2
;
hence
(a * b) + (1 / (a * b)) >= 17 / 4
by A4, A3, XXREAL_0:2; verum