let a, b, c be real positive number ; :: thesis: (((9 * a) * b) * c) / (((a ^2 ) + (b ^2 )) + (c ^2 )) <= (a + b) + c
A1: (((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 )) ;
A2: ( (a ^2 ) * (b + c) >= (a ^2 ) * (2 * (sqrt (b * c))) & (b ^2 ) * (a + c) >= (b ^2 ) * (2 * (sqrt (a * c))) & (c ^2 ) * (a + b) >= (c ^2 ) * (2 * (sqrt (a * b))) ) 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 XREAL_1:9;
then A3: (((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;
( sqrt (b * c) > 0 & sqrt (a * c) > 0 & sqrt (a * b) > 0 ) by SQUARE_1:93;
then ( (a ^2 ) * (sqrt (b * c)) > 0 & (b ^2 ) * (sqrt (a * c)) > 0 & (c ^2 ) * (sqrt (a * b)) > 0 ) ;
then ( 2 * ((a ^2 ) * (sqrt (b * c))) > 0 & 2 * ((b ^2 ) * (sqrt (a * c))) > 0 & 2 * ((c ^2 ) * (sqrt (a * b))) > 0 ) ;
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 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 (((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;
then A4: (((((a * (b ^2 )) + (a * (c ^2 ))) + (b * (a ^2 ))) + (b * (c ^2 ))) + (c * (a ^2 ))) + (c * (b ^2 )) >= ((6 * a) * b) * c by A3, XXREAL_0:2;
((a |^ 3) + (b |^ 3)) + (c |^ 3) >= ((3 * a) * b) * c by SERIES_3:12;
then A5: (((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 A4, XREAL_1:9;
(((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 A1, A5, 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 ; :: thesis: verum