let a, b, c be real positive number ; (((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:66;
A2:
(c ^2 ) * (a + b) >= (c ^2 ) * (2 * (sqrt (a * b)))
by SIN_COS2:1, XREAL_1:66;
A3:
sqrt (a * b) > 0
by SQUARE_1:93;
A4:
sqrt (a * c) > 0
by SQUARE_1:93;
sqrt (b * c) > 0
by SQUARE_1:93;
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:5;
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:66;
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:9;
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:9;
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:9;
(((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:100
.=
((((((((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:11
.=
((((((((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:100
.=
((((((((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:11
.=
((((((((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:100
.=
((((((((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:11
.=
((((((((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:74;
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:78;
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