let a, b, c be real positive number ; :: thesis: ( a + b > c & b + c > a & a + c > b implies ((1 / ((a + b) - c)) + (1 / ((b + c) - a))) + (1 / ((c + a) - b)) >= 9 / ((a + b) + c) )
assume ( a + b > c & b + c > a & a + c > b ) ; :: thesis: ((1 / ((a + b) - c)) + (1 / ((b + c) - a))) + (1 / ((c + a) - b)) >= 9 / ((a + b) + c)
then A1: ( (a + b) - c > 0 & (b + c) - a > 0 & (a + c) - b > 0 ) by XREAL_1:52;
set d = (a + b) - c;
set e = (b + c) - a;
set f = (c + a) - b;
A2: ( 1 / ((a + b) - c) > 0 & 1 / ((b + c) - a) > 0 & 1 / ((c + a) - b) > 0 ) by A1;
then (1 / ((a + b) - c)) * (1 / ((b + c) - a)) > 0 ;
then (1 * 1) / (((a + b) - c) * ((b + c) - a)) > 0 by XCMPLX_1:77;
then ((1 * 1) / (((a + b) - c) * ((b + c) - a))) * (1 / ((c + a) - b)) > 0 by A2;
then 1 / ((((a + b) - c) * ((b + c) - a)) * ((c + a) - b)) > 0 by XCMPLX_1:77;
then 3 -root (1 / ((((a + b) - c) * ((b + c) - a)) * ((c + a) - b))) >= 0 by POWER:8;
then A4: 3 * (3 -root (1 / ((((a + b) - c) * ((b + c) - a)) * ((c + a) - b)))) >= 0 ;
A5: (((a + b) - c) + ((b + c) - a)) + ((c + a) - b) >= 3 * (3 -root ((((a + b) - c) * ((b + c) - a)) * ((c + a) - b))) by A1, SERIES_3:15;
A6: (((a + b) - c) * ((b + c) - a)) * ((c + a) - b) > 0 by A1;
then 3 -root ((((a + b) - c) * ((b + c) - a)) * ((c + a) - b)) >= 0 by POWER:8;
then A7: 3 * (3 -root ((((a + b) - c) * ((b + c) - a)) * ((c + a) - b))) >= 0 ;
((1 / ((a + b) - c)) + (1 / ((b + c) - a))) + (1 / ((c + a) - b)) >= 3 * (3 -root (((1 / ((a + b) - c)) * (1 / ((b + c) - a))) * (1 / ((c + a) - b)))) by A2, SERIES_3:15;
then ((1 / ((a + b) - c)) + (1 / ((b + c) - a))) + (1 / ((c + a) - b)) >= 3 * (3 -root (1 / ((((a + b) - c) * ((b + c) - a)) * ((c + a) - b)))) by Lm3;
then ((((a + b) - c) + ((b + c) - a)) + ((c + a) - b)) * (((1 / ((a + b) - c)) + (1 / ((b + c) - a))) + (1 / ((c + a) - b))) >= (3 * (3 -root ((((a + b) - c) * ((b + c) - a)) * ((c + a) - b)))) * (3 * (3 -root (1 / ((((a + b) - c) * ((b + c) - a)) * ((c + a) - b))))) by A4, A5, A7, XREAL_1:68;
then ((((a + b) - c) + ((b + c) - a)) + ((c + a) - b)) * (((1 / ((a + b) - c)) + (1 / ((b + c) - a))) + (1 / ((c + a) - b))) >= 9 * ((3 -root ((((a + b) - c) * ((b + c) - a)) * ((c + a) - b))) * (3 -root (1 / ((((a + b) - c) * ((b + c) - a)) * ((c + a) - b))))) ;
then ((((a + b) - c) + ((b + c) - a)) + ((c + a) - b)) * (((1 / ((a + b) - c)) + (1 / ((b + c) - a))) + (1 / ((c + a) - b))) >= 9 * (3 -root (((((a + b) - c) * ((b + c) - a)) * ((c + a) - b)) * (1 / ((((a + b) - c) * ((b + c) - a)) * ((c + a) - b))))) by A6, POWER:12;
then ((((a + b) - c) + ((b + c) - a)) + ((c + a) - b)) * (((1 / ((a + b) - c)) + (1 / ((b + c) - a))) + (1 / ((c + a) - b))) >= 9 * (3 -root (((((a + b) - c) * ((b + c) - a)) * ((c + a) - b)) / (((((a + b) - c) * ((b + c) - a)) * ((c + a) - b)) / 1))) by XCMPLX_1:80;
then ((((a + b) - c) + ((b + c) - a)) + ((c + a) - b)) * (((1 / ((a + b) - c)) + (1 / ((b + c) - a))) + (1 / ((c + a) - b))) >= 9 * (3 -root 1) by A6, XCMPLX_1:60;
then ((((a + b) - c) + ((b + c) - a)) + ((c + a) - b)) * (((1 / ((a + b) - c)) + (1 / ((b + c) - a))) + (1 / ((c + a) - b))) >= 9 * 1 by POWER:7;
hence ((1 / ((a + b) - c)) + (1 / ((b + c) - a))) + (1 / ((c + a) - b)) >= 9 / ((a + b) + c) by XREAL_1:81; :: thesis: verum