Metamath Proof Explorer

Theorem quart

Description: The quartic equation, writing out all roots using square and cube root functions so that only direct substitutions remain, and we can actually claim to have a "quartic equation". Naturally, this theorem is ridiculously long (see quartfull ) if all the substitutions are performed. This is Metamath 100 proof #46. (Contributed by Mario Carneiro, 6-May-2015)

Ref Expression
Hypotheses quart.a ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
quart.b ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
quart.c ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
quart.d ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
quart.x ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
quart.e ⊢ ( 𝜑 → 𝐸 = - ( 𝐴 / 4 ) )
quart.p ⊢ ( 𝜑 → 𝑃 = ( 𝐵 − ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) ) )
quart.q ⊢ ( 𝜑 → 𝑄 = ( ( 𝐶 − ( ( 𝐴 · 𝐵 ) / 2 ) ) + ( ( 𝐴 ↑ 3 ) / 8 ) ) )
quart.r ⊢ ( 𝜑 → 𝑅 = ( ( 𝐷 − ( ( 𝐶 · 𝐴 ) / 4 ) ) + ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / 1 6 ) − ( ( 3 / 2 5 6 ) · ( 𝐴 ↑ 4 ) ) ) ) )
quart.u ⊢ ( 𝜑 → 𝑈 = ( ( 𝑃 ↑ 2 ) + ( 1 2 · 𝑅 ) ) )
quart.v ⊢ ( 𝜑 → 𝑉 = ( ( - ( 2 · ( 𝑃 ↑ 3 ) ) − ( 2 7 · ( 𝑄 ↑ 2 ) ) ) + ( 7 2 · ( 𝑃 · 𝑅 ) ) ) )
quart.w ⊢ ( 𝜑 → 𝑊 = ( √ ‘ ( ( 𝑉 ↑ 2 ) − ( 4 · ( 𝑈 ↑ 3 ) ) ) ) )
quart.s ⊢ ( 𝜑 → 𝑆 = ( ( √ ‘ 𝑀 ) / 2 ) )
quart.m ⊢ ( 𝜑 → 𝑀 = - ( ( ( ( 2 · 𝑃 ) + 𝑇 ) + ( 𝑈 / 𝑇 ) ) / 3 ) )
quart.t ⊢ ( 𝜑 → 𝑇 = ( ( ( 𝑉 + 𝑊 ) / 2 ) ↑𝑐 ( 1 / 3 ) ) )
quart.t0 ⊢ ( 𝜑 → 𝑇 ≠ 0 )
quart.m0 ⊢ ( 𝜑 → 𝑀 ≠ 0 )
quart.i ⊢ ( 𝜑 → 𝐼 = ( √ ‘ ( ( - ( 𝑆 ↑ 2 ) − ( 𝑃 / 2 ) ) + ( ( 𝑄 / 4 ) / 𝑆 ) ) ) )
quart.j ⊢ ( 𝜑 → 𝐽 = ( √ ‘ ( ( - ( 𝑆 ↑ 2 ) − ( 𝑃 / 2 ) ) − ( ( 𝑄 / 4 ) / 𝑆 ) ) ) )
Assertion quart ( 𝜑 → ( ( ( ( 𝑋 ↑ 4 ) + ( 𝐴 · ( 𝑋 ↑ 3 ) ) ) + ( ( 𝐵 · ( 𝑋 ↑ 2 ) ) + ( ( 𝐶 · 𝑋 ) + 𝐷 ) ) ) = 0 ↔ ( ( 𝑋 = ( ( 𝐸 − 𝑆 ) + 𝐼 ) ∨ 𝑋 = ( ( 𝐸 − 𝑆 ) − 𝐼 ) ) ∨ ( 𝑋 = ( ( 𝐸 + 𝑆 ) + 𝐽 ) ∨ 𝑋 = ( ( 𝐸 + 𝑆 ) − 𝐽 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 quart.a ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2 quart.b ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
3 quart.c ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
4 quart.d ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
5 quart.x ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
6 quart.e ⊢ ( 𝜑 → 𝐸 = - ( 𝐴 / 4 ) )
7 quart.p ⊢ ( 𝜑 → 𝑃 = ( 𝐵 − ( ( 3 / 8 ) · ( 𝐴 ↑ 2 ) ) ) )
8 quart.q ⊢ ( 𝜑 → 𝑄 = ( ( 𝐶 − ( ( 𝐴 · 𝐵 ) / 2 ) ) + ( ( 𝐴 ↑ 3 ) / 8 ) ) )
9 quart.r ⊢ ( 𝜑 → 𝑅 = ( ( 𝐷 − ( ( 𝐶 · 𝐴 ) / 4 ) ) + ( ( ( ( 𝐴 ↑ 2 ) · 𝐵 ) / 1 6 ) − ( ( 3 / 2 5 6 ) · ( 𝐴 ↑ 4 ) ) ) ) )
10 quart.u ⊢ ( 𝜑 → 𝑈 = ( ( 𝑃 ↑ 2 ) + ( 1 2 · 𝑅 ) ) )
11 quart.v ⊢ ( 𝜑 → 𝑉 = ( ( - ( 2 · ( 𝑃 ↑ 3 ) ) − ( 2 7 · ( 𝑄 ↑ 2 ) ) ) + ( 7 2 · ( 𝑃 · 𝑅 ) ) ) )
12 quart.w ⊢ ( 𝜑 → 𝑊 = ( √ ‘ ( ( 𝑉 ↑ 2 ) − ( 4 · ( 𝑈 ↑ 3 ) ) ) ) )
13 quart.s ⊢ ( 𝜑 → 𝑆 = ( ( √ ‘ 𝑀 ) / 2 ) )
14 quart.m ⊢ ( 𝜑 → 𝑀 = - ( ( ( ( 2 · 𝑃 ) + 𝑇 ) + ( 𝑈 / 𝑇 ) ) / 3 ) )
15 quart.t ⊢ ( 𝜑 → 𝑇 = ( ( ( 𝑉 + 𝑊 ) / 2 ) ↑𝑐 ( 1 / 3 ) ) )
16 quart.t0 ⊢ ( 𝜑 → 𝑇 ≠ 0 )
17 quart.m0 ⊢ ( 𝜑 → 𝑀 ≠ 0 )
18 quart.i ⊢ ( 𝜑 → 𝐼 = ( √ ‘ ( ( - ( 𝑆 ↑ 2 ) − ( 𝑃 / 2 ) ) + ( ( 𝑄 / 4 ) / 𝑆 ) ) ) )
19 quart.j ⊢ ( 𝜑 → 𝐽 = ( √ ‘ ( ( - ( 𝑆 ↑ 2 ) − ( 𝑃 / 2 ) ) − ( ( 𝑄 / 4 ) / 𝑆 ) ) ) )
20 6 oveq2d ⊢ ( 𝜑 → ( 𝑋 − 𝐸 ) = ( 𝑋 − - ( 𝐴 / 4 ) ) )
21 4cn ⊢ 4 ∈ ℂ
22 21 a1i ⊢ ( 𝜑 → 4 ∈ ℂ )
23 4ne0 ⊢ 4 ≠ 0
24 23 a1i ⊢ ( 𝜑 → 4 ≠ 0 )
25 1 22 24 divcld ⊢ ( 𝜑 → ( 𝐴 / 4 ) ∈ ℂ )
26 5 25 subnegd ⊢ ( 𝜑 → ( 𝑋 − - ( 𝐴 / 4 ) ) = ( 𝑋 + ( 𝐴 / 4 ) ) )
27 20 26 eqtrd ⊢ ( 𝜑 → ( 𝑋 − 𝐸 ) = ( 𝑋 + ( 𝐴 / 4 ) ) )
28 1 2 3 4 7 8 9 5 27 quart1 ⊢ ( 𝜑 → ( ( ( 𝑋 ↑ 4 ) + ( 𝐴 · ( 𝑋 ↑ 3 ) ) ) + ( ( 𝐵 · ( 𝑋 ↑ 2 ) ) + ( ( 𝐶 · 𝑋 ) + 𝐷 ) ) ) = ( ( ( ( 𝑋 − 𝐸 ) ↑ 4 ) + ( 𝑃 · ( ( 𝑋 − 𝐸 ) ↑ 2 ) ) ) + ( ( 𝑄 · ( 𝑋 − 𝐸 ) ) + 𝑅 ) ) )
29 28 eqeq1d ⊢ ( 𝜑 → ( ( ( ( 𝑋 ↑ 4 ) + ( 𝐴 · ( 𝑋 ↑ 3 ) ) ) + ( ( 𝐵 · ( 𝑋 ↑ 2 ) ) + ( ( 𝐶 · 𝑋 ) + 𝐷 ) ) ) = 0 ↔ ( ( ( ( 𝑋 − 𝐸 ) ↑ 4 ) + ( 𝑃 · ( ( 𝑋 − 𝐸 ) ↑ 2 ) ) ) + ( ( 𝑄 · ( 𝑋 − 𝐸 ) ) + 𝑅 ) ) = 0 ) )
30 1 2 3 4 7 8 9 quart1cl ⊢ ( 𝜑 → ( 𝑃 ∈ ℂ ∧ 𝑄 ∈ ℂ ∧ 𝑅 ∈ ℂ ) )
31 30 simp1d ⊢ ( 𝜑 → 𝑃 ∈ ℂ )
32 30 simp2d ⊢ ( 𝜑 → 𝑄 ∈ ℂ )
33 25 negcld ⊢ ( 𝜑 → - ( 𝐴 / 4 ) ∈ ℂ )
34 6 33 eqeltrd ⊢ ( 𝜑 → 𝐸 ∈ ℂ )
35 5 34 subcld ⊢ ( 𝜑 → ( 𝑋 − 𝐸 ) ∈ ℂ )
36 1 2 3 4 1 6 7 8 9 10 11 12 13 14 15 16 quartlem3 ⊢ ( 𝜑 → ( 𝑆 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑇 ∈ ℂ ) )
37 36 simp1d ⊢ ( 𝜑 → 𝑆 ∈ ℂ )
38 13 oveq2d ⊢ ( 𝜑 → ( 2 · 𝑆 ) = ( 2 · ( ( √ ‘ 𝑀 ) / 2 ) ) )
39 36 simp2d ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
40 39 sqrtcld ⊢ ( 𝜑 → ( √ ‘ 𝑀 ) ∈ ℂ )
41 2cnd ⊢ ( 𝜑 → 2 ∈ ℂ )
42 2ne0 ⊢ 2 ≠ 0
43 42 a1i ⊢ ( 𝜑 → 2 ≠ 0 )
44 40 41 43 divcan2d ⊢ ( 𝜑 → ( 2 · ( ( √ ‘ 𝑀 ) / 2 ) ) = ( √ ‘ 𝑀 ) )
45 38 44 eqtrd ⊢ ( 𝜑 → ( 2 · 𝑆 ) = ( √ ‘ 𝑀 ) )
46 45 oveq1d ⊢ ( 𝜑 → ( ( 2 · 𝑆 ) ↑ 2 ) = ( ( √ ‘ 𝑀 ) ↑ 2 ) )
47 39 sqsqrtd ⊢ ( 𝜑 → ( ( √ ‘ 𝑀 ) ↑ 2 ) = 𝑀 )
48 46 47 eqtr2d ⊢ ( 𝜑 → 𝑀 = ( ( 2 · 𝑆 ) ↑ 2 ) )
49 1 2 3 4 1 6 7 8 9 10 11 12 13 14 15 16 17 18 19 quartlem4 ⊢ ( 𝜑 → ( 𝑆 ≠ 0 ∧ 𝐼 ∈ ℂ ∧ 𝐽 ∈ ℂ ) )
50 49 simp2d ⊢ ( 𝜑 → 𝐼 ∈ ℂ )
51 18 oveq1d ⊢ ( 𝜑 → ( 𝐼 ↑ 2 ) = ( ( √ ‘ ( ( - ( 𝑆 ↑ 2 ) − ( 𝑃 / 2 ) ) + ( ( 𝑄 / 4 ) / 𝑆 ) ) ) ↑ 2 ) )
52 37 sqcld ⊢ ( 𝜑 → ( 𝑆 ↑ 2 ) ∈ ℂ )
53 52 negcld ⊢ ( 𝜑 → - ( 𝑆 ↑ 2 ) ∈ ℂ )
54 31 halfcld ⊢ ( 𝜑 → ( 𝑃 / 2 ) ∈ ℂ )
55 53 54 subcld ⊢ ( 𝜑 → ( - ( 𝑆 ↑ 2 ) − ( 𝑃 / 2 ) ) ∈ ℂ )
56 32 22 24 divcld ⊢ ( 𝜑 → ( 𝑄 / 4 ) ∈ ℂ )
57 49 simp1d ⊢ ( 𝜑 → 𝑆 ≠ 0 )
58 56 37 57 divcld ⊢ ( 𝜑 → ( ( 𝑄 / 4 ) / 𝑆 ) ∈ ℂ )
59 55 58 addcld ⊢ ( 𝜑 → ( ( - ( 𝑆 ↑ 2 ) − ( 𝑃 / 2 ) ) + ( ( 𝑄 / 4 ) / 𝑆 ) ) ∈ ℂ )
60 59 sqsqrtd ⊢ ( 𝜑 → ( ( √ ‘ ( ( - ( 𝑆 ↑ 2 ) − ( 𝑃 / 2 ) ) + ( ( 𝑄 / 4 ) / 𝑆 ) ) ) ↑ 2 ) = ( ( - ( 𝑆 ↑ 2 ) − ( 𝑃 / 2 ) ) + ( ( 𝑄 / 4 ) / 𝑆 ) ) )
61 51 60 eqtrd ⊢ ( 𝜑 → ( 𝐼 ↑ 2 ) = ( ( - ( 𝑆 ↑ 2 ) − ( 𝑃 / 2 ) ) + ( ( 𝑄 / 4 ) / 𝑆 ) ) )
62 30 simp3d ⊢ ( 𝜑 → 𝑅 ∈ ℂ )
63 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
64 3z ⊢ 3 ∈ ℤ
65 1exp ⊢ ( 3 ∈ ℤ → ( 1 ↑ 3 ) = 1 )
66 64 65 mp1i ⊢ ( 𝜑 → ( 1 ↑ 3 ) = 1 )
67 36 simp3d ⊢ ( 𝜑 → 𝑇 ∈ ℂ )
68 67 mulid2d ⊢ ( 𝜑 → ( 1 · 𝑇 ) = 𝑇 )
69 68 oveq2d ⊢ ( 𝜑 → ( ( 2 · 𝑃 ) + ( 1 · 𝑇 ) ) = ( ( 2 · 𝑃 ) + 𝑇 ) )
70 68 oveq2d ⊢ ( 𝜑 → ( 𝑈 / ( 1 · 𝑇 ) ) = ( 𝑈 / 𝑇 ) )
71 69 70 oveq12d ⊢ ( 𝜑 → ( ( ( 2 · 𝑃 ) + ( 1 · 𝑇 ) ) + ( 𝑈 / ( 1 · 𝑇 ) ) ) = ( ( ( 2 · 𝑃 ) + 𝑇 ) + ( 𝑈 / 𝑇 ) ) )
72 71 oveq1d ⊢ ( 𝜑 → ( ( ( ( 2 · 𝑃 ) + ( 1 · 𝑇 ) ) + ( 𝑈 / ( 1 · 𝑇 ) ) ) / 3 ) = ( ( ( ( 2 · 𝑃 ) + 𝑇 ) + ( 𝑈 / 𝑇 ) ) / 3 ) )
73 72 negeqd ⊢ ( 𝜑 → - ( ( ( ( 2 · 𝑃 ) + ( 1 · 𝑇 ) ) + ( 𝑈 / ( 1 · 𝑇 ) ) ) / 3 ) = - ( ( ( ( 2 · 𝑃 ) + 𝑇 ) + ( 𝑈 / 𝑇 ) ) / 3 ) )
74 14 73 eqtr4d ⊢ ( 𝜑 → 𝑀 = - ( ( ( ( 2 · 𝑃 ) + ( 1 · 𝑇 ) ) + ( 𝑈 / ( 1 · 𝑇 ) ) ) / 3 ) )
75 oveq1 ⊢ ( 𝑥 = 1 → ( 𝑥 ↑ 3 ) = ( 1 ↑ 3 ) )
76 75 eqeq1d ⊢ ( 𝑥 = 1 → ( ( 𝑥 ↑ 3 ) = 1 ↔ ( 1 ↑ 3 ) = 1 ) )
77 oveq1 ⊢ ( 𝑥 = 1 → ( 𝑥 · 𝑇 ) = ( 1 · 𝑇 ) )
78 77 oveq2d ⊢ ( 𝑥 = 1 → ( ( 2 · 𝑃 ) + ( 𝑥 · 𝑇 ) ) = ( ( 2 · 𝑃 ) + ( 1 · 𝑇 ) ) )
79 77 oveq2d ⊢ ( 𝑥 = 1 → ( 𝑈 / ( 𝑥 · 𝑇 ) ) = ( 𝑈 / ( 1 · 𝑇 ) ) )
80 78 79 oveq12d ⊢ ( 𝑥 = 1 → ( ( ( 2 · 𝑃 ) + ( 𝑥 · 𝑇 ) ) + ( 𝑈 / ( 𝑥 · 𝑇 ) ) ) = ( ( ( 2 · 𝑃 ) + ( 1 · 𝑇 ) ) + ( 𝑈 / ( 1 · 𝑇 ) ) ) )
81 80 oveq1d ⊢ ( 𝑥 = 1 → ( ( ( ( 2 · 𝑃 ) + ( 𝑥 · 𝑇 ) ) + ( 𝑈 / ( 𝑥 · 𝑇 ) ) ) / 3 ) = ( ( ( ( 2 · 𝑃 ) + ( 1 · 𝑇 ) ) + ( 𝑈 / ( 1 · 𝑇 ) ) ) / 3 ) )
82 81 negeqd ⊢ ( 𝑥 = 1 → - ( ( ( ( 2 · 𝑃 ) + ( 𝑥 · 𝑇 ) ) + ( 𝑈 / ( 𝑥 · 𝑇 ) ) ) / 3 ) = - ( ( ( ( 2 · 𝑃 ) + ( 1 · 𝑇 ) ) + ( 𝑈 / ( 1 · 𝑇 ) ) ) / 3 ) )
83 82 eqeq2d ⊢ ( 𝑥 = 1 → ( 𝑀 = - ( ( ( ( 2 · 𝑃 ) + ( 𝑥 · 𝑇 ) ) + ( 𝑈 / ( 𝑥 · 𝑇 ) ) ) / 3 ) ↔ 𝑀 = - ( ( ( ( 2 · 𝑃 ) + ( 1 · 𝑇 ) ) + ( 𝑈 / ( 1 · 𝑇 ) ) ) / 3 ) ) )
84 76 83 anbi12d ⊢ ( 𝑥 = 1 → ( ( ( 𝑥 ↑ 3 ) = 1 ∧ 𝑀 = - ( ( ( ( 2 · 𝑃 ) + ( 𝑥 · 𝑇 ) ) + ( 𝑈 / ( 𝑥 · 𝑇 ) ) ) / 3 ) ) ↔ ( ( 1 ↑ 3 ) = 1 ∧ 𝑀 = - ( ( ( ( 2 · 𝑃 ) + ( 1 · 𝑇 ) ) + ( 𝑈 / ( 1 · 𝑇 ) ) ) / 3 ) ) ) )
85 84 rspcev ⊢ ( ( 1 ∈ ℂ ∧ ( ( 1 ↑ 3 ) = 1 ∧ 𝑀 = - ( ( ( ( 2 · 𝑃 ) + ( 1 · 𝑇 ) ) + ( 𝑈 / ( 1 · 𝑇 ) ) ) / 3 ) ) ) → ∃ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 3 ) = 1 ∧ 𝑀 = - ( ( ( ( 2 · 𝑃 ) + ( 𝑥 · 𝑇 ) ) + ( 𝑈 / ( 𝑥 · 𝑇 ) ) ) / 3 ) ) )
86 63 66 74 85 syl12anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 3 ) = 1 ∧ 𝑀 = - ( ( ( ( 2 · 𝑃 ) + ( 𝑥 · 𝑇 ) ) + ( 𝑈 / ( 𝑥 · 𝑇 ) ) ) / 3 ) ) )
87 2cn ⊢ 2 ∈ ℂ
88 mulcl ⊢ ( ( 2 ∈ ℂ ∧ 𝑃 ∈ ℂ ) → ( 2 · 𝑃 ) ∈ ℂ )
89 87 31 88 sylancr ⊢ ( 𝜑 → ( 2 · 𝑃 ) ∈ ℂ )
90 31 sqcld ⊢ ( 𝜑 → ( 𝑃 ↑ 2 ) ∈ ℂ )
91 mulcl ⊢ ( ( 4 ∈ ℂ ∧ 𝑅 ∈ ℂ ) → ( 4 · 𝑅 ) ∈ ℂ )
92 21 62 91 sylancr ⊢ ( 𝜑 → ( 4 · 𝑅 ) ∈ ℂ )
93 90 92 subcld ⊢ ( 𝜑 → ( ( 𝑃 ↑ 2 ) − ( 4 · 𝑅 ) ) ∈ ℂ )
94 32 sqcld ⊢ ( 𝜑 → ( 𝑄 ↑ 2 ) ∈ ℂ )
95 94 negcld ⊢ ( 𝜑 → - ( 𝑄 ↑ 2 ) ∈ ℂ )
96 15 oveq1d ⊢ ( 𝜑 → ( 𝑇 ↑ 3 ) = ( ( ( ( 𝑉 + 𝑊 ) / 2 ) ↑𝑐 ( 1 / 3 ) ) ↑ 3 ) )
97 1 2 3 4 1 6 7 8 9 10 11 12 quartlem2 ⊢ ( 𝜑 → ( 𝑈 ∈ ℂ ∧ 𝑉 ∈ ℂ ∧ 𝑊 ∈ ℂ ) )
98 97 simp2d ⊢ ( 𝜑 → 𝑉 ∈ ℂ )
99 97 simp3d ⊢ ( 𝜑 → 𝑊 ∈ ℂ )
100 98 99 addcld ⊢ ( 𝜑 → ( 𝑉 + 𝑊 ) ∈ ℂ )
101 100 halfcld ⊢ ( 𝜑 → ( ( 𝑉 + 𝑊 ) / 2 ) ∈ ℂ )
102 3nn ⊢ 3 ∈ ℕ
103 cxproot ⊢ ( ( ( ( 𝑉 + 𝑊 ) / 2 ) ∈ ℂ ∧ 3 ∈ ℕ ) → ( ( ( ( 𝑉 + 𝑊 ) / 2 ) ↑𝑐 ( 1 / 3 ) ) ↑ 3 ) = ( ( 𝑉 + 𝑊 ) / 2 ) )
104 101 102 103 sylancl ⊢ ( 𝜑 → ( ( ( ( 𝑉 + 𝑊 ) / 2 ) ↑𝑐 ( 1 / 3 ) ) ↑ 3 ) = ( ( 𝑉 + 𝑊 ) / 2 ) )
105 96 104 eqtrd ⊢ ( 𝜑 → ( 𝑇 ↑ 3 ) = ( ( 𝑉 + 𝑊 ) / 2 ) )
106 12 oveq1d ⊢ ( 𝜑 → ( 𝑊 ↑ 2 ) = ( ( √ ‘ ( ( 𝑉 ↑ 2 ) − ( 4 · ( 𝑈 ↑ 3 ) ) ) ) ↑ 2 ) )
107 98 sqcld ⊢ ( 𝜑 → ( 𝑉 ↑ 2 ) ∈ ℂ )
108 97 simp1d ⊢ ( 𝜑 → 𝑈 ∈ ℂ )
109 3nn0 ⊢ 3 ∈ ℕ0
110 expcl ⊢ ( ( 𝑈 ∈ ℂ ∧ 3 ∈ ℕ0 ) → ( 𝑈 ↑ 3 ) ∈ ℂ )
111 108 109 110 sylancl ⊢ ( 𝜑 → ( 𝑈 ↑ 3 ) ∈ ℂ )
112 mulcl ⊢ ( ( 4 ∈ ℂ ∧ ( 𝑈 ↑ 3 ) ∈ ℂ ) → ( 4 · ( 𝑈 ↑ 3 ) ) ∈ ℂ )
113 21 111 112 sylancr ⊢ ( 𝜑 → ( 4 · ( 𝑈 ↑ 3 ) ) ∈ ℂ )
114 107 113 subcld ⊢ ( 𝜑 → ( ( 𝑉 ↑ 2 ) − ( 4 · ( 𝑈 ↑ 3 ) ) ) ∈ ℂ )
115 114 sqsqrtd ⊢ ( 𝜑 → ( ( √ ‘ ( ( 𝑉 ↑ 2 ) − ( 4 · ( 𝑈 ↑ 3 ) ) ) ) ↑ 2 ) = ( ( 𝑉 ↑ 2 ) − ( 4 · ( 𝑈 ↑ 3 ) ) ) )
116 106 115 eqtrd ⊢ ( 𝜑 → ( 𝑊 ↑ 2 ) = ( ( 𝑉 ↑ 2 ) − ( 4 · ( 𝑈 ↑ 3 ) ) ) )
117 31 32 62 10 11 quartlem1 ⊢ ( 𝜑 → ( 𝑈 = ( ( ( 2 · 𝑃 ) ↑ 2 ) − ( 3 · ( ( 𝑃 ↑ 2 ) − ( 4 · 𝑅 ) ) ) ) ∧ 𝑉 = ( ( ( 2 · ( ( 2 · 𝑃 ) ↑ 3 ) ) − ( 9 · ( ( 2 · 𝑃 ) · ( ( 𝑃 ↑ 2 ) − ( 4 · 𝑅 ) ) ) ) ) + ( 2 7 · - ( 𝑄 ↑ 2 ) ) ) ) )
118 117 simpld ⊢ ( 𝜑 → 𝑈 = ( ( ( 2 · 𝑃 ) ↑ 2 ) − ( 3 · ( ( 𝑃 ↑ 2 ) − ( 4 · 𝑅 ) ) ) ) )
119 117 simprd ⊢ ( 𝜑 → 𝑉 = ( ( ( 2 · ( ( 2 · 𝑃 ) ↑ 3 ) ) − ( 9 · ( ( 2 · 𝑃 ) · ( ( 𝑃 ↑ 2 ) − ( 4 · 𝑅 ) ) ) ) ) + ( 2 7 · - ( 𝑄 ↑ 2 ) ) ) )
120 89 93 95 39 67 105 99 116 118 119 16 mcubic ⊢ ( 𝜑 → ( ( ( ( 𝑀 ↑ 3 ) + ( ( 2 · 𝑃 ) · ( 𝑀 ↑ 2 ) ) ) + ( ( ( ( 𝑃 ↑ 2 ) − ( 4 · 𝑅 ) ) · 𝑀 ) + - ( 𝑄 ↑ 2 ) ) ) = 0 ↔ ∃ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 3 ) = 1 ∧ 𝑀 = - ( ( ( ( 2 · 𝑃 ) + ( 𝑥 · 𝑇 ) ) + ( 𝑈 / ( 𝑥 · 𝑇 ) ) ) / 3 ) ) ) )
121 86 120 mpbird ⊢ ( 𝜑 → ( ( ( 𝑀 ↑ 3 ) + ( ( 2 · 𝑃 ) · ( 𝑀 ↑ 2 ) ) ) + ( ( ( ( 𝑃 ↑ 2 ) − ( 4 · 𝑅 ) ) · 𝑀 ) + - ( 𝑄 ↑ 2 ) ) ) = 0 )
122 49 simp3d ⊢ ( 𝜑 → 𝐽 ∈ ℂ )
123 19 oveq1d ⊢ ( 𝜑 → ( 𝐽 ↑ 2 ) = ( ( √ ‘ ( ( - ( 𝑆 ↑ 2 ) − ( 𝑃 / 2 ) ) − ( ( 𝑄 / 4 ) / 𝑆 ) ) ) ↑ 2 ) )
124 55 58 subcld ⊢ ( 𝜑 → ( ( - ( 𝑆 ↑ 2 ) − ( 𝑃 / 2 ) ) − ( ( 𝑄 / 4 ) / 𝑆 ) ) ∈ ℂ )
125 124 sqsqrtd ⊢ ( 𝜑 → ( ( √ ‘ ( ( - ( 𝑆 ↑ 2 ) − ( 𝑃 / 2 ) ) − ( ( 𝑄 / 4 ) / 𝑆 ) ) ) ↑ 2 ) = ( ( - ( 𝑆 ↑ 2 ) − ( 𝑃 / 2 ) ) − ( ( 𝑄 / 4 ) / 𝑆 ) ) )
126 123 125 eqtrd ⊢ ( 𝜑 → ( 𝐽 ↑ 2 ) = ( ( - ( 𝑆 ↑ 2 ) − ( 𝑃 / 2 ) ) − ( ( 𝑄 / 4 ) / 𝑆 ) ) )
127 31 32 35 37 48 17 50 61 62 121 122 126 dquart ⊢ ( 𝜑 → ( ( ( ( ( 𝑋 − 𝐸 ) ↑ 4 ) + ( 𝑃 · ( ( 𝑋 − 𝐸 ) ↑ 2 ) ) ) + ( ( 𝑄 · ( 𝑋 − 𝐸 ) ) + 𝑅 ) ) = 0 ↔ ( ( ( 𝑋 − 𝐸 ) = ( - 𝑆 + 𝐼 ) ∨ ( 𝑋 − 𝐸 ) = ( - 𝑆 − 𝐼 ) ) ∨ ( ( 𝑋 − 𝐸 ) = ( 𝑆 + 𝐽 ) ∨ ( 𝑋 − 𝐸 ) = ( 𝑆 − 𝐽 ) ) ) ) )
128 37 negcld ⊢ ( 𝜑 → - 𝑆 ∈ ℂ )
129 128 50 addcld ⊢ ( 𝜑 → ( - 𝑆 + 𝐼 ) ∈ ℂ )
130 5 34 129 subaddd ⊢ ( 𝜑 → ( ( 𝑋 − 𝐸 ) = ( - 𝑆 + 𝐼 ) ↔ ( 𝐸 + ( - 𝑆 + 𝐼 ) ) = 𝑋 ) )
131 34 37 negsubd ⊢ ( 𝜑 → ( 𝐸 + - 𝑆 ) = ( 𝐸 − 𝑆 ) )
132 131 oveq1d ⊢ ( 𝜑 → ( ( 𝐸 + - 𝑆 ) + 𝐼 ) = ( ( 𝐸 − 𝑆 ) + 𝐼 ) )
133 34 128 50 addassd ⊢ ( 𝜑 → ( ( 𝐸 + - 𝑆 ) + 𝐼 ) = ( 𝐸 + ( - 𝑆 + 𝐼 ) ) )
134 132 133 eqtr3d ⊢ ( 𝜑 → ( ( 𝐸 − 𝑆 ) + 𝐼 ) = ( 𝐸 + ( - 𝑆 + 𝐼 ) ) )
135 134 eqeq1d ⊢ ( 𝜑 → ( ( ( 𝐸 − 𝑆 ) + 𝐼 ) = 𝑋 ↔ ( 𝐸 + ( - 𝑆 + 𝐼 ) ) = 𝑋 ) )
136 130 135 bitr4d ⊢ ( 𝜑 → ( ( 𝑋 − 𝐸 ) = ( - 𝑆 + 𝐼 ) ↔ ( ( 𝐸 − 𝑆 ) + 𝐼 ) = 𝑋 ) )
137 eqcom ⊢ ( ( ( 𝐸 − 𝑆 ) + 𝐼 ) = 𝑋 ↔ 𝑋 = ( ( 𝐸 − 𝑆 ) + 𝐼 ) )
138 136 137 bitrdi ⊢ ( 𝜑 → ( ( 𝑋 − 𝐸 ) = ( - 𝑆 + 𝐼 ) ↔ 𝑋 = ( ( 𝐸 − 𝑆 ) + 𝐼 ) ) )
139 128 50 subcld ⊢ ( 𝜑 → ( - 𝑆 − 𝐼 ) ∈ ℂ )
140 5 34 139 subaddd ⊢ ( 𝜑 → ( ( 𝑋 − 𝐸 ) = ( - 𝑆 − 𝐼 ) ↔ ( 𝐸 + ( - 𝑆 − 𝐼 ) ) = 𝑋 ) )
141 131 oveq1d ⊢ ( 𝜑 → ( ( 𝐸 + - 𝑆 ) − 𝐼 ) = ( ( 𝐸 − 𝑆 ) − 𝐼 ) )
142 34 128 50 addsubassd ⊢ ( 𝜑 → ( ( 𝐸 + - 𝑆 ) − 𝐼 ) = ( 𝐸 + ( - 𝑆 − 𝐼 ) ) )
143 141 142 eqtr3d ⊢ ( 𝜑 → ( ( 𝐸 − 𝑆 ) − 𝐼 ) = ( 𝐸 + ( - 𝑆 − 𝐼 ) ) )
144 143 eqeq1d ⊢ ( 𝜑 → ( ( ( 𝐸 − 𝑆 ) − 𝐼 ) = 𝑋 ↔ ( 𝐸 + ( - 𝑆 − 𝐼 ) ) = 𝑋 ) )
145 140 144 bitr4d ⊢ ( 𝜑 → ( ( 𝑋 − 𝐸 ) = ( - 𝑆 − 𝐼 ) ↔ ( ( 𝐸 − 𝑆 ) − 𝐼 ) = 𝑋 ) )
146 eqcom ⊢ ( ( ( 𝐸 − 𝑆 ) − 𝐼 ) = 𝑋 ↔ 𝑋 = ( ( 𝐸 − 𝑆 ) − 𝐼 ) )
147 145 146 bitrdi ⊢ ( 𝜑 → ( ( 𝑋 − 𝐸 ) = ( - 𝑆 − 𝐼 ) ↔ 𝑋 = ( ( 𝐸 − 𝑆 ) − 𝐼 ) ) )
148 138 147 orbi12d ⊢ ( 𝜑 → ( ( ( 𝑋 − 𝐸 ) = ( - 𝑆 + 𝐼 ) ∨ ( 𝑋 − 𝐸 ) = ( - 𝑆 − 𝐼 ) ) ↔ ( 𝑋 = ( ( 𝐸 − 𝑆 ) + 𝐼 ) ∨ 𝑋 = ( ( 𝐸 − 𝑆 ) − 𝐼 ) ) ) )
149 37 122 addcld ⊢ ( 𝜑 → ( 𝑆 + 𝐽 ) ∈ ℂ )
150 5 34 149 subaddd ⊢ ( 𝜑 → ( ( 𝑋 − 𝐸 ) = ( 𝑆 + 𝐽 ) ↔ ( 𝐸 + ( 𝑆 + 𝐽 ) ) = 𝑋 ) )
151 34 37 122 addassd ⊢ ( 𝜑 → ( ( 𝐸 + 𝑆 ) + 𝐽 ) = ( 𝐸 + ( 𝑆 + 𝐽 ) ) )
152 151 eqeq1d ⊢ ( 𝜑 → ( ( ( 𝐸 + 𝑆 ) + 𝐽 ) = 𝑋 ↔ ( 𝐸 + ( 𝑆 + 𝐽 ) ) = 𝑋 ) )
153 150 152 bitr4d ⊢ ( 𝜑 → ( ( 𝑋 − 𝐸 ) = ( 𝑆 + 𝐽 ) ↔ ( ( 𝐸 + 𝑆 ) + 𝐽 ) = 𝑋 ) )
154 eqcom ⊢ ( ( ( 𝐸 + 𝑆 ) + 𝐽 ) = 𝑋 ↔ 𝑋 = ( ( 𝐸 + 𝑆 ) + 𝐽 ) )
155 153 154 bitrdi ⊢ ( 𝜑 → ( ( 𝑋 − 𝐸 ) = ( 𝑆 + 𝐽 ) ↔ 𝑋 = ( ( 𝐸 + 𝑆 ) + 𝐽 ) ) )
156 37 122 subcld ⊢ ( 𝜑 → ( 𝑆 − 𝐽 ) ∈ ℂ )
157 5 34 156 subaddd ⊢ ( 𝜑 → ( ( 𝑋 − 𝐸 ) = ( 𝑆 − 𝐽 ) ↔ ( 𝐸 + ( 𝑆 − 𝐽 ) ) = 𝑋 ) )
158 34 37 122 addsubassd ⊢ ( 𝜑 → ( ( 𝐸 + 𝑆 ) − 𝐽 ) = ( 𝐸 + ( 𝑆 − 𝐽 ) ) )
159 158 eqeq1d ⊢ ( 𝜑 → ( ( ( 𝐸 + 𝑆 ) − 𝐽 ) = 𝑋 ↔ ( 𝐸 + ( 𝑆 − 𝐽 ) ) = 𝑋 ) )
160 157 159 bitr4d ⊢ ( 𝜑 → ( ( 𝑋 − 𝐸 ) = ( 𝑆 − 𝐽 ) ↔ ( ( 𝐸 + 𝑆 ) − 𝐽 ) = 𝑋 ) )
161 eqcom ⊢ ( ( ( 𝐸 + 𝑆 ) − 𝐽 ) = 𝑋 ↔ 𝑋 = ( ( 𝐸 + 𝑆 ) − 𝐽 ) )
162 160 161 bitrdi ⊢ ( 𝜑 → ( ( 𝑋 − 𝐸 ) = ( 𝑆 − 𝐽 ) ↔ 𝑋 = ( ( 𝐸 + 𝑆 ) − 𝐽 ) ) )
163 155 162 orbi12d ⊢ ( 𝜑 → ( ( ( 𝑋 − 𝐸 ) = ( 𝑆 + 𝐽 ) ∨ ( 𝑋 − 𝐸 ) = ( 𝑆 − 𝐽 ) ) ↔ ( 𝑋 = ( ( 𝐸 + 𝑆 ) + 𝐽 ) ∨ 𝑋 = ( ( 𝐸 + 𝑆 ) − 𝐽 ) ) ) )
164 148 163 orbi12d ⊢ ( 𝜑 → ( ( ( ( 𝑋 − 𝐸 ) = ( - 𝑆 + 𝐼 ) ∨ ( 𝑋 − 𝐸 ) = ( - 𝑆 − 𝐼 ) ) ∨ ( ( 𝑋 − 𝐸 ) = ( 𝑆 + 𝐽 ) ∨ ( 𝑋 − 𝐸 ) = ( 𝑆 − 𝐽 ) ) ) ↔ ( ( 𝑋 = ( ( 𝐸 − 𝑆 ) + 𝐼 ) ∨ 𝑋 = ( ( 𝐸 − 𝑆 ) − 𝐼 ) ) ∨ ( 𝑋 = ( ( 𝐸 + 𝑆 ) + 𝐽 ) ∨ 𝑋 = ( ( 𝐸 + 𝑆 ) − 𝐽 ) ) ) ) )
165 29 127 164 3bitrd ⊢ ( 𝜑 → ( ( ( ( 𝑋 ↑ 4 ) + ( 𝐴 · ( 𝑋 ↑ 3 ) ) ) + ( ( 𝐵 · ( 𝑋 ↑ 2 ) ) + ( ( 𝐶 · 𝑋 ) + 𝐷 ) ) ) = 0 ↔ ( ( 𝑋 = ( ( 𝐸 − 𝑆 ) + 𝐼 ) ∨ 𝑋 = ( ( 𝐸 − 𝑆 ) − 𝐼 ) ) ∨ ( 𝑋 = ( ( 𝐸 + 𝑆 ) + 𝐽 ) ∨ 𝑋 = ( ( 𝐸 + 𝑆 ) − 𝐽 ) ) ) ) )