let a, b, c, x, y be Real; ( a <> 0 & ((b ^2) - ((4 * a) * c)) + (8 * (a ^2)) > 0 & y = x + (1 / x) & Polynom (a,b,c,b,a,x) = 0 implies for y1, y2 being Real st y1 = ((- b) + (sqrt (((b ^2) - ((4 * a) * c)) + (8 * (a ^2))))) / (2 * a) & y2 = ((- b) - (sqrt (((b ^2) - ((4 * a) * c)) + (8 * (a ^2))))) / (2 * a) holds
( x <> 0 & ( x = (y1 + (sqrt (delta (1,(- y1),1)))) / 2 or x = (y2 + (sqrt (delta (1,(- y2),1)))) / 2 or x = (y1 - (sqrt (delta (1,(- y1),1)))) / 2 or x = (y2 - (sqrt (delta (1,(- y2),1)))) / 2 ) ) )
assume that
A1:
a <> 0
and
A2:
((b ^2) - ((4 * a) * c)) + (8 * (a ^2)) > 0
and
A3:
y = x + (1 / x)
and
A4:
Polynom (a,b,c,b,a,x) = 0
; for y1, y2 being Real st y1 = ((- b) + (sqrt (((b ^2) - ((4 * a) * c)) + (8 * (a ^2))))) / (2 * a) & y2 = ((- b) - (sqrt (((b ^2) - ((4 * a) * c)) + (8 * (a ^2))))) / (2 * a) holds
( x <> 0 & ( x = (y1 + (sqrt (delta (1,(- y1),1)))) / 2 or x = (y2 + (sqrt (delta (1,(- y2),1)))) / 2 or x = (y1 - (sqrt (delta (1,(- y1),1)))) / 2 or x = (y2 - (sqrt (delta (1,(- y2),1)))) / 2 ) )
A5:
x <> 0
by A1, A3, A4, Th2;
set f = c - (2 * a);
(((a * (y ^2)) + (b * y)) + c) - (2 * a) = 0
by A1, A3, A4, Th2;
then
((a * (y ^2)) + (b * y)) + (c - (2 * a)) = 0
;
then A6:
Polynom (a,b,(c - (2 * a)),y) = 0
by POLYEQ_1:def 2;
let y1, y2 be Real; ( y1 = ((- b) + (sqrt (((b ^2) - ((4 * a) * c)) + (8 * (a ^2))))) / (2 * a) & y2 = ((- b) - (sqrt (((b ^2) - ((4 * a) * c)) + (8 * (a ^2))))) / (2 * a) implies ( x <> 0 & ( x = (y1 + (sqrt (delta (1,(- y1),1)))) / 2 or x = (y2 + (sqrt (delta (1,(- y2),1)))) / 2 or x = (y1 - (sqrt (delta (1,(- y1),1)))) / 2 or x = (y2 - (sqrt (delta (1,(- y2),1)))) / 2 ) ) )
assume A7:
( y1 = ((- b) + (sqrt (((b ^2) - ((4 * a) * c)) + (8 * (a ^2))))) / (2 * a) & y2 = ((- b) - (sqrt (((b ^2) - ((4 * a) * c)) + (8 * (a ^2))))) / (2 * a) )
; ( x <> 0 & ( x = (y1 + (sqrt (delta (1,(- y1),1)))) / 2 or x = (y2 + (sqrt (delta (1,(- y2),1)))) / 2 or x = (y1 - (sqrt (delta (1,(- y1),1)))) / 2 or x = (y2 - (sqrt (delta (1,(- y2),1)))) / 2 ) )
x * y = (x ^2) + (x * (1 / x))
by A3;
then
(x * y) + 0 = (x ^2) + 1
by A5, XCMPLX_1:106;
then
((1 * (x ^2)) + ((- y) * x)) + 1 = 0
;
then A8:
Polynom (1,(- y),1,x) = 0
by POLYEQ_1:def 2;
delta (1,(- y),1) =
((- y) ^2) - ((4 * 1) * 1)
by QUIN_1:def 1
.=
(((x ^2) + (2 * (x * (1 / x)))) + ((1 / x) ^2)) - 4
by A3
.=
(((x ^2) + (2 * 1)) + ((1 / x) ^2)) - 4
by A5, XCMPLX_1:106
.=
(x ^2) + ((- (2 * 1)) + ((1 / x) ^2))
.=
(x ^2) + ((- (2 * (x * (1 / x)))) + ((1 / x) ^2))
by A5, XCMPLX_1:106
.=
(x - (1 / x)) ^2
;
then A9:
( x = ((- (- y)) + (sqrt (delta (1,(- y),1)))) / (2 * 1) or x = ((- (- y)) - (sqrt (delta (1,(- y),1)))) / (2 * 1) )
by A8, POLYEQ_1:5, XREAL_1:63;
A10:
(b ^2) - ((4 * a) * (c - (2 * a))) = ((b ^2) - ((4 * a) * c)) + (8 * (a ^2))
;
then
delta (a,b,(c - (2 * a))) > 0
by A2, QUIN_1:def 1;
then
( y = ((- b) + (sqrt (delta (a,b,(c - (2 * a)))))) / (2 * a) or y = ((- b) - (sqrt (delta (a,b,(c - (2 * a)))))) / (2 * a) )
by A1, A6, POLYEQ_1:5;
then
( y = y1 or y = y2 )
by A7, A10, QUIN_1:def 1;
hence
( x <> 0 & ( x = (y1 + (sqrt (delta (1,(- y1),1)))) / 2 or x = (y2 + (sqrt (delta (1,(- y2),1)))) / 2 or x = (y1 - (sqrt (delta (1,(- y1),1)))) / 2 or x = (y2 - (sqrt (delta (1,(- y2),1)))) / 2 ) )
by A1, A3, A4, A9, Th2; verum