let a, b, c be real positive number ; :: thesis: ( 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 A1: ( a >= b & b >= c ) ; :: thesis: ((a to_power a) * (b to_power b)) * (c to_power c) >= ((a * b) * c) to_power (((a + b) + c) / 3)
then A2: a >= c by XXREAL_0:2;
then A3: ( a / b >= 1 & b / c >= 1 & a / c >= 1 ) by A1, XREAL_1:183;
set u = a to_power ((a - b) / 3);
set v = b to_power ((a - b) / 3);
set w = b to_power ((b - c) / 3);
set h = c to_power ((b - c) / 3);
set i = a to_power ((a - c) / 3);
set j = c to_power ((a - c) / 3);
set o = a to_power a;
set p = a to_power (((a + b) + c) / 3);
set q = c to_power c;
set r = c to_power (((a + b) + c) / 3);
set s = b to_power b;
set t = b to_power (((a + b) + c) / 3);
A4: ( a - b >= b - b & b - c >= c - c & a - c >= c - c ) by A1, A2, XREAL_1:11;
A5: ( (a / b) to_power ((a - b) / 3) = (a / b) #R ((a - b) / 3) & (b / c) to_power ((b - c) / 3) = (b / c) #R ((b - c) / 3) & (a / c) to_power ((a - c) / 3) = (a / c) #R ((a - c) / 3) ) by POWER:def 2;
A6: (((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:77
.= (((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:77
.= (((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:32
.= ((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:32
.= ((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:77
.= ((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:34
.= ((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:33
.= ((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:34
.= (((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:34
.= (((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:34
.= (((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:77
.= (((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:77 ;
A7: ( (a / b) to_power ((a - b) / 3) >= 1 & (b / c) to_power ((b - c) / 3) >= 1 & (a / c) to_power ((a - c) / 3) >= 1 ) by A3, A4, A5, PREPOWER:99;
then ((a / b) to_power ((a - b) / 3)) * ((b / c) to_power ((b - c) / 3)) >= 1 * 1 by XREAL_1:68;
then (((a / b) to_power ((a - b) / 3)) * ((b / c) to_power ((b - c) / 3))) * ((a / c) to_power ((a - c) / 3)) >= 1 by A7, XREAL_1:68;
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:36;
then (((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:36;
then A8: (((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 A6, POWER:36;
A9: ( a to_power (((a + b) + c) / 3) > 0 & c to_power (((a + b) + c) / 3) > 0 & b to_power (((a + b) + c) / 3) > 0 ) by POWER:39;
A10: ((a to_power (((a + b) + c) / 3)) * (c to_power (((a + b) + c) / 3))) * (b to_power (((a + b) + c) / 3)) > 0 by A9;
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 A8, XREAL_1:66;
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 A10, XCMPLX_1:88;
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:35;
then (a to_power a) * ((b to_power b) * (c to_power c)) >= ((a * c) * b) to_power (((a + b) + c) / 3) by POWER:35;
hence ((a to_power a) * (b to_power b)) * (c to_power c) >= ((a * b) * c) to_power (((a + b) + c) / 3) ; :: thesis: verum