let a, k, y be Real; ( a <> 0 & ( for x being Real holds (x |^ 4) + (a |^ 4) = ((k * a) * x) * ((x ^2) + (a ^2)) ) implies (((y |^ 4) - (k * (y |^ 3))) - (k * y)) + 1 = 0 )
assume that
A1:
a <> 0
and
A2:
for x being Real holds (x |^ 4) + (a |^ 4) = ((k * a) * x) * ((x ^2) + (a ^2))
; (((y |^ 4) - (k * (y |^ 3))) - (k * y)) + 1 = 0
((a * y) |^ 4) + (a |^ 4) =
((k * a) * (a * y)) * (((a * y) ^2) + (a ^2))
by A2
.=
(k * ((a ^2) * y)) * (((a ^2) * (y ^2)) + ((a ^2) * 1))
;
then ((a * y) |^ 4) + (a |^ 4) =
k * ((((a ^2) * (a ^2)) * y) * ((y ^2) + 1))
.=
k * (((a |^ 4) * y) * ((y ^2) + 1))
by Th4
.=
((a |^ 4) * (k * y)) * ((y ^2) + 1)
;
then
((a |^ 4) * (y |^ 4)) + ((a |^ 4) * 1) = (a |^ 4) * ((k * y) * ((y ^2) + 1))
by NEWTON:7;
then
((a |^ 4) ") * ((a |^ 4) * (((y |^ 4) + 1) - ((k * y) * ((y ^2) + 1)))) = 0
;
then
(((a |^ 4) ") * (a |^ 4)) * (((y |^ 4) + 1) - ((k * y) * ((y ^2) + 1))) = 0
;
then A3:
((1 / (a |^ 4)) * (a |^ 4)) * (((y |^ 4) + 1) - ((k * y) * ((y ^2) + 1))) = 0
by XCMPLX_1:215;
a |^ 4 <> 0
by A1, PREPOWER:5;
then
1 * (((y |^ 4) + 1) - ((k * y) * ((y ^2) + 1))) = 0
by A3, XCMPLX_1:106;
then
(((y |^ 4) - (k * ((y ^2) * y))) - (k * y)) + 1 = 0
;
hence
(((y |^ 4) - (k * (y |^ 3))) - (k * y)) + 1 = 0
by Th4; verum