let a, b, c, x, y be real number ; :: thesis: ( a <> 0 & y = x + (1 / x) & Polynom a,b,c,b,a,x = 0 implies ( x <> 0 & (((a * (y ^2 )) + (b * y)) + c) - (2 * a) = 0 ) )
assume that
A1: a <> 0 and
A2: y = x + (1 / x) ; :: thesis: ( not Polynom a,b,c,b,a,x = 0 or ( x <> 0 & (((a * (y ^2 )) + (b * y)) + c) - (2 * a) = 0 ) )
assume A3: Polynom a,b,c,b,a,x = 0 ; :: thesis: ( x <> 0 & (((a * (y ^2 )) + (b * y)) + c) - (2 * a) = 0 )
A4: x <> 0

proof

assume x = 0 ; :: thesis: contradiction
then ((a * (0 to_power 4)) + (b * (0 |^ 3))) + a = 0 by A3;
then ((a * 0 ) + (b * (0 |^ 3))) + a = 0 by POWER:def 2;
then ((a * 0 ) + (b * 0 )) + a = 0 by NEWTON:16;
hence contradiction by A1; :: thesis: verum

end;

then A5: ( ( x > 0 or x < 0 ) & x ^2 > 0 ) by SQUARE_1:74, XXREAL_0:1;
A6: x |^ 4 = x to_power (2 + 2) by POWER:46;

A7: now

per cases ( x > 0 or x < 0 ) by A4, XXREAL_0:1;

case A8: x > 0 ; :: thesis: ( a * ((x ^2 ) + (1 / (x ^2 ))) = (- (b * (x + (1 / x)))) - c & ((x ^2 ) - (x * y)) + 1 = 0 )

then A9: x |^ 4 = (x to_power 2) * (x to_power 2) by A6, POWER:32
.= (x ^2 ) * (x to_power 2) by POWER:53
.= (x ^2 ) * (x ^2 ) by POWER:53 ;
x |^ 3 = x to_power (2 + 1) by POWER:46
.= (x to_power 2) * (x to_power 1) by A8, POWER:32 ;
then A10: x |^ 3 = (x to_power 2) * x by POWER:30
.= (x ^2 ) * x by POWER:53 ;
set m = (a * (x ^2 )) + ((b * x) + c);
set n = - ((b * x) + a);
((a * (x ^2 )) + ((b * x) + c)) * (x ^2 ) = (- ((b * x) + a)) * 1 by A3, A9, A10;
then ((a * (x ^2 )) + ((b * x) + c)) / 1 = (- ((b * x) + a)) / (x ^2 ) by A5, XCMPLX_1:95;
then (a * (x ^2 )) + ((b * x) + c) = (- ((b * x) + a)) * (1 / (x ^2 )) by XCMPLX_1:100
.= (- ((b * x) + a)) * ((x ^2 ) " ) by XCMPLX_1:217
.= (- (b * (x * ((x ^2 ) " )))) - (a * ((x ^2 ) " )) ;
then a * ((x ^2 ) + ((x ^2 ) " )) = (- (b * ((x * ((x ^2 ) " )) + x))) - c ;
then A11: a * ((x ^2 ) + (1 / (x ^2 ))) = (- (b * ((x * ((x ^2 ) " )) + x))) - c by XCMPLX_1:217
.= (- (b * ((x * (1 / (x ^2 ))) + x))) - c by XCMPLX_1:217 ;
1 / (x * x) = (1 / x) * (1 / x) by XCMPLX_1:103;
then a * ((x ^2 ) + (1 / (x ^2 ))) = (- (b * (((x * (1 / x)) * (1 / x)) + x))) - c by A11;
then A12: a * ((x ^2 ) + (1 / (x ^2 ))) = (- (b * ((1 * (1 / x)) + x))) - c by A8, XCMPLX_1:107;
x * y = (x * x) + (x * (1 / x)) by A2;
then (x * y) + 0 = (x ^2 ) + 1 by A4, XCMPLX_1:107;
hence ( a * ((x ^2 ) + (1 / (x ^2 ))) = (- (b * (x + (1 / x)))) - c & ((x ^2 ) - (x * y)) + 1 = 0 ) by A12; :: thesis: verum

end;

case A13: x < 0 ; :: thesis: ( a * ((x ^2 ) + (1 / (x ^2 ))) = (- (b * (x + (1 / x)))) - c & ((x ^2 ) - (x * y)) + 1 = 0 )

then A14: 0 < - x by XREAL_1:60;
(- x) |^ 4 = x |^ 4 by Lm1, POWER:1;
then A15: x |^ 4 = (- x) to_power (2 + 2) by POWER:46
.= ((- x) to_power 2) * ((- x) to_power 2) by A14, POWER:32
.= ((- x) ^2 ) * ((- x) to_power 2) by POWER:53
.= (x ^2 ) * ((- x) ^2 ) by POWER:53 ;
(- x) |^ 3 = (- x) to_power (2 + 1) by POWER:46
.= ((- x) to_power 2) * ((- x) to_power 1) by A14, POWER:32 ;
then A16: (- x) |^ 3 = ((- x) to_power 2) * (- x) by POWER:30;
A17: (- x) to_power 2 = (- x) ^2 by POWER:53
.= x ^2 ;
3 = (2 * 1) + 1 ;
then ((- x) |^ 3) + (x |^ 3) = - ((x |^ 3) + (- (x |^ 3))) by POWER:2
.= (x |^ 3) - (x |^ 3) ;
then A18: x |^ 3 = - ((- x) |^ 3) ;
set m = (a * (x ^2 )) + ((b * x) + c);
set n = - ((b * x) + a);
((a * (x ^2 )) + ((b * x) + c)) * (x ^2 ) = (- ((b * x) + a)) * 1 by A3, A15, A16, A17, A18;
then ((a * (x ^2 )) + ((b * x) + c)) / 1 = (- ((b * x) + a)) / (x ^2 ) by A5, XCMPLX_1:95;
then (a * (x ^2 )) + ((b * x) + c) = (- ((b * x) + a)) * (1 / (x ^2 )) by XCMPLX_1:100
.= (- ((b * x) + a)) * ((x ^2 ) " ) by XCMPLX_1:217
.= (- (b * (x * ((x ^2 ) " )))) - (a * ((x ^2 ) " )) ;
then a * ((x ^2 ) + ((x ^2 ) " )) = (- (b * ((x * ((x ^2 ) " )) + x))) - c ;
then a * ((x ^2 ) + (1 / (x ^2 ))) = (- (b * ((x * ((x ^2 ) " )) + x))) - c by XCMPLX_1:217
.= (- (b * ((x * (1 / (x ^2 ))) + x))) - c by XCMPLX_1:217 ;
then a * ((x ^2 ) + (1 / (x ^2 ))) = (- (b * ((x * ((1 / x) * (1 / x))) + x))) - c by XCMPLX_1:103
.= (- (b * (((x * (1 / x)) * (1 / x)) + x))) - c ;
then A19: a * ((x ^2 ) + (1 / (x ^2 ))) = (- (b * ((1 * (1 / x)) + x))) - c by A13, XCMPLX_1:107;
x * y = (x * x) + (x * (1 / x)) by A2
.= (x * x) + 1 by A13, XCMPLX_1:107 ;
hence ( a * ((x ^2 ) + (1 / (x ^2 ))) = (- (b * (x + (1 / x)))) - c & ((x ^2 ) - (x * y)) + 1 = 0 ) by A19; :: thesis: verum

end;

end;

end;

y ^2 = ((x ^2 ) + (2 * (x * (1 / x)))) + ((1 / x) ^2 ) by A2
.= ((x ^2 ) + (2 * 1)) + ((1 / x) ^2 ) by A4, XCMPLX_1:107
.= ((x ^2 ) + 2) + ((1 ^2 ) / (x ^2 )) by XCMPLX_1:77
.= (x ^2 ) - ((- 2) - (1 / (x ^2 ))) ;
then (a * (y ^2 )) - (2 * a) = (- (b * y)) - c by A2, A7;
hence ( x <> 0 & (((a * (y ^2 )) + (b * y)) + c) - (2 * a) = 0 ) by A4; :: thesis: verum