let x, a, b, c be Real; ( a <> 0 & delta (a,b,c) >= 0 & ((a * (x ^2)) + (b * x)) + c = 0 & not x = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) implies x = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) )
assume that
A1:
a <> 0
and
A2:
delta (a,b,c) >= 0
and
A3:
((a * (x ^2)) + (b * x)) + c = 0
; ( x = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) or x = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) )
((((2 * a) * x) + b) ^2) - (delta (a,b,c)) = 0
by A1, A3, Th14;
then
(((2 * a) * x) + b) ^2 = (sqrt (delta (a,b,c))) ^2
by A2, SQUARE_1:def 2;
then A4:
( ((2 * a) * x) + b = sqrt (delta (a,b,c)) or ((2 * a) * x) + b = - (sqrt (delta (a,b,c))) )
by Lm1;
2 * a <> 0
by A1;
hence
( x = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) or x = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) )
by A4, XCMPLX_1:89; verum