let z, a0, a1, a2, s1, s2, a3, q, r, s3, p be Complex; ( p = ((8 * a2) - (3 * (a3 |^ 2))) / 32 & q = (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64 & q <> 0 & r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 & s1 = 2 -root (1_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) & s2 = 2 -root (2_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) & s3 = - (q / (s1 * s2)) implies ( ((((z |^ 4) + (a3 * (z |^ 3))) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 iff ( z = ((s1 + s2) + s3) - (a3 / 4) or z = ((s1 - s2) - s3) - (a3 / 4) or z = (((- s1) + s2) - s3) - (a3 / 4) or z = (((- s1) - s2) + s3) - (a3 / 4) ) ) )
assume A1:
p = ((8 * a2) - (3 * (a3 |^ 2))) / 32
; ( not q = (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64 or not q <> 0 or not r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 or not s1 = 2 -root (1_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) or not s2 = 2 -root (2_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) or not s3 = - (q / (s1 * s2)) or ( ((((z |^ 4) + (a3 * (z |^ 3))) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 iff ( z = ((s1 + s2) + s3) - (a3 / 4) or z = ((s1 - s2) - s3) - (a3 / 4) or z = (((- s1) + s2) - s3) - (a3 / 4) or z = (((- s1) - s2) + s3) - (a3 / 4) ) ) )
set x = z + (a3 / 4);
assume that
A2:
q = (((8 * a1) - ((4 * a2) * a3)) + (a3 |^ 3)) / 64
and
A3:
q <> 0
; ( not r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024 or not s1 = 2 -root (1_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) or not s2 = 2 -root (2_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) or not s3 = - (q / (s1 * s2)) or ( ((((z |^ 4) + (a3 * (z |^ 3))) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 iff ( z = ((s1 + s2) + s3) - (a3 / 4) or z = ((s1 - s2) - s3) - (a3 / 4) or z = (((- s1) + s2) - s3) - (a3 / 4) or z = (((- s1) - s2) + s3) - (a3 / 4) ) ) )
assume A4:
r = ((((256 * a0) - ((64 * a3) * a1)) + ((16 * (a3 |^ 2)) * a2)) - (3 * (a3 |^ 4))) / 1024
; ( not s1 = 2 -root (1_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) or not s2 = 2 -root (2_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) or not s3 = - (q / (s1 * s2)) or ( ((((z |^ 4) + (a3 * (z |^ 3))) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 iff ( z = ((s1 + s2) + s3) - (a3 / 4) or z = ((s1 - s2) - s3) - (a3 / 4) or z = (((- s1) + s2) - s3) - (a3 / 4) or z = (((- s1) - s2) + s3) - (a3 / 4) ) ) )
A5:
z = (z + (a3 / 4)) - (a3 / 4)
;
assume
( s1 = 2 -root (1_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) & s2 = 2 -root (2_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) & s3 = - (q / (s1 * s2)) )
; ( ((((z |^ 4) + (a3 * (z |^ 3))) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 iff ( z = ((s1 + s2) + s3) - (a3 / 4) or z = ((s1 - s2) - s3) - (a3 / 4) or z = (((- s1) + s2) - s3) - (a3 / 4) or z = (((- s1) - s2) + s3) - (a3 / 4) ) )
then
( ((((z + (a3 / 4)) |^ 4) + ((4 * p) * ((z + (a3 / 4)) |^ 2))) + ((8 * q) * (z + (a3 / 4)))) + (4 * r) = 0 iff ( z + (a3 / 4) = (s1 + s2) + s3 or z + (a3 / 4) = (s1 - s2) - s3 or z + (a3 / 4) = ((- s1) + s2) - s3 or z + (a3 / 4) = ((- s1) - s2) + s3 ) )
by A3, Th23;
hence
( ((((z |^ 4) + (a3 * (z |^ 3))) + (a2 * (z |^ 2))) + (a1 * z)) + a0 = 0 iff ( z = ((s1 + s2) + s3) - (a3 / 4) or z = ((s1 - s2) - s3) - (a3 / 4) or z = (((- s1) + s2) - s3) - (a3 / 4) or z = (((- s1) - s2) + s3) - (a3 / 4) ) )
by A1, A2, A4, A5, Th21; verum