let a, b, c be real positive number ; :: thesis: ( (a + b) + c = 1 implies ((1 + (1 / a)) * (1 + (1 / b))) * (1 + (1 / c)) >= 64 )
assume A1: (a + b) + c = 1 ; :: thesis: ((1 + (1 / a)) * (1 + (1 / b))) * (1 + (1 / c)) >= 64
then A2: ((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 A1, Lm19
.= ((2 + ((b + c) / a)) * (2 + ((a + c) / b))) * (1 + (((a + b) / c) + (c / c))) by A1, XCMPLX_1:63
.= ((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)) ;
( (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;
then ( 2 + ((b + c) / a) >= 2 + ((2 * (sqrt (b * c))) / a) & 2 + ((a + c) / b) >= 2 + ((2 * (sqrt (a * c))) / b) & 2 + ((a + b) / c) >= 2 + ((2 * (sqrt (a * b))) / c) ) by XREAL_1:8;
then A3: ( 2 + ((b + c) / a) >= 2 + (2 * ((sqrt (b * c)) / a)) & 2 + ((a + c) / b) >= 2 + (2 * ((sqrt (a * c)) / b)) & 2 + ((a + b) / c) >= 2 + (2 * ((sqrt (a * b)) / c)) ) by XCMPLX_1:75;
( sqrt (b * c) > 0 & sqrt (a * c) > 0 & sqrt (a * b) > 0 ) by SQUARE_1:93;
then ( (sqrt (b * c)) / a > 0 & (sqrt (a * c)) / b > 0 & (sqrt (a * b)) / c > 0 ) ;
then ( 2 * ((sqrt (b * c)) / a) > 0 & 2 * ((sqrt (a * c)) / b) > 0 & 2 * ((sqrt (a * b)) / c) > 0 ) ;
then A4: ( 2 + (2 * ((sqrt (b * c)) / a)) > 0 & 2 + (2 * ((sqrt (a * c)) / b)) > 0 & 2 + (2 * ((sqrt (a * b)) / c)) > 0 ) ;
then A5: (2 + ((b + c) / a)) * (2 + ((a + c) / b)) >= (2 * (1 + ((sqrt (b * c)) / a))) * (2 * (1 + ((sqrt (a * c)) / b))) by A3, XREAL_1:68;
((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 A3, A4, A5, XREAL_1:68;
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 A2;
then A6: ((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;
((((((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:8;
then 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:66;
hence ((1 + (1 / a)) * (1 + (1 / b))) * (1 + (1 / c)) >= 64 by A6, XXREAL_0:2; :: thesis: verum