MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  quart Structured version   Visualization version   GIF version

Theorem quart 25441
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 32414) if all the substitutions are performed. This is Metamath 100 proof #46. (Contributed by Mario Carneiro, 6-May-2015.)
Hypotheses
Ref Expression
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) · 𝐵) / 16) − ((3 / 256) · (𝐴↑4)))))
quart.u (𝜑𝑈 = ((𝑃↑2) + (12 · 𝑅)))
quart.v (𝜑𝑉 = ((-(2 · (𝑃↑3)) − (27 · (𝑄↑2))) + (72 · (𝑃 · 𝑅))))
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
Ref Expression
quart (𝜑 → ((((𝑋↑4) + (𝐴 · (𝑋↑3))) + ((𝐵 · (𝑋↑2)) + ((𝐶 · 𝑋) + 𝐷))) = 0 ↔ ((𝑋 = ((𝐸𝑆) + 𝐼) ∨ 𝑋 = ((𝐸𝑆) − 𝐼)) ∨ (𝑋 = ((𝐸 + 𝑆) + 𝐽) ∨ 𝑋 = ((𝐸 + 𝑆) − 𝐽)))))

Proof of Theorem quart
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 quart.a . . . 4 (𝜑𝐴 ∈ ℂ)
2 quart.b . . . 4 (𝜑𝐵 ∈ ℂ)
3 quart.c . . . 4 (𝜑𝐶 ∈ ℂ)
4 quart.d . . . 4 (𝜑𝐷 ∈ ℂ)
5 quart.p . . . 4 (𝜑𝑃 = (𝐵 − ((3 / 8) · (𝐴↑2))))
6 quart.q . . . 4 (𝜑𝑄 = ((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8)))
7 quart.r . . . 4 (𝜑𝑅 = ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / 16) − ((3 / 256) · (𝐴↑4)))))
8 quart.x . . . 4 (𝜑𝑋 ∈ ℂ)
9 quart.e . . . . . 6 (𝜑𝐸 = -(𝐴 / 4))
109oveq2d 7174 . . . . 5 (𝜑 → (𝑋𝐸) = (𝑋 − -(𝐴 / 4)))
11 4cn 11725 . . . . . . . 8 4 ∈ ℂ
1211a1i 11 . . . . . . 7 (𝜑 → 4 ∈ ℂ)
13 4ne0 11748 . . . . . . . 8 4 ≠ 0
1413a1i 11 . . . . . . 7 (𝜑 → 4 ≠ 0)
151, 12, 14divcld 11418 . . . . . 6 (𝜑 → (𝐴 / 4) ∈ ℂ)
168, 15subnegd 11006 . . . . 5 (𝜑 → (𝑋 − -(𝐴 / 4)) = (𝑋 + (𝐴 / 4)))
1710, 16eqtrd 2858 . . . 4 (𝜑 → (𝑋𝐸) = (𝑋 + (𝐴 / 4)))
181, 2, 3, 4, 5, 6, 7, 8, 17quart1 25436 . . 3 (𝜑 → (((𝑋↑4) + (𝐴 · (𝑋↑3))) + ((𝐵 · (𝑋↑2)) + ((𝐶 · 𝑋) + 𝐷))) = ((((𝑋𝐸)↑4) + (𝑃 · ((𝑋𝐸)↑2))) + ((𝑄 · (𝑋𝐸)) + 𝑅)))
1918eqeq1d 2825 . 2 (𝜑 → ((((𝑋↑4) + (𝐴 · (𝑋↑3))) + ((𝐵 · (𝑋↑2)) + ((𝐶 · 𝑋) + 𝐷))) = 0 ↔ ((((𝑋𝐸)↑4) + (𝑃 · ((𝑋𝐸)↑2))) + ((𝑄 · (𝑋𝐸)) + 𝑅)) = 0))
201, 2, 3, 4, 5, 6, 7quart1cl 25434 . . . 4 (𝜑 → (𝑃 ∈ ℂ ∧ 𝑄 ∈ ℂ ∧ 𝑅 ∈ ℂ))
2120simp1d 1138 . . 3 (𝜑𝑃 ∈ ℂ)
2220simp2d 1139 . . 3 (𝜑𝑄 ∈ ℂ)
2315negcld 10986 . . . . 5 (𝜑 → -(𝐴 / 4) ∈ ℂ)
249, 23eqeltrd 2915 . . . 4 (𝜑𝐸 ∈ ℂ)
258, 24subcld 10999 . . 3 (𝜑 → (𝑋𝐸) ∈ ℂ)
26 quart.u . . . . 5 (𝜑𝑈 = ((𝑃↑2) + (12 · 𝑅)))
27 quart.v . . . . 5 (𝜑𝑉 = ((-(2 · (𝑃↑3)) − (27 · (𝑄↑2))) + (72 · (𝑃 · 𝑅))))
28 quart.w . . . . 5 (𝜑𝑊 = (√‘((𝑉↑2) − (4 · (𝑈↑3)))))
29 quart.s . . . . 5 (𝜑𝑆 = ((√‘𝑀) / 2))
30 quart.m . . . . 5 (𝜑𝑀 = -((((2 · 𝑃) + 𝑇) + (𝑈 / 𝑇)) / 3))
31 quart.t . . . . 5 (𝜑𝑇 = (((𝑉 + 𝑊) / 2)↑𝑐(1 / 3)))
32 quart.t0 . . . . 5 (𝜑𝑇 ≠ 0)
331, 2, 3, 4, 1, 9, 5, 6, 7, 26, 27, 28, 29, 30, 31, 32quartlem3 25439 . . . 4 (𝜑 → (𝑆 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑇 ∈ ℂ))
3433simp1d 1138 . . 3 (𝜑𝑆 ∈ ℂ)
3529oveq2d 7174 . . . . . 6 (𝜑 → (2 · 𝑆) = (2 · ((√‘𝑀) / 2)))
3633simp2d 1139 . . . . . . . 8 (𝜑𝑀 ∈ ℂ)
3736sqrtcld 14799 . . . . . . 7 (𝜑 → (√‘𝑀) ∈ ℂ)
38 2cnd 11718 . . . . . . 7 (𝜑 → 2 ∈ ℂ)
39 2ne0 11744 . . . . . . . 8 2 ≠ 0
4039a1i 11 . . . . . . 7 (𝜑 → 2 ≠ 0)
4137, 38, 40divcan2d 11420 . . . . . 6 (𝜑 → (2 · ((√‘𝑀) / 2)) = (√‘𝑀))
4235, 41eqtrd 2858 . . . . 5 (𝜑 → (2 · 𝑆) = (√‘𝑀))
4342oveq1d 7173 . . . 4 (𝜑 → ((2 · 𝑆)↑2) = ((√‘𝑀)↑2))
4436sqsqrtd 14801 . . . 4 (𝜑 → ((√‘𝑀)↑2) = 𝑀)
4543, 44eqtr2d 2859 . . 3 (𝜑𝑀 = ((2 · 𝑆)↑2))
46 quart.m0 . . 3 (𝜑𝑀 ≠ 0)
47 quart.i . . . . 5 (𝜑𝐼 = (√‘((-(𝑆↑2) − (𝑃 / 2)) + ((𝑄 / 4) / 𝑆))))
48 quart.j . . . . 5 (𝜑𝐽 = (√‘((-(𝑆↑2) − (𝑃 / 2)) − ((𝑄 / 4) / 𝑆))))
491, 2, 3, 4, 1, 9, 5, 6, 7, 26, 27, 28, 29, 30, 31, 32, 46, 47, 48quartlem4 25440 . . . 4 (𝜑 → (𝑆 ≠ 0 ∧ 𝐼 ∈ ℂ ∧ 𝐽 ∈ ℂ))
5049simp2d 1139 . . 3 (𝜑𝐼 ∈ ℂ)
5147oveq1d 7173 . . . 4 (𝜑 → (𝐼↑2) = ((√‘((-(𝑆↑2) − (𝑃 / 2)) + ((𝑄 / 4) / 𝑆)))↑2))
5234sqcld 13511 . . . . . . . 8 (𝜑 → (𝑆↑2) ∈ ℂ)
5352negcld 10986 . . . . . . 7 (𝜑 → -(𝑆↑2) ∈ ℂ)
5421halfcld 11885 . . . . . . 7 (𝜑 → (𝑃 / 2) ∈ ℂ)
5553, 54subcld 10999 . . . . . 6 (𝜑 → (-(𝑆↑2) − (𝑃 / 2)) ∈ ℂ)
5622, 12, 14divcld 11418 . . . . . . 7 (𝜑 → (𝑄 / 4) ∈ ℂ)
5749simp1d 1138 . . . . . . 7 (𝜑𝑆 ≠ 0)
5856, 34, 57divcld 11418 . . . . . 6 (𝜑 → ((𝑄 / 4) / 𝑆) ∈ ℂ)
5955, 58addcld 10662 . . . . 5 (𝜑 → ((-(𝑆↑2) − (𝑃 / 2)) + ((𝑄 / 4) / 𝑆)) ∈ ℂ)
6059sqsqrtd 14801 . . . 4 (𝜑 → ((√‘((-(𝑆↑2) − (𝑃 / 2)) + ((𝑄 / 4) / 𝑆)))↑2) = ((-(𝑆↑2) − (𝑃 / 2)) + ((𝑄 / 4) / 𝑆)))
6151, 60eqtrd 2858 . . 3 (𝜑 → (𝐼↑2) = ((-(𝑆↑2) − (𝑃 / 2)) + ((𝑄 / 4) / 𝑆)))
6220simp3d 1140 . . 3 (𝜑𝑅 ∈ ℂ)
63 1cnd 10638 . . . . 5 (𝜑 → 1 ∈ ℂ)
64 3z 12018 . . . . . 6 3 ∈ ℤ
65 1exp 13461 . . . . . 6 (3 ∈ ℤ → (1↑3) = 1)
6664, 65mp1i 13 . . . . 5 (𝜑 → (1↑3) = 1)
6733simp3d 1140 . . . . . . . . . . 11 (𝜑𝑇 ∈ ℂ)
6867mulid2d 10661 . . . . . . . . . 10 (𝜑 → (1 · 𝑇) = 𝑇)
6968oveq2d 7174 . . . . . . . . 9 (𝜑 → ((2 · 𝑃) + (1 · 𝑇)) = ((2 · 𝑃) + 𝑇))
7068oveq2d 7174 . . . . . . . . 9 (𝜑 → (𝑈 / (1 · 𝑇)) = (𝑈 / 𝑇))
7169, 70oveq12d 7176 . . . . . . . 8 (𝜑 → (((2 · 𝑃) + (1 · 𝑇)) + (𝑈 / (1 · 𝑇))) = (((2 · 𝑃) + 𝑇) + (𝑈 / 𝑇)))
7271oveq1d 7173 . . . . . . 7 (𝜑 → ((((2 · 𝑃) + (1 · 𝑇)) + (𝑈 / (1 · 𝑇))) / 3) = ((((2 · 𝑃) + 𝑇) + (𝑈 / 𝑇)) / 3))
7372negeqd 10882 . . . . . 6 (𝜑 → -((((2 · 𝑃) + (1 · 𝑇)) + (𝑈 / (1 · 𝑇))) / 3) = -((((2 · 𝑃) + 𝑇) + (𝑈 / 𝑇)) / 3))
7430, 73eqtr4d 2861 . . . . 5 (𝜑𝑀 = -((((2 · 𝑃) + (1 · 𝑇)) + (𝑈 / (1 · 𝑇))) / 3))
75 oveq1 7165 . . . . . . . 8 (𝑥 = 1 → (𝑥↑3) = (1↑3))
7675eqeq1d 2825 . . . . . . 7 (𝑥 = 1 → ((𝑥↑3) = 1 ↔ (1↑3) = 1))
77 oveq1 7165 . . . . . . . . . . . 12 (𝑥 = 1 → (𝑥 · 𝑇) = (1 · 𝑇))
7877oveq2d 7174 . . . . . . . . . . 11 (𝑥 = 1 → ((2 · 𝑃) + (𝑥 · 𝑇)) = ((2 · 𝑃) + (1 · 𝑇)))
7977oveq2d 7174 . . . . . . . . . . 11 (𝑥 = 1 → (𝑈 / (𝑥 · 𝑇)) = (𝑈 / (1 · 𝑇)))
8078, 79oveq12d 7176 . . . . . . . . . 10 (𝑥 = 1 → (((2 · 𝑃) + (𝑥 · 𝑇)) + (𝑈 / (𝑥 · 𝑇))) = (((2 · 𝑃) + (1 · 𝑇)) + (𝑈 / (1 · 𝑇))))
8180oveq1d 7173 . . . . . . . . 9 (𝑥 = 1 → ((((2 · 𝑃) + (𝑥 · 𝑇)) + (𝑈 / (𝑥 · 𝑇))) / 3) = ((((2 · 𝑃) + (1 · 𝑇)) + (𝑈 / (1 · 𝑇))) / 3))
8281negeqd 10882 . . . . . . . 8 (𝑥 = 1 → -((((2 · 𝑃) + (𝑥 · 𝑇)) + (𝑈 / (𝑥 · 𝑇))) / 3) = -((((2 · 𝑃) + (1 · 𝑇)) + (𝑈 / (1 · 𝑇))) / 3))
8382eqeq2d 2834 . . . . . . 7 (𝑥 = 1 → (𝑀 = -((((2 · 𝑃) + (𝑥 · 𝑇)) + (𝑈 / (𝑥 · 𝑇))) / 3) ↔ 𝑀 = -((((2 · 𝑃) + (1 · 𝑇)) + (𝑈 / (1 · 𝑇))) / 3)))
8476, 83anbi12d 632 . . . . . 6 (𝑥 = 1 → (((𝑥↑3) = 1 ∧ 𝑀 = -((((2 · 𝑃) + (𝑥 · 𝑇)) + (𝑈 / (𝑥 · 𝑇))) / 3)) ↔ ((1↑3) = 1 ∧ 𝑀 = -((((2 · 𝑃) + (1 · 𝑇)) + (𝑈 / (1 · 𝑇))) / 3))))
8584rspcev 3625 . . . . 5 ((1 ∈ ℂ ∧ ((1↑3) = 1 ∧ 𝑀 = -((((2 · 𝑃) + (1 · 𝑇)) + (𝑈 / (1 · 𝑇))) / 3))) → ∃𝑥 ∈ ℂ ((𝑥↑3) = 1 ∧ 𝑀 = -((((2 · 𝑃) + (𝑥 · 𝑇)) + (𝑈 / (𝑥 · 𝑇))) / 3)))
8663, 66, 74, 85syl12anc 834 . . . 4 (𝜑 → ∃𝑥 ∈ ℂ ((𝑥↑3) = 1 ∧ 𝑀 = -((((2 · 𝑃) + (𝑥 · 𝑇)) + (𝑈 / (𝑥 · 𝑇))) / 3)))
87 2cn 11715 . . . . . 6 2 ∈ ℂ
88 mulcl 10623 . . . . . 6 ((2 ∈ ℂ ∧ 𝑃 ∈ ℂ) → (2 · 𝑃) ∈ ℂ)
8987, 21, 88sylancr 589 . . . . 5 (𝜑 → (2 · 𝑃) ∈ ℂ)
9021sqcld 13511 . . . . . 6 (𝜑 → (𝑃↑2) ∈ ℂ)
91 mulcl 10623 . . . . . . 7 ((4 ∈ ℂ ∧ 𝑅 ∈ ℂ) → (4 · 𝑅) ∈ ℂ)
9211, 62, 91sylancr 589 . . . . . 6 (𝜑 → (4 · 𝑅) ∈ ℂ)
9390, 92subcld 10999 . . . . 5 (𝜑 → ((𝑃↑2) − (4 · 𝑅)) ∈ ℂ)
9422sqcld 13511 . . . . . 6 (𝜑 → (𝑄↑2) ∈ ℂ)
9594negcld 10986 . . . . 5 (𝜑 → -(𝑄↑2) ∈ ℂ)
9631oveq1d 7173 . . . . . 6 (𝜑 → (𝑇↑3) = ((((𝑉 + 𝑊) / 2)↑𝑐(1 / 3))↑3))
971, 2, 3, 4, 1, 9, 5, 6, 7, 26, 27, 28quartlem2 25438 . . . . . . . . . 10 (𝜑 → (𝑈 ∈ ℂ ∧ 𝑉 ∈ ℂ ∧ 𝑊 ∈ ℂ))
9897simp2d 1139 . . . . . . . . 9 (𝜑𝑉 ∈ ℂ)
9997simp3d 1140 . . . . . . . . 9 (𝜑𝑊 ∈ ℂ)
10098, 99addcld 10662 . . . . . . . 8 (𝜑 → (𝑉 + 𝑊) ∈ ℂ)
101100halfcld 11885 . . . . . . 7 (𝜑 → ((𝑉 + 𝑊) / 2) ∈ ℂ)
102 3nn 11719 . . . . . . 7 3 ∈ ℕ
103 cxproot 25275 . . . . . . 7 ((((𝑉 + 𝑊) / 2) ∈ ℂ ∧ 3 ∈ ℕ) → ((((𝑉 + 𝑊) / 2)↑𝑐(1 / 3))↑3) = ((𝑉 + 𝑊) / 2))
104101, 102, 103sylancl 588 . . . . . 6 (𝜑 → ((((𝑉 + 𝑊) / 2)↑𝑐(1 / 3))↑3) = ((𝑉 + 𝑊) / 2))
10596, 104eqtrd 2858 . . . . 5 (𝜑 → (𝑇↑3) = ((𝑉 + 𝑊) / 2))
10628oveq1d 7173 . . . . . 6 (𝜑 → (𝑊↑2) = ((√‘((𝑉↑2) − (4 · (𝑈↑3))))↑2))
10798sqcld 13511 . . . . . . . 8 (𝜑 → (𝑉↑2) ∈ ℂ)
10897simp1d 1138 . . . . . . . . . 10 (𝜑𝑈 ∈ ℂ)
109 3nn0 11918 . . . . . . . . . 10 3 ∈ ℕ0
110 expcl 13450 . . . . . . . . . 10 ((𝑈 ∈ ℂ ∧ 3 ∈ ℕ0) → (𝑈↑3) ∈ ℂ)
111108, 109, 110sylancl 588 . . . . . . . . 9 (𝜑 → (𝑈↑3) ∈ ℂ)
112 mulcl 10623 . . . . . . . . 9 ((4 ∈ ℂ ∧ (𝑈↑3) ∈ ℂ) → (4 · (𝑈↑3)) ∈ ℂ)
11311, 111, 112sylancr 589 . . . . . . . 8 (𝜑 → (4 · (𝑈↑3)) ∈ ℂ)
114107, 113subcld 10999 . . . . . . 7 (𝜑 → ((𝑉↑2) − (4 · (𝑈↑3))) ∈ ℂ)
115114sqsqrtd 14801 . . . . . 6 (𝜑 → ((√‘((𝑉↑2) − (4 · (𝑈↑3))))↑2) = ((𝑉↑2) − (4 · (𝑈↑3))))
116106, 115eqtrd 2858 . . . . 5 (𝜑 → (𝑊↑2) = ((𝑉↑2) − (4 · (𝑈↑3))))
11721, 22, 62, 26, 27quartlem1 25437 . . . . . 6 (𝜑 → (𝑈 = (((2 · 𝑃)↑2) − (3 · ((𝑃↑2) − (4 · 𝑅)))) ∧ 𝑉 = (((2 · ((2 · 𝑃)↑3)) − (9 · ((2 · 𝑃) · ((𝑃↑2) − (4 · 𝑅))))) + (27 · -(𝑄↑2)))))
118117simpld 497 . . . . 5 (𝜑𝑈 = (((2 · 𝑃)↑2) − (3 · ((𝑃↑2) − (4 · 𝑅)))))
119117simprd 498 . . . . 5 (𝜑𝑉 = (((2 · ((2 · 𝑃)↑3)) − (9 · ((2 · 𝑃) · ((𝑃↑2) − (4 · 𝑅))))) + (27 · -(𝑄↑2))))
12089, 93, 95, 36, 67, 105, 99, 116, 118, 119, 32mcubic 25427 . . . 4 (𝜑 → ((((𝑀↑3) + ((2 · 𝑃) · (𝑀↑2))) + ((((𝑃↑2) − (4 · 𝑅)) · 𝑀) + -(𝑄↑2))) = 0 ↔ ∃𝑥 ∈ ℂ ((𝑥↑3) = 1 ∧ 𝑀 = -((((2 · 𝑃) + (𝑥 · 𝑇)) + (𝑈 / (𝑥 · 𝑇))) / 3))))
12186, 120mpbird 259 . . 3 (𝜑 → (((𝑀↑3) + ((2 · 𝑃) · (𝑀↑2))) + ((((𝑃↑2) − (4 · 𝑅)) · 𝑀) + -(𝑄↑2))) = 0)
12249simp3d 1140 . . 3 (𝜑𝐽 ∈ ℂ)
12348oveq1d 7173 . . . 4 (𝜑 → (𝐽↑2) = ((√‘((-(𝑆↑2) − (𝑃 / 2)) − ((𝑄 / 4) / 𝑆)))↑2))
12455, 58subcld 10999 . . . . 5 (𝜑 → ((-(𝑆↑2) − (𝑃 / 2)) − ((𝑄 / 4) / 𝑆)) ∈ ℂ)
125124sqsqrtd 14801 . . . 4 (𝜑 → ((√‘((-(𝑆↑2) − (𝑃 / 2)) − ((𝑄 / 4) / 𝑆)))↑2) = ((-(𝑆↑2) − (𝑃 / 2)) − ((𝑄 / 4) / 𝑆)))
126123, 125eqtrd 2858 . . 3 (𝜑 → (𝐽↑2) = ((-(𝑆↑2) − (𝑃 / 2)) − ((𝑄 / 4) / 𝑆)))
12721, 22, 25, 34, 45, 46, 50, 61, 62, 121, 122, 126dquart 25433 . 2 (𝜑 → (((((𝑋𝐸)↑4) + (𝑃 · ((𝑋𝐸)↑2))) + ((𝑄 · (𝑋𝐸)) + 𝑅)) = 0 ↔ (((𝑋𝐸) = (-𝑆 + 𝐼) ∨ (𝑋𝐸) = (-𝑆𝐼)) ∨ ((𝑋𝐸) = (𝑆 + 𝐽) ∨ (𝑋𝐸) = (𝑆𝐽)))))
12834negcld 10986 . . . . . . . 8 (𝜑 → -𝑆 ∈ ℂ)
129128, 50addcld 10662 . . . . . . 7 (𝜑 → (-𝑆 + 𝐼) ∈ ℂ)
1308, 24, 129subaddd 11017 . . . . . 6 (𝜑 → ((𝑋𝐸) = (-𝑆 + 𝐼) ↔ (𝐸 + (-𝑆 + 𝐼)) = 𝑋))
13124, 34negsubd 11005 . . . . . . . . 9 (𝜑 → (𝐸 + -𝑆) = (𝐸𝑆))
132131oveq1d 7173 . . . . . . . 8 (𝜑 → ((𝐸 + -𝑆) + 𝐼) = ((𝐸𝑆) + 𝐼))
13324, 128, 50addassd 10665 . . . . . . . 8 (𝜑 → ((𝐸 + -𝑆) + 𝐼) = (𝐸 + (-𝑆 + 𝐼)))
134132, 133eqtr3d 2860 . . . . . . 7 (𝜑 → ((𝐸𝑆) + 𝐼) = (𝐸 + (-𝑆 + 𝐼)))
135134eqeq1d 2825 . . . . . 6 (𝜑 → (((𝐸𝑆) + 𝐼) = 𝑋 ↔ (𝐸 + (-𝑆 + 𝐼)) = 𝑋))
136130, 135bitr4d 284 . . . . 5 (𝜑 → ((𝑋𝐸) = (-𝑆 + 𝐼) ↔ ((𝐸𝑆) + 𝐼) = 𝑋))
137 eqcom 2830 . . . . 5 (((𝐸𝑆) + 𝐼) = 𝑋𝑋 = ((𝐸𝑆) + 𝐼))
138136, 137syl6bb 289 . . . 4 (𝜑 → ((𝑋𝐸) = (-𝑆 + 𝐼) ↔ 𝑋 = ((𝐸𝑆) + 𝐼)))
139128, 50subcld 10999 . . . . . . 7 (𝜑 → (-𝑆𝐼) ∈ ℂ)
1408, 24, 139subaddd 11017 . . . . . 6 (𝜑 → ((𝑋𝐸) = (-𝑆𝐼) ↔ (𝐸 + (-𝑆𝐼)) = 𝑋))
141131oveq1d 7173 . . . . . . . 8 (𝜑 → ((𝐸 + -𝑆) − 𝐼) = ((𝐸𝑆) − 𝐼))
14224, 128, 50addsubassd 11019 . . . . . . . 8 (𝜑 → ((𝐸 + -𝑆) − 𝐼) = (𝐸 + (-𝑆𝐼)))
143141, 142eqtr3d 2860 . . . . . . 7 (𝜑 → ((𝐸𝑆) − 𝐼) = (𝐸 + (-𝑆𝐼)))
144143eqeq1d 2825 . . . . . 6 (𝜑 → (((𝐸𝑆) − 𝐼) = 𝑋 ↔ (𝐸 + (-𝑆𝐼)) = 𝑋))
145140, 144bitr4d 284 . . . . 5 (𝜑 → ((𝑋𝐸) = (-𝑆𝐼) ↔ ((𝐸𝑆) − 𝐼) = 𝑋))
146 eqcom 2830 . . . . 5 (((𝐸𝑆) − 𝐼) = 𝑋𝑋 = ((𝐸𝑆) − 𝐼))
147145, 146syl6bb 289 . . . 4 (𝜑 → ((𝑋𝐸) = (-𝑆𝐼) ↔ 𝑋 = ((𝐸𝑆) − 𝐼)))
148138, 147orbi12d 915 . . 3 (𝜑 → (((𝑋𝐸) = (-𝑆 + 𝐼) ∨ (𝑋𝐸) = (-𝑆𝐼)) ↔ (𝑋 = ((𝐸𝑆) + 𝐼) ∨ 𝑋 = ((𝐸𝑆) − 𝐼))))
14934, 122addcld 10662 . . . . . . 7 (𝜑 → (𝑆 + 𝐽) ∈ ℂ)
1508, 24, 149subaddd 11017 . . . . . 6 (𝜑 → ((𝑋𝐸) = (𝑆 + 𝐽) ↔ (𝐸 + (𝑆 + 𝐽)) = 𝑋))
15124, 34, 122addassd 10665 . . . . . . 7 (𝜑 → ((𝐸 + 𝑆) + 𝐽) = (𝐸 + (𝑆 + 𝐽)))
152151eqeq1d 2825 . . . . . 6 (𝜑 → (((𝐸 + 𝑆) + 𝐽) = 𝑋 ↔ (𝐸 + (𝑆 + 𝐽)) = 𝑋))
153150, 152bitr4d 284 . . . . 5 (𝜑 → ((𝑋𝐸) = (𝑆 + 𝐽) ↔ ((𝐸 + 𝑆) + 𝐽) = 𝑋))
154 eqcom 2830 . . . . 5 (((𝐸 + 𝑆) + 𝐽) = 𝑋𝑋 = ((𝐸 + 𝑆) + 𝐽))
155153, 154syl6bb 289 . . . 4 (𝜑 → ((𝑋𝐸) = (𝑆 + 𝐽) ↔ 𝑋 = ((𝐸 + 𝑆) + 𝐽)))
15634, 122subcld 10999 . . . . . . 7 (𝜑 → (𝑆𝐽) ∈ ℂ)
1578, 24, 156subaddd 11017 . . . . . 6 (𝜑 → ((𝑋𝐸) = (𝑆𝐽) ↔ (𝐸 + (𝑆𝐽)) = 𝑋))
15824, 34, 122addsubassd 11019 . . . . . . 7 (𝜑 → ((𝐸 + 𝑆) − 𝐽) = (𝐸 + (𝑆𝐽)))
159158eqeq1d 2825 . . . . . 6 (𝜑 → (((𝐸 + 𝑆) − 𝐽) = 𝑋 ↔ (𝐸 + (𝑆𝐽)) = 𝑋))
160157, 159bitr4d 284 . . . . 5 (𝜑 → ((𝑋𝐸) = (𝑆𝐽) ↔ ((𝐸 + 𝑆) − 𝐽) = 𝑋))
161 eqcom 2830 . . . . 5 (((𝐸 + 𝑆) − 𝐽) = 𝑋𝑋 = ((𝐸 + 𝑆) − 𝐽))
162160, 161syl6bb 289 . . . 4 (𝜑 → ((𝑋𝐸) = (𝑆𝐽) ↔ 𝑋 = ((𝐸 + 𝑆) − 𝐽)))
163155, 162orbi12d 915 . . 3 (𝜑 → (((𝑋𝐸) = (𝑆 + 𝐽) ∨ (𝑋𝐸) = (𝑆𝐽)) ↔ (𝑋 = ((𝐸 + 𝑆) + 𝐽) ∨ 𝑋 = ((𝐸 + 𝑆) − 𝐽))))
164148, 163orbi12d 915 . 2 (𝜑 → ((((𝑋𝐸) = (-𝑆 + 𝐼) ∨ (𝑋𝐸) = (-𝑆𝐼)) ∨ ((𝑋𝐸) = (𝑆 + 𝐽) ∨ (𝑋𝐸) = (𝑆𝐽))) ↔ ((𝑋 = ((𝐸𝑆) + 𝐼) ∨ 𝑋 = ((𝐸𝑆) − 𝐼)) ∨ (𝑋 = ((𝐸 + 𝑆) + 𝐽) ∨ 𝑋 = ((𝐸 + 𝑆) − 𝐽)))))
16519, 127, 1643bitrd 307 1 (𝜑 → ((((𝑋↑4) + (𝐴 · (𝑋↑3))) + ((𝐵 · (𝑋↑2)) + ((𝐶 · 𝑋) + 𝐷))) = 0 ↔ ((𝑋 = ((𝐸𝑆) + 𝐼) ∨ 𝑋 = ((𝐸𝑆) − 𝐼)) ∨ (𝑋 = ((𝐸 + 𝑆) + 𝐽) ∨ 𝑋 = ((𝐸 + 𝑆) − 𝐽)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wa 398  wo 843   = wceq 1537  wcel 2114  wne 3018  wrex 3141  cfv 6357  (class class class)co 7158  cc 10537  0cc0 10539  1c1 10540   + caddc 10542   · cmul 10544  cmin 10872  -cneg 10873   / cdiv 11299  cn 11640  2c2 11695  3c3 11696  4c4 11697  5c5 11698  6c6 11699  7c7 11700  8c8 11701  9c9 11702  0cn0 11900  cz 11984  cdc 12101  cexp 13432  csqrt 14594  𝑐ccxp 25141
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-rep 5192  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463  ax-inf2 9106  ax-cnex 10595  ax-resscn 10596  ax-1cn 10597  ax-icn 10598  ax-addcl 10599  ax-addrcl 10600  ax-mulcl 10601  ax-mulrcl 10602  ax-mulcom 10603  ax-addass 10604  ax-mulass 10605  ax-distr 10606  ax-i2m1 10607  ax-1ne0 10608  ax-1rid 10609  ax-rnegex 10610  ax-rrecex 10611  ax-cnre 10612  ax-pre-lttri 10613  ax-pre-lttrn 10614  ax-pre-ltadd 10615  ax-pre-mulgt0 10616  ax-pre-sup 10617  ax-addf 10618  ax-mulf 10619
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-fal 1550  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-nel 3126  df-ral 3145  df-rex 3146  df-reu 3147  df-rmo 3148  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-pss 3956  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-tp 4574  df-op 4576  df-uni 4841  df-int 4879  df-iun 4923  df-iin 4924  df-br 5069  df-opab 5131  df-mpt 5149  df-tr 5175  df-id 5462  df-eprel 5467  df-po 5476  df-so 5477  df-fr 5516  df-se 5517  df-we 5518  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-pred 6150  df-ord 6196  df-on 6197  df-lim 6198  df-suc 6199  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364  df-fv 6365  df-isom 6366  df-riota 7116  df-ov 7161  df-oprab 7162  df-mpo 7163  df-of 7411  df-om 7583  df-1st 7691  df-2nd 7692  df-supp 7833  df-wrecs 7949  df-recs 8010  df-rdg 8048  df-1o 8104  df-2o 8105  df-oadd 8108  df-er 8291  df-map 8410  df-pm 8411  df-ixp 8464  df-en 8512  df-dom 8513  df-sdom 8514  df-fin 8515  df-fsupp 8836  df-fi 8877  df-sup 8908  df-inf 8909  df-oi 8976  df-card 9370  df-pnf 10679  df-mnf 10680  df-xr 10681  df-ltxr 10682  df-le 10683  df-sub 10874  df-neg 10875  df-div 11300  df-nn 11641  df-2 11703  df-3 11704  df-4 11705  df-5 11706  df-6 11707  df-7 11708  df-8 11709  df-9 11710  df-n0 11901  df-z 11985  df-dec 12102  df-uz 12247  df-q 12352  df-rp 12393  df-xneg 12510  df-xadd 12511  df-xmul 12512  df-ioo 12745  df-ioc 12746  df-ico 12747  df-icc 12748  df-fz 12896  df-fzo 13037  df-fl 13165  df-mod 13241  df-seq 13373  df-exp 13433  df-fac 13637  df-bc 13666  df-hash 13694  df-shft 14428  df-cj 14460  df-re 14461  df-im 14462  df-sqrt 14596  df-abs 14597  df-limsup 14830  df-clim 14847  df-rlim 14848  df-sum 15045  df-ef 15423  df-sin 15425  df-cos 15426  df-pi 15428  df-dvds 15610  df-struct 16487  df-ndx 16488  df-slot 16489  df-base 16491  df-sets 16492  df-ress 16493  df-plusg 16580  df-mulr 16581  df-starv 16582  df-sca 16583  df-vsca 16584  df-ip 16585  df-tset 16586  df-ple 16587  df-ds 16589  df-unif 16590  df-hom 16591  df-cco 16592  df-rest 16698  df-topn 16699  df-0g 16717  df-gsum 16718  df-topgen 16719  df-pt 16720  df-prds 16723  df-xrs 16777  df-qtop 16782  df-imas 16783  df-xps 16785  df-mre 16859  df-mrc 16860  df-acs 16862  df-mgm 17854  df-sgrp 17903  df-mnd 17914  df-submnd 17959  df-mulg 18227  df-cntz 18449  df-cmn 18910  df-psmet 20539  df-xmet 20540  df-met 20541  df-bl 20542  df-mopn 20543  df-fbas 20544  df-fg 20545  df-cnfld 20548  df-top 21504  df-topon 21521  df-topsp 21543  df-bases 21556  df-cld 21629  df-ntr 21630  df-cls 21631  df-nei 21708  df-lp 21746  df-perf 21747  df-cn 21837  df-cnp 21838  df-haus 21925  df-tx 22172  df-hmeo 22365  df-fil 22456  df-fm 22548  df-flim 22549  df-flf 22550  df-xms 22932  df-ms 22933  df-tms 22934  df-cncf 23488  df-limc 24466  df-dv 24467  df-log 25142  df-cxp 25143
This theorem is referenced by:  quartfull  32414
  Copyright terms: Public domain W3C validator