let a, b, c, x, y be real number ; :: 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 number ; :: 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:107;
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:107
.= (x ^2 ) + ((- (2 * 1)) + ((1 / x) ^2 ))
.= (x ^2 ) + ((- (2 * (x * (1 / x)))) + ((1 / x) ^2 )) by A5, XCMPLX_1:107
.= (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:65;
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: