let a, b, c be positive Real; ( 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 that
A1:
a + b > c
and
A2:
b + c > a
and
A3:
a + c > b
; ((1 / ((a + b) - c)) + (1 / ((b + c) - a))) + (1 / ((c + a) - b)) >= 9 / ((a + b) + c)
A4:
(a + c) - b > 0
by A3, XREAL_1:50;
set f = (c + a) - b;
set e = (b + c) - a;
set d = (a + b) - c;
A5:
(b + c) - a > 0
by A2, XREAL_1:50;
A6:
(a + b) - c > 0
by A1, XREAL_1:50;
then A7:
(((a + b) - c) + ((b + c) - a)) + ((c + a) - b) >= 3 * (3 -root ((((a + b) - c) * ((b + c) - a)) * ((c + a) - b)))
by A5, A4, SERIES_3:15;
((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 A6, A5, A4, SERIES_3:15;
then A8:
((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;
A9:
3 -root ((((a + b) - c) * ((b + c) - a)) * ((c + a) - b)) >= 0
by A6, A5, A4, POWER:7;
3 -root (1 / ((((a + b) - c) * ((b + c) - a)) * ((c + a) - b))) >= 0
by A6, A5, A4, POWER:7;
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 A7, A9, A8, XREAL_1:66;
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, A5, A4, POWER:11;
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:79;
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, A5, A4, 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:6;
hence
((1 / ((a + b) - c)) + (1 / ((b + c) - a))) + (1 / ((c + a) - b)) >= 9 / ((a + b) + c)
by XREAL_1:79; verum