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

Theorem mcubic 24865
Description: Solutions to a monic cubic equation, a special case of cubic 24867. (Contributed by Mario Carneiro, 24-Apr-2015.)
Hypotheses
Ref Expression
mcubic.b (𝜑𝐵 ∈ ℂ)
mcubic.c (𝜑𝐶 ∈ ℂ)
mcubic.d (𝜑𝐷 ∈ ℂ)
mcubic.x (𝜑𝑋 ∈ ℂ)
mcubic.t (𝜑𝑇 ∈ ℂ)
mcubic.3 (𝜑 → (𝑇↑3) = ((𝑁 + 𝐺) / 2))
mcubic.g (𝜑𝐺 ∈ ℂ)
mcubic.2 (𝜑 → (𝐺↑2) = ((𝑁↑2) − (4 · (𝑀↑3))))
mcubic.m (𝜑𝑀 = ((𝐵↑2) − (3 · 𝐶)))
mcubic.n (𝜑𝑁 = (((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) + (27 · 𝐷)))
mcubic.0 (𝜑𝑇 ≠ 0)
Assertion
Ref Expression
mcubic (𝜑 → ((((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((𝐶 · 𝑋) + 𝐷)) = 0 ↔ ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3))))
Distinct variable groups:   𝐵,𝑟   𝑀,𝑟   𝑁,𝑟   𝜑,𝑟   𝑇,𝑟   𝑋,𝑟
Allowed substitution hints:   𝐶(𝑟)   𝐷(𝑟)   𝐺(𝑟)

Proof of Theorem mcubic
StepHypRef Expression
1 mcubic.m . . . . . 6 (𝜑𝑀 = ((𝐵↑2) − (3 · 𝐶)))
2 mcubic.b . . . . . . . 8 (𝜑𝐵 ∈ ℂ)
32sqcld 13213 . . . . . . 7 (𝜑 → (𝐵↑2) ∈ ℂ)
4 3cn 11353 . . . . . . . 8 3 ∈ ℂ
5 mcubic.c . . . . . . . 8 (𝜑𝐶 ∈ ℂ)
6 mulcl 10273 . . . . . . . 8 ((3 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (3 · 𝐶) ∈ ℂ)
74, 5, 6sylancr 581 . . . . . . 7 (𝜑 → (3 · 𝐶) ∈ ℂ)
83, 7subcld 10646 . . . . . 6 (𝜑 → ((𝐵↑2) − (3 · 𝐶)) ∈ ℂ)
91, 8eqeltrd 2844 . . . . 5 (𝜑𝑀 ∈ ℂ)
104a1i 11 . . . . 5 (𝜑 → 3 ∈ ℂ)
11 3ne0 11385 . . . . . 6 3 ≠ 0
1211a1i 11 . . . . 5 (𝜑 → 3 ≠ 0)
139, 10, 12divcld 11055 . . . 4 (𝜑 → (𝑀 / 3) ∈ ℂ)
1413negcld 10633 . . 3 (𝜑 → -(𝑀 / 3) ∈ ℂ)
15 mcubic.n . . . . 5 (𝜑𝑁 = (((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) + (27 · 𝐷)))
16 2cn 11347 . . . . . . . 8 2 ∈ ℂ
17 3nn0 11558 . . . . . . . . 9 3 ∈ ℕ0
18 expcl 13085 . . . . . . . . 9 ((𝐵 ∈ ℂ ∧ 3 ∈ ℕ0) → (𝐵↑3) ∈ ℂ)
192, 17, 18sylancl 580 . . . . . . . 8 (𝜑 → (𝐵↑3) ∈ ℂ)
20 mulcl 10273 . . . . . . . 8 ((2 ∈ ℂ ∧ (𝐵↑3) ∈ ℂ) → (2 · (𝐵↑3)) ∈ ℂ)
2116, 19, 20sylancr 581 . . . . . . 7 (𝜑 → (2 · (𝐵↑3)) ∈ ℂ)
22 9cn 11378 . . . . . . . 8 9 ∈ ℂ
232, 5mulcld 10314 . . . . . . . 8 (𝜑 → (𝐵 · 𝐶) ∈ ℂ)
24 mulcl 10273 . . . . . . . 8 ((9 ∈ ℂ ∧ (𝐵 · 𝐶) ∈ ℂ) → (9 · (𝐵 · 𝐶)) ∈ ℂ)
2522, 23, 24sylancr 581 . . . . . . 7 (𝜑 → (9 · (𝐵 · 𝐶)) ∈ ℂ)
2621, 25subcld 10646 . . . . . 6 (𝜑 → ((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) ∈ ℂ)
27 2nn0 11557 . . . . . . . . 9 2 ∈ ℕ0
28 7nn 11368 . . . . . . . . 9 7 ∈ ℕ
2927, 28decnncl 11761 . . . . . . . 8 27 ∈ ℕ
3029nncni 11285 . . . . . . 7 27 ∈ ℂ
31 mcubic.d . . . . . . 7 (𝜑𝐷 ∈ ℂ)
32 mulcl 10273 . . . . . . 7 ((27 ∈ ℂ ∧ 𝐷 ∈ ℂ) → (27 · 𝐷) ∈ ℂ)
3330, 31, 32sylancr 581 . . . . . 6 (𝜑 → (27 · 𝐷) ∈ ℂ)
3426, 33addcld 10313 . . . . 5 (𝜑 → (((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) + (27 · 𝐷)) ∈ ℂ)
3515, 34eqeltrd 2844 . . . 4 (𝜑𝑁 ∈ ℂ)
3630a1i 11 . . . 4 (𝜑27 ∈ ℂ)
3729nnne0i 11312 . . . . 5 27 ≠ 0
3837a1i 11 . . . 4 (𝜑27 ≠ 0)
3935, 36, 38divcld 11055 . . 3 (𝜑 → (𝑁 / 27) ∈ ℂ)
40 mcubic.x . . . 4 (𝜑𝑋 ∈ ℂ)
412, 10, 12divcld 11055 . . . 4 (𝜑 → (𝐵 / 3) ∈ ℂ)
4240, 41addcld 10313 . . 3 (𝜑 → (𝑋 + (𝐵 / 3)) ∈ ℂ)
43 mcubic.t . . . . 5 (𝜑𝑇 ∈ ℂ)
4443, 10, 12divcld 11055 . . . 4 (𝜑 → (𝑇 / 3) ∈ ℂ)
4544negcld 10633 . . 3 (𝜑 → -(𝑇 / 3) ∈ ℂ)
46 3nn 11351 . . . . . 6 3 ∈ ℕ
4746a1i 11 . . . . 5 (𝜑 → 3 ∈ ℕ)
48 2nn 11345 . . . . . . 7 2 ∈ ℕ
49 1nn0 11556 . . . . . . 7 1 ∈ ℕ0
50 1nn 11287 . . . . . . 7 1 ∈ ℕ
51 2t1e2 11441 . . . . . . . . 9 (2 · 1) = 2
5251oveq1i 6852 . . . . . . . 8 ((2 · 1) + 1) = (2 + 1)
53 2p1e3 11421 . . . . . . . 8 (2 + 1) = 3
5452, 53eqtri 2787 . . . . . . 7 ((2 · 1) + 1) = 3
55 1lt2 11449 . . . . . . 7 1 < 2
5648, 49, 50, 54, 55ndvdsi 15419 . . . . . 6 ¬ 2 ∥ 3
5756a1i 11 . . . . 5 (𝜑 → ¬ 2 ∥ 3)
58 oexpneg 15353 . . . . 5 (((𝑇 / 3) ∈ ℂ ∧ 3 ∈ ℕ ∧ ¬ 2 ∥ 3) → (-(𝑇 / 3)↑3) = -((𝑇 / 3)↑3))
5944, 47, 57, 58syl3anc 1490 . . . 4 (𝜑 → (-(𝑇 / 3)↑3) = -((𝑇 / 3)↑3))
6017a1i 11 . . . . . . 7 (𝜑 → 3 ∈ ℕ0)
6143, 10, 12, 60expdivd 13229 . . . . . 6 (𝜑 → ((𝑇 / 3)↑3) = ((𝑇↑3) / (3↑3)))
62 mcubic.3 . . . . . . 7 (𝜑 → (𝑇↑3) = ((𝑁 + 𝐺) / 2))
63 3exp3 16074 . . . . . . . 8 (3↑3) = 27
6463a1i 11 . . . . . . 7 (𝜑 → (3↑3) = 27)
6562, 64oveq12d 6860 . . . . . 6 (𝜑 → ((𝑇↑3) / (3↑3)) = (((𝑁 + 𝐺) / 2) / 27))
66 mcubic.g . . . . . . . . 9 (𝜑𝐺 ∈ ℂ)
6735, 66addcld 10313 . . . . . . . 8 (𝜑 → (𝑁 + 𝐺) ∈ ℂ)
68 2cnd 11350 . . . . . . . 8 (𝜑 → 2 ∈ ℂ)
69 2ne0 11383 . . . . . . . . 9 2 ≠ 0
7069a1i 11 . . . . . . . 8 (𝜑 → 2 ≠ 0)
7167, 68, 36, 70, 38divdiv32d 11080 . . . . . . 7 (𝜑 → (((𝑁 + 𝐺) / 2) / 27) = (((𝑁 + 𝐺) / 27) / 2))
7235, 66addcomd 10492 . . . . . . . . . 10 (𝜑 → (𝑁 + 𝐺) = (𝐺 + 𝑁))
7372oveq1d 6857 . . . . . . . . 9 (𝜑 → ((𝑁 + 𝐺) / 27) = ((𝐺 + 𝑁) / 27))
7466, 35, 36, 38divdird 11093 . . . . . . . . 9 (𝜑 → ((𝐺 + 𝑁) / 27) = ((𝐺 / 27) + (𝑁 / 27)))
7573, 74eqtrd 2799 . . . . . . . 8 (𝜑 → ((𝑁 + 𝐺) / 27) = ((𝐺 / 27) + (𝑁 / 27)))
7675oveq1d 6857 . . . . . . 7 (𝜑 → (((𝑁 + 𝐺) / 27) / 2) = (((𝐺 / 27) + (𝑁 / 27)) / 2))
7766, 36, 38divcld 11055 . . . . . . . 8 (𝜑 → (𝐺 / 27) ∈ ℂ)
7877, 39, 68, 70divdird 11093 . . . . . . 7 (𝜑 → (((𝐺 / 27) + (𝑁 / 27)) / 2) = (((𝐺 / 27) / 2) + ((𝑁 / 27) / 2)))
7971, 76, 783eqtrd 2803 . . . . . 6 (𝜑 → (((𝑁 + 𝐺) / 2) / 27) = (((𝐺 / 27) / 2) + ((𝑁 / 27) / 2)))
8061, 65, 793eqtrd 2803 . . . . 5 (𝜑 → ((𝑇 / 3)↑3) = (((𝐺 / 27) / 2) + ((𝑁 / 27) / 2)))
8180negeqd 10529 . . . 4 (𝜑 → -((𝑇 / 3)↑3) = -(((𝐺 / 27) / 2) + ((𝑁 / 27) / 2)))
8277halfcld 11523 . . . . 5 (𝜑 → ((𝐺 / 27) / 2) ∈ ℂ)
8339halfcld 11523 . . . . 5 (𝜑 → ((𝑁 / 27) / 2) ∈ ℂ)
8482, 83negdi2d 10660 . . . 4 (𝜑 → -(((𝐺 / 27) / 2) + ((𝑁 / 27) / 2)) = (-((𝐺 / 27) / 2) − ((𝑁 / 27) / 2)))
8559, 81, 843eqtrd 2803 . . 3 (𝜑 → (-(𝑇 / 3)↑3) = (-((𝐺 / 27) / 2) − ((𝑁 / 27) / 2)))
8682negcld 10633 . . 3 (𝜑 → -((𝐺 / 27) / 2) ∈ ℂ)
87 sqneg 13130 . . . . 5 (((𝐺 / 27) / 2) ∈ ℂ → (-((𝐺 / 27) / 2)↑2) = (((𝐺 / 27) / 2)↑2))
8882, 87syl 17 . . . 4 (𝜑 → (-((𝐺 / 27) / 2)↑2) = (((𝐺 / 27) / 2)↑2))
8977, 68, 70sqdivd 13228 . . . 4 (𝜑 → (((𝐺 / 27) / 2)↑2) = (((𝐺 / 27)↑2) / (2↑2)))
9039, 68, 70sqdivd 13228 . . . . . . . 8 (𝜑 → (((𝑁 / 27) / 2)↑2) = (((𝑁 / 27)↑2) / (2↑2)))
9135, 36, 38sqdivd 13228 . . . . . . . . 9 (𝜑 → ((𝑁 / 27)↑2) = ((𝑁↑2) / (27↑2)))
9291oveq1d 6857 . . . . . . . 8 (𝜑 → (((𝑁 / 27)↑2) / (2↑2)) = (((𝑁↑2) / (27↑2)) / (2↑2)))
9390, 92eqtr2d 2800 . . . . . . 7 (𝜑 → (((𝑁↑2) / (27↑2)) / (2↑2)) = (((𝑁 / 27) / 2)↑2))
94 4cn 11358 . . . . . . . . . . . 12 4 ∈ ℂ
9594a1i 11 . . . . . . . . . . 11 (𝜑 → 4 ∈ ℂ)
96 expcl 13085 . . . . . . . . . . . 12 ((𝑀 ∈ ℂ ∧ 3 ∈ ℕ0) → (𝑀↑3) ∈ ℂ)
979, 17, 96sylancl 580 . . . . . . . . . . 11 (𝜑 → (𝑀↑3) ∈ ℂ)
9830sqcli 13151 . . . . . . . . . . . 12 (27↑2) ∈ ℂ
9998a1i 11 . . . . . . . . . . 11 (𝜑 → (27↑2) ∈ ℂ)
100 sqne0 13137 . . . . . . . . . . . . 13 (27 ∈ ℂ → ((27↑2) ≠ 0 ↔ 27 ≠ 0))
10136, 100syl 17 . . . . . . . . . . . 12 (𝜑 → ((27↑2) ≠ 0 ↔ 27 ≠ 0))
10238, 101mpbird 248 . . . . . . . . . . 11 (𝜑 → (27↑2) ≠ 0)
10395, 97, 99, 102divassd 11090 . . . . . . . . . 10 (𝜑 → ((4 · (𝑀↑3)) / (27↑2)) = (4 · ((𝑀↑3) / (27↑2))))
10422a1i 11 . . . . . . . . . . . . 13 (𝜑 → 9 ∈ ℂ)
105 9nn 11376 . . . . . . . . . . . . . . 15 9 ∈ ℕ
106105nnne0i 11312 . . . . . . . . . . . . . 14 9 ≠ 0
107106a1i 11 . . . . . . . . . . . . 13 (𝜑 → 9 ≠ 0)
1089, 104, 107, 60expdivd 13229 . . . . . . . . . . . 12 (𝜑 → ((𝑀 / 9)↑3) = ((𝑀↑3) / (9↑3)))
10916, 4mulcomi 10302 . . . . . . . . . . . . . . . 16 (2 · 3) = (3 · 2)
110109oveq2i 6853 . . . . . . . . . . . . . . 15 (3↑(2 · 3)) = (3↑(3 · 2))
111 expmul 13112 . . . . . . . . . . . . . . . 16 ((3 ∈ ℂ ∧ 2 ∈ ℕ0 ∧ 3 ∈ ℕ0) → (3↑(2 · 3)) = ((3↑2)↑3))
1124, 27, 17, 111mp3an 1585 . . . . . . . . . . . . . . 15 (3↑(2 · 3)) = ((3↑2)↑3)
113 expmul 13112 . . . . . . . . . . . . . . . 16 ((3 ∈ ℂ ∧ 3 ∈ ℕ0 ∧ 2 ∈ ℕ0) → (3↑(3 · 2)) = ((3↑3)↑2))
1144, 17, 27, 113mp3an 1585 . . . . . . . . . . . . . . 15 (3↑(3 · 2)) = ((3↑3)↑2)
115110, 112, 1143eqtr3i 2795 . . . . . . . . . . . . . 14 ((3↑2)↑3) = ((3↑3)↑2)
116 sq3 13168 . . . . . . . . . . . . . . 15 (3↑2) = 9
117116oveq1i 6852 . . . . . . . . . . . . . 14 ((3↑2)↑3) = (9↑3)
11863oveq1i 6852 . . . . . . . . . . . . . 14 ((3↑3)↑2) = (27↑2)
119115, 117, 1183eqtr3i 2795 . . . . . . . . . . . . 13 (9↑3) = (27↑2)
120119oveq2i 6853 . . . . . . . . . . . 12 ((𝑀↑3) / (9↑3)) = ((𝑀↑3) / (27↑2))
121108, 120syl6eq 2815 . . . . . . . . . . 11 (𝜑 → ((𝑀 / 9)↑3) = ((𝑀↑3) / (27↑2)))
122121oveq2d 6858 . . . . . . . . . 10 (𝜑 → (4 · ((𝑀 / 9)↑3)) = (4 · ((𝑀↑3) / (27↑2))))
123103, 122eqtr4d 2802 . . . . . . . . 9 (𝜑 → ((4 · (𝑀↑3)) / (27↑2)) = (4 · ((𝑀 / 9)↑3)))
124123oveq1d 6857 . . . . . . . 8 (𝜑 → (((4 · (𝑀↑3)) / (27↑2)) / (2↑2)) = ((4 · ((𝑀 / 9)↑3)) / (2↑2)))
125 sq2 13167 . . . . . . . . . 10 (2↑2) = 4
126125oveq2i 6853 . . . . . . . . 9 ((4 · ((𝑀 / 9)↑3)) / (2↑2)) = ((4 · ((𝑀 / 9)↑3)) / 4)
1279, 104, 107divcld 11055 . . . . . . . . . . 11 (𝜑 → (𝑀 / 9) ∈ ℂ)
128 expcl 13085 . . . . . . . . . . 11 (((𝑀 / 9) ∈ ℂ ∧ 3 ∈ ℕ0) → ((𝑀 / 9)↑3) ∈ ℂ)
129127, 17, 128sylancl 580 . . . . . . . . . 10 (𝜑 → ((𝑀 / 9)↑3) ∈ ℂ)
130 4ne0 11387 . . . . . . . . . . 11 4 ≠ 0
131130a1i 11 . . . . . . . . . 10 (𝜑 → 4 ≠ 0)
132129, 95, 131divcan3d 11060 . . . . . . . . 9 (𝜑 → ((4 · ((𝑀 / 9)↑3)) / 4) = ((𝑀 / 9)↑3))
133126, 132syl5eq 2811 . . . . . . . 8 (𝜑 → ((4 · ((𝑀 / 9)↑3)) / (2↑2)) = ((𝑀 / 9)↑3))
134124, 133eqtrd 2799 . . . . . . 7 (𝜑 → (((4 · (𝑀↑3)) / (27↑2)) / (2↑2)) = ((𝑀 / 9)↑3))
13593, 134oveq12d 6860 . . . . . 6 (𝜑 → ((((𝑁↑2) / (27↑2)) / (2↑2)) − (((4 · (𝑀↑3)) / (27↑2)) / (2↑2))) = ((((𝑁 / 27) / 2)↑2) − ((𝑀 / 9)↑3)))
13635sqcld 13213 . . . . . . . 8 (𝜑 → (𝑁↑2) ∈ ℂ)
137136, 99, 102divcld 11055 . . . . . . 7 (𝜑 → ((𝑁↑2) / (27↑2)) ∈ ℂ)
138 mulcl 10273 . . . . . . . . 9 ((4 ∈ ℂ ∧ (𝑀↑3) ∈ ℂ) → (4 · (𝑀↑3)) ∈ ℂ)
13994, 97, 138sylancr 581 . . . . . . . 8 (𝜑 → (4 · (𝑀↑3)) ∈ ℂ)
140139, 99, 102divcld 11055 . . . . . . 7 (𝜑 → ((4 · (𝑀↑3)) / (27↑2)) ∈ ℂ)
14116sqcli 13151 . . . . . . . 8 (2↑2) ∈ ℂ
142141a1i 11 . . . . . . 7 (𝜑 → (2↑2) ∈ ℂ)
143125, 130eqnetri 3007 . . . . . . . 8 (2↑2) ≠ 0
144143a1i 11 . . . . . . 7 (𝜑 → (2↑2) ≠ 0)
145137, 140, 142, 144divsubdird 11094 . . . . . 6 (𝜑 → ((((𝑁↑2) / (27↑2)) − ((4 · (𝑀↑3)) / (27↑2))) / (2↑2)) = ((((𝑁↑2) / (27↑2)) / (2↑2)) − (((4 · (𝑀↑3)) / (27↑2)) / (2↑2))))
14683sqcld 13213 . . . . . . 7 (𝜑 → (((𝑁 / 27) / 2)↑2) ∈ ℂ)
147146, 129negsubd 10652 . . . . . 6 (𝜑 → ((((𝑁 / 27) / 2)↑2) + -((𝑀 / 9)↑3)) = ((((𝑁 / 27) / 2)↑2) − ((𝑀 / 9)↑3)))
148135, 145, 1473eqtr4d 2809 . . . . 5 (𝜑 → ((((𝑁↑2) / (27↑2)) − ((4 · (𝑀↑3)) / (27↑2))) / (2↑2)) = ((((𝑁 / 27) / 2)↑2) + -((𝑀 / 9)↑3)))
14966, 36, 38sqdivd 13228 . . . . . . 7 (𝜑 → ((𝐺 / 27)↑2) = ((𝐺↑2) / (27↑2)))
150 mcubic.2 . . . . . . . 8 (𝜑 → (𝐺↑2) = ((𝑁↑2) − (4 · (𝑀↑3))))
151150oveq1d 6857 . . . . . . 7 (𝜑 → ((𝐺↑2) / (27↑2)) = (((𝑁↑2) − (4 · (𝑀↑3))) / (27↑2)))
152136, 139, 99, 102divsubdird 11094 . . . . . . 7 (𝜑 → (((𝑁↑2) − (4 · (𝑀↑3))) / (27↑2)) = (((𝑁↑2) / (27↑2)) − ((4 · (𝑀↑3)) / (27↑2))))
153149, 151, 1523eqtrd 2803 . . . . . 6 (𝜑 → ((𝐺 / 27)↑2) = (((𝑁↑2) / (27↑2)) − ((4 · (𝑀↑3)) / (27↑2))))
154153oveq1d 6857 . . . . 5 (𝜑 → (((𝐺 / 27)↑2) / (2↑2)) = ((((𝑁↑2) / (27↑2)) − ((4 · (𝑀↑3)) / (27↑2))) / (2↑2)))
155 oexpneg 15353 . . . . . . 7 (((𝑀 / 9) ∈ ℂ ∧ 3 ∈ ℕ ∧ ¬ 2 ∥ 3) → (-(𝑀 / 9)↑3) = -((𝑀 / 9)↑3))
156127, 47, 57, 155syl3anc 1490 . . . . . 6 (𝜑 → (-(𝑀 / 9)↑3) = -((𝑀 / 9)↑3))
157156oveq2d 6858 . . . . 5 (𝜑 → ((((𝑁 / 27) / 2)↑2) + (-(𝑀 / 9)↑3)) = ((((𝑁 / 27) / 2)↑2) + -((𝑀 / 9)↑3)))
158148, 154, 1573eqtr4d 2809 . . . 4 (𝜑 → (((𝐺 / 27)↑2) / (2↑2)) = ((((𝑁 / 27) / 2)↑2) + (-(𝑀 / 9)↑3)))
15988, 89, 1583eqtrd 2803 . . 3 (𝜑 → (-((𝐺 / 27) / 2)↑2) = ((((𝑁 / 27) / 2)↑2) + (-(𝑀 / 9)↑3)))
1609, 10, 10, 12, 12divdiv1d 11086 . . . . . 6 (𝜑 → ((𝑀 / 3) / 3) = (𝑀 / (3 · 3)))
161 3t3e9 11445 . . . . . . 7 (3 · 3) = 9
162161oveq2i 6853 . . . . . 6 (𝑀 / (3 · 3)) = (𝑀 / 9)
163160, 162syl6eq 2815 . . . . 5 (𝜑 → ((𝑀 / 3) / 3) = (𝑀 / 9))
164163negeqd 10529 . . . 4 (𝜑 → -((𝑀 / 3) / 3) = -(𝑀 / 9))
16513, 10, 12divnegd 11068 . . . 4 (𝜑 → -((𝑀 / 3) / 3) = (-(𝑀 / 3) / 3))
166164, 165eqtr3d 2801 . . 3 (𝜑 → -(𝑀 / 9) = (-(𝑀 / 3) / 3))
167 eqidd 2766 . . 3 (𝜑 → ((𝑁 / 27) / 2) = ((𝑁 / 27) / 2))
168 mcubic.0 . . . . 5 (𝜑𝑇 ≠ 0)
16943, 10, 168, 12divne0d 11071 . . . 4 (𝜑 → (𝑇 / 3) ≠ 0)
17044, 169negne0d 10644 . . 3 (𝜑 → -(𝑇 / 3) ≠ 0)
17114, 39, 42, 45, 85, 86, 159, 166, 167, 170dcubic 24864 . 2 (𝜑 → ((((𝑋 + (𝐵 / 3))↑3) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27))) = 0 ↔ ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ (𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))))))
172 binom3 13192 . . . . . . 7 ((𝑋 ∈ ℂ ∧ (𝐵 / 3) ∈ ℂ) → ((𝑋 + (𝐵 / 3))↑3) = (((𝑋↑3) + (3 · ((𝑋↑2) · (𝐵 / 3)))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))))
17340, 41, 172syl2anc 579 . . . . . 6 (𝜑 → ((𝑋 + (𝐵 / 3))↑3) = (((𝑋↑3) + (3 · ((𝑋↑2) · (𝐵 / 3)))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))))
17440sqcld 13213 . . . . . . . . . 10 (𝜑 → (𝑋↑2) ∈ ℂ)
17510, 174, 41mul12d 10499 . . . . . . . . 9 (𝜑 → (3 · ((𝑋↑2) · (𝐵 / 3))) = ((𝑋↑2) · (3 · (𝐵 / 3))))
1762, 10, 12divcan2d 11057 . . . . . . . . . 10 (𝜑 → (3 · (𝐵 / 3)) = 𝐵)
177176oveq2d 6858 . . . . . . . . 9 (𝜑 → ((𝑋↑2) · (3 · (𝐵 / 3))) = ((𝑋↑2) · 𝐵))
178174, 2mulcomd 10315 . . . . . . . . 9 (𝜑 → ((𝑋↑2) · 𝐵) = (𝐵 · (𝑋↑2)))
179175, 177, 1783eqtrd 2803 . . . . . . . 8 (𝜑 → (3 · ((𝑋↑2) · (𝐵 / 3))) = (𝐵 · (𝑋↑2)))
180179oveq2d 6858 . . . . . . 7 (𝜑 → ((𝑋↑3) + (3 · ((𝑋↑2) · (𝐵 / 3)))) = ((𝑋↑3) + (𝐵 · (𝑋↑2))))
181180oveq1d 6857 . . . . . 6 (𝜑 → (((𝑋↑3) + (3 · ((𝑋↑2) · (𝐵 / 3)))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))) = (((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))))
182173, 181eqtrd 2799 . . . . 5 (𝜑 → ((𝑋 + (𝐵 / 3))↑3) = (((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))))
183182oveq1d 6857 . . . 4 (𝜑 → (((𝑋 + (𝐵 / 3))↑3) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27))) = ((((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27))))
184 expcl 13085 . . . . . . 7 ((𝑋 ∈ ℂ ∧ 3 ∈ ℕ0) → (𝑋↑3) ∈ ℂ)
18540, 17, 184sylancl 580 . . . . . 6 (𝜑 → (𝑋↑3) ∈ ℂ)
1862, 174mulcld 10314 . . . . . 6 (𝜑 → (𝐵 · (𝑋↑2)) ∈ ℂ)
187185, 186addcld 10313 . . . . 5 (𝜑 → ((𝑋↑3) + (𝐵 · (𝑋↑2))) ∈ ℂ)
18841sqcld 13213 . . . . . . . 8 (𝜑 → ((𝐵 / 3)↑2) ∈ ℂ)
18940, 188mulcld 10314 . . . . . . 7 (𝜑 → (𝑋 · ((𝐵 / 3)↑2)) ∈ ℂ)
19010, 189mulcld 10314 . . . . . 6 (𝜑 → (3 · (𝑋 · ((𝐵 / 3)↑2))) ∈ ℂ)
191 expcl 13085 . . . . . . 7 (((𝐵 / 3) ∈ ℂ ∧ 3 ∈ ℕ0) → ((𝐵 / 3)↑3) ∈ ℂ)
19241, 17, 191sylancl 580 . . . . . 6 (𝜑 → ((𝐵 / 3)↑3) ∈ ℂ)
193190, 192addcld 10313 . . . . 5 (𝜑 → ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) ∈ ℂ)
19414, 42mulcld 10314 . . . . . 6 (𝜑 → (-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) ∈ ℂ)
195194, 39addcld 10313 . . . . 5 (𝜑 → ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27)) ∈ ℂ)
196187, 193, 195addassd 10316 . . . 4 (𝜑 → ((((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27))) = (((𝑋↑3) + (𝐵 · (𝑋↑2))) + (((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27)))))
19714, 40, 41adddid 10318 . . . . . . . . . 10 (𝜑 → (-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) = ((-(𝑀 / 3) · 𝑋) + (-(𝑀 / 3) · (𝐵 / 3))))
198197oveq1d 6857 . . . . . . . . 9 (𝜑 → ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27)) = (((-(𝑀 / 3) · 𝑋) + (-(𝑀 / 3) · (𝐵 / 3))) + (𝑁 / 27)))
19914, 40mulcld 10314 . . . . . . . . . 10 (𝜑 → (-(𝑀 / 3) · 𝑋) ∈ ℂ)
20014, 41mulcld 10314 . . . . . . . . . 10 (𝜑 → (-(𝑀 / 3) · (𝐵 / 3)) ∈ ℂ)
201199, 200, 39addassd 10316 . . . . . . . . 9 (𝜑 → (((-(𝑀 / 3) · 𝑋) + (-(𝑀 / 3) · (𝐵 / 3))) + (𝑁 / 27)) = ((-(𝑀 / 3) · 𝑋) + ((-(𝑀 / 3) · (𝐵 / 3)) + (𝑁 / 27))))
2021oveq1d 6857 . . . . . . . . . . . . . . 15 (𝜑 → (𝑀 / 3) = (((𝐵↑2) − (3 · 𝐶)) / 3))
2033, 7, 10, 12divsubdird 11094 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐵↑2) − (3 · 𝐶)) / 3) = (((𝐵↑2) / 3) − ((3 · 𝐶) / 3)))
2045, 10, 12divcan3d 11060 . . . . . . . . . . . . . . . 16 (𝜑 → ((3 · 𝐶) / 3) = 𝐶)
205204oveq2d 6858 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐵↑2) / 3) − ((3 · 𝐶) / 3)) = (((𝐵↑2) / 3) − 𝐶))
206202, 203, 2053eqtrd 2803 . . . . . . . . . . . . . 14 (𝜑 → (𝑀 / 3) = (((𝐵↑2) / 3) − 𝐶))
207206negeqd 10529 . . . . . . . . . . . . 13 (𝜑 → -(𝑀 / 3) = -(((𝐵↑2) / 3) − 𝐶))
2083, 10, 12divcld 11055 . . . . . . . . . . . . . 14 (𝜑 → ((𝐵↑2) / 3) ∈ ℂ)
209208, 5negsubdi2d 10662 . . . . . . . . . . . . 13 (𝜑 → -(((𝐵↑2) / 3) − 𝐶) = (𝐶 − ((𝐵↑2) / 3)))
210207, 209eqtrd 2799 . . . . . . . . . . . 12 (𝜑 → -(𝑀 / 3) = (𝐶 − ((𝐵↑2) / 3)))
211210oveq1d 6857 . . . . . . . . . . 11 (𝜑 → (-(𝑀 / 3) · 𝑋) = ((𝐶 − ((𝐵↑2) / 3)) · 𝑋))
2125, 208, 40subdird 10741 . . . . . . . . . . 11 (𝜑 → ((𝐶 − ((𝐵↑2) / 3)) · 𝑋) = ((𝐶 · 𝑋) − (((𝐵↑2) / 3) · 𝑋)))
213208, 40mulcomd 10315 . . . . . . . . . . . . 13 (𝜑 → (((𝐵↑2) / 3) · 𝑋) = (𝑋 · ((𝐵↑2) / 3)))
2144sqvali 13150 . . . . . . . . . . . . . . . . . 18 (3↑2) = (3 · 3)
215214oveq2i 6853 . . . . . . . . . . . . . . . . 17 ((𝐵↑2) / (3↑2)) = ((𝐵↑2) / (3 · 3))
2162, 10, 12sqdivd 13228 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐵 / 3)↑2) = ((𝐵↑2) / (3↑2)))
2173, 10, 10, 12, 12divdiv1d 11086 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝐵↑2) / 3) / 3) = ((𝐵↑2) / (3 · 3)))
218215, 216, 2173eqtr4a 2825 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐵 / 3)↑2) = (((𝐵↑2) / 3) / 3))
219218oveq2d 6858 . . . . . . . . . . . . . . 15 (𝜑 → (3 · ((𝐵 / 3)↑2)) = (3 · (((𝐵↑2) / 3) / 3)))
220208, 10, 12divcan2d 11057 . . . . . . . . . . . . . . 15 (𝜑 → (3 · (((𝐵↑2) / 3) / 3)) = ((𝐵↑2) / 3))
221219, 220eqtrd 2799 . . . . . . . . . . . . . 14 (𝜑 → (3 · ((𝐵 / 3)↑2)) = ((𝐵↑2) / 3))
222221oveq2d 6858 . . . . . . . . . . . . 13 (𝜑 → (𝑋 · (3 · ((𝐵 / 3)↑2))) = (𝑋 · ((𝐵↑2) / 3)))
22340, 10, 188mul12d 10499 . . . . . . . . . . . . 13 (𝜑 → (𝑋 · (3 · ((𝐵 / 3)↑2))) = (3 · (𝑋 · ((𝐵 / 3)↑2))))
224213, 222, 2233eqtr2d 2805 . . . . . . . . . . . 12 (𝜑 → (((𝐵↑2) / 3) · 𝑋) = (3 · (𝑋 · ((𝐵 / 3)↑2))))
225224oveq2d 6858 . . . . . . . . . . 11 (𝜑 → ((𝐶 · 𝑋) − (((𝐵↑2) / 3) · 𝑋)) = ((𝐶 · 𝑋) − (3 · (𝑋 · ((𝐵 / 3)↑2)))))
226211, 212, 2253eqtrd 2803 . . . . . . . . . 10 (𝜑 → (-(𝑀 / 3) · 𝑋) = ((𝐶 · 𝑋) − (3 · (𝑋 · ((𝐵 / 3)↑2)))))
227210oveq1d 6857 . . . . . . . . . . . . 13 (𝜑 → (-(𝑀 / 3) · (𝐵 / 3)) = ((𝐶 − ((𝐵↑2) / 3)) · (𝐵 / 3)))
2285, 208, 41subdird 10741 . . . . . . . . . . . . 13 (𝜑 → ((𝐶 − ((𝐵↑2) / 3)) · (𝐵 / 3)) = ((𝐶 · (𝐵 / 3)) − (((𝐵↑2) / 3) · (𝐵 / 3))))
2295, 2, 10, 12divassd 11090 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐶 · 𝐵) / 3) = (𝐶 · (𝐵 / 3)))
2305, 2mulcomd 10315 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐶 · 𝐵) = (𝐵 · 𝐶))
231230oveq1d 6857 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐶 · 𝐵) / 3) = ((𝐵 · 𝐶) / 3))
232229, 231eqtr3d 2801 . . . . . . . . . . . . . 14 (𝜑 → (𝐶 · (𝐵 / 3)) = ((𝐵 · 𝐶) / 3))
2333, 10, 2, 10, 12, 12divmuldivd 11096 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐵↑2) / 3) · (𝐵 / 3)) = (((𝐵↑2) · 𝐵) / (3 · 3)))
234 df-3 11336 . . . . . . . . . . . . . . . . . 18 3 = (2 + 1)
235234oveq2i 6853 . . . . . . . . . . . . . . . . 17 (𝐵↑3) = (𝐵↑(2 + 1))
236 expp1 13074 . . . . . . . . . . . . . . . . . 18 ((𝐵 ∈ ℂ ∧ 2 ∈ ℕ0) → (𝐵↑(2 + 1)) = ((𝐵↑2) · 𝐵))
2372, 27, 236sylancl 580 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵↑(2 + 1)) = ((𝐵↑2) · 𝐵))
238235, 237syl5req 2812 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐵↑2) · 𝐵) = (𝐵↑3))
239161a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → (3 · 3) = 9)
240238, 239oveq12d 6860 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐵↑2) · 𝐵) / (3 · 3)) = ((𝐵↑3) / 9))
241233, 240eqtrd 2799 . . . . . . . . . . . . . 14 (𝜑 → (((𝐵↑2) / 3) · (𝐵 / 3)) = ((𝐵↑3) / 9))
242232, 241oveq12d 6860 . . . . . . . . . . . . 13 (𝜑 → ((𝐶 · (𝐵 / 3)) − (((𝐵↑2) / 3) · (𝐵 / 3))) = (((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)))
243227, 228, 2423eqtrd 2803 . . . . . . . . . . . 12 (𝜑 → (-(𝑀 / 3) · (𝐵 / 3)) = (((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)))
24415oveq1d 6857 . . . . . . . . . . . . 13 (𝜑 → (𝑁 / 27) = ((((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) + (27 · 𝐷)) / 27))
24526, 33, 36, 38divdird 11093 . . . . . . . . . . . . 13 (𝜑 → ((((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) + (27 · 𝐷)) / 27) = ((((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) / 27) + ((27 · 𝐷) / 27)))
24621, 25, 36, 38divsubdird 11094 . . . . . . . . . . . . . . 15 (𝜑 → (((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) / 27) = (((2 · (𝐵↑3)) / 27) − ((9 · (𝐵 · 𝐶)) / 27)))
247 9t3e27 11864 . . . . . . . . . . . . . . . . . 18 (9 · 3) = 27
248247oveq2i 6853 . . . . . . . . . . . . . . . . 17 ((9 · (𝐵 · 𝐶)) / (9 · 3)) = ((9 · (𝐵 · 𝐶)) / 27)
24923, 10, 104, 12, 107divcan5d 11081 . . . . . . . . . . . . . . . . 17 (𝜑 → ((9 · (𝐵 · 𝐶)) / (9 · 3)) = ((𝐵 · 𝐶) / 3))
250248, 249syl5eqr 2813 . . . . . . . . . . . . . . . 16 (𝜑 → ((9 · (𝐵 · 𝐶)) / 27) = ((𝐵 · 𝐶) / 3))
251250oveq2d 6858 . . . . . . . . . . . . . . 15 (𝜑 → (((2 · (𝐵↑3)) / 27) − ((9 · (𝐵 · 𝐶)) / 27)) = (((2 · (𝐵↑3)) / 27) − ((𝐵 · 𝐶) / 3)))
252246, 251eqtrd 2799 . . . . . . . . . . . . . 14 (𝜑 → (((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) / 27) = (((2 · (𝐵↑3)) / 27) − ((𝐵 · 𝐶) / 3)))
25331, 36, 38divcan3d 11060 . . . . . . . . . . . . . 14 (𝜑 → ((27 · 𝐷) / 27) = 𝐷)
254252, 253oveq12d 6860 . . . . . . . . . . . . 13 (𝜑 → ((((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) / 27) + ((27 · 𝐷) / 27)) = ((((2 · (𝐵↑3)) / 27) − ((𝐵 · 𝐶) / 3)) + 𝐷))
255244, 245, 2543eqtrd 2803 . . . . . . . . . . . 12 (𝜑 → (𝑁 / 27) = ((((2 · (𝐵↑3)) / 27) − ((𝐵 · 𝐶) / 3)) + 𝐷))
256243, 255oveq12d 6860 . . . . . . . . . . 11 (𝜑 → ((-(𝑀 / 3) · (𝐵 / 3)) + (𝑁 / 27)) = ((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + ((((2 · (𝐵↑3)) / 27) − ((𝐵 · 𝐶) / 3)) + 𝐷)))
25719, 104, 107divcld 11055 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐵↑3) / 9) ∈ ℂ)
25821, 36, 38divcld 11055 . . . . . . . . . . . . . . 15 (𝜑 → ((2 · (𝐵↑3)) / 27) ∈ ℂ)
259257, 258negsubdi2d 10662 . . . . . . . . . . . . . 14 (𝜑 → -(((𝐵↑3) / 9) − ((2 · (𝐵↑3)) / 27)) = (((2 · (𝐵↑3)) / 27) − ((𝐵↑3) / 9)))
2602, 10, 12, 60expdivd 13229 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐵 / 3)↑3) = ((𝐵↑3) / (3↑3)))
26163oveq2i 6853 . . . . . . . . . . . . . . . . 17 ((𝐵↑3) / (3↑3)) = ((𝐵↑3) / 27)
262 ax-1cn 10247 . . . . . . . . . . . . . . . . . . . . . . 23 1 ∈ ℂ
2634, 16, 262, 53subaddrii 10624 . . . . . . . . . . . . . . . . . . . . . 22 (3 − 2) = 1
264263oveq1i 6852 . . . . . . . . . . . . . . . . . . . . 21 ((3 − 2) · (𝐵↑3)) = (1 · (𝐵↑3))
26519mulid2d 10312 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (1 · (𝐵↑3)) = (𝐵↑3))
266264, 265syl5eq 2811 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((3 − 2) · (𝐵↑3)) = (𝐵↑3))
26710, 68, 19subdird 10741 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((3 − 2) · (𝐵↑3)) = ((3 · (𝐵↑3)) − (2 · (𝐵↑3))))
268266, 267eqtr3d 2801 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐵↑3) = ((3 · (𝐵↑3)) − (2 · (𝐵↑3))))
269268oveq1d 6857 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐵↑3) / 27) = (((3 · (𝐵↑3)) − (2 · (𝐵↑3))) / 27))
270 mulcl 10273 . . . . . . . . . . . . . . . . . . . 20 ((3 ∈ ℂ ∧ (𝐵↑3) ∈ ℂ) → (3 · (𝐵↑3)) ∈ ℂ)
2714, 19, 270sylancr 581 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (3 · (𝐵↑3)) ∈ ℂ)
272271, 21, 36, 38divsubdird 11094 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((3 · (𝐵↑3)) − (2 · (𝐵↑3))) / 27) = (((3 · (𝐵↑3)) / 27) − ((2 · (𝐵↑3)) / 27)))
273269, 272eqtrd 2799 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐵↑3) / 27) = (((3 · (𝐵↑3)) / 27) − ((2 · (𝐵↑3)) / 27)))
274261, 273syl5eq 2811 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐵↑3) / (3↑3)) = (((3 · (𝐵↑3)) / 27) − ((2 · (𝐵↑3)) / 27)))
27522, 4, 247mulcomli 10303 . . . . . . . . . . . . . . . . . . 19 (3 · 9) = 27
276275oveq2i 6853 . . . . . . . . . . . . . . . . . 18 ((3 · (𝐵↑3)) / (3 · 9)) = ((3 · (𝐵↑3)) / 27)
27719, 104, 10, 107, 12divcan5d 11081 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((3 · (𝐵↑3)) / (3 · 9)) = ((𝐵↑3) / 9))
278276, 277syl5eqr 2813 . . . . . . . . . . . . . . . . 17 (𝜑 → ((3 · (𝐵↑3)) / 27) = ((𝐵↑3) / 9))
279278oveq1d 6857 . . . . . . . . . . . . . . . 16 (𝜑 → (((3 · (𝐵↑3)) / 27) − ((2 · (𝐵↑3)) / 27)) = (((𝐵↑3) / 9) − ((2 · (𝐵↑3)) / 27)))
280260, 274, 2793eqtrd 2803 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐵 / 3)↑3) = (((𝐵↑3) / 9) − ((2 · (𝐵↑3)) / 27)))
281280negeqd 10529 . . . . . . . . . . . . . 14 (𝜑 → -((𝐵 / 3)↑3) = -(((𝐵↑3) / 9) − ((2 · (𝐵↑3)) / 27)))
28223, 10, 12divcld 11055 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐵 · 𝐶) / 3) ∈ ℂ)
283282, 257, 258npncan3d 10682 . . . . . . . . . . . . . 14 (𝜑 → ((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + (((2 · (𝐵↑3)) / 27) − ((𝐵 · 𝐶) / 3))) = (((2 · (𝐵↑3)) / 27) − ((𝐵↑3) / 9)))
284259, 281, 2833eqtr4d 2809 . . . . . . . . . . . . 13 (𝜑 → -((𝐵 / 3)↑3) = ((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + (((2 · (𝐵↑3)) / 27) − ((𝐵 · 𝐶) / 3))))
285284oveq1d 6857 . . . . . . . . . . . 12 (𝜑 → (-((𝐵 / 3)↑3) + 𝐷) = (((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + (((2 · (𝐵↑3)) / 27) − ((𝐵 · 𝐶) / 3))) + 𝐷))
286192negcld 10633 . . . . . . . . . . . . 13 (𝜑 → -((𝐵 / 3)↑3) ∈ ℂ)
287286, 31addcomd 10492 . . . . . . . . . . . 12 (𝜑 → (-((𝐵 / 3)↑3) + 𝐷) = (𝐷 + -((𝐵 / 3)↑3)))
288243, 200eqeltrrd 2845 . . . . . . . . . . . . 13 (𝜑 → (((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) ∈ ℂ)
289258, 282subcld 10646 . . . . . . . . . . . . 13 (𝜑 → (((2 · (𝐵↑3)) / 27) − ((𝐵 · 𝐶) / 3)) ∈ ℂ)
290288, 289, 31addassd 10316 . . . . . . . . . . . 12 (𝜑 → (((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + (((2 · (𝐵↑3)) / 27) − ((𝐵 · 𝐶) / 3))) + 𝐷) = ((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + ((((2 · (𝐵↑3)) / 27) − ((𝐵 · 𝐶) / 3)) + 𝐷)))
291285, 287, 2903eqtr3d 2807 . . . . . . . . . . 11 (𝜑 → (𝐷 + -((𝐵 / 3)↑3)) = ((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + ((((2 · (𝐵↑3)) / 27) − ((𝐵 · 𝐶) / 3)) + 𝐷)))
29231, 192negsubd 10652 . . . . . . . . . . 11 (𝜑 → (𝐷 + -((𝐵 / 3)↑3)) = (𝐷 − ((𝐵 / 3)↑3)))
293256, 291, 2923eqtr2d 2805 . . . . . . . . . 10 (𝜑 → ((-(𝑀 / 3) · (𝐵 / 3)) + (𝑁 / 27)) = (𝐷 − ((𝐵 / 3)↑3)))
294226, 293oveq12d 6860 . . . . . . . . 9 (𝜑 → ((-(𝑀 / 3) · 𝑋) + ((-(𝑀 / 3) · (𝐵 / 3)) + (𝑁 / 27))) = (((𝐶 · 𝑋) − (3 · (𝑋 · ((𝐵 / 3)↑2)))) + (𝐷 − ((𝐵 / 3)↑3))))
295198, 201, 2943eqtrd 2803 . . . . . . . 8 (𝜑 → ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27)) = (((𝐶 · 𝑋) − (3 · (𝑋 · ((𝐵 / 3)↑2)))) + (𝐷 − ((𝐵 / 3)↑3))))
2965, 40mulcld 10314 . . . . . . . . 9 (𝜑 → (𝐶 · 𝑋) ∈ ℂ)
297296, 31, 190, 192addsub4d 10693 . . . . . . . 8 (𝜑 → (((𝐶 · 𝑋) + 𝐷) − ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))) = (((𝐶 · 𝑋) − (3 · (𝑋 · ((𝐵 / 3)↑2)))) + (𝐷 − ((𝐵 / 3)↑3))))
298295, 297eqtr4d 2802 . . . . . . 7 (𝜑 → ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27)) = (((𝐶 · 𝑋) + 𝐷) − ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))))
299298oveq2d 6858 . . . . . 6 (𝜑 → (((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27))) = (((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) + (((𝐶 · 𝑋) + 𝐷) − ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)))))
300296, 31addcld 10313 . . . . . . 7 (𝜑 → ((𝐶 · 𝑋) + 𝐷) ∈ ℂ)
301193, 300pncan3d 10649 . . . . . 6 (𝜑 → (((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) + (((𝐶 · 𝑋) + 𝐷) − ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)))) = ((𝐶 · 𝑋) + 𝐷))
302299, 301eqtrd 2799 . . . . 5 (𝜑 → (((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27))) = ((𝐶 · 𝑋) + 𝐷))
303302oveq2d 6858 . . . 4 (𝜑 → (((𝑋↑3) + (𝐵 · (𝑋↑2))) + (((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27)))) = (((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((𝐶 · 𝑋) + 𝐷)))
304183, 196, 3033eqtrd 2803 . . 3 (𝜑 → (((𝑋 + (𝐵 / 3))↑3) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27))) = (((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((𝐶 · 𝑋) + 𝐷)))
305304eqeq1d 2767 . 2 (𝜑 → ((((𝑋 + (𝐵 / 3))↑3) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27))) = 0 ↔ (((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((𝐶 · 𝑋) + 𝐷)) = 0))
306 oveq1 6849 . . . . . . . 8 (𝑟 = 0 → (𝑟↑3) = (0↑3))
307 0exp 13102 . . . . . . . . 9 (3 ∈ ℕ → (0↑3) = 0)
30846, 307ax-mp 5 . . . . . . . 8 (0↑3) = 0
309306, 308syl6eq 2815 . . . . . . 7 (𝑟 = 0 → (𝑟↑3) = 0)
310 0ne1 11343 . . . . . . . 8 0 ≠ 1
311310a1i 11 . . . . . . 7 (𝑟 = 0 → 0 ≠ 1)
312309, 311eqnetrd 3004 . . . . . 6 (𝑟 = 0 → (𝑟↑3) ≠ 1)
313312necon2i 2971 . . . . 5 ((𝑟↑3) = 1 → 𝑟 ≠ 0)
314 eqcom 2772 . . . . . . . 8 (𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) ↔ -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = 𝑋)
3152adantr 472 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝐵 ∈ ℂ)
316 simprl 787 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑟 ∈ ℂ)
31743adantr 472 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑇 ∈ ℂ)
318316, 317mulcld 10314 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑟 · 𝑇) ∈ ℂ)
3199adantr 472 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑀 ∈ ℂ)
320 simprr 789 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑟 ≠ 0)
321168adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑇 ≠ 0)
322316, 317, 320, 321mulne0d 10933 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑟 · 𝑇) ≠ 0)
323319, 318, 322divcld 11055 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑀 / (𝑟 · 𝑇)) ∈ ℂ)
324318, 323addcld 10313 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) ∈ ℂ)
3254a1i 11 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 3 ∈ ℂ)
32611a1i 11 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 3 ≠ 0)
327315, 324, 325, 326divdird 11093 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝐵 + ((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇)))) / 3) = ((𝐵 / 3) + (((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)))
328315, 318, 323addassd 10316 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) = (𝐵 + ((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇)))))
329328oveq1d 6857 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = ((𝐵 + ((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇)))) / 3))
33041adantr 472 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝐵 / 3) ∈ ℂ)
331324, 325, 326divcld 11055 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) ∈ ℂ)
332330, 331subnegd 10653 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝐵 / 3) − -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)) = ((𝐵 / 3) + (((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)))
333327, 329, 3323eqtr4d 2809 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = ((𝐵 / 3) − -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)))
334333negeqd 10529 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = -((𝐵 / 3) − -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)))
335331negcld 10633 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) ∈ ℂ)
336330, 335negsubdi2d 10662 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -((𝐵 / 3) − -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)) = (-(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) − (𝐵 / 3)))
337334, 336eqtrd 2799 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = (-(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) − (𝐵 / 3)))
338337eqeq1d 2767 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (-(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = 𝑋 ↔ (-(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) − (𝐵 / 3)) = 𝑋))
339314, 338syl5bb 274 . . . . . . 7 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) ↔ (-(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) − (𝐵 / 3)) = 𝑋))
34040adantr 472 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑋 ∈ ℂ)
341335, 330, 340subadd2d 10665 . . . . . . 7 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((-(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) − (𝐵 / 3)) = 𝑋 ↔ (𝑋 + (𝐵 / 3)) = -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)))
342318, 323, 325, 326divdird 11093 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) = (((𝑟 · 𝑇) / 3) + ((𝑀 / (𝑟 · 𝑇)) / 3)))
343342negeqd 10529 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) = -(((𝑟 · 𝑇) / 3) + ((𝑀 / (𝑟 · 𝑇)) / 3)))
344318, 325, 326divcld 11055 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑟 · 𝑇) / 3) ∈ ℂ)
345323, 325, 326divcld 11055 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑀 / (𝑟 · 𝑇)) / 3) ∈ ℂ)
346344, 345negdi2d 10660 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝑟 · 𝑇) / 3) + ((𝑀 / (𝑟 · 𝑇)) / 3)) = (-((𝑟 · 𝑇) / 3) − ((𝑀 / (𝑟 · 𝑇)) / 3)))
347316, 317, 325, 326divassd 11090 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑟 · 𝑇) / 3) = (𝑟 · (𝑇 / 3)))
348347negeqd 10529 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -((𝑟 · 𝑇) / 3) = -(𝑟 · (𝑇 / 3)))
34944adantr 472 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑇 / 3) ∈ ℂ)
350316, 349mulneg2d 10738 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑟 · -(𝑇 / 3)) = -(𝑟 · (𝑇 / 3)))
351348, 350eqtr4d 2802 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -((𝑟 · 𝑇) / 3) = (𝑟 · -(𝑇 / 3)))
352319, 318, 325, 322, 326divdiv32d 11080 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑀 / (𝑟 · 𝑇)) / 3) = ((𝑀 / 3) / (𝑟 · 𝑇)))
35313adantr 472 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑀 / 3) ∈ ℂ)
354353, 318, 325, 322, 326divcan7d 11083 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝑀 / 3) / 3) / ((𝑟 · 𝑇) / 3)) = ((𝑀 / 3) / (𝑟 · 𝑇)))
355163oveq1d 6857 . . . . . . . . . . . . 13 (𝜑 → (((𝑀 / 3) / 3) / ((𝑟 · 𝑇) / 3)) = ((𝑀 / 9) / ((𝑟 · 𝑇) / 3)))
356355adantr 472 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝑀 / 3) / 3) / ((𝑟 · 𝑇) / 3)) = ((𝑀 / 9) / ((𝑟 · 𝑇) / 3)))
357352, 354, 3563eqtr2d 2805 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑀 / (𝑟 · 𝑇)) / 3) = ((𝑀 / 9) / ((𝑟 · 𝑇) / 3)))
358127adantr 472 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑀 / 9) ∈ ℂ)
359318, 325, 322, 326divne0d 11071 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑟 · 𝑇) / 3) ≠ 0)
360358, 344, 359div2negd 11070 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (-(𝑀 / 9) / -((𝑟 · 𝑇) / 3)) = ((𝑀 / 9) / ((𝑟 · 𝑇) / 3)))
361351oveq2d 6858 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (-(𝑀 / 9) / -((𝑟 · 𝑇) / 3)) = (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3))))
362357, 360, 3613eqtr2d 2805 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑀 / (𝑟 · 𝑇)) / 3) = (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3))))
363351, 362oveq12d 6860 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (-((𝑟 · 𝑇) / 3) − ((𝑀 / (𝑟 · 𝑇)) / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))))
364343, 346, 3633eqtrd 2803 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))))
365364eqeq2d 2775 . . . . . . 7 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑋 + (𝐵 / 3)) = -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) ↔ (𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3))))))
366339, 341, 3653bitrrd 297 . . . . . 6 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))) ↔ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3)))
367366anassrs 459 . . . . 5 (((𝜑𝑟 ∈ ℂ) ∧ 𝑟 ≠ 0) → ((𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))) ↔ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3)))
368313, 367sylan2 586 . . . 4 (((𝜑𝑟 ∈ ℂ) ∧ (𝑟↑3) = 1) → ((𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))) ↔ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3)))
369368pm5.32da 574 . . 3 ((𝜑𝑟 ∈ ℂ) → (((𝑟↑3) = 1 ∧ (𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3))))) ↔ ((𝑟↑3) = 1 ∧ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3))))
370369rexbidva 3196 . 2 (𝜑 → (∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ (𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3))))) ↔ ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3))))
371171, 305, 3703bitr3d 300 1 (𝜑 → ((((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((𝐶 · 𝑋) + 𝐷)) = 0 ↔ ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384   = wceq 1652  wcel 2155  wne 2937  wrex 3056   class class class wbr 4809  (class class class)co 6842  cc 10187  0cc0 10189  1c1 10190   + caddc 10192   · cmul 10194  cmin 10520  -cneg 10521   / cdiv 10938  cn 11274  2c2 11327  3c3 11328  4c4 11329  7c7 11332  9c9 11334  0cn0 11538  cdc 11740  cexp 13067  cdvds 15267
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266  ax-pre-sup 10267
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-om 7264  df-1st 7366  df-2nd 7367  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-er 7947  df-en 8161  df-dom 8162  df-sdom 8163  df-sup 8555  df-inf 8556  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-div 10939  df-nn 11275  df-2 11335  df-3 11336  df-4 11337  df-5 11338  df-6 11339  df-7 11340  df-8 11341  df-9 11342  df-n0 11539  df-z 11625  df-dec 11741  df-uz 11887  df-rp 12029  df-fz 12534  df-seq 13009  df-exp 13068  df-cj 14126  df-re 14127  df-im 14128  df-sqrt 14262  df-abs 14263  df-dvds 15268
This theorem is referenced by:  cubic2  24866  quart  24879
  Copyright terms: Public domain W3C validator