let a, k, y be real number ; :: thesis: ( a <> 0 & ( for x being real number 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 number holds (x |^ 4) + (a |^ 4) = ((k * a) * x) * ((x ^2 ) + (a ^2 )) ; :: thesis: (((y |^ 4) - (k * (y |^ 3))) - (k * y)) + 1 = 0
A3: ((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)) ;
A4: a |^ 4 <> 0 by A1, PREPOWER:12;
((a * y) |^ 4) + (a |^ 4) = k * ((((a ^2 ) * (a ^2 )) * y) * ((y ^2 ) + 1)) by A3
.= 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:12;
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 ((1 / (a |^ 4)) * (a |^ 4)) * (((y |^ 4) + 1) - ((k * y) * ((y ^2 ) + 1))) = 0 by XCMPLX_1:217;
then 1 * (((y |^ 4) + 1) - ((k * y) * ((y ^2 ) + 1))) = 0 by A4, XCMPLX_1:107;
then (((y |^ 4) - (k * ((y ^2 ) * y))) - (k * y)) + 1 = 0 ;
hence (((y |^ 4) - (k * (y |^ 3))) - (k * y)) + 1 = 0 by Th4; :: thesis: verum