let a, b, c, x be Complex; ( a <> 0 & delta (a,b,c) = 0 & Polynom (a,b,c,x) = 0 implies x = - (b / (2 * a)) )
assume that
A1:
a <> 0
and
A2:
delta (a,b,c) = 0
; ( not Polynom (a,b,c,x) = 0 or x = - (b / (2 * a)) )
set y = x;
set t = ((a ^2) * (x ^2)) + ((a * b) * x);
A3:
(b ^2) - ((4 * a) * c) = delta (a,b,c)
by QUIN_1:def 1;
assume
Polynom (a,b,c,x) = 0
; x = - (b / (2 * a))
then
a * (((a * (x ^2)) + (b * x)) + c) = 0
;
then
(((a ^2) * (x ^2)) + ((a * b) * x)) + (a * c) = 0
;
then
(((a * x) ^2) + (2 * (((a * x) * b) * (2 ")))) + ((b / 2) ^2) = 0
by A2, A3;
then
((a * x) + (b / 2)) ^2 = 0
;
then
(a * x) + (b / 2) = 0
by XCMPLX_1:6;
then x =
(- (b * (2 "))) / a
by A1, XCMPLX_1:89
.=
((- 1) * (b * (2 "))) * (a ")
by XCMPLX_0:def 9
.=
- ((b * ((2 ") * (a "))) * 1)
.=
- (b * ((2 * a) "))
by XCMPLX_1:204
;
hence
x = - (b / (2 * a))
by XCMPLX_0:def 9; verum