let a, b, c be positive Real; ( (a + b) + c = 1 implies ((1 / a) + (1 / b)) + (1 / c) >= 9 )
assume A1:
(a + b) + c = 1
; ((1 / a) + (1 / b)) + (1 / c) >= 9
A2:
3 -root ((a * b) * c) >= 0
by POWER:7;
((1 / a) + (1 / b)) + (1 / c) >= 3 * (3 -root (((1 / a) * (1 / b)) * (1 / c)))
by SERIES_3:15;
then A3:
((1 / a) + (1 / b)) + (1 / c) >= 3 * (3 -root (1 / ((a * b) * c)))
by Lm3;
A4:
3 -root (1 / ((a * b) * c)) >= 0
by POWER:7;
(a + b) + c >= 3 * (3 -root ((a * b) * c))
by SERIES_3:15;
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:66;
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:11;
then
((1 / a) + (1 / b)) + (1 / c) >= 9 * (3 -root (((a * b) * c) / (((a * b) * c) / 1)))
by XCMPLX_1:79;
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:6;
hence
((1 / a) + (1 / b)) + (1 / c) >= 9
; verum