let a, b, c, x, y be Real; ( 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)
; ( 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
; ( x <> 0 & (((a * (y ^2)) + (b * y)) + c) - (2 * a) = 0 )
A4:
x <> 0
then A5:
x ^2 > 0
by SQUARE_1:12;
A6:
x |^ 4 = x to_power (2 + 2)
by POWER:41;
A7:
now ( ( 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 A12:
x < 0
;
( 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;
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; verum