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

Theorem quart 25768
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 32863) 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 7247 . . . . 5 (𝜑 → (𝑋𝐸) = (𝑋 − -(𝐴 / 4)))
11 4cn 11939 . . . . . . . 8 4 ∈ ℂ
1211a1i 11 . . . . . . 7 (𝜑 → 4 ∈ ℂ)
13 4ne0 11962 . . . . . . . 8 4 ≠ 0
1413a1i 11 . . . . . . 7 (𝜑 → 4 ≠ 0)
151, 12, 14divcld 11632 . . . . . 6 (𝜑 → (𝐴 / 4) ∈ ℂ)
168, 15subnegd 11220 . . . . 5 (𝜑 → (𝑋 − -(𝐴 / 4)) = (𝑋 + (𝐴 / 4)))
1710, 16eqtrd 2778 . . . 4 (𝜑 → (𝑋𝐸) = (𝑋 + (𝐴 / 4)))
181, 2, 3, 4, 5, 6, 7, 8, 17quart1 25763 . . 3 (𝜑 → (((𝑋↑4) + (𝐴 · (𝑋↑3))) + ((𝐵 · (𝑋↑2)) + ((𝐶 · 𝑋) + 𝐷))) = ((((𝑋𝐸)↑4) + (𝑃 · ((𝑋𝐸)↑2))) + ((𝑄 · (𝑋𝐸)) + 𝑅)))
1918eqeq1d 2740 . 2 (𝜑 → ((((𝑋↑4) + (𝐴 · (𝑋↑3))) + ((𝐵 · (𝑋↑2)) + ((𝐶 · 𝑋) + 𝐷))) = 0 ↔ ((((𝑋𝐸)↑4) + (𝑃 · ((𝑋𝐸)↑2))) + ((𝑄 · (𝑋𝐸)) + 𝑅)) = 0))
201, 2, 3, 4, 5, 6, 7quart1cl 25761 . . . 4 (𝜑 → (𝑃 ∈ ℂ ∧ 𝑄 ∈ ℂ ∧ 𝑅 ∈ ℂ))
2120simp1d 1144 . . 3 (𝜑𝑃 ∈ ℂ)
2220simp2d 1145 . . 3 (𝜑𝑄 ∈ ℂ)
2315negcld 11200 . . . . 5 (𝜑 → -(𝐴 / 4) ∈ ℂ)
249, 23eqeltrd 2839 . . . 4 (𝜑𝐸 ∈ ℂ)
258, 24subcld 11213 . . 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 25766 . . . 4 (𝜑 → (𝑆 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑇 ∈ ℂ))
3433simp1d 1144 . . 3 (𝜑𝑆 ∈ ℂ)
3529oveq2d 7247 . . . . . 6 (𝜑 → (2 · 𝑆) = (2 · ((√‘𝑀) / 2)))
3633simp2d 1145 . . . . . . . 8 (𝜑𝑀 ∈ ℂ)
3736sqrtcld 15025 . . . . . . 7 (𝜑 → (√‘𝑀) ∈ ℂ)
38 2cnd 11932 . . . . . . 7 (𝜑 → 2 ∈ ℂ)
39 2ne0 11958 . . . . . . . 8 2 ≠ 0
4039a1i 11 . . . . . . 7 (𝜑 → 2 ≠ 0)
4137, 38, 40divcan2d 11634 . . . . . 6 (𝜑 → (2 · ((√‘𝑀) / 2)) = (√‘𝑀))
4235, 41eqtrd 2778 . . . . 5 (𝜑 → (2 · 𝑆) = (√‘𝑀))
4342oveq1d 7246 . . . 4 (𝜑 → ((2 · 𝑆)↑2) = ((√‘𝑀)↑2))
4436sqsqrtd 15027 . . . 4 (𝜑 → ((√‘𝑀)↑2) = 𝑀)
4543, 44eqtr2d 2779 . . 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 25767 . . . 4 (𝜑 → (𝑆 ≠ 0 ∧ 𝐼 ∈ ℂ ∧ 𝐽 ∈ ℂ))
5049simp2d 1145 . . 3 (𝜑𝐼 ∈ ℂ)
5147oveq1d 7246 . . . 4 (𝜑 → (𝐼↑2) = ((√‘((-(𝑆↑2) − (𝑃 / 2)) + ((𝑄 / 4) / 𝑆)))↑2))
5234sqcld 13738 . . . . . . . 8 (𝜑 → (𝑆↑2) ∈ ℂ)
5352negcld 11200 . . . . . . 7 (𝜑 → -(𝑆↑2) ∈ ℂ)
5421halfcld 12099 . . . . . . 7 (𝜑 → (𝑃 / 2) ∈ ℂ)
5553, 54subcld 11213 . . . . . 6 (𝜑 → (-(𝑆↑2) − (𝑃 / 2)) ∈ ℂ)
5622, 12, 14divcld 11632 . . . . . . 7 (𝜑 → (𝑄 / 4) ∈ ℂ)
5749simp1d 1144 . . . . . . 7 (𝜑𝑆 ≠ 0)
5856, 34, 57divcld 11632 . . . . . 6 (𝜑 → ((𝑄 / 4) / 𝑆) ∈ ℂ)
5955, 58addcld 10876 . . . . 5 (𝜑 → ((-(𝑆↑2) − (𝑃 / 2)) + ((𝑄 / 4) / 𝑆)) ∈ ℂ)
6059sqsqrtd 15027 . . . 4 (𝜑 → ((√‘((-(𝑆↑2) − (𝑃 / 2)) + ((𝑄 / 4) / 𝑆)))↑2) = ((-(𝑆↑2) − (𝑃 / 2)) + ((𝑄 / 4) / 𝑆)))
6151, 60eqtrd 2778 . . 3 (𝜑 → (𝐼↑2) = ((-(𝑆↑2) − (𝑃 / 2)) + ((𝑄 / 4) / 𝑆)))
6220simp3d 1146 . . 3 (𝜑𝑅 ∈ ℂ)
63 1cnd 10852 . . . . 5 (𝜑 → 1 ∈ ℂ)
64 3z 12234 . . . . . 6 3 ∈ ℤ
65 1exp 13688 . . . . . 6 (3 ∈ ℤ → (1↑3) = 1)
6664, 65mp1i 13 . . . . 5 (𝜑 → (1↑3) = 1)
6733simp3d 1146 . . . . . . . . . . 11 (𝜑𝑇 ∈ ℂ)
6867mulid2d 10875 . . . . . . . . . 10 (𝜑 → (1 · 𝑇) = 𝑇)
6968oveq2d 7247 . . . . . . . . 9 (𝜑 → ((2 · 𝑃) + (1 · 𝑇)) = ((2 · 𝑃) + 𝑇))
7068oveq2d 7247 . . . . . . . . 9 (𝜑 → (𝑈 / (1 · 𝑇)) = (𝑈 / 𝑇))
7169, 70oveq12d 7249 . . . . . . . 8 (𝜑 → (((2 · 𝑃) + (1 · 𝑇)) + (𝑈 / (1 · 𝑇))) = (((2 · 𝑃) + 𝑇) + (𝑈 / 𝑇)))
7271oveq1d 7246 . . . . . . 7 (𝜑 → ((((2 · 𝑃) + (1 · 𝑇)) + (𝑈 / (1 · 𝑇))) / 3) = ((((2 · 𝑃) + 𝑇) + (𝑈 / 𝑇)) / 3))
7372negeqd 11096 . . . . . 6 (𝜑 → -((((2 · 𝑃) + (1 · 𝑇)) + (𝑈 / (1 · 𝑇))) / 3) = -((((2 · 𝑃) + 𝑇) + (𝑈 / 𝑇)) / 3))
7430, 73eqtr4d 2781 . . . . 5 (𝜑𝑀 = -((((2 · 𝑃) + (1 · 𝑇)) + (𝑈 / (1 · 𝑇))) / 3))
75 oveq1 7238 . . . . . . . 8 (𝑥 = 1 → (𝑥↑3) = (1↑3))
7675eqeq1d 2740 . . . . . . 7 (𝑥 = 1 → ((𝑥↑3) = 1 ↔ (1↑3) = 1))
77 oveq1 7238 . . . . . . . . . . . 12 (𝑥 = 1 → (𝑥 · 𝑇) = (1 · 𝑇))
7877oveq2d 7247 . . . . . . . . . . 11 (𝑥 = 1 → ((2 · 𝑃) + (𝑥 · 𝑇)) = ((2 · 𝑃) + (1 · 𝑇)))
7977oveq2d 7247 . . . . . . . . . . 11 (𝑥 = 1 → (𝑈 / (𝑥 · 𝑇)) = (𝑈 / (1 · 𝑇)))
8078, 79oveq12d 7249 . . . . . . . . . 10 (𝑥 = 1 → (((2 · 𝑃) + (𝑥 · 𝑇)) + (𝑈 / (𝑥 · 𝑇))) = (((2 · 𝑃) + (1 · 𝑇)) + (𝑈 / (1 · 𝑇))))
8180oveq1d 7246 . . . . . . . . 9 (𝑥 = 1 → ((((2 · 𝑃) + (𝑥 · 𝑇)) + (𝑈 / (𝑥 · 𝑇))) / 3) = ((((2 · 𝑃) + (1 · 𝑇)) + (𝑈 / (1 · 𝑇))) / 3))
8281negeqd 11096 . . . . . . . 8 (𝑥 = 1 → -((((2 · 𝑃) + (𝑥 · 𝑇)) + (𝑈 / (𝑥 · 𝑇))) / 3) = -((((2 · 𝑃) + (1 · 𝑇)) + (𝑈 / (1 · 𝑇))) / 3))
8382eqeq2d 2749 . . . . . . 7 (𝑥 = 1 → (𝑀 = -((((2 · 𝑃) + (𝑥 · 𝑇)) + (𝑈 / (𝑥 · 𝑇))) / 3) ↔ 𝑀 = -((((2 · 𝑃) + (1 · 𝑇)) + (𝑈 / (1 · 𝑇))) / 3)))
8476, 83anbi12d 634 . . . . . 6 (𝑥 = 1 → (((𝑥↑3) = 1 ∧ 𝑀 = -((((2 · 𝑃) + (𝑥 · 𝑇)) + (𝑈 / (𝑥 · 𝑇))) / 3)) ↔ ((1↑3) = 1 ∧ 𝑀 = -((((2 · 𝑃) + (1 · 𝑇)) + (𝑈 / (1 · 𝑇))) / 3))))
8584rspcev 3549 . . . . 5 ((1 ∈ ℂ ∧ ((1↑3) = 1 ∧ 𝑀 = -((((2 · 𝑃) + (1 · 𝑇)) + (𝑈 / (1 · 𝑇))) / 3))) → ∃𝑥 ∈ ℂ ((𝑥↑3) = 1 ∧ 𝑀 = -((((2 · 𝑃) + (𝑥 · 𝑇)) + (𝑈 / (𝑥 · 𝑇))) / 3)))
8663, 66, 74, 85syl12anc 837 . . . 4 (𝜑 → ∃𝑥 ∈ ℂ ((𝑥↑3) = 1 ∧ 𝑀 = -((((2 · 𝑃) + (𝑥 · 𝑇)) + (𝑈 / (𝑥 · 𝑇))) / 3)))
87 2cn 11929 . . . . . 6 2 ∈ ℂ
88 mulcl 10837 . . . . . 6 ((2 ∈ ℂ ∧ 𝑃 ∈ ℂ) → (2 · 𝑃) ∈ ℂ)
8987, 21, 88sylancr 590 . . . . 5 (𝜑 → (2 · 𝑃) ∈ ℂ)
9021sqcld 13738 . . . . . 6 (𝜑 → (𝑃↑2) ∈ ℂ)
91 mulcl 10837 . . . . . . 7 ((4 ∈ ℂ ∧ 𝑅 ∈ ℂ) → (4 · 𝑅) ∈ ℂ)
9211, 62, 91sylancr 590 . . . . . 6 (𝜑 → (4 · 𝑅) ∈ ℂ)
9390, 92subcld 11213 . . . . 5 (𝜑 → ((𝑃↑2) − (4 · 𝑅)) ∈ ℂ)
9422sqcld 13738 . . . . . 6 (𝜑 → (𝑄↑2) ∈ ℂ)
9594negcld 11200 . . . . 5 (𝜑 → -(𝑄↑2) ∈ ℂ)
9631oveq1d 7246 . . . . . 6 (𝜑 → (𝑇↑3) = ((((𝑉 + 𝑊) / 2)↑𝑐(1 / 3))↑3))
971, 2, 3, 4, 1, 9, 5, 6, 7, 26, 27, 28quartlem2 25765 . . . . . . . . . 10 (𝜑 → (𝑈 ∈ ℂ ∧ 𝑉 ∈ ℂ ∧ 𝑊 ∈ ℂ))
9897simp2d 1145 . . . . . . . . 9 (𝜑𝑉 ∈ ℂ)
9997simp3d 1146 . . . . . . . . 9 (𝜑𝑊 ∈ ℂ)
10098, 99addcld 10876 . . . . . . . 8 (𝜑 → (𝑉 + 𝑊) ∈ ℂ)
101100halfcld 12099 . . . . . . 7 (𝜑 → ((𝑉 + 𝑊) / 2) ∈ ℂ)
102 3nn 11933 . . . . . . 7 3 ∈ ℕ
103 cxproot 25602 . . . . . . 7 ((((𝑉 + 𝑊) / 2) ∈ ℂ ∧ 3 ∈ ℕ) → ((((𝑉 + 𝑊) / 2)↑𝑐(1 / 3))↑3) = ((𝑉 + 𝑊) / 2))
104101, 102, 103sylancl 589 . . . . . 6 (𝜑 → ((((𝑉 + 𝑊) / 2)↑𝑐(1 / 3))↑3) = ((𝑉 + 𝑊) / 2))
10596, 104eqtrd 2778 . . . . 5 (𝜑 → (𝑇↑3) = ((𝑉 + 𝑊) / 2))
10628oveq1d 7246 . . . . . 6 (𝜑 → (𝑊↑2) = ((√‘((𝑉↑2) − (4 · (𝑈↑3))))↑2))
10798sqcld 13738 . . . . . . . 8 (𝜑 → (𝑉↑2) ∈ ℂ)
10897simp1d 1144 . . . . . . . . . 10 (𝜑𝑈 ∈ ℂ)
109 3nn0 12132 . . . . . . . . . 10 3 ∈ ℕ0
110 expcl 13677 . . . . . . . . . 10 ((𝑈 ∈ ℂ ∧ 3 ∈ ℕ0) → (𝑈↑3) ∈ ℂ)
111108, 109, 110sylancl 589 . . . . . . . . 9 (𝜑 → (𝑈↑3) ∈ ℂ)
112 mulcl 10837 . . . . . . . . 9 ((4 ∈ ℂ ∧ (𝑈↑3) ∈ ℂ) → (4 · (𝑈↑3)) ∈ ℂ)
11311, 111, 112sylancr 590 . . . . . . . 8 (𝜑 → (4 · (𝑈↑3)) ∈ ℂ)
114107, 113subcld 11213 . . . . . . 7 (𝜑 → ((𝑉↑2) − (4 · (𝑈↑3))) ∈ ℂ)
115114sqsqrtd 15027 . . . . . 6 (𝜑 → ((√‘((𝑉↑2) − (4 · (𝑈↑3))))↑2) = ((𝑉↑2) − (4 · (𝑈↑3))))
116106, 115eqtrd 2778 . . . . 5 (𝜑 → (𝑊↑2) = ((𝑉↑2) − (4 · (𝑈↑3))))
11721, 22, 62, 26, 27quartlem1 25764 . . . . . 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 25754 . . . 4 (𝜑 → ((((𝑀↑3) + ((2 · 𝑃) · (𝑀↑2))) + ((((𝑃↑2) − (4 · 𝑅)) · 𝑀) + -(𝑄↑2))) = 0 ↔ ∃𝑥 ∈ ℂ ((𝑥↑3) = 1 ∧ 𝑀 = -((((2 · 𝑃) + (𝑥 · 𝑇)) + (𝑈 / (𝑥 · 𝑇))) / 3))))
12186, 120mpbird 260 . . 3 (𝜑 → (((𝑀↑3) + ((2 · 𝑃) · (𝑀↑2))) + ((((𝑃↑2) − (4 · 𝑅)) · 𝑀) + -(𝑄↑2))) = 0)
12249simp3d 1146 . . 3 (𝜑𝐽 ∈ ℂ)
12348oveq1d 7246 . . . 4 (𝜑 → (𝐽↑2) = ((√‘((-(𝑆↑2) − (𝑃 / 2)) − ((𝑄 / 4) / 𝑆)))↑2))
12455, 58subcld 11213 . . . . 5 (𝜑 → ((-(𝑆↑2) − (𝑃 / 2)) − ((𝑄 / 4) / 𝑆)) ∈ ℂ)
125124sqsqrtd 15027 . . . 4 (𝜑 → ((√‘((-(𝑆↑2) − (𝑃 / 2)) − ((𝑄 / 4) / 𝑆)))↑2) = ((-(𝑆↑2) − (𝑃 / 2)) − ((𝑄 / 4) / 𝑆)))
126123, 125eqtrd 2778 . . 3 (𝜑 → (𝐽↑2) = ((-(𝑆↑2) − (𝑃 / 2)) − ((𝑄 / 4) / 𝑆)))
12721, 22, 25, 34, 45, 46, 50, 61, 62, 121, 122, 126dquart 25760 . 2 (𝜑 → (((((𝑋𝐸)↑4) + (𝑃 · ((𝑋𝐸)↑2))) + ((𝑄 · (𝑋𝐸)) + 𝑅)) = 0 ↔ (((𝑋𝐸) = (-𝑆 + 𝐼) ∨ (𝑋𝐸) = (-𝑆𝐼)) ∨ ((𝑋𝐸) = (𝑆 + 𝐽) ∨ (𝑋𝐸) = (𝑆𝐽)))))
12834negcld 11200 . . . . . . . 8 (𝜑 → -𝑆 ∈ ℂ)
129128, 50addcld 10876 . . . . . . 7 (𝜑 → (-𝑆 + 𝐼) ∈ ℂ)
1308, 24, 129subaddd 11231 . . . . . 6 (𝜑 → ((𝑋𝐸) = (-𝑆 + 𝐼) ↔ (𝐸 + (-𝑆 + 𝐼)) = 𝑋))
13124, 34negsubd 11219 . . . . . . . . 9 (𝜑 → (𝐸 + -𝑆) = (𝐸𝑆))
132131oveq1d 7246 . . . . . . . 8 (𝜑 → ((𝐸 + -𝑆) + 𝐼) = ((𝐸𝑆) + 𝐼))
13324, 128, 50addassd 10879 . . . . . . . 8 (𝜑 → ((𝐸 + -𝑆) + 𝐼) = (𝐸 + (-𝑆 + 𝐼)))
134132, 133eqtr3d 2780 . . . . . . 7 (𝜑 → ((𝐸𝑆) + 𝐼) = (𝐸 + (-𝑆 + 𝐼)))
135134eqeq1d 2740 . . . . . 6 (𝜑 → (((𝐸𝑆) + 𝐼) = 𝑋 ↔ (𝐸 + (-𝑆 + 𝐼)) = 𝑋))
136130, 135bitr4d 285 . . . . 5 (𝜑 → ((𝑋𝐸) = (-𝑆 + 𝐼) ↔ ((𝐸𝑆) + 𝐼) = 𝑋))
137 eqcom 2745 . . . . 5 (((𝐸𝑆) + 𝐼) = 𝑋𝑋 = ((𝐸𝑆) + 𝐼))
138136, 137bitrdi 290 . . . 4 (𝜑 → ((𝑋𝐸) = (-𝑆 + 𝐼) ↔ 𝑋 = ((𝐸𝑆) + 𝐼)))
139128, 50subcld 11213 . . . . . . 7 (𝜑 → (-𝑆𝐼) ∈ ℂ)
1408, 24, 139subaddd 11231 . . . . . 6 (𝜑 → ((𝑋𝐸) = (-𝑆𝐼) ↔ (𝐸 + (-𝑆𝐼)) = 𝑋))
141131oveq1d 7246 . . . . . . . 8 (𝜑 → ((𝐸 + -𝑆) − 𝐼) = ((𝐸𝑆) − 𝐼))
14224, 128, 50addsubassd 11233 . . . . . . . 8 (𝜑 → ((𝐸 + -𝑆) − 𝐼) = (𝐸 + (-𝑆𝐼)))
143141, 142eqtr3d 2780 . . . . . . 7 (𝜑 → ((𝐸𝑆) − 𝐼) = (𝐸 + (-𝑆𝐼)))
144143eqeq1d 2740 . . . . . 6 (𝜑 → (((𝐸𝑆) − 𝐼) = 𝑋 ↔ (𝐸 + (-𝑆𝐼)) = 𝑋))
145140, 144bitr4d 285 . . . . 5 (𝜑 → ((𝑋𝐸) = (-𝑆𝐼) ↔ ((𝐸𝑆) − 𝐼) = 𝑋))
146 eqcom 2745 . . . . 5 (((𝐸𝑆) − 𝐼) = 𝑋𝑋 = ((𝐸𝑆) − 𝐼))
147145, 146bitrdi 290 . . . 4 (𝜑 → ((𝑋𝐸) = (-𝑆𝐼) ↔ 𝑋 = ((𝐸𝑆) − 𝐼)))
148138, 147orbi12d 919 . . 3 (𝜑 → (((𝑋𝐸) = (-𝑆 + 𝐼) ∨ (𝑋𝐸) = (-𝑆𝐼)) ↔ (𝑋 = ((𝐸𝑆) + 𝐼) ∨ 𝑋 = ((𝐸𝑆) − 𝐼))))
14934, 122addcld 10876 . . . . . . 7 (𝜑 → (𝑆 + 𝐽) ∈ ℂ)
1508, 24, 149subaddd 11231 . . . . . 6 (𝜑 → ((𝑋𝐸) = (𝑆 + 𝐽) ↔ (𝐸 + (𝑆 + 𝐽)) = 𝑋))
15124, 34, 122addassd 10879 . . . . . . 7 (𝜑 → ((𝐸 + 𝑆) + 𝐽) = (𝐸 + (𝑆 + 𝐽)))
152151eqeq1d 2740 . . . . . 6 (𝜑 → (((𝐸 + 𝑆) + 𝐽) = 𝑋 ↔ (𝐸 + (𝑆 + 𝐽)) = 𝑋))
153150, 152bitr4d 285 . . . . 5 (𝜑 → ((𝑋𝐸) = (𝑆 + 𝐽) ↔ ((𝐸 + 𝑆) + 𝐽) = 𝑋))
154 eqcom 2745 . . . . 5 (((𝐸 + 𝑆) + 𝐽) = 𝑋𝑋 = ((𝐸 + 𝑆) + 𝐽))
155153, 154bitrdi 290 . . . 4 (𝜑 → ((𝑋𝐸) = (𝑆 + 𝐽) ↔ 𝑋 = ((𝐸 + 𝑆) + 𝐽)))
15634, 122subcld 11213 . . . . . . 7 (𝜑 → (𝑆𝐽) ∈ ℂ)
1578, 24, 156subaddd 11231 . . . . . 6 (𝜑 → ((𝑋𝐸) = (𝑆𝐽) ↔ (𝐸 + (𝑆𝐽)) = 𝑋))
15824, 34, 122addsubassd 11233 . . . . . . 7 (𝜑 → ((𝐸 + 𝑆) − 𝐽) = (𝐸 + (𝑆𝐽)))
159158eqeq1d 2740 . . . . . 6 (𝜑 → (((𝐸 + 𝑆) − 𝐽) = 𝑋 ↔ (𝐸 + (𝑆𝐽)) = 𝑋))
160157, 159bitr4d 285 . . . . 5 (𝜑 → ((𝑋𝐸) = (𝑆𝐽) ↔ ((𝐸 + 𝑆) − 𝐽) = 𝑋))
161 eqcom 2745 . . . . 5 (((𝐸 + 𝑆) − 𝐽) = 𝑋𝑋 = ((𝐸 + 𝑆) − 𝐽))
162160, 161bitrdi 290 . . . 4 (𝜑 → ((𝑋𝐸) = (𝑆𝐽) ↔ 𝑋 = ((𝐸 + 𝑆) − 𝐽)))
163155, 162orbi12d 919 . . 3 (𝜑 → (((𝑋𝐸) = (𝑆 + 𝐽) ∨ (𝑋𝐸) = (𝑆𝐽)) ↔ (𝑋 = ((𝐸 + 𝑆) + 𝐽) ∨ 𝑋 = ((𝐸 + 𝑆) − 𝐽))))
164148, 163orbi12d 919 . 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 847   = wceq 1543  wcel 2111  wne 2941  wrex 3063  cfv 6397  (class class class)co 7231  cc 10751  0cc0 10753  1c1 10754   + caddc 10756   · cmul 10758  cmin 11086  -cneg 11087   / cdiv 11513  cn 11854  2c2 11909  3c3 11910  4c4 11911  5c5 11912  6c6 11913  7c7 11914  8c8 11915  9c9 11916  0cn0 12114  cz 12200  cdc 12317  cexp 13659  csqrt 14820  𝑐ccxp 25468
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709  ax-rep 5193  ax-sep 5206  ax-nul 5213  ax-pow 5272  ax-pr 5336  ax-un 7541  ax-inf2 9280  ax-cnex 10809  ax-resscn 10810  ax-1cn 10811  ax-icn 10812  ax-addcl 10813  ax-addrcl 10814  ax-mulcl 10815  ax-mulrcl 10816  ax-mulcom 10817  ax-addass 10818  ax-mulass 10819  ax-distr 10820  ax-i2m1 10821  ax-1ne0 10822  ax-1rid 10823  ax-rnegex 10824  ax-rrecex 10825  ax-cnre 10826  ax-pre-lttri 10827  ax-pre-lttrn 10828  ax-pre-ltadd 10829  ax-pre-mulgt0 10830  ax-pre-sup 10831  ax-addf 10832  ax-mulf 10833
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2072  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3067  df-rex 3068  df-reu 3069  df-rmo 3070  df-rab 3071  df-v 3422  df-sbc 3709  df-csb 3826  df-dif 3883  df-un 3885  df-in 3887  df-ss 3897  df-pss 3899  df-nul 4252  df-if 4454  df-pw 4529  df-sn 4556  df-pr 4558  df-tp 4560  df-op 4562  df-uni 4834  df-int 4874  df-iun 4920  df-iin 4921  df-br 5068  df-opab 5130  df-mpt 5150  df-tr 5176  df-id 5469  df-eprel 5474  df-po 5482  df-so 5483  df-fr 5523  df-se 5524  df-we 5525  df-xp 5571  df-rel 5572  df-cnv 5573  df-co 5574  df-dm 5575  df-rn 5576  df-res 5577  df-ima 5578  df-pred 6175  df-ord 6233  df-on 6234  df-lim 6235  df-suc 6236  df-iota 6355  df-fun 6399  df-fn 6400  df-f 6401  df-f1 6402  df-fo 6403  df-f1o 6404  df-fv 6405  df-isom 6406  df-riota 7188  df-ov 7234  df-oprab 7235  df-mpo 7236  df-of 7487  df-om 7663  df-1st 7779  df-2nd 7780  df-supp 7924  df-wrecs 8067  df-recs 8128  df-rdg 8166  df-1o 8222  df-2o 8223  df-er 8411  df-map 8530  df-pm 8531  df-ixp 8599  df-en 8647  df-dom 8648  df-sdom 8649  df-fin 8650  df-fsupp 9010  df-fi 9051  df-sup 9082  df-inf 9083  df-oi 9150  df-card 9579  df-pnf 10893  df-mnf 10894  df-xr 10895  df-ltxr 10896  df-le 10897  df-sub 11088  df-neg 11089  df-div 11514  df-nn 11855  df-2 11917  df-3 11918  df-4 11919  df-5 11920  df-6 11921  df-7 11922  df-8 11923  df-9 11924  df-n0 12115  df-z 12201  df-dec 12318  df-uz 12463  df-q 12569  df-rp 12611  df-xneg 12728  df-xadd 12729  df-xmul 12730  df-ioo 12963  df-ioc 12964  df-ico 12965  df-icc 12966  df-fz 13120  df-fzo 13263  df-fl 13391  df-mod 13467  df-seq 13599  df-exp 13660  df-fac 13864  df-bc 13893  df-hash 13921  df-shft 14654  df-cj 14686  df-re 14687  df-im 14688  df-sqrt 14822  df-abs 14823  df-limsup 15056  df-clim 15073  df-rlim 15074  df-sum 15274  df-ef 15653  df-sin 15655  df-cos 15656  df-pi 15658  df-dvds 15840  df-struct 16724  df-sets 16741  df-slot 16759  df-ndx 16769  df-base 16785  df-ress 16809  df-plusg 16839  df-mulr 16840  df-starv 16841  df-sca 16842  df-vsca 16843  df-ip 16844  df-tset 16845  df-ple 16846  df-ds 16848  df-unif 16849  df-hom 16850  df-cco 16851  df-rest 16951  df-topn 16952  df-0g 16970  df-gsum 16971  df-topgen 16972  df-pt 16973  df-prds 16976  df-xrs 17031  df-qtop 17036  df-imas 17037  df-xps 17039  df-mre 17113  df-mrc 17114  df-acs 17116  df-mgm 18138  df-sgrp 18187  df-mnd 18198  df-submnd 18243  df-mulg 18513  df-cntz 18735  df-cmn 19196  df-psmet 20379  df-xmet 20380  df-met 20381  df-bl 20382  df-mopn 20383  df-fbas 20384  df-fg 20385  df-cnfld 20388  df-top 21815  df-topon 21832  df-topsp 21854  df-bases 21867  df-cld 21940  df-ntr 21941  df-cls 21942  df-nei 22019  df-lp 22057  df-perf 22058  df-cn 22148  df-cnp 22149  df-haus 22236  df-tx 22483  df-hmeo 22676  df-fil 22767  df-fm 22859  df-flim 22860  df-flf 22861  df-xms 23242  df-ms 23243  df-tms 23244  df-cncf 23799  df-limc 24787  df-dv 24788  df-log 25469  df-cxp 25470
This theorem is referenced by:  quartfull  32863
  Copyright terms: Public domain W3C validator