let a, b, c be positive Real; ( 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 that
A1:
a > b
and
A2:
b > c
; ((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))
A3:
b / c > 1
by A2, XREAL_1:187;
set e = ((a to_power (b + c)) * (b to_power (a + c))) * (c to_power (a + b));
A4:
b to_power (c + a) > 0
by POWER:34;
b - c > 0
by A2, XREAL_1:50;
then A5:
(b / c) to_power (b - c) > 1
by A3, POWER:35;
A6:
a / b > 1
by A1, XREAL_1:187;
a - b > 0
by A1, XREAL_1:50;
then
(a / b) to_power (a - b) > 1
by A6, POWER:35;
then A7:
((a / b) to_power (a - b)) * ((b / c) to_power (b - c)) > 1
by A5, XREAL_1:161;
A8:
c to_power (a + b) > 0
by POWER:34;
A9:
a > c
by A1, A2, XXREAL_0:2;
then A10:
a / c > 1
by XREAL_1:187;
set d = ((a to_power (2 * a)) * (b to_power (2 * b))) * (c to_power (2 * c));
A11:
a to_power (b + c) > 0
by POWER:34;
a - c > 0
by A9, XREAL_1:50;
then
(a / c) to_power (a - c) > 1
by A10, POWER:35;
then
(((a / b) to_power (a - b)) * ((b / c) to_power (b - c))) * ((a / c) to_power (- (c - a))) > 1
by A7, XREAL_1:161;
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:31;
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:31;
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:31;
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:76;
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:76;
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:29;
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:85;
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:29;
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:29;
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:29;
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:29;
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:76;
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:29;
then
(((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:76;
then
((((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 A11, A4, A8, XREAL_1:68;
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 A11, A4, A8, XCMPLX_1:87; verum