let x, y, z be real number ; :: thesis: ( x > 0 & y > 0 & z < 0 & (x + y) + z = 0 implies (((x |^ 2) + (y |^ 2)) + (z |^ 2)) |^ 3 >= 6 * ((((x |^ 3) + (y |^ 3)) + (z |^ 3)) ^2 ) )
assume A1: ( x > 0 & y > 0 & z < 0 & (x + y) + z = 0 ) ; :: thesis: (((x |^ 2) + (y |^ 2)) + (z |^ 2)) |^ 3 >= 6 * ((((x |^ 3) + (y |^ 3)) + (z |^ 3)) ^2 )
then A2: z = - (x + y) ;
then A3: z |^ 3 = - ((x + y) |^ 3) by Lm5
.= - ((((x |^ 3) + ((3 * (x ^2 )) * y)) + ((3 * x) * (y ^2 ))) + (y |^ 3)) by Lm6 ;
A5: x * ((x + y) / 2) > 0 * x by A1;
A6: y * ((x + y) / 2) > 0 * y by A1;
A7: x * y > 0 by A1;
((x * (x + y)) / 2) + ((y * (x + y)) / 2) > 0 by A5, A6;
then A8: (((x * (x + y)) / 2) + ((y * (x + y)) / 2)) + (x * y) > 0 by A7;
((x ^2 ) + (y ^2 )) / 2 >= x * y by Th7;
then ((x |^ 2) + (y ^2 )) / 2 >= x * y by Lm1;
then ((x |^ 2) + (y |^ 2)) / 2 >= x * y by Lm1;
then ((((x |^ 2) + (x * y)) / 2) + (((x * y) + (y |^ 2)) / 2)) + (((x |^ 2) + (y |^ 2)) / 2) >= ((((x |^ 2) + (x * y)) / 2) + (((x * y) + (y |^ 2)) / 2)) + (x * y) by XREAL_1:8;
then ((((x |^ 2) + (x * y)) / 2) + (((x * y) + (y |^ 2)) / 2)) + (((x |^ 2) + (y |^ 2)) / 2) >= ((((x ^2 ) + (x * y)) / 2) + (((x * y) + (y |^ 2)) / 2)) + (x * y) by Lm1;
then ((((x |^ 2) + (x * y)) / 2) + (((x * y) + (y |^ 2)) / 2)) + (((x |^ 2) + (y |^ 2)) / 2) >= ((((x * x) + (x * y)) / 2) + (((x * y) + (y ^2 )) / 2)) + (x * y) by Lm1;
then (((((x |^ 2) + (x * y)) / 2) + (((x * y) + (y |^ 2)) / 2)) + (((x |^ 2) + (y |^ 2)) / 2)) |^ 3 >= ((((x * (x + y)) / 2) + ((y * (x + y)) / 2)) + (x * y)) |^ 3 by A8, PREPOWER:17;
then A9: 8 * ((((((x |^ 2) + (x * y)) / 2) + (((x * y) + (y |^ 2)) / 2)) + (((x |^ 2) + (y |^ 2)) / 2)) |^ 3) >= 8 * (((((x * (x + y)) / 2) + ((y * (x + y)) / 2)) + (x * y)) |^ 3) by XREAL_1:66;
(((x * (x + y)) / 2) + ((y * (x + y)) / 2)) + (x * y) >= 3 * (3 -root ((((x * (x + y)) / 2) * ((y * (x + y)) / 2)) * (x * y))) by A5, A6, A7, Th15;
then (((x * (x + y)) / 2) + ((y * (x + y)) / 2)) + (x * y) >= 3 * (3 -root ((((x ^2 ) * (y ^2 )) * ((x + y) * (x + y))) / 4)) ;
then A10: (((x * (x + y)) / 2) + ((y * (x + y)) / 2)) + (x * y) >= 3 * (3 -root ((((x ^2 ) * (y ^2 )) * ((- z) ^2 )) / 4)) by A1;
A11: ( x ^2 > 0 & y ^2 > 0 & z ^2 > 0 ) by A1;
((x ^2 ) * (y ^2 )) * (z ^2 ) > 0 by A11;
then A12: (((x ^2 ) * (y ^2 )) * (z ^2 )) / 4 > 0 ;
A13: (3 * (3 -root ((((x ^2 ) * (y ^2 )) * (z ^2 )) / 4))) |^ 3 = (3 |^ 3) * ((3 -root ((((x ^2 ) * (y ^2 )) * (z ^2 )) / 4)) |^ 3) by NEWTON:12
.= 27 * ((3 -Root ((((x ^2 ) * (y ^2 )) * (z ^2 )) / 4)) |^ 3) by A12, Lm4, POWER:def 1
.= 27 * ((((x ^2 ) * (y ^2 )) * (z ^2 )) / 4) by A12, PREPOWER:28 ;
3 -Root ((((x ^2 ) * (y ^2 )) * (z ^2 )) / 4) > 0 by A12, PREPOWER:def 3;
then 3 -root ((((x ^2 ) * (y ^2 )) * (z ^2 )) / 4) > 0 by A12, POWER:def 1;
then 3 * (3 -root ((((x ^2 ) * (y ^2 )) * (z ^2 )) / 4)) > 0 ;
then ((((x * (x + y)) / 2) + ((y * (x + y)) / 2)) + (x * y)) |^ 3 >= 27 * ((((x ^2 ) * (y ^2 )) * (z ^2 )) / 4) by A10, A13, PREPOWER:17;
then 8 * (((((x * (x + y)) / 2) + ((y * (x + y)) / 2)) + (x * y)) |^ 3) >= 8 * (27 * ((((x ^2 ) * (y ^2 )) * (z ^2 )) / 4)) by XREAL_1:66;
then 8 * ((((x |^ 2) + (x * y)) + (y |^ 2)) |^ 3) >= 54 * (((x ^2 ) * (y ^2 )) * (z ^2 )) by A9, XXREAL_0:2;
then (2 * (((x |^ 2) + (x * y)) + (y |^ 2))) |^ 3 >= 54 * (((x ^2 ) * (y ^2 )) * (z ^2 )) by Lm3, NEWTON:12;
then (((((x |^ 2) + ((2 * x) * y)) + (y |^ 2)) + (x |^ 2)) + (y |^ 2)) |^ 3 >= 54 * (((x ^2 ) * (y ^2 )) * (z ^2 )) ;
then (((((x ^2 ) + ((2 * x) * y)) + (y |^ 2)) + (x |^ 2)) + (y |^ 2)) |^ 3 >= 54 * (((x ^2 ) * (y ^2 )) * (z ^2 )) by Lm1;
then (((((x ^2 ) + ((2 * x) * y)) + (y |^ 2)) + (x ^2 )) + (y |^ 2)) |^ 3 >= 54 * (((x ^2 ) * (y ^2 )) * (z ^2 )) by Lm1;
then (((((x ^2 ) + ((2 * x) * y)) + (y ^2 )) + (x ^2 )) + (y |^ 2)) |^ 3 >= 54 * (((x ^2 ) * (y ^2 )) * (z ^2 )) by Lm1;
then (((((x ^2 ) + ((2 * x) * y)) + (y ^2 )) + (x ^2 )) + (y ^2 )) |^ 3 >= 54 * (((x ^2 ) * (y ^2 )) * (z ^2 )) by Lm1;
then (((z |^ 2) + (x ^2 )) + (y ^2 )) |^ 3 >= 6 * ((((x |^ 3) + (y |^ 3)) + (z |^ 3)) ^2 ) by A2, A3, Lm1;
then (((z |^ 2) + (x |^ 2)) + (y ^2 )) |^ 3 >= 6 * ((((x |^ 3) + (y |^ 3)) + (z |^ 3)) ^2 ) by Lm1;
then (((z |^ 2) + (x |^ 2)) + (y |^ 2)) |^ 3 >= 6 * ((((x |^ 3) + (y |^ 3)) + (z |^ 3)) ^2 ) by Lm1;
hence (((x |^ 2) + (y |^ 2)) + (z |^ 2)) |^ 3 >= 6 * ((((x |^ 3) + (y |^ 3)) + (z |^ 3)) ^2 ) ; :: thesis: verum