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

Theorem quart 25426
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 32420) 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 7146 . . . . 5 (𝜑 → (𝑋𝐸) = (𝑋 − -(𝐴 / 4)))
11 4cn 11700 . . . . . . . 8 4 ∈ ℂ
1211a1i 11 . . . . . . 7 (𝜑 → 4 ∈ ℂ)
13 4ne0 11723 . . . . . . . 8 4 ≠ 0
1413a1i 11 . . . . . . 7 (𝜑 → 4 ≠ 0)
151, 12, 14divcld 11393 . . . . . 6 (𝜑 → (𝐴 / 4) ∈ ℂ)
168, 15subnegd 10981 . . . . 5 (𝜑 → (𝑋 − -(𝐴 / 4)) = (𝑋 + (𝐴 / 4)))
1710, 16eqtrd 2856 . . . 4 (𝜑 → (𝑋𝐸) = (𝑋 + (𝐴 / 4)))
181, 2, 3, 4, 5, 6, 7, 8, 17quart1 25421 . . 3 (𝜑 → (((𝑋↑4) + (𝐴 · (𝑋↑3))) + ((𝐵 · (𝑋↑2)) + ((𝐶 · 𝑋) + 𝐷))) = ((((𝑋𝐸)↑4) + (𝑃 · ((𝑋𝐸)↑2))) + ((𝑄 · (𝑋𝐸)) + 𝑅)))
1918eqeq1d 2823 . 2 (𝜑 → ((((𝑋↑4) + (𝐴 · (𝑋↑3))) + ((𝐵 · (𝑋↑2)) + ((𝐶 · 𝑋) + 𝐷))) = 0 ↔ ((((𝑋𝐸)↑4) + (𝑃 · ((𝑋𝐸)↑2))) + ((𝑄 · (𝑋𝐸)) + 𝑅)) = 0))
201, 2, 3, 4, 5, 6, 7quart1cl 25419 . . . 4 (𝜑 → (𝑃 ∈ ℂ ∧ 𝑄 ∈ ℂ ∧ 𝑅 ∈ ℂ))
2120simp1d 1139 . . 3 (𝜑𝑃 ∈ ℂ)
2220simp2d 1140 . . 3 (𝜑𝑄 ∈ ℂ)
2315negcld 10961 . . . . 5 (𝜑 → -(𝐴 / 4) ∈ ℂ)
249, 23eqeltrd 2912 . . . 4 (𝜑𝐸 ∈ ℂ)
258, 24subcld 10974 . . 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 25424 . . . 4 (𝜑 → (𝑆 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑇 ∈ ℂ))
3433simp1d 1139 . . 3 (𝜑𝑆 ∈ ℂ)
3529oveq2d 7146 . . . . . 6 (𝜑 → (2 · 𝑆) = (2 · ((√‘𝑀) / 2)))
3633simp2d 1140 . . . . . . . 8 (𝜑𝑀 ∈ ℂ)
3736sqrtcld 14776 . . . . . . 7 (𝜑 → (√‘𝑀) ∈ ℂ)
38 2cnd 11693 . . . . . . 7 (𝜑 → 2 ∈ ℂ)
39 2ne0 11719 . . . . . . . 8 2 ≠ 0
4039a1i 11 . . . . . . 7 (𝜑 → 2 ≠ 0)
4137, 38, 40divcan2d 11395 . . . . . 6 (𝜑 → (2 · ((√‘𝑀) / 2)) = (√‘𝑀))
4235, 41eqtrd 2856 . . . . 5 (𝜑 → (2 · 𝑆) = (√‘𝑀))
4342oveq1d 7145 . . . 4 (𝜑 → ((2 · 𝑆)↑2) = ((√‘𝑀)↑2))
4436sqsqrtd 14778 . . . 4 (𝜑 → ((√‘𝑀)↑2) = 𝑀)
4543, 44eqtr2d 2857 . . 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 25425 . . . 4 (𝜑 → (𝑆 ≠ 0 ∧ 𝐼 ∈ ℂ ∧ 𝐽 ∈ ℂ))
5049simp2d 1140 . . 3 (𝜑𝐼 ∈ ℂ)
5147oveq1d 7145 . . . 4 (𝜑 → (𝐼↑2) = ((√‘((-(𝑆↑2) − (𝑃 / 2)) + ((𝑄 / 4) / 𝑆)))↑2))
5234sqcld 13492 . . . . . . . 8 (𝜑 → (𝑆↑2) ∈ ℂ)
5352negcld 10961 . . . . . . 7 (𝜑 → -(𝑆↑2) ∈ ℂ)
5421halfcld 11860 . . . . . . 7 (𝜑 → (𝑃 / 2) ∈ ℂ)
5553, 54subcld 10974 . . . . . 6 (𝜑 → (-(𝑆↑2) − (𝑃 / 2)) ∈ ℂ)
5622, 12, 14divcld 11393 . . . . . . 7 (𝜑 → (𝑄 / 4) ∈ ℂ)
5749simp1d 1139 . . . . . . 7 (𝜑𝑆 ≠ 0)
5856, 34, 57divcld 11393 . . . . . 6 (𝜑 → ((𝑄 / 4) / 𝑆) ∈ ℂ)
5955, 58addcld 10637 . . . . 5 (𝜑 → ((-(𝑆↑2) − (𝑃 / 2)) + ((𝑄 / 4) / 𝑆)) ∈ ℂ)
6059sqsqrtd 14778 . . . 4 (𝜑 → ((√‘((-(𝑆↑2) − (𝑃 / 2)) + ((𝑄 / 4) / 𝑆)))↑2) = ((-(𝑆↑2) − (𝑃 / 2)) + ((𝑄 / 4) / 𝑆)))
6151, 60eqtrd 2856 . . 3 (𝜑 → (𝐼↑2) = ((-(𝑆↑2) − (𝑃 / 2)) + ((𝑄 / 4) / 𝑆)))
6220simp3d 1141 . . 3 (𝜑𝑅 ∈ ℂ)
63 1cnd 10613 . . . . 5 (𝜑 → 1 ∈ ℂ)
64 3z 11993 . . . . . 6 3 ∈ ℤ
65 1exp 13442 . . . . . 6 (3 ∈ ℤ → (1↑3) = 1)
6664, 65mp1i 13 . . . . 5 (𝜑 → (1↑3) = 1)
6733simp3d 1141 . . . . . . . . . . 11 (𝜑𝑇 ∈ ℂ)
6867mulid2d 10636 . . . . . . . . . 10 (𝜑 → (1 · 𝑇) = 𝑇)
6968oveq2d 7146 . . . . . . . . 9 (𝜑 → ((2 · 𝑃) + (1 · 𝑇)) = ((2 · 𝑃) + 𝑇))
7068oveq2d 7146 . . . . . . . . 9 (𝜑 → (𝑈 / (1 · 𝑇)) = (𝑈 / 𝑇))
7169, 70oveq12d 7148 . . . . . . . 8 (𝜑 → (((2 · 𝑃) + (1 · 𝑇)) + (𝑈 / (1 · 𝑇))) = (((2 · 𝑃) + 𝑇) + (𝑈 / 𝑇)))
7271oveq1d 7145 . . . . . . 7 (𝜑 → ((((2 · 𝑃) + (1 · 𝑇)) + (𝑈 / (1 · 𝑇))) / 3) = ((((2 · 𝑃) + 𝑇) + (𝑈 / 𝑇)) / 3))
7372negeqd 10857 . . . . . 6 (𝜑 → -((((2 · 𝑃) + (1 · 𝑇)) + (𝑈 / (1 · 𝑇))) / 3) = -((((2 · 𝑃) + 𝑇) + (𝑈 / 𝑇)) / 3))
7430, 73eqtr4d 2859 . . . . 5 (𝜑𝑀 = -((((2 · 𝑃) + (1 · 𝑇)) + (𝑈 / (1 · 𝑇))) / 3))
75 oveq1 7137 . . . . . . . 8 (𝑥 = 1 → (𝑥↑3) = (1↑3))
7675eqeq1d 2823 . . . . . . 7 (𝑥 = 1 → ((𝑥↑3) = 1 ↔ (1↑3) = 1))
77 oveq1 7137 . . . . . . . . . . . 12 (𝑥 = 1 → (𝑥 · 𝑇) = (1 · 𝑇))
7877oveq2d 7146 . . . . . . . . . . 11 (𝑥 = 1 → ((2 · 𝑃) + (𝑥 · 𝑇)) = ((2 · 𝑃) + (1 · 𝑇)))
7977oveq2d 7146 . . . . . . . . . . 11 (𝑥 = 1 → (𝑈 / (𝑥 · 𝑇)) = (𝑈 / (1 · 𝑇)))
8078, 79oveq12d 7148 . . . . . . . . . 10 (𝑥 = 1 → (((2 · 𝑃) + (𝑥 · 𝑇)) + (𝑈 / (𝑥 · 𝑇))) = (((2 · 𝑃) + (1 · 𝑇)) + (𝑈 / (1 · 𝑇))))
8180oveq1d 7145 . . . . . . . . 9 (𝑥 = 1 → ((((2 · 𝑃) + (𝑥 · 𝑇)) + (𝑈 / (𝑥 · 𝑇))) / 3) = ((((2 · 𝑃) + (1 · 𝑇)) + (𝑈 / (1 · 𝑇))) / 3))
8281negeqd 10857 . . . . . . . 8 (𝑥 = 1 → -((((2 · 𝑃) + (𝑥 · 𝑇)) + (𝑈 / (𝑥 · 𝑇))) / 3) = -((((2 · 𝑃) + (1 · 𝑇)) + (𝑈 / (1 · 𝑇))) / 3))
8382eqeq2d 2832 . . . . . . 7 (𝑥 = 1 → (𝑀 = -((((2 · 𝑃) + (𝑥 · 𝑇)) + (𝑈 / (𝑥 · 𝑇))) / 3) ↔ 𝑀 = -((((2 · 𝑃) + (1 · 𝑇)) + (𝑈 / (1 · 𝑇))) / 3)))
8476, 83anbi12d 633 . . . . . 6 (𝑥 = 1 → (((𝑥↑3) = 1 ∧ 𝑀 = -((((2 · 𝑃) + (𝑥 · 𝑇)) + (𝑈 / (𝑥 · 𝑇))) / 3)) ↔ ((1↑3) = 1 ∧ 𝑀 = -((((2 · 𝑃) + (1 · 𝑇)) + (𝑈 / (1 · 𝑇))) / 3))))
8584rspcev 3600 . . . . 5 ((1 ∈ ℂ ∧ ((1↑3) = 1 ∧ 𝑀 = -((((2 · 𝑃) + (1 · 𝑇)) + (𝑈 / (1 · 𝑇))) / 3))) → ∃𝑥 ∈ ℂ ((𝑥↑3) = 1 ∧ 𝑀 = -((((2 · 𝑃) + (𝑥 · 𝑇)) + (𝑈 / (𝑥 · 𝑇))) / 3)))
8663, 66, 74, 85syl12anc 835 . . . 4 (𝜑 → ∃𝑥 ∈ ℂ ((𝑥↑3) = 1 ∧ 𝑀 = -((((2 · 𝑃) + (𝑥 · 𝑇)) + (𝑈 / (𝑥 · 𝑇))) / 3)))
87 2cn 11690 . . . . . 6 2 ∈ ℂ
88 mulcl 10598 . . . . . 6 ((2 ∈ ℂ ∧ 𝑃 ∈ ℂ) → (2 · 𝑃) ∈ ℂ)
8987, 21, 88sylancr 590 . . . . 5 (𝜑 → (2 · 𝑃) ∈ ℂ)
9021sqcld 13492 . . . . . 6 (𝜑 → (𝑃↑2) ∈ ℂ)
91 mulcl 10598 . . . . . . 7 ((4 ∈ ℂ ∧ 𝑅 ∈ ℂ) → (4 · 𝑅) ∈ ℂ)
9211, 62, 91sylancr 590 . . . . . 6 (𝜑 → (4 · 𝑅) ∈ ℂ)
9390, 92subcld 10974 . . . . 5 (𝜑 → ((𝑃↑2) − (4 · 𝑅)) ∈ ℂ)
9422sqcld 13492 . . . . . 6 (𝜑 → (𝑄↑2) ∈ ℂ)
9594negcld 10961 . . . . 5 (𝜑 → -(𝑄↑2) ∈ ℂ)
9631oveq1d 7145 . . . . . 6 (𝜑 → (𝑇↑3) = ((((𝑉 + 𝑊) / 2)↑𝑐(1 / 3))↑3))
971, 2, 3, 4, 1, 9, 5, 6, 7, 26, 27, 28quartlem2 25423 . . . . . . . . . 10 (𝜑 → (𝑈 ∈ ℂ ∧ 𝑉 ∈ ℂ ∧ 𝑊 ∈ ℂ))
9897simp2d 1140 . . . . . . . . 9 (𝜑𝑉 ∈ ℂ)
9997simp3d 1141 . . . . . . . . 9 (𝜑𝑊 ∈ ℂ)
10098, 99addcld 10637 . . . . . . . 8 (𝜑 → (𝑉 + 𝑊) ∈ ℂ)
101100halfcld 11860 . . . . . . 7 (𝜑 → ((𝑉 + 𝑊) / 2) ∈ ℂ)
102 3nn 11694 . . . . . . 7 3 ∈ ℕ
103 cxproot 25260 . . . . . . 7 ((((𝑉 + 𝑊) / 2) ∈ ℂ ∧ 3 ∈ ℕ) → ((((𝑉 + 𝑊) / 2)↑𝑐(1 / 3))↑3) = ((𝑉 + 𝑊) / 2))
104101, 102, 103sylancl 589 . . . . . 6 (𝜑 → ((((𝑉 + 𝑊) / 2)↑𝑐(1 / 3))↑3) = ((𝑉 + 𝑊) / 2))
10596, 104eqtrd 2856 . . . . 5 (𝜑 → (𝑇↑3) = ((𝑉 + 𝑊) / 2))
10628oveq1d 7145 . . . . . 6 (𝜑 → (𝑊↑2) = ((√‘((𝑉↑2) − (4 · (𝑈↑3))))↑2))
10798sqcld 13492 . . . . . . . 8 (𝜑 → (𝑉↑2) ∈ ℂ)
10897simp1d 1139 . . . . . . . . . 10 (𝜑𝑈 ∈ ℂ)
109 3nn0 11893 . . . . . . . . . 10 3 ∈ ℕ0
110 expcl 13431 . . . . . . . . . 10 ((𝑈 ∈ ℂ ∧ 3 ∈ ℕ0) → (𝑈↑3) ∈ ℂ)
111108, 109, 110sylancl 589 . . . . . . . . 9 (𝜑 → (𝑈↑3) ∈ ℂ)
112 mulcl 10598 . . . . . . . . 9 ((4 ∈ ℂ ∧ (𝑈↑3) ∈ ℂ) → (4 · (𝑈↑3)) ∈ ℂ)
11311, 111, 112sylancr 590 . . . . . . . 8 (𝜑 → (4 · (𝑈↑3)) ∈ ℂ)
114107, 113subcld 10974 . . . . . . 7 (𝜑 → ((𝑉↑2) − (4 · (𝑈↑3))) ∈ ℂ)
115114sqsqrtd 14778 . . . . . 6 (𝜑 → ((√‘((𝑉↑2) − (4 · (𝑈↑3))))↑2) = ((𝑉↑2) − (4 · (𝑈↑3))))
116106, 115eqtrd 2856 . . . . 5 (𝜑 → (𝑊↑2) = ((𝑉↑2) − (4 · (𝑈↑3))))
11721, 22, 62, 26, 27quartlem1 25422 . . . . . 6 (𝜑 → (𝑈 = (((2 · 𝑃)↑2) − (3 · ((𝑃↑2) − (4 · 𝑅)))) ∧ 𝑉 = (((2 · ((2 · 𝑃)↑3)) − (9 · ((2 · 𝑃) · ((𝑃↑2) − (4 · 𝑅))))) + (27 · -(𝑄↑2)))))
118117simpld 498 . . . . 5 (𝜑𝑈 = (((2 · 𝑃)↑2) − (3 · ((𝑃↑2) − (4 · 𝑅)))))
119117simprd 499 . . . . 5 (𝜑𝑉 = (((2 · ((2 · 𝑃)↑3)) − (9 · ((2 · 𝑃) · ((𝑃↑2) − (4 · 𝑅))))) + (27 · -(𝑄↑2))))
12089, 93, 95, 36, 67, 105, 99, 116, 118, 119, 32mcubic 25412 . . . 4 (𝜑 → ((((𝑀↑3) + ((2 · 𝑃) · (𝑀↑2))) + ((((𝑃↑2) − (4 · 𝑅)) · 𝑀) + -(𝑄↑2))) = 0 ↔ ∃𝑥 ∈ ℂ ((𝑥↑3) = 1 ∧ 𝑀 = -((((2 · 𝑃) + (𝑥 · 𝑇)) + (𝑈 / (𝑥 · 𝑇))) / 3))))
12186, 120mpbird 260 . . 3 (𝜑 → (((𝑀↑3) + ((2 · 𝑃) · (𝑀↑2))) + ((((𝑃↑2) − (4 · 𝑅)) · 𝑀) + -(𝑄↑2))) = 0)
12249simp3d 1141 . . 3 (𝜑𝐽 ∈ ℂ)
12348oveq1d 7145 . . . 4 (𝜑 → (𝐽↑2) = ((√‘((-(𝑆↑2) − (𝑃 / 2)) − ((𝑄 / 4) / 𝑆)))↑2))
12455, 58subcld 10974 . . . . 5 (𝜑 → ((-(𝑆↑2) − (𝑃 / 2)) − ((𝑄 / 4) / 𝑆)) ∈ ℂ)
125124sqsqrtd 14778 . . . 4 (𝜑 → ((√‘((-(𝑆↑2) − (𝑃 / 2)) − ((𝑄 / 4) / 𝑆)))↑2) = ((-(𝑆↑2) − (𝑃 / 2)) − ((𝑄 / 4) / 𝑆)))
126123, 125eqtrd 2856 . . 3 (𝜑 → (𝐽↑2) = ((-(𝑆↑2) − (𝑃 / 2)) − ((𝑄 / 4) / 𝑆)))
12721, 22, 25, 34, 45, 46, 50, 61, 62, 121, 122, 126dquart 25418 . 2 (𝜑 → (((((𝑋𝐸)↑4) + (𝑃 · ((𝑋𝐸)↑2))) + ((𝑄 · (𝑋𝐸)) + 𝑅)) = 0 ↔ (((𝑋𝐸) = (-𝑆 + 𝐼) ∨ (𝑋𝐸) = (-𝑆𝐼)) ∨ ((𝑋𝐸) = (𝑆 + 𝐽) ∨ (𝑋𝐸) = (𝑆𝐽)))))
12834negcld 10961 . . . . . . . 8 (𝜑 → -𝑆 ∈ ℂ)
129128, 50addcld 10637 . . . . . . 7 (𝜑 → (-𝑆 + 𝐼) ∈ ℂ)
1308, 24, 129subaddd 10992 . . . . . 6 (𝜑 → ((𝑋𝐸) = (-𝑆 + 𝐼) ↔ (𝐸 + (-𝑆 + 𝐼)) = 𝑋))
13124, 34negsubd 10980 . . . . . . . . 9 (𝜑 → (𝐸 + -𝑆) = (𝐸𝑆))
132131oveq1d 7145 . . . . . . . 8 (𝜑 → ((𝐸 + -𝑆) + 𝐼) = ((𝐸𝑆) + 𝐼))
13324, 128, 50addassd 10640 . . . . . . . 8 (𝜑 → ((𝐸 + -𝑆) + 𝐼) = (𝐸 + (-𝑆 + 𝐼)))
134132, 133eqtr3d 2858 . . . . . . 7 (𝜑 → ((𝐸𝑆) + 𝐼) = (𝐸 + (-𝑆 + 𝐼)))
135134eqeq1d 2823 . . . . . 6 (𝜑 → (((𝐸𝑆) + 𝐼) = 𝑋 ↔ (𝐸 + (-𝑆 + 𝐼)) = 𝑋))
136130, 135bitr4d 285 . . . . 5 (𝜑 → ((𝑋𝐸) = (-𝑆 + 𝐼) ↔ ((𝐸𝑆) + 𝐼) = 𝑋))
137 eqcom 2828 . . . . 5 (((𝐸𝑆) + 𝐼) = 𝑋𝑋 = ((𝐸𝑆) + 𝐼))
138136, 137syl6bb 290 . . . 4 (𝜑 → ((𝑋𝐸) = (-𝑆 + 𝐼) ↔ 𝑋 = ((𝐸𝑆) + 𝐼)))
139128, 50subcld 10974 . . . . . . 7 (𝜑 → (-𝑆𝐼) ∈ ℂ)
1408, 24, 139subaddd 10992 . . . . . 6 (𝜑 → ((𝑋𝐸) = (-𝑆𝐼) ↔ (𝐸 + (-𝑆𝐼)) = 𝑋))
141131oveq1d 7145 . . . . . . . 8 (𝜑 → ((𝐸 + -𝑆) − 𝐼) = ((𝐸𝑆) − 𝐼))
14224, 128, 50addsubassd 10994 . . . . . . . 8 (𝜑 → ((𝐸 + -𝑆) − 𝐼) = (𝐸 + (-𝑆𝐼)))
143141, 142eqtr3d 2858 . . . . . . 7 (𝜑 → ((𝐸𝑆) − 𝐼) = (𝐸 + (-𝑆𝐼)))
144143eqeq1d 2823 . . . . . 6 (𝜑 → (((𝐸𝑆) − 𝐼) = 𝑋 ↔ (𝐸 + (-𝑆𝐼)) = 𝑋))
145140, 144bitr4d 285 . . . . 5 (𝜑 → ((𝑋𝐸) = (-𝑆𝐼) ↔ ((𝐸𝑆) − 𝐼) = 𝑋))
146 eqcom 2828 . . . . 5 (((𝐸𝑆) − 𝐼) = 𝑋𝑋 = ((𝐸𝑆) − 𝐼))
147145, 146syl6bb 290 . . . 4 (𝜑 → ((𝑋𝐸) = (-𝑆𝐼) ↔ 𝑋 = ((𝐸𝑆) − 𝐼)))
148138, 147orbi12d 916 . . 3 (𝜑 → (((𝑋𝐸) = (-𝑆 + 𝐼) ∨ (𝑋𝐸) = (-𝑆𝐼)) ↔ (𝑋 = ((𝐸𝑆) + 𝐼) ∨ 𝑋 = ((𝐸𝑆) − 𝐼))))
14934, 122addcld 10637 . . . . . . 7 (𝜑 → (𝑆 + 𝐽) ∈ ℂ)
1508, 24, 149subaddd 10992 . . . . . 6 (𝜑 → ((𝑋𝐸) = (𝑆 + 𝐽) ↔ (𝐸 + (𝑆 + 𝐽)) = 𝑋))
15124, 34, 122addassd 10640 . . . . . . 7 (𝜑 → ((𝐸 + 𝑆) + 𝐽) = (𝐸 + (𝑆 + 𝐽)))
152151eqeq1d 2823 . . . . . 6 (𝜑 → (((𝐸 + 𝑆) + 𝐽) = 𝑋 ↔ (𝐸 + (𝑆 + 𝐽)) = 𝑋))
153150, 152bitr4d 285 . . . . 5 (𝜑 → ((𝑋𝐸) = (𝑆 + 𝐽) ↔ ((𝐸 + 𝑆) + 𝐽) = 𝑋))
154 eqcom 2828 . . . . 5 (((𝐸 + 𝑆) + 𝐽) = 𝑋𝑋 = ((𝐸 + 𝑆) + 𝐽))
155153, 154syl6bb 290 . . . 4 (𝜑 → ((𝑋𝐸) = (𝑆 + 𝐽) ↔ 𝑋 = ((𝐸 + 𝑆) + 𝐽)))
15634, 122subcld 10974 . . . . . . 7 (𝜑 → (𝑆𝐽) ∈ ℂ)
1578, 24, 156subaddd 10992 . . . . . 6 (𝜑 → ((𝑋𝐸) = (𝑆𝐽) ↔ (𝐸 + (𝑆𝐽)) = 𝑋))
15824, 34, 122addsubassd 10994 . . . . . . 7 (𝜑 → ((𝐸 + 𝑆) − 𝐽) = (𝐸 + (𝑆𝐽)))
159158eqeq1d 2823 . . . . . 6 (𝜑 → (((𝐸 + 𝑆) − 𝐽) = 𝑋 ↔ (𝐸 + (𝑆𝐽)) = 𝑋))
160157, 159bitr4d 285 . . . . 5 (𝜑 → ((𝑋𝐸) = (𝑆𝐽) ↔ ((𝐸 + 𝑆) − 𝐽) = 𝑋))
161 eqcom 2828 . . . . 5 (((𝐸 + 𝑆) − 𝐽) = 𝑋𝑋 = ((𝐸 + 𝑆) − 𝐽))
162160, 161syl6bb 290 . . . 4 (𝜑 → ((𝑋𝐸) = (𝑆𝐽) ↔ 𝑋 = ((𝐸 + 𝑆) − 𝐽)))
163155, 162orbi12d 916 . . 3 (𝜑 → (((𝑋𝐸) = (𝑆 + 𝐽) ∨ (𝑋𝐸) = (𝑆𝐽)) ↔ (𝑋 = ((𝐸 + 𝑆) + 𝐽) ∨ 𝑋 = ((𝐸 + 𝑆) − 𝐽))))
164148, 163orbi12d 916 . 2 (𝜑 → ((((𝑋𝐸) = (-𝑆 + 𝐼) ∨ (𝑋𝐸) = (-𝑆𝐼)) ∨ ((𝑋𝐸) = (𝑆 + 𝐽) ∨ (𝑋𝐸) = (𝑆𝐽))) ↔ ((𝑋 = ((𝐸𝑆) + 𝐼) ∨ 𝑋 = ((𝐸𝑆) − 𝐼)) ∨ (𝑋 = ((𝐸 + 𝑆) + 𝐽) ∨ 𝑋 = ((𝐸 + 𝑆) − 𝐽)))))
16519, 127, 1643bitrd 308 1 (𝜑 → ((((𝑋↑4) + (𝐴 · (𝑋↑3))) + ((𝐵 · (𝑋↑2)) + ((𝐶 · 𝑋) + 𝐷))) = 0 ↔ ((𝑋 = ((𝐸𝑆) + 𝐼) ∨ 𝑋 = ((𝐸𝑆) − 𝐼)) ∨ (𝑋 = ((𝐸 + 𝑆) + 𝐽) ∨ 𝑋 = ((𝐸 + 𝑆) − 𝐽)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  wo 844   = wceq 1538  wcel 2115  wne 3007  wrex 3127  cfv 6328  (class class class)co 7130  cc 10512  0cc0 10514  1c1 10515   + caddc 10517   · cmul 10519  cmin 10847  -cneg 10848   / cdiv 11274  cn 11615  2c2 11670  3c3 11671  4c4 11672  5c5 11673  6c6 11674  7c7 11675  8c8 11676  9c9 11677  0cn0 11875  cz 11959  cdc 12076  cexp 13413  csqrt 14571  𝑐ccxp 25126
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793  ax-rep 5163  ax-sep 5176  ax-nul 5183  ax-pow 5239  ax-pr 5303  ax-un 7436  ax-inf2 9080  ax-cnex 10570  ax-resscn 10571  ax-1cn 10572  ax-icn 10573  ax-addcl 10574  ax-addrcl 10575  ax-mulcl 10576  ax-mulrcl 10577  ax-mulcom 10578  ax-addass 10579  ax-mulass 10580  ax-distr 10581  ax-i2m1 10582  ax-1ne0 10583  ax-1rid 10584  ax-rnegex 10585  ax-rrecex 10586  ax-cnre 10587  ax-pre-lttri 10588  ax-pre-lttrn 10589  ax-pre-ltadd 10590  ax-pre-mulgt0 10591  ax-pre-sup 10592  ax-addf 10593  ax-mulf 10594
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2623  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-ne 3008  df-nel 3112  df-ral 3131  df-rex 3132  df-reu 3133  df-rmo 3134  df-rab 3135  df-v 3473  df-sbc 3750  df-csb 3858  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4267  df-if 4441  df-pw 4514  df-sn 4541  df-pr 4543  df-tp 4545  df-op 4547  df-uni 4812  df-int 4850  df-iun 4894  df-iin 4895  df-br 5040  df-opab 5102  df-mpt 5120  df-tr 5146  df-id 5433  df-eprel 5438  df-po 5447  df-so 5448  df-fr 5487  df-se 5488  df-we 5489  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-pred 6121  df-ord 6167  df-on 6168  df-lim 6169  df-suc 6170  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-isom 6337  df-riota 7088  df-ov 7133  df-oprab 7134  df-mpo 7135  df-of 7384  df-om 7556  df-1st 7664  df-2nd 7665  df-supp 7806  df-wrecs 7922  df-recs 7983  df-rdg 8021  df-1o 8077  df-2o 8078  df-oadd 8081  df-er 8264  df-map 8383  df-pm 8384  df-ixp 8437  df-en 8485  df-dom 8486  df-sdom 8487  df-fin 8488  df-fsupp 8810  df-fi 8851  df-sup 8882  df-inf 8883  df-oi 8950  df-card 9344  df-pnf 10654  df-mnf 10655  df-xr 10656  df-ltxr 10657  df-le 10658  df-sub 10849  df-neg 10850  df-div 11275  df-nn 11616  df-2 11678  df-3 11679  df-4 11680  df-5 11681  df-6 11682  df-7 11683  df-8 11684  df-9 11685  df-n0 11876  df-z 11960  df-dec 12077  df-uz 12222  df-q 12327  df-rp 12368  df-xneg 12485  df-xadd 12486  df-xmul 12487  df-ioo 12720  df-ioc 12721  df-ico 12722  df-icc 12723  df-fz 12876  df-fzo 13017  df-fl 13145  df-mod 13221  df-seq 13353  df-exp 13414  df-fac 13618  df-bc 13647  df-hash 13675  df-shft 14405  df-cj 14437  df-re 14438  df-im 14439  df-sqrt 14573  df-abs 14574  df-limsup 14807  df-clim 14824  df-rlim 14825  df-sum 15022  df-ef 15400  df-sin 15402  df-cos 15403  df-pi 15405  df-dvds 15587  df-struct 16464  df-ndx 16465  df-slot 16466  df-base 16468  df-sets 16469  df-ress 16470  df-plusg 16557  df-mulr 16558  df-starv 16559  df-sca 16560  df-vsca 16561  df-ip 16562  df-tset 16563  df-ple 16564  df-ds 16566  df-unif 16567  df-hom 16568  df-cco 16569  df-rest 16675  df-topn 16676  df-0g 16694  df-gsum 16695  df-topgen 16696  df-pt 16697  df-prds 16700  df-xrs 16754  df-qtop 16759  df-imas 16760  df-xps 16762  df-mre 16836  df-mrc 16837  df-acs 16839  df-mgm 17831  df-sgrp 17880  df-mnd 17891  df-submnd 17936  df-mulg 18204  df-cntz 18426  df-cmn 18887  df-psmet 20513  df-xmet 20514  df-met 20515  df-bl 20516  df-mopn 20517  df-fbas 20518  df-fg 20519  df-cnfld 20522  df-top 21478  df-topon 21495  df-topsp 21517  df-bases 21530  df-cld 21603  df-ntr 21604  df-cls 21605  df-nei 21682  df-lp 21720  df-perf 21721  df-cn 21811  df-cnp 21812  df-haus 21899  df-tx 22146  df-hmeo 22339  df-fil 22430  df-fm 22522  df-flim 22523  df-flf 22524  df-xms 22906  df-ms 22907  df-tms 22908  df-cncf 23462  df-limc 24448  df-dv 24449  df-log 25127  df-cxp 25128
This theorem is referenced by:  quartfull  32420
  Copyright terms: Public domain W3C validator