let a, b be Real; ( a <> 0 & - 1 < a & a < 1 & b = (2 + (sqrt (delta ((a * a),(- 2),1)))) / ((2 * a) * a) implies (((((1 + (a * a)) * b) * b) - (2 * b)) + 1) - (b * b) = 0 )
assume that
A1:
a <> 0
and
A2:
( - 1 < a & a < 1 )
and
A3:
b = (2 + (sqrt (delta ((a * a),(- 2),1)))) / ((2 * a) * a)
; (((((1 + (a * a)) * b) * b) - (2 * b)) + 1) - (b * b) = 0
set x1 = ((- (- 2)) - (sqrt (delta ((a * a),(- 2),1)))) / (2 * (a * a));
set x2 = ((- (- 2)) + (sqrt (delta ((a * a),(- 2),1)))) / (2 * (a * a));
A4:
0 <= 1 - (a ^2)
delta ((a * a),(- 2),1) >= 0
then (((a * a) * (b ^2)) + ((- 2) * b)) + 1 =
((a * a) * (b - (((- (- 2)) - (sqrt (delta ((a * a),(- 2),1)))) / (2 * (a * a))))) * ((((- (- 2)) + (sqrt (delta ((a * a),(- 2),1)))) / (2 * (a * a))) - (((- (- 2)) + (sqrt (delta ((a * a),(- 2),1)))) / (2 * (a * a))))
by A3, A1, QUIN_1:16
.=
0
;
hence
(((((1 + (a * a)) * b) * b) - (2 * b)) + 1) - (b * b) = 0
; verum