let a, b, c be real positive number ; ( a >= b & b >= c implies ((a to_power a) * (b to_power b)) * (c to_power c) >= ((a * b) * c) to_power (((a + b) + c) / 3) )
assume that
A1:
a >= b
and
A2:
b >= c
; ((a to_power a) * (b to_power b)) * (c to_power c) >= ((a * b) * c) to_power (((a + b) + c) / 3)
A3:
(b / c) to_power ((b - c) / 3) = (b / c) #R ((b - c) / 3)
by POWER:def 2;
( b / c >= 1 & b - c >= c - c )
by A2, XREAL_1:9, XREAL_1:181;
then A4:
(b / c) to_power ((b - c) / 3) >= 1
by A3, PREPOWER:85;
A5:
(a / b) to_power ((a - b) / 3) = (a / b) #R ((a - b) / 3)
by POWER:def 2;
( a / b >= 1 & a - b >= b - b )
by A1, XREAL_1:9, XREAL_1:181;
then
(a / b) to_power ((a - b) / 3) >= 1
by A5, PREPOWER:85;
then A6:
((a / b) to_power ((a - b) / 3)) * ((b / c) to_power ((b - c) / 3)) >= 1 * 1
by A4, XREAL_1:66;
a >= c
by A1, A2, XXREAL_0:2;
then A7:
( a / c >= 1 & a - c >= c - c )
by XREAL_1:9, XREAL_1:181;
(a / c) to_power ((a - c) / 3) = (a / c) #R ((a - c) / 3)
by POWER:def 2;
then
(a / c) to_power ((a - c) / 3) >= 1
by A7, PREPOWER:85;
then
(((a / b) to_power ((a - b) / 3)) * ((b / c) to_power ((b - c) / 3))) * ((a / c) to_power ((a - c) / 3)) >= 1
by A6, XREAL_1:66;
then
(((a to_power ((a - b) / 3)) / (b to_power ((a - b) / 3))) * ((b / c) to_power ((b - c) / 3))) * ((a / c) to_power ((a - c) / 3)) >= 1
by POWER:31;
then A8:
(((a to_power ((a - b) / 3)) / (b to_power ((a - b) / 3))) * ((b to_power ((b - c) / 3)) / (c to_power ((b - c) / 3)))) * ((a / c) to_power ((a - c) / 3)) >= 1
by POWER:31;
set t = b to_power (((a + b) + c) / 3);
set s = b to_power b;
set r = c to_power (((a + b) + c) / 3);
set q = c to_power c;
set p = a to_power (((a + b) + c) / 3);
set o = a to_power a;
set j = c to_power ((a - c) / 3);
set i = a to_power ((a - c) / 3);
set h = c to_power ((b - c) / 3);
set w = b to_power ((b - c) / 3);
set v = b to_power ((a - b) / 3);
set u = a to_power ((a - b) / 3);
A9:
( a to_power (((a + b) + c) / 3) > 0 & c to_power (((a + b) + c) / 3) > 0 )
by POWER:34;
A10:
b to_power (((a + b) + c) / 3) > 0
by POWER:34;
(((a to_power ((a - b) / 3)) / (b to_power ((a - b) / 3))) * ((b to_power ((b - c) / 3)) / (c to_power ((b - c) / 3)))) * ((a to_power ((a - c) / 3)) / (c to_power ((a - c) / 3))) =
(((a to_power ((a - b) / 3)) * (b to_power ((b - c) / 3))) / ((b to_power ((a - b) / 3)) * (c to_power ((b - c) / 3)))) * ((a to_power ((a - c) / 3)) / (c to_power ((a - c) / 3)))
by XCMPLX_1:76
.=
(((a to_power ((a - b) / 3)) * (b to_power ((b - c) / 3))) * (a to_power ((a - c) / 3))) / (((b to_power ((a - b) / 3)) * (c to_power ((b - c) / 3))) * (c to_power ((a - c) / 3)))
by XCMPLX_1:76
.=
(((a to_power ((a - b) / 3)) * (a to_power ((a - c) / 3))) * (b to_power ((b - c) / 3))) / (((b to_power ((a - b) / 3)) * (c to_power ((a - c) / 3))) * (c to_power ((b - c) / 3)))
.=
((a to_power (((a - b) / 3) + ((a - c) / 3))) * (b to_power ((b - c) / 3))) / (((b to_power ((a - b) / 3)) * (c to_power ((a - c) / 3))) * (c to_power ((b - c) / 3)))
by POWER:27
.=
((a to_power ((((2 * a) - b) - c) / 3)) * (b to_power ((b - c) / 3))) / ((b to_power ((a - b) / 3)) * ((c to_power ((a - c) / 3)) * (c to_power ((b - c) / 3))))
.=
((a to_power ((((2 * a) - b) - c) / 3)) * (b to_power ((b - c) / 3))) / ((b to_power ((a - b) / 3)) * (c to_power (((a - c) / 3) + ((b - c) / 3))))
by POWER:27
.=
((a to_power ((((2 * a) - b) - c) / 3)) / (c to_power (((a + b) - (2 * c)) / 3))) * ((b to_power ((b - c) / 3)) / (b to_power ((a - b) / 3)))
by XCMPLX_1:76
.=
((a to_power ((((2 * a) - b) - c) / 3)) / (c to_power (((a + b) - (2 * c)) / 3))) * (b to_power (((b - c) / 3) - ((a - b) / 3)))
by POWER:29
.=
((1 / (c to_power (((a + b) - (2 * c)) / 3))) * (b to_power ((((2 * b) - a) - c) / 3))) * (a to_power ((((2 * a) - b) - c) / 3))
.=
((c to_power (- (((a + b) - (2 * c)) / 3))) * (b to_power ((((2 * b) - a) - c) / 3))) * (a to_power ((((2 * a) - b) - c) / 3))
by POWER:28
.=
((a to_power (((3 * a) / 3) - (((a + b) + c) / 3))) * (c to_power (((3 * c) / 3) - (((a + b) + c) / 3)))) * (b to_power (((3 * b) / 3) - (((a + b) + c) / 3)))
.=
(((a to_power ((3 * a) / 3)) / (a to_power (((a + b) + c) / 3))) * (c to_power (((3 * c) / 3) - (((a + b) + c) / 3)))) * (b to_power (((3 * b) / 3) - (((a + b) + c) / 3)))
by POWER:29
.=
(((a to_power ((3 * a) / 3)) / (a to_power (((a + b) + c) / 3))) * ((c to_power ((3 * c) / 3)) / (c to_power (((a + b) + c) / 3)))) * (b to_power (((3 * b) / 3) - (((a + b) + c) / 3)))
by POWER:29
.=
(((a to_power a) / (a to_power (((a + b) + c) / 3))) * ((c to_power c) / (c to_power (((a + b) + c) / 3)))) * ((b to_power b) / (b to_power (((a + b) + c) / 3)))
by POWER:29
.=
(((a to_power a) * (c to_power c)) / ((a to_power (((a + b) + c) / 3)) * (c to_power (((a + b) + c) / 3)))) * ((b to_power b) / (b to_power (((a + b) + c) / 3)))
by XCMPLX_1:76
.=
(((a to_power a) * (c to_power c)) * (b to_power b)) / (((a to_power (((a + b) + c) / 3)) * (c to_power (((a + b) + c) / 3))) * (b to_power (((a + b) + c) / 3)))
by XCMPLX_1:76
;
then
(((a to_power a) * (c to_power c)) * (b to_power b)) / (((a to_power (((a + b) + c) / 3)) * (c to_power (((a + b) + c) / 3))) * (b to_power (((a + b) + c) / 3))) >= 1
by A8, POWER:31;
then
((((a to_power a) * (c to_power c)) * (b to_power b)) / (((a to_power (((a + b) + c) / 3)) * (c to_power (((a + b) + c) / 3))) * (b to_power (((a + b) + c) / 3)))) * (((a to_power (((a + b) + c) / 3)) * (c to_power (((a + b) + c) / 3))) * (b to_power (((a + b) + c) / 3))) >= 1 * (((a to_power (((a + b) + c) / 3)) * (c to_power (((a + b) + c) / 3))) * (b to_power (((a + b) + c) / 3)))
by A9, A10, XREAL_1:64;
then
((a to_power a) * (c to_power c)) * (b to_power b) >= ((a to_power (((a + b) + c) / 3)) * (c to_power (((a + b) + c) / 3))) * (b to_power (((a + b) + c) / 3))
by A9, A10, XCMPLX_1:87;
then
((a to_power a) * (c to_power c)) * (b to_power b) >= ((a * c) to_power (((a + b) + c) / 3)) * (b to_power (((a + b) + c) / 3))
by POWER:30;
then
(a to_power a) * ((b to_power b) * (c to_power c)) >= ((a * c) * b) to_power (((a + b) + c) / 3)
by POWER:30;
hence
((a to_power a) * (b to_power b)) * (c to_power c) >= ((a * b) * c) to_power (((a + b) + c) / 3)
; verum