let z, a0, a1, a2, s1, s2, a3, s3, s4 be Complex; ( a3 = - (((s1 + s2) + s3) + s4) & a2 = (((((s1 * s2) + (s1 * s3)) + (s1 * s4)) + (s2 * s3)) + (s2 * s4)) + (s3 * s4) & a1 = - (((((s1 * s2) * s3) + ((s1 * s2) * s4)) + ((s1 * s3) * s4)) + ((s2 * s3) * s4)) & a0 = ((s1 * s2) * s3) * s4 implies ( ((((z |^ 4) + (a3 * (z |^ 3))) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 iff ( z = s1 or z = s2 or z = s3 or z = s4 ) ) )
assume
( a3 = - (((s1 + s2) + s3) + s4) & a2 = (((((s1 * s2) + (s1 * s3)) + (s1 * s4)) + (s2 * s3)) + (s2 * s4)) + (s3 * s4) & a1 = - (((((s1 * s2) * s3) + ((s1 * s2) * s4)) + ((s1 * s3) * s4)) + ((s2 * s3) * s4)) & a0 = ((s1 * s2) * s3) * s4 )
; ( ((((z |^ 4) + (a3 * (z |^ 3))) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 iff ( z = s1 or z = s2 or z = s3 or z = s4 ) )
then A1: (((z - s1) * (z - s2)) * (z - s3)) * (z - s4) =
((((((z * z) * z) * z) + (((a3 * z) * z) * z)) + ((a2 * z) * z)) + (a1 * z)) + a0
.=
((((z |^ 4) + (a3 * ((z * z) * z))) + ((a2 * z) * z)) + (a1 * z)) + a0
by Th3
.=
((((z |^ 4) + (a3 * (z |^ 3))) + (a2 * (z * z))) + (a1 * z)) + a0
by Th2
.=
((((z |^ 4) + (a3 * (z |^ 3))) + (a2 * (z |^ 2))) + (a1 * z)) + a0
by Th1
;
hereby ( ( z = s1 or z = s2 or z = s3 or z = s4 ) implies ((((z |^ 4) + (a3 * (z |^ 3))) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 )
assume
((((z |^ 4) + (a3 * (z |^ 3))) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0
;
( not z = s1 & not z = s2 & not z = s3 implies z = s4 )then A2:
(
((z - s1) * (z - s2)) * (z - s3) = 0 or
z - s4 = 0 )
by A1;
assume that A3:
( not
z = s1 & not
z = s2 )
and A4:
not
z = s3
;
z = s4A5:
z - s3 <> 0
by A4;
(
z - s1 <> 0 &
z - s2 <> 0 )
by A3;
hence
z = s4
by A2, A5;
verum
end;
assume
( z = s1 or z = s2 or z = s3 or z = s4 )
; ((((z |^ 4) + (a3 * (z |^ 3))) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0
hence
((((z |^ 4) + (a3 * (z |^ 3))) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0
by A1; verum