let z, a0, a1, a2 be Complex; ( a2 <> 0 implies ( ((a2 * (z |^ 2)) + (a1 * z)) + a0 = 0 iff ( z = (- (a1 / (2 * a2))) + ((2 -root (delta (a0,a1,a2))) / (2 * a2)) or z = (- (a1 / (2 * a2))) - ((2 -root (delta (a0,a1,a2))) / (2 * a2)) ) ) )
set s1 = (- (a1 / (2 * a2))) + ((2 -root (delta (a0,a1,a2))) / (2 * a2));
set s2 = (- (a1 / (2 * a2))) - ((2 -root (delta (a0,a1,a2))) / (2 * a2));
A1: - (((- (a1 / (2 * a2))) + ((2 -root (delta (a0,a1,a2))) / (2 * a2))) + ((- (a1 / (2 * a2))) - ((2 -root (delta (a0,a1,a2))) / (2 * a2)))) =
(a1 / (2 * a2)) + (a1 / (2 * a2))
.=
((1 / 2) * (a1 / a2)) + (a1 / (2 * a2))
by XCMPLX_1:103
.=
((1 / 2) * (a1 / a2)) + ((1 / 2) * (a1 / a2))
by XCMPLX_1:103
.=
a1 / a2
;
assume A2:
a2 <> 0
; ( ((a2 * (z |^ 2)) + (a1 * z)) + a0 = 0 iff ( z = (- (a1 / (2 * a2))) + ((2 -root (delta (a0,a1,a2))) / (2 * a2)) or z = (- (a1 / (2 * a2))) - ((2 -root (delta (a0,a1,a2))) / (2 * a2)) ) )
then ((a2 * (z |^ 2)) + (a1 * z)) + a0 =
((((a2 * (z |^ 2)) + (a1 * z)) + a0) / a2) * a2
by XCMPLX_1:87
.=
((((a2 * (z |^ 2)) / a2) + ((a1 * z) / a2)) + (a0 / a2)) * a2
by XCMPLX_1:63
.=
(((z |^ 2) + ((a1 * z) / a2)) + (a0 / a2)) * a2
by A2, XCMPLX_1:89
.=
(((z |^ 2) + (a1 * (z / a2))) + (a0 / a2)) * a2
by XCMPLX_1:74
.=
(((z |^ 2) + (z / (a2 / a1))) + (a0 / a2)) * a2
by XCMPLX_1:81
.=
(((z |^ 2) + ((a1 / a2) * z)) + (a0 / a2)) * a2
by XCMPLX_1:79
;
then A3:
( ((a2 * (z |^ 2)) + (a1 * z)) + a0 = 0 iff ((z |^ 2) + ((a1 / a2) * z)) + (a0 / a2) = 0 )
by A2;
((- (a1 / (2 * a2))) + ((2 -root (delta (a0,a1,a2))) / (2 * a2))) * ((- (a1 / (2 * a2))) - ((2 -root (delta (a0,a1,a2))) / (2 * a2))) =
((a1 / (2 * a2)) * (a1 / (2 * a2))) - (((2 -root (delta (a0,a1,a2))) / (2 * a2)) * ((2 -root (delta (a0,a1,a2))) / (2 * a2)))
.=
((a1 * a1) / ((2 * a2) * (2 * a2))) - (((2 -root (delta (a0,a1,a2))) / (2 * a2)) * ((2 -root (delta (a0,a1,a2))) / (2 * a2)))
by XCMPLX_1:76
.=
((a1 * a1) / ((4 * a2) * a2)) - (((2 -root (delta (a0,a1,a2))) * (2 -root (delta (a0,a1,a2)))) / ((2 * a2) * (2 * a2)))
by XCMPLX_1:76
.=
((a1 * a1) / ((4 * a2) * a2)) - (((2 -root (delta (a0,a1,a2))) |^ 2) / ((2 * a2) * (2 * a2)))
by Th1
.=
((a1 * a1) / ((4 * a2) * a2)) - ((delta (a0,a1,a2)) / ((2 * a2) * (2 * a2)))
by Th7
.=
((a1 * a1) - (delta (a0,a1,a2))) / ((4 * a2) * a2)
by XCMPLX_1:120
.=
(a0 * (4 * a2)) / (a2 * (4 * a2))
.=
(a0 / a2) * ((4 * a2) / (4 * a2))
by XCMPLX_1:76
.=
(a0 / a2) * 1
by A2, XCMPLX_1:60
.=
a0 / a2
;
hence
( ((a2 * (z |^ 2)) + (a1 * z)) + a0 = 0 iff ( z = (- (a1 / (2 * a2))) + ((2 -root (delta (a0,a1,a2))) / (2 * a2)) or z = (- (a1 / (2 * a2))) - ((2 -root (delta (a0,a1,a2))) / (2 * a2)) ) )
by A3, A1, Th11; verum