let z, a0, a1, s1, s2 be Complex; ( a1 = - (s1 + s2) & a0 = s1 * s2 implies ( ((z |^ 2) + (a1 * z)) + a0 = 0 iff ( z = s1 or z = s2 ) ) )
assume
( a1 = - (s1 + s2) & a0 = s1 * s2 )
; ( ((z |^ 2) + (a1 * z)) + a0 = 0 iff ( z = s1 or z = s2 ) )
then A1: (z - s1) * (z - s2) =
((z * z) + (a1 * z)) + a0
.=
((z |^ 2) + (a1 * z)) + a0
by Th1
;
hereby ( ( z = s1 or z = s2 ) implies ((z |^ 2) + (a1 * z)) + a0 = 0 )
assume
((z |^ 2) + (a1 * z)) + a0 = 0
;
( not z = s1 implies z = s2 )then A2:
(
z - s1 = 0 or
z - s2 = 0 )
by A1;
assume
not
z = s1
;
z = s2hence
z = s2
by A2;
verum
end;
assume
( z = s1 or z = s2 )
; ((z |^ 2) + (a1 * z)) + a0 = 0
hence
((z |^ 2) + (a1 * z)) + a0 = 0
by A1; verum