let a, b, c be real positive number ; :: thesis: ( a > b & b > c implies ((a to_power (2 * a)) * (b to_power (2 * b))) * (c to_power (2 * c)) > ((a to_power (b + c)) * (b to_power (a + c))) * (c to_power (a + b)) )
assume A1: ( a > b & b > c ) ; :: thesis: ((a to_power (2 * a)) * (b to_power (2 * b))) * (c to_power (2 * c)) > ((a to_power (b + c)) * (b to_power (a + c))) * (c to_power (a + b))
then A2: ( a - b > 0 & b - c > 0 ) by XREAL_1:52;
A3: a > c by A1, XXREAL_0:2;
then A4: a - c > 0 by XREAL_1:52;
A5: ( a / b > 1 & b / c > 1 ) by A1, XREAL_1:189;
a / c > 1 by A3, XREAL_1:189;
then A6: ( (a / b) to_power (a - b) > 1 & (b / c) to_power (b - c) > 1 & (a / c) to_power (a - c) > 1 ) by A2, A4, A5, POWER:40;
then ((a / b) to_power (a - b)) * ((b / c) to_power (b - c)) > 1 by XREAL_1:163;
then (((a / b) to_power (a - b)) * ((b / c) to_power (b - c))) * ((a / c) to_power (- (c - a))) > 1 by A6, XREAL_1:163;
then (((a / b) to_power (a - b)) * ((b / c) to_power (b - c))) * ((c / a) to_power (c - a)) > 1 by Lm4;
then (((a to_power (a - b)) / (b to_power (a - b))) * ((b / c) to_power (b - c))) * ((c / a) to_power (c - a)) > 1 by POWER:36;
then (((a to_power (a - b)) / (b to_power (a - b))) * ((b to_power (b - c)) / (c to_power (b - c)))) * ((c / a) to_power (c - a)) > 1 by POWER:36;
then (((a to_power (a - b)) / (b to_power (a - b))) * ((b to_power (b - c)) / (c to_power (b - c)))) * ((c to_power (c - a)) / (a to_power (c - a))) > 1 by POWER:36;
then (((a to_power (a - b)) * (b to_power (b - c))) / ((c to_power (b - c)) * (b to_power (a - b)))) * ((c to_power (c - a)) / (a to_power (c - a))) > 1 by XCMPLX_1:77;
then (((a to_power (a - b)) / (c to_power (b - c))) * ((b to_power (b - c)) / (b to_power (a - b)))) * ((c to_power (c - a)) / (a to_power (c - a))) > 1 by XCMPLX_1:77;
then (((a to_power (a - b)) / (c to_power (b - c))) * (b to_power ((b - c) - (a - b)))) * ((c to_power (c - a)) / (a to_power (c - a))) > 1 by POWER:34;
then (((a to_power (a - b)) / (c to_power (b - c))) * ((c to_power (c - a)) / (a to_power (c - a)))) * (b to_power (((2 * b) - a) - c)) > 1 ;
then (((a to_power (a - b)) / (a to_power (c - a))) * ((c to_power (c - a)) / (c to_power (b - c)))) * (b to_power (((2 * b) - a) - c)) > 1 by XCMPLX_1:86;
then ((a to_power ((a - b) - (c - a))) * ((c to_power (c - a)) / (c to_power (b - c)))) * (b to_power (((2 * b) - a) - c)) > 1 by POWER:34;
then ((a to_power (((2 * a) - b) - c)) * (c to_power ((c - a) - (b - c)))) * (b to_power (((2 * b) - a) - c)) > 1 by POWER:34;
then ((a to_power ((2 * a) - (b + c))) * (c to_power ((2 * c) - (a + b)))) * (b to_power ((2 * b) - (a + c))) > 1 ;
then (((a to_power (2 * a)) / (a to_power (b + c))) * (c to_power ((2 * c) - (a + b)))) * (b to_power ((2 * b) - (a + c))) > 1 by POWER:34;
then (((a to_power (2 * a)) / (a to_power (b + c))) * ((c to_power (2 * c)) / (c to_power (a + b)))) * (b to_power ((2 * b) - (a + c))) > 1 by POWER:34;
then (((a to_power (2 * a)) * (c to_power (2 * c))) / ((a to_power (b + c)) * (c to_power (a + b)))) * (b to_power ((2 * b) - (a + c))) > 1 by XCMPLX_1:77;
then (((a to_power (2 * a)) * (c to_power (2 * c))) / ((a to_power (b + c)) * (c to_power (a + b)))) * ((b to_power (2 * b)) / (b to_power (a + c))) > 1 by POWER:34;
then A7: (((a to_power (2 * a)) * (c to_power (2 * c))) * (b to_power (2 * b))) / (((a to_power (b + c)) * (c to_power (a + b))) * (b to_power (a + c))) > 1 by XCMPLX_1:77;
A8: ( a to_power (b + c) > 0 & b to_power (c + a) > 0 & c to_power (a + b) > 0 ) by POWER:39;
A9: ((a to_power (b + c)) * (c to_power (a + b))) * (b to_power (a + c)) > 0 by A8;
set d = ((a to_power (2 * a)) * (b to_power (2 * b))) * (c to_power (2 * c));
set e = ((a to_power (b + c)) * (b to_power (a + c))) * (c to_power (a + b));
((((a to_power (2 * a)) * (b to_power (2 * b))) * (c to_power (2 * c))) / (((a to_power (b + c)) * (b to_power (a + c))) * (c to_power (a + b)))) * (((a to_power (b + c)) * (b to_power (a + c))) * (c to_power (a + b))) > 1 * (((a to_power (b + c)) * (b to_power (a + c))) * (c to_power (a + b))) by A7, A9, XREAL_1:70;
hence ((a to_power (2 * a)) * (b to_power (2 * b))) * (c to_power (2 * c)) > ((a to_power (b + c)) * (b to_power (a + c))) * (c to_power (a + b)) by A9, XCMPLX_1:88; :: thesis: verum