let a, b, c be real positive number ; :: thesis: ((a |^ 3) + (b |^ 3)) + (c |^ 3) >= ((3 * a) * b) * c
A1: ((a + b) |^ 3) - (((3 * (a ^2 )) * b) + ((3 * a) * (b ^2 ))) = ((((a |^ 3) + ((3 * (a ^2 )) * b)) + ((3 * a) * (b ^2 ))) + (b |^ 3)) - (((3 * (a ^2 )) * b) + ((3 * a) * (b ^2 ))) by Lm6;
A2: ((b + c) |^ 3) - (((3 * (b ^2 )) * c) + ((3 * b) * (c ^2 ))) = ((((b |^ 3) + ((3 * (b ^2 )) * c)) + ((3 * b) * (c ^2 ))) + (c |^ 3)) - (((3 * (b ^2 )) * c) + ((3 * b) * (c ^2 ))) by Lm6;
A3: ((a + c) |^ 3) - (((3 * (a ^2 )) * c) + ((3 * a) * (c ^2 ))) = ((((a |^ 3) + ((3 * (a ^2 )) * c)) + ((3 * a) * (c ^2 ))) + (c |^ 3)) - (((3 * (a ^2 )) * c) + ((3 * a) * (c ^2 ))) by Lm6;
((a + b) ^2 ) * (a + b) >= ((4 * a) * b) * (a + b) by Th9, XREAL_1:66;
then ((a + b) |^ 2) * (a + b) >= ((4 * a) * b) * (a + b) by Lm1;
then A4: (a + b) |^ (2 + 1) >= ((4 * a) * b) * (a + b) by NEWTON:11;
((b + c) ^2 ) * (b + c) >= ((4 * b) * c) * (b + c) by Th9, XREAL_1:66;
then ((b + c) |^ 2) * (b + c) >= ((4 * b) * c) * (b + c) by Lm1;
then (b + c) |^ (2 + 1) >= ((4 * b) * c) * (b + c) by NEWTON:11;
then A5: ((a + b) |^ 3) + ((b + c) |^ 3) >= (((4 * (a ^2 )) * b) + ((4 * a) * (b ^2 ))) + (((4 * (b ^2 )) * c) + ((4 * b) * (c ^2 ))) by A4, XREAL_1:9;
((a + c) ^2 ) * (a + c) >= ((4 * a) * c) * (a + c) by Th9, XREAL_1:66;
then ((a + c) |^ 2) * (a + c) >= ((4 * a) * c) * (a + c) by Lm1;
then (a + c) |^ (2 + 1) >= ((4 * a) * c) * (a + c) by NEWTON:11;
then (((a + b) |^ 3) + ((b + c) |^ 3)) + ((a + c) |^ 3) >= (((((4 * (a ^2 )) * b) + ((4 * a) * (b ^2 ))) + ((4 * (b ^2 )) * c)) + ((4 * b) * (c ^2 ))) + (((4 * (a ^2 )) * c) + ((4 * a) * (c ^2 ))) by A5, XREAL_1:9;
then A6: ((((a + b) |^ 3) + ((b + c) |^ 3)) + ((a + c) |^ 3)) + ((((((- ((3 * (a ^2 )) * b)) - ((3 * a) * (b ^2 ))) - ((3 * (b ^2 )) * c)) - ((3 * b) * (c ^2 ))) - ((3 * (a ^2 )) * c)) - ((3 * a) * (c ^2 ))) >= (((((((4 * (a ^2 )) * b) + ((4 * a) * (b ^2 ))) + ((4 * (b ^2 )) * c)) + ((4 * b) * (c ^2 ))) + ((4 * (a ^2 )) * c)) + ((4 * a) * (c ^2 ))) + ((((((- ((3 * (a ^2 )) * b)) - ((3 * a) * (b ^2 ))) - ((3 * (b ^2 )) * c)) - ((3 * b) * (c ^2 ))) - ((3 * (a ^2 )) * c)) - ((3 * a) * (c ^2 ))) by XREAL_1:8;
A7: a * ((b ^2 ) + (c ^2 )) >= a * ((2 * b) * c) by Th6, XREAL_1:66;
b * ((a ^2 ) + (c ^2 )) >= b * ((2 * a) * c) by Th6, XREAL_1:66;
then A8: (b * ((a ^2 ) + (c ^2 ))) + (a * ((b ^2 ) + (c ^2 ))) >= (((2 * a) * b) * c) + (((2 * a) * b) * c) by A7, XREAL_1:9;
c * ((a ^2 ) + (b ^2 )) >= ((2 * a) * b) * c by Th6, XREAL_1:66;
then ((b * ((a ^2 ) + (c ^2 ))) + (a * ((b ^2 ) + (c ^2 )))) + (c * ((a ^2 ) + (b ^2 ))) >= (((4 * a) * b) * c) + (((2 * a) * b) * c) by A8, XREAL_1:9;
then 2 * (((a |^ 3) + (b |^ 3)) + (c |^ 3)) >= ((6 * a) * b) * c by A1, A2, A3, A6, XXREAL_0:2;
then (2 * (((a |^ 3) + (b |^ 3)) + (c |^ 3))) / 2 >= (((6 * a) * b) * c) / 2 by XREAL_1:74;
hence ((a |^ 3) + (b |^ 3)) + (c |^ 3) >= ((3 * a) * b) * c ; :: thesis: verum