let a, b, c be positive Real; (((9 * a) * b) * c) / (((a ^2) + (b ^2)) + (c ^2)) <= (a + b) + c
A1:
(b ^2) * (a + c) >= (b ^2) * (2 * (sqrt (a * c)))
by SIN_COS2:1, XREAL_1:64;
A2:
(c ^2) * (a + b) >= (c ^2) * (2 * (sqrt (a * b)))
by SIN_COS2:1, XREAL_1:64;
A3:
sqrt (a * b) > 0
by SQUARE_1:25;
A4:
sqrt (a * c) > 0
by SQUARE_1:25;
sqrt (b * c) > 0
by SQUARE_1:25;
then
(((2 * (a ^2)) * (sqrt (b * c))) + ((2 * (b ^2)) * (sqrt (a * c)))) + ((2 * (c ^2)) * (sqrt (a * b))) >= 3 * (3 -root ((((2 * (a ^2)) * (sqrt (b * c))) * ((2 * (b ^2)) * (sqrt (a * c)))) * ((2 * (c ^2)) * (sqrt (a * b)))))
by A4, A3, SERIES_3:15;
then
(((2 * (a ^2)) * (sqrt (b * c))) + ((2 * (b ^2)) * (sqrt (a * c)))) + ((2 * (c ^2)) * (sqrt (a * b))) >= 3 * (3 -root ((((((((2 * (a ^2)) * (sqrt (b * c))) * 2) * (b ^2)) * (sqrt (a * c))) * 2) * (c ^2)) * (sqrt (a * b))))
;
then
(((2 * (a ^2)) * (sqrt (b * c))) + ((2 * (b ^2)) * (sqrt (a * c)))) + ((2 * (c ^2)) * (sqrt (a * b))) >= 3 * (3 -root ((((2 * a) * b) * c) |^ 3))
by Lm9;
then A5:
(((2 * (a ^2)) * (sqrt (b * c))) + ((2 * (b ^2)) * (sqrt (a * c)))) + ((2 * (c ^2)) * (sqrt (a * b))) >= 3 * (((2 * a) * b) * c)
by POWER:4;
A6:
((a |^ 3) + (b |^ 3)) + (c |^ 3) >= ((3 * a) * b) * c
by SERIES_3:12;
(a ^2) * (b + c) >= (a ^2) * (2 * (sqrt (b * c)))
by SIN_COS2:1, XREAL_1:64;
then
((a ^2) * (b + c)) + ((b ^2) * (a + c)) >= ((a ^2) * (2 * (sqrt (b * c)))) + ((b ^2) * (2 * (sqrt (a * c))))
by A1, XREAL_1:7;
then
(((a ^2) * (b + c)) + ((b ^2) * (a + c))) + ((c ^2) * (a + b)) >= (((2 * (a ^2)) * (sqrt (b * c))) + ((2 * (b ^2)) * (sqrt (a * c)))) + ((2 * (c ^2)) * (sqrt (a * b)))
by A2, XREAL_1:7;
then
(((((a * (b ^2)) + (a * (c ^2))) + (b * (a ^2))) + (b * (c ^2))) + (c * (a ^2))) + (c * (b ^2)) >= ((6 * a) * b) * c
by A5, XXREAL_0:2;
then A7:
(((a |^ 3) + (b |^ 3)) + (c |^ 3)) + ((((((a * (b ^2)) + (a * (c ^2))) + (b * (a ^2))) + (b * (c ^2))) + (c * (a ^2))) + (c * (b ^2))) >= (((3 * a) * b) * c) + (((6 * a) * b) * c)
by A6, XREAL_1:7;
(((a ^2) + (b ^2)) + (c ^2)) * ((a + b) + c) =
((((((((a * (a ^2)) + (a * (b ^2))) + (a * (c ^2))) + (b * (a ^2))) + (b * (b ^2))) + (b * (c ^2))) + (c * (a ^2))) + (c * (b ^2))) + (c * (c ^2))
.=
((((((((a * (a |^ 2)) + (a * (b ^2))) + (a * (c ^2))) + (b * (a ^2))) + (b * (b ^2))) + (b * (c ^2))) + (c * (a ^2))) + (c * (b ^2))) + (c * (c ^2))
by NEWTON:81
.=
((((((((a |^ (2 + 1)) + (a * (b ^2))) + (a * (c ^2))) + (b * (a ^2))) + (b * (b ^2))) + (b * (c ^2))) + (c * (a ^2))) + (c * (b ^2))) + (c * (c ^2))
by NEWTON:6
.=
((((((((a |^ 3) + (a * (b ^2))) + (a * (c ^2))) + (b * (a ^2))) + (b * (b |^ 2))) + (b * (c ^2))) + (c * (a ^2))) + (c * (b ^2))) + (c * (c ^2))
by NEWTON:81
.=
((((((((a |^ 3) + (a * (b ^2))) + (a * (c ^2))) + (b * (a ^2))) + (b |^ (2 + 1))) + (b * (c ^2))) + (c * (a ^2))) + (c * (b ^2))) + (c * (c ^2))
by NEWTON:6
.=
((((((((a |^ 3) + (a * (b ^2))) + (a * (c ^2))) + (b * (a ^2))) + (b |^ 3)) + (b * (c ^2))) + (c * (a ^2))) + (c * (b ^2))) + (c * (c |^ 2))
by NEWTON:81
.=
((((((((a |^ 3) + (a * (b ^2))) + (a * (c ^2))) + (b * (a ^2))) + (b |^ 3)) + (b * (c ^2))) + (c * (a ^2))) + (c * (b ^2))) + (c |^ (2 + 1))
by NEWTON:6
.=
((((((((a |^ 3) + (b |^ 3)) + (c |^ 3)) + (a * (b ^2))) + (a * (c ^2))) + (b * (a ^2))) + (b * (c ^2))) + (c * (a ^2))) + (c * (b ^2))
;
then
(((a + b) + c) * (((a ^2) + (b ^2)) + (c ^2))) / (((a ^2) + (b ^2)) + (c ^2)) >= (((9 * a) * b) * c) / (((a ^2) + (b ^2)) + (c ^2))
by A7, XREAL_1:72;
then
((a + b) + c) / ((((a ^2) + (b ^2)) + (c ^2)) / (((a ^2) + (b ^2)) + (c ^2))) >= (((9 * a) * b) * c) / (((a ^2) + (b ^2)) + (c ^2))
by XCMPLX_1:77;
then
((a + b) + c) / 1 >= (((9 * a) * b) * c) / (((a ^2) + (b ^2)) + (c ^2))
by XCMPLX_1:60;
hence
(((9 * a) * b) * c) / (((a ^2) + (b ^2)) + (c ^2)) <= (a + b) + c
; verum