let x, y, z be Real; ( 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 that
A1:
( x > 0 & y > 0 )
and
A2:
z < 0
and
A3:
(x + y) + z = 0
; (((x |^ 2) + (y |^ 2)) + (z |^ 2)) |^ 3 >= 6 * ((((x |^ 3) + (y |^ 3)) + (z |^ 3)) ^2)
3 -Root ((((x ^2) * (y ^2)) * (z ^2)) / 4) > 0
by A1, A2, PREPOWER:def 2;
then A4:
3 -root ((((x ^2) * (y ^2)) * (z ^2)) / 4) > 0
by A1, A2, POWER:def 1;
(((x * (x + y)) / 2) + ((y * (x + y)) / 2)) + (x * y) >= 3 * (3 -root ((((x * (x + y)) / 2) * ((y * (x + y)) / 2)) * (x * y)))
by A1, 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 A5:
(((x * (x + y)) / 2) + ((y * (x + y)) / 2)) + (x * y) >= 3 * (3 -root ((((x ^2) * (y ^2)) * ((- z) ^2)) / 4))
by A3;
(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:7
.=
27 * ((3 -Root ((((x ^2) * (y ^2)) * (z ^2)) / 4)) |^ 3)
by A1, A2, Lm3, POWER:def 1
.=
27 * ((((x ^2) * (y ^2)) * (z ^2)) / 4)
by A1, A2, PREPOWER:19
;
then
((((x * (x + y)) / 2) + ((y * (x + y)) / 2)) + (x * y)) |^ 3 >= 27 * ((((x ^2) * (y ^2)) * (z ^2)) / 4)
by A5, A4, PREPOWER:9;
then A6:
8 * (((((x * (x + y)) / 2) + ((y * (x + y)) / 2)) + (x * y)) |^ 3) >= 8 * (27 * ((((x ^2) * (y ^2)) * (z ^2)) / 4))
by XREAL_1:64;
((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:6;
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 A1, PREPOWER:9;
then
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:64;
then
8 * ((((x |^ 2) + (x * y)) + (y |^ 2)) |^ 3) >= 54 * (((x ^2) * (y ^2)) * (z ^2))
by A6, XXREAL_0:2;
then
(2 * (((x |^ 2) + (x * y)) + (y |^ 2))) |^ 3 >= 54 * (((x ^2) * (y ^2)) * (z ^2))
by Lm2, NEWTON:7;
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 A7:
(((((x ^2) + ((2 * x) * y)) + (y ^2)) + (x ^2)) + (y ^2)) |^ 3 >= 54 * (((x ^2) * (y ^2)) * (z ^2))
by Lm1;
A8:
z = - (x + y)
by A3;
then z |^ 3 =
- ((x + y) |^ 3)
by Lm4
.=
- ((((x |^ 3) + ((3 * (x ^2)) * y)) + ((3 * x) * (y ^2))) + (y |^ 3))
by Lm5
;
then
(((z |^ 2) + (x ^2)) + (y ^2)) |^ 3 >= 6 * ((((x |^ 3) + (y |^ 3)) + (z |^ 3)) ^2)
by A8, A7, 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)
; verum