let a, b, c, x, y be Real; :: 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:11;
hence contradiction by A1; :: thesis: verum
end;
then A5: x ^2 > 0 by SQUARE_1:12;
A6: x |^ 4 = x to_power (2 + 2) by POWER:41;
A7: now :: thesis: ( ( x > 0 & a * ((x ^2) + (1 / (x ^2))) = (- (b * (x + (1 / x)))) - c & ((x ^2) - (x * y)) + 1 = 0 ) or ( x < 0 & a * ((x ^2) + (1 / (x ^2))) = (- (b * (x + (1 / x)))) - c & ((x ^2) - (x * y)) + 1 = 0 ) )
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 )
set n = - ((b * x) + a);
set m = (a * (x ^2)) + ((b * x) + c);
x |^ 3 = x to_power (2 + 1) by POWER:41
.= (x to_power 2) * (x to_power 1) by A8, POWER:27 ;
then A9: x |^ 3 = (x to_power 2) * x
.= (x ^2) * x by POWER:46 ;
x |^ 4 = (x to_power 2) * (x to_power 2) by A6, A8, POWER:27
.= (x ^2) * (x to_power 2) by POWER:46
.= (x ^2) * (x ^2) by POWER:46 ;
then ((a * (x ^2)) + ((b * x) + c)) * (x ^2) = (- ((b * x) + a)) * 1 by A3, A9;
then ((a * (x ^2)) + ((b * x) + c)) / 1 = (- ((b * x) + a)) / (x ^2) by A5, XCMPLX_1:94;
then (a * (x ^2)) + ((b * x) + c) = (- ((b * x) + a)) * (1 / (x ^2)) by XCMPLX_1:99
.= (- ((b * x) + a)) * ((x ^2) ") by XCMPLX_1:215
.= (- (b * (x * ((x ^2) ")))) - (a * ((x ^2) ")) ;
then a * ((x ^2) + ((x ^2) ")) = (- (b * ((x * ((x ^2) ")) + x))) - c ;
then A10: a * ((x ^2) + (1 / (x ^2))) = (- (b * ((x * ((x ^2) ")) + x))) - c by XCMPLX_1:215
.= (- (b * ((x * (1 / (x ^2))) + x))) - c by XCMPLX_1:215 ;
1 / (x * x) = (1 / x) * (1 / x) by XCMPLX_1:102;
then a * ((x ^2) + (1 / (x ^2))) = (- (b * (((x * (1 / x)) * (1 / x)) + x))) - c by A10;
then A11: a * ((x ^2) + (1 / (x ^2))) = (- (b * ((1 * (1 / x)) + x))) - c by A8, XCMPLX_1:106;
x * y = (x * x) + (x * (1 / x)) by A2;
then (x * y) + 0 = (x ^2) + 1 by A4, XCMPLX_1:106;
hence ( a * ((x ^2) + (1 / (x ^2))) = (- (b * (x + (1 / x)))) - c & ((x ^2) - (x * y)) + 1 = 0 ) by A11; :: thesis: verum
end;
case A12: x < 0 ; :: thesis: ( a * ((x ^2) + (1 / (x ^2))) = (- (b * (x + (1 / x)))) - c & ((x ^2) - (x * y)) + 1 = 0 )
set n = - ((b * x) + a);
set m = (a * (x ^2)) + ((b * x) + c);
((- x) |^ 3) + (x |^ 3) = - ((x |^ 3) + (- (x |^ 3))) by Lm2, POWER:2
.= (x |^ 3) - (x |^ 3) ;
then A13: x |^ 3 = - ((- x) |^ 3) ;
A14: 0 < - x by A12, XREAL_1:58;
(- x) |^ 4 = x |^ 4 by Lm1, POWER:1;
then A15: x |^ 4 = (- x) to_power (2 + 2) by POWER:41
.= ((- x) to_power 2) * ((- x) to_power 2) by A14, POWER:27
.= ((- x) ^2) * ((- x) to_power 2) by POWER:46
.= (x ^2) * ((- x) ^2) by POWER:46 ;
(- x) |^ 3 = (- x) to_power (2 + 1) by POWER:41
.= ((- x) to_power 2) * ((- x) to_power 1) by A14, POWER:27 ;
then A16: (- x) |^ 3 = ((- x) to_power 2) * (- x) ;
(- x) to_power 2 = (- x) ^2 by POWER:46
.= x ^2 ;
then ((a * (x ^2)) + ((b * x) + c)) * (x ^2) = (- ((b * x) + a)) * 1 by A3, A15, A16, A13;
then ((a * (x ^2)) + ((b * x) + c)) / 1 = (- ((b * x) + a)) / (x ^2) by A5, XCMPLX_1:94;
then (a * (x ^2)) + ((b * x) + c) = (- ((b * x) + a)) * (1 / (x ^2)) by XCMPLX_1:99
.= (- ((b * x) + a)) * ((x ^2) ") by XCMPLX_1:215
.= (- (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:215
.= (- (b * ((x * (1 / (x ^2))) + x))) - c by XCMPLX_1:215 ;
then a * ((x ^2) + (1 / (x ^2))) = (- (b * ((x * ((1 / x) * (1 / x))) + x))) - c by XCMPLX_1:102
.= (- (b * (((x * (1 / x)) * (1 / x)) + x))) - c ;
then A17: a * ((x ^2) + (1 / (x ^2))) = (- (b * ((1 * (1 / x)) + x))) - c by A12, XCMPLX_1:106;
x * y = (x * x) + (x * (1 / x)) by A2
.= (x * x) + 1 by A12, XCMPLX_1:106 ;
hence ( a * ((x ^2) + (1 / (x ^2))) = (- (b * (x + (1 / x)))) - c & ((x ^2) - (x * y)) + 1 = 0 ) by A17; :: 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:106
.= ((x ^2) + 2) + ((1 ^2) / (x ^2)) by XCMPLX_1:76
.= (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