let a, b, c be real positive number ; :: thesis: ( (a + b) + c = 1 implies (((1 / a) - 1) * ((1 / b) - 1)) * ((1 / c) - 1) >= 8 )
assume A1: (a + b) + c = 1 ; :: thesis: (((1 / a) - 1) * ((1 / b) - 1)) * ((1 / c) - 1) >= 8
then A2: (((1 / a) - 1) * ((1 / b) - 1)) * ((1 / c) - 1) = (((b + c) / a) * ((1 / b) - 1)) * ((1 / c) - 1) by Lm17
.= (((b + c) / a) * ((a + c) / b)) * ((1 / c) - 1) by A1, Lm17
.= (((b + c) / a) * ((a + c) / b)) * ((((a + b) / c) + (c / c)) - 1) by A1, XCMPLX_1:63
.= (((b + c) / a) * ((a + c) / b)) * ((((a + b) / c) + 1) - 1) by XCMPLX_1:60
.= (((b + c) / a) * ((a + c) / b)) * ((a + b) / c) ;
A3: ( (b + c) / a >= (2 * (sqrt (b * c))) / a & (a + c) / b >= (2 * (sqrt (a * c))) / b & (a + b) / c >= (2 * (sqrt (a * b))) / c ) by SIN_COS2:1, XREAL_1:74;
( sqrt (b * c) > 0 & sqrt (a * c) > 0 & sqrt (a * b) > 0 ) by SQUARE_1:93;
then ( 2 * (sqrt (b * c)) > 0 & 2 * (sqrt (a * c)) > 0 & 2 * (sqrt (a * b)) > 0 ) ;
then A4: ( (2 * (sqrt (b * c))) / a > 0 & (2 * (sqrt (a * c))) / b > 0 & (2 * (sqrt (a * b))) / c > 0 ) ;
then A5: ((b + c) / a) * ((a + c) / b) >= ((2 * (sqrt (b * c))) / a) * ((2 * (sqrt (a * c))) / b) by A3, XREAL_1:68;
(((1 / a) - 1) * ((1 / b) - 1)) * ((1 / c) - 1) >= (((2 * (sqrt (b * c))) / a) * ((2 * (sqrt (a * c))) / b)) * ((2 * (sqrt (a * b))) / c) by A2, A3, A4, A5, XREAL_1:68;
hence (((1 / a) - 1) * ((1 / b) - 1)) * ((1 / c) - 1) >= 8 by Lm18; :: thesis: verum