let a, b, c be real positive number ; ((a |^ 3) + (b |^ 3)) + (c |^ 3) >= ((3 * a) * b) * c
A1:
((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 ) + (c ^2 )) >= a * ((2 * b) * c) & b * ((a ^2 ) + (c ^2 )) >= b * ((2 * a) * c) )
by Th6, XREAL_1:66;
then A2:
(b * ((a ^2 ) + (c ^2 ))) + (a * ((b ^2 ) + (c ^2 ))) >= (((2 * a) * b) * c) + (((2 * a) * b) * c)
by 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 A3:
(a + c) |^ (2 + 1) >= ((4 * a) * c) * (a + c)
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 A4:
(b + c) |^ (2 + 1) >= ((4 * b) * c) * (b + c)
by NEWTON:11;
((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
(a + b) |^ (2 + 1) >= ((4 * a) * b) * (a + b)
by NEWTON:11;
then
((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;
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 A3, XREAL_1:9;
then A5:
((((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;
c * ((a ^2 ) + (b ^2 )) >= ((2 * a) * b) * c
by Th6, XREAL_1:66;
then A6:
((b * ((a ^2 ) + (c ^2 ))) + (a * ((b ^2 ) + (c ^2 )))) + (c * ((a ^2 ) + (b ^2 ))) >= (((4 * a) * b) * c) + (((2 * a) * b) * c)
by A2, XREAL_1:9;
( ((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 ))) & ((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;
then
2 * (((a |^ 3) + (b |^ 3)) + (c |^ 3)) >= ((6 * a) * b) * c
by A1, A5, 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
; verum