let a, b, c be real positive number ; :: thesis: ( (a + b) + c = 1 implies ((1 / a) + (1 / b)) + (1 / c) >= 9 )
assume A1: (a + b) + c = 1 ; :: thesis: ((1 / a) + (1 / b)) + (1 / c) >= 9
A2: (a + b) + c >= 3 * (3 -root ((a * b) * c)) by SERIES_3:15;
3 -root ((a * b) * c) >= 0 by POWER:8;
then A3: 3 * (3 -root ((a * b) * c)) >= 0 ;
((1 / a) + (1 / b)) + (1 / c) >= 3 * (3 -root (((1 / a) * (1 / b)) * (1 / c))) by SERIES_3:15;
then A4: ((1 / a) + (1 / b)) + (1 / c) >= 3 * (3 -root (1 / ((a * b) * c))) by Lm3;
3 -root (1 / ((a * b) * c)) >= 0 by POWER:8;
then 3 * (3 -root (1 / ((a * b) * c))) >= 0 ;
then ((a + b) + c) * (((1 / a) + (1 / b)) + (1 / c)) >= (3 * (3 -root ((a * b) * c))) * (3 * (3 -root (1 / ((a * b) * c)))) by A2, A3, A4, XREAL_1:68;
then ((1 / a) + (1 / b)) + (1 / c) >= 9 * ((3 -root ((a * b) * c)) * (3 -root (1 / ((a * b) * c)))) by A1;
then ((1 / a) + (1 / b)) + (1 / c) >= 9 * (3 -root (((a * b) * c) * (1 / ((a * b) * c)))) by POWER:12;
then ((1 / a) + (1 / b)) + (1 / c) >= 9 * (3 -root (((a * b) * c) / (((a * b) * c) / 1))) by XCMPLX_1:80;
then ((1 / a) + (1 / b)) + (1 / c) >= 9 * (3 -root 1) by XCMPLX_1:60;
then ((1 / a) + (1 / b)) + (1 / c) >= 9 * 1 by POWER:7;
hence ((1 / a) + (1 / b)) + (1 / c) >= 9 ; :: thesis: verum