let x, y, z be real number ; ( 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 3;
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:12
.=
27 * ((3 -Root ((((x ^2 ) * (y ^2 )) * (z ^2 )) / 4)) |^ 3)
by A1, A2, Lm4, POWER:def 1
.=
27 * ((((x ^2 ) * (y ^2 )) * (z ^2 )) / 4)
by A1, A2, PREPOWER:28
;
then
((((x * (x + y)) / 2) + ((y * (x + y)) / 2)) + (x * y)) |^ 3 >= 27 * ((((x ^2 ) * (y ^2 )) * (z ^2 )) / 4)
by A5, A4, PREPOWER:17;
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:66;
((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 A1, PREPOWER:17;
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:66;
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 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 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 Lm5
.=
- ((((x |^ 3) + ((3 * (x ^2 )) * y)) + ((3 * x) * (y ^2 ))) + (y |^ 3))
by Lm6
;
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