let a, b, c, x, y be Real; :: thesis:
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 ; :: thesis:
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; :: thesis:
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) ) ; :: thesis:
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; :: thesis: