let a, b, c be positive Real; ( (a + b) + c = 1 implies ((1 + (1 / a)) * (1 + (1 / b))) * (1 + (1 / c)) >= 64 )
A1:
sqrt (b * c) > 0
by SQUARE_1:25;
(a + b) / c >= (2 * (sqrt (a * b))) / c
by SIN_COS2:1, XREAL_1:72;
then
2 + ((a + b) / c) >= 2 + ((2 * (sqrt (a * b))) / c)
by XREAL_1:6;
then A2:
2 + ((a + b) / c) >= 2 + (2 * ((sqrt (a * b)) / c))
by XCMPLX_1:74;
A3:
sqrt (a * b) > 0
by SQUARE_1:25;
(a + c) / b >= (2 * (sqrt (a * c))) / b
by SIN_COS2:1, XREAL_1:72;
then
2 + ((a + c) / b) >= 2 + ((2 * (sqrt (a * c))) / b)
by XREAL_1:6;
then A4:
2 + ((a + c) / b) >= 2 + (2 * ((sqrt (a * c)) / b))
by XCMPLX_1:74;
A5:
sqrt (a * c) > 0
by SQUARE_1:25;
(b + c) / a >= (2 * (sqrt (b * c))) / a
by SIN_COS2:1, XREAL_1:72;
then
2 + ((b + c) / a) >= 2 + ((2 * (sqrt (b * c))) / a)
by XREAL_1:6;
then
2 + ((b + c) / a) >= 2 + (2 * ((sqrt (b * c)) / a))
by XCMPLX_1:74;
then
(2 + ((b + c) / a)) * (2 + ((a + c) / b)) >= (2 * (1 + ((sqrt (b * c)) / a))) * (2 * (1 + ((sqrt (a * c)) / b)))
by A4, A1, A5, XREAL_1:66;
then A6:
((2 + ((b + c) / a)) * (2 + ((a + c) / b))) * (2 + ((a + b) / c)) >= ((2 * (1 + ((sqrt (b * c)) / a))) * (2 * (1 + ((sqrt (a * c)) / b)))) * (2 * (1 + ((sqrt (a * b)) / c)))
by A2, A1, A5, A3, XREAL_1:66;
((((((sqrt (a * c)) / b) + (b / (sqrt (a * c)))) + ((sqrt (a * b)) / c)) + (c / (sqrt (b * a)))) + (a / (sqrt (b * c)))) + ((sqrt (b * c)) / a) >= 6
by Lm23;
then
2 + (((((((sqrt (a * c)) / b) + (b / (sqrt (a * c)))) + ((sqrt (a * b)) / c)) + (c / (sqrt (b * a)))) + (a / (sqrt (b * c)))) + ((sqrt (b * c)) / a)) >= 6 + 2
by XREAL_1:6;
then A7:
8 * ((((((2 + ((sqrt (a * c)) / b)) + (b / (sqrt (a * c)))) + ((sqrt (a * b)) / c)) + (c / (sqrt (b * a)))) + (a / (sqrt (b * c)))) + ((sqrt (b * c)) / a)) >= 8 * 8
by XREAL_1:64;
assume A8:
(a + b) + c = 1
; ((1 + (1 / a)) * (1 + (1 / b))) * (1 + (1 / c)) >= 64
then ((1 + (1 / a)) * (1 + (1 / b))) * (1 + (1 / c)) =
((2 + ((b + c) / a)) * (1 + (1 / b))) * (1 + (1 / c))
by Lm19
.=
((2 + ((b + c) / a)) * (2 + ((a + c) / b))) * (1 + (1 / c))
by A8, Lm19
.=
((2 + ((b + c) / a)) * (2 + ((a + c) / b))) * (1 + (((a + b) / c) + (c / c)))
by A8, XCMPLX_1:62
.=
((2 + ((b + c) / a)) * (2 + ((a + c) / b))) * ((1 + ((a + b) / c)) + 1)
by XCMPLX_1:60
.=
((2 + ((b + c) / a)) * (2 + ((a + c) / b))) * (2 + ((a + b) / c))
;
then
((1 + (1 / a)) * (1 + (1 / b))) * (1 + (1 / c)) >= 8 * (((1 + ((sqrt (b * c)) / a)) * (1 + ((sqrt (a * c)) / b))) * (1 + ((sqrt (a * b)) / c)))
by A6;
then
((1 + (1 / a)) * (1 + (1 / b))) * (1 + (1 / c)) >= 8 * ((((((2 + ((sqrt (a * c)) / b)) + (b / (sqrt (a * c)))) + ((sqrt (a * b)) / c)) + (c / (sqrt (b * a)))) + (a / (sqrt (b * c)))) + ((sqrt (b * c)) / a))
by Lm22;
hence
((1 + (1 / a)) * (1 + (1 / b))) * (1 + (1 / c)) >= 64
by A7, XXREAL_0:2; verum