let z, s1, s2, q, r, s3, p be complex number ; :: thesis: ( q <> 0 & 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) + ((4 * p) * (z |^ 2))) + ((8 * q) * z)) + (4 * r) = 0 iff ( z = (s1 + s2) + s3 or z = (s1 - s2) - s3 or z = ((- s1) + s2) - s3 or z = ((- s1) - s2) + s3 ) ) )
assume q <> 0 ; :: thesis: ( 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) + ((4 * p) * (z |^ 2))) + ((8 * q) * z)) + (4 * r) = 0 iff ( z = (s1 + s2) + s3 or z = (s1 - s2) - s3 or z = ((- s1) + s2) - s3 or z = ((- s1) - s2) + s3 ) ) )
then A1: q * q <> 0 ;
assume A2: s1 = 2 -root (1_root_of_cubic (- (q |^ 2)),((p |^ 2) - r),(2 * p)) ; :: thesis: ( not s2 = 2 -root (2_root_of_cubic (- (q |^ 2)),((p |^ 2) - r),(2 * p)) or not s3 = - (q / (s1 * s2)) or ( (((z |^ 4) + ((4 * p) * (z |^ 2))) + ((8 * q) * z)) + (4 * r) = 0 iff ( z = (s1 + s2) + s3 or z = (s1 - s2) - s3 or z = ((- s1) + s2) - s3 or z = ((- s1) - s2) + s3 ) ) )
assume A3: s2 = 2 -root (2_root_of_cubic (- (q |^ 2)),((p |^ 2) - r),(2 * p)) ; :: thesis: ( not s3 = - (q / (s1 * s2)) or ( (((z |^ 4) + ((4 * p) * (z |^ 2))) + ((8 * q) * z)) + (4 * r) = 0 iff ( z = (s1 + s2) + s3 or z = (s1 - s2) - s3 or z = ((- s1) + s2) - s3 or z = ((- s1) - s2) + s3 ) ) )
assume A4: s3 = - (q / (s1 * s2)) ; :: thesis: ( (((z |^ 4) + ((4 * p) * (z |^ 2))) + ((8 * q) * z)) + (4 * r) = 0 iff ( z = (s1 + s2) + s3 or z = (s1 - s2) - s3 or z = ((- s1) + s2) - s3 or z = ((- s1) - s2) + s3 ) )
set z1 = (s1 + s2) + s3;
set z2 = (s1 - s2) - s3;
set z3 = ((- s1) + s2) - s3;
set z4 = ((- s1) - s2) + s3;
A5: s1 * s1 = s1 |^ 2 by Th1
.= 1_root_of_cubic (- (q |^ 2)),((p |^ 2) - r),(2 * p) by A2, Th8 ;
A6: s2 * s2 = s2 |^ 2 by Th1
.= 2_root_of_cubic (- (q |^ 2)),((p |^ 2) - r),(2 * p) by A3, Th8 ;
A7: ((s1 * s1) * (s2 * s2)) * (3_root_of_cubic (- (q |^ 2)),((p |^ 2) - r),(2 * p)) = - (- (q |^ 2)) by A5, A6, Th19;
then A8: (s1 * s1) * (s2 * s2) <> 0 by A1, Th1;
(s1 * s2) * (s1 * s2) <> 0 by A7, A1, Th1;
then A9: s1 * s2 <> 0 ;
A10: s3 * s3 = ((- q) / (s1 * s2)) * (- (q / (s1 * s2))) by A4, XCMPLX_1:188
.= ((- q) / (s1 * s2)) * ((- q) / (s1 * s2)) by XCMPLX_1:188
.= ((- q) * (- q)) / ((s1 * s2) * (s1 * s2)) by XCMPLX_1:77
.= (q * q) / ((s1 * s1) * (s2 * s2))
.= ((3_root_of_cubic (- (q |^ 2)),((p |^ 2) - r),(2 * p)) * ((s1 * s1) * (s2 * s2))) / ((s1 * s1) * (s2 * s2)) by A7, Th1
.= 3_root_of_cubic (- (q |^ 2)),((p |^ 2) - r),(2 * p) by A8, XCMPLX_1:90 ;
A11: ((s1 * s1) + (s2 * s2)) + (s3 * s3) = - (2 * p) by Th18, A5, A6, A10;
A12: - (((((s1 + s2) + s3) + ((s1 - s2) - s3)) + (((- s1) + s2) - s3)) + (((- s1) - s2) + s3)) = 0 ;
A13: (((((((s1 + s2) + s3) * ((s1 - s2) - s3)) + (((s1 + s2) + s3) * (((- s1) + s2) - s3))) + (((s1 + s2) + s3) * (((- s1) - s2) + s3))) + (((s1 - s2) - s3) * (((- s1) + s2) - s3))) + (((s1 - s2) - s3) * (((- s1) - s2) + s3))) + ((((- s1) + s2) - s3) * (((- s1) - s2) + s3)) = 4 * p by A11;
A14: - (((((((s1 + s2) + s3) * ((s1 - s2) - s3)) * (((- s1) + s2) - s3)) + ((((s1 + s2) + s3) * ((s1 - s2) - s3)) * (((- s1) - s2) + s3))) + ((((s1 + s2) + s3) * (((- s1) + s2) - s3)) * (((- s1) - s2) + s3))) + ((((s1 - s2) - s3) * (((- s1) + s2) - s3)) * (((- s1) - s2) + s3))) = - ((8 * (s1 * s2)) * (- (q / (s1 * s2)))) by A4
.= - ((8 * (s1 * s2)) * ((- q) / (s1 * s2))) by XCMPLX_1:188
.= - (8 * ((s1 * s2) * ((- q) / (s1 * s2))))
.= - (8 * ((- q) / ((s1 * s2) / (s1 * s2)))) by XCMPLX_1:82
.= - (8 * ((- q) / 1)) by A9, XCMPLX_1:60
.= 8 * q ;
((((s1 + s2) + s3) * ((s1 - s2) - s3)) * (((- s1) + s2) - s3)) * (((- s1) - s2) + s3) = ((((s1 * s1) + (s2 * s2)) + (s3 * s3)) * (((s1 * s1) + (s2 * s2)) + (s3 * s3))) - (4 * ((((s1 * s1) * (s2 * s2)) + ((s1 * s1) * (s3 * s3))) + ((s2 * s2) * (s3 * s3))))
.= ((- (2 * p)) * (- (2 * p))) - (4 * ((((s1 * s1) * (s2 * s2)) + ((s1 * s1) * (s3 * s3))) + ((s2 * s2) * (s3 * s3)))) by A11
.= (4 * (p * p)) - (4 * ((p |^ 2) - r)) by Th20, A5, A6, A10
.= (4 * (p |^ 2)) - (4 * ((p |^ 2) - r)) by Th1
.= 4 * r ;
then ( ((((z |^ 4) + (0 * (z |^ 3))) + ((4 * p) * (z |^ 2))) + ((8 * q) * z)) + (4 * r) = 0 iff ( z = (s1 + s2) + s3 or z = (s1 - s2) - s3 or z = ((- s1) + s2) - s3 or z = ((- s1) - s2) + s3 ) ) by A12, A13, A14, Th23;
hence ( (((z |^ 4) + ((4 * p) * (z |^ 2))) + ((8 * q) * z)) + (4 * r) = 0 iff ( z = (s1 + s2) + s3 or z = (s1 - s2) - s3 or z = ((- s1) + s2) - s3 or z = ((- s1) - s2) + s3 ) ) ; :: thesis: verum