let a, b, c be positive Real; ( ( not a = b or not b = c ) implies (((a + b) + c) / 3) |^ 3 > (a * b) * c )
assume H1:
( not a = b or not b = c )
; (((a + b) + c) / 3) |^ 3 > (a * b) * c
set u = 3 -root a;
set v = 3 -root b;
set w = 3 -root c;
reconsider u = 3 -root a, v = 3 -root b, w = 3 -root c as positive Real by PositiveRoot;
A1:
( a = u |^ 3 & b = v |^ 3 & c = w |^ 3 )
;
T1:
( (u - v) |^ 2 = (u - v) ^2 & (v - w) |^ 2 = (v - w) ^2 & (w - u) |^ 2 = (w - u) ^2 )
by NEWTON:81;
T3:
(((u - v) |^ 2) + ((v - w) |^ 2)) + ((w - u) |^ 2) > 0
proof
assume
(((u - v) |^ 2) + ((v - w) |^ 2)) + ((w - u) |^ 2) <= 0
;
contradiction
then
(
u - v = 0 &
v - w = 0 &
w - u = 0 )
;
hence
contradiction
by A1, H1;
verum
end;
(((u + v) + w) / 2) * ((((u - v) |^ 2) + ((v - w) |^ 2)) + ((w - u) |^ 2)) =
((((((u ^2) * u) + ((v ^2) * u)) + ((w ^2) * u)) - (u * (((u * v) + (w * u)) + (v * w)))) + (((((u ^2) * v) + ((v ^2) * v)) + ((w ^2) * v)) - (v * (((u * v) + (w * u)) + (v * w))))) + (((((u ^2) * w) + ((v ^2) * w)) + ((w ^2) * w)) - (w * (((u * v) + (w * u)) + (v * w))))
by T1
.=
((((((u ^2) * u) + ((v ^2) * u)) + ((w ^2) * u)) - (u * (((u * v) + (w * u)) + (v * w)))) + (((((u ^2) * v) + (v |^ 3)) + ((w ^2) * v)) - (v * (((u * v) + (w * u)) + (v * w))))) + (((((u ^2) * w) + ((v ^2) * w)) + ((w ^2) * w)) - (w * (((u * v) + (w * u)) + (v * w))))
by POLYEQ_2:4
.=
(((((u |^ 3) + ((v ^2) * u)) + ((w ^2) * u)) - (u * (((u * v) + (w * u)) + (v * w)))) + (((((u ^2) * v) + (v |^ 3)) + ((w ^2) * v)) - (v * (((u * v) + (w * u)) + (v * w))))) + (((((u ^2) * w) + ((v ^2) * w)) + ((w ^2) * w)) - (w * (((u * v) + (w * u)) + (v * w))))
by POLYEQ_2:4
.=
(((((u |^ 3) + ((v ^2) * u)) + ((w ^2) * u)) - (u * (((u * v) + (w * u)) + (v * w)))) + (((((u ^2) * v) + (v |^ 3)) + ((w ^2) * v)) - (v * (((u * v) + (w * u)) + (v * w))))) + (((((u ^2) * w) + ((v ^2) * w)) + (w |^ 3)) - (w * (((u * v) + (w * u)) + (v * w))))
by POLYEQ_2:4
.=
(((u |^ 3) + (v |^ 3)) + (w |^ 3)) - (((3 * u) * v) * w)
;
then
((((u |^ 3) + (v |^ 3)) + (w |^ 3)) - (((3 * u) * v) * w)) + (((3 * u) * v) * w) > 0 + (((3 * u) * v) * w)
by T3, XREAL_1:8;
then
(((u |^ 3) + (v |^ 3)) + (w |^ 3)) / 3 > (((3 * u) * v) * w) / 3
by XREAL_1:74;
then
((((u |^ 3) + (v |^ 3)) + (w |^ 3)) / 3) |^ 3 > ((u * v) * w) |^ 3
by PREPOWER:10;
then
((((u |^ 3) + (v |^ 3)) + (w |^ 3)) / 3) |^ 3 > ((u * v) |^ 3) * (w |^ 3)
by NEWTON:7;
hence
(((a + b) + c) / 3) |^ 3 > (a * b) * c
by NEWTON:7; verum