let z, s1, s2, q, r, s3, p be Complex; ( 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 ) ) )
set z1 = (s1 + s2) + s3;
set z2 = (s1 - s2) - s3;
set z3 = ((- s1) + s2) - s3;
set z4 = ((- s1) - s2) + s3;
assume
q <> 0
; ( 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)))
; ( 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)))
; ( 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 ) ) )
A4: s2 * s2 =
s2 |^ 2
by Th1
.=
2_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))
by A3, Th7
;
A5: s1 * s1 =
s1 |^ 2
by Th1
.=
1_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))
by A2, Th7
;
then A6:
((s1 * s1) * (s2 * s2)) * (3_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))) = - (- (q |^ 2))
by A4, Th19;
then A7:
(s1 * s1) * (s2 * s2) <> 0
by A1, Th1;
(s1 * s2) * (s1 * s2) <> 0
by A1, A6, Th1;
then A8:
s1 * s2 <> 0
;
assume A9:
s3 = - (q / (s1 * s2))
; ( (((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 A10: - (((((((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))))
.=
- ((8 * (s1 * s2)) * ((- q) / (s1 * s2)))
by XCMPLX_1:187
.=
- (8 * ((s1 * s2) * ((- q) / (s1 * s2))))
.=
- (8 * ((- q) / ((s1 * s2) / (s1 * s2))))
by XCMPLX_1:81
.=
- (8 * ((- q) / 1))
by A8, XCMPLX_1:60
.=
8 * q
;
A11: s3 * s3 =
((- q) / (s1 * s2)) * (- (q / (s1 * s2)))
by A9, XCMPLX_1:187
.=
((- q) / (s1 * s2)) * ((- q) / (s1 * s2))
by XCMPLX_1:187
.=
((- q) * (- q)) / ((s1 * s2) * (s1 * s2))
by XCMPLX_1:76
.=
(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 A6, Th1
.=
3_root_of_cubic ((- (q |^ 2)),((p |^ 2) - r),(2 * p))
by A7, XCMPLX_1:89
;
then A12:
((s1 * s1) + (s2 * s2)) + (s3 * s3) = - (2 * p)
by A5, A4, Th17;
then A13:
( - (((((s1 + s2) + s3) + ((s1 - s2) - s3)) + (((- s1) + s2) - s3)) + (((- s1) - s2) + s3)) = 0 & (((((((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 )
;
((((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 A12
.=
(4 * (p * p)) - (4 * ((p |^ 2) - r))
by A5, A4, A11, Th18
.=
(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 A13, A10, Th22;
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 ) )
; verum