let a, b, c be positive Real; ((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 Lm5;
( a * ((b ^2) + (c ^2)) >= a * ((2 * b) * c) & b * ((a ^2) + (c ^2)) >= b * ((2 * a) * c) )
by Th6, XREAL_1:64;
then A2:
(b * ((a ^2) + (c ^2))) + (a * ((b ^2) + (c ^2))) >= (((2 * a) * b) * c) + (((2 * a) * b) * c)
by XREAL_1:7;
((a + c) ^2) * (a + c) >= ((4 * a) * c) * (a + c)
by Th9, XREAL_1:64;
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:6;
((b + c) ^2) * (b + c) >= ((4 * b) * c) * (b + c)
by Th9, XREAL_1:64;
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:6;
((a + b) ^2) * (a + b) >= ((4 * a) * b) * (a + b)
by Th9, XREAL_1:64;
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:6;
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:7;
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:7;
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:6;
c * ((a ^2) + (b ^2)) >= ((2 * a) * b) * c
by Th6, XREAL_1:64;
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:7;
( ((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 Lm5;
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:72;
hence
((a |^ 3) + (b |^ 3)) + (c |^ 3) >= ((3 * a) * b) * c
; verum