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

Theorem mcubic 24491
Description: Solutions to a monic cubic equation, a special case of cubic 24493. (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 12954 . . . . . . 7 (𝜑 → (𝐵↑2) ∈ ℂ)
4 3cn 11047 . . . . . . . 8 3 ∈ ℂ
5 mcubic.c . . . . . . . 8 (𝜑𝐶 ∈ ℂ)
6 mulcl 9972 . . . . . . . 8 ((3 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (3 · 𝐶) ∈ ℂ)
74, 5, 6sylancr 694 . . . . . . 7 (𝜑 → (3 · 𝐶) ∈ ℂ)
83, 7subcld 10344 . . . . . 6 (𝜑 → ((𝐵↑2) − (3 · 𝐶)) ∈ ℂ)
91, 8eqeltrd 2698 . . . . 5 (𝜑𝑀 ∈ ℂ)
104a1i 11 . . . . 5 (𝜑 → 3 ∈ ℂ)
11 3ne0 11067 . . . . . 6 3 ≠ 0
1211a1i 11 . . . . 5 (𝜑 → 3 ≠ 0)
139, 10, 12divcld 10753 . . . 4 (𝜑 → (𝑀 / 3) ∈ ℂ)
1413negcld 10331 . . 3 (𝜑 → -(𝑀 / 3) ∈ ℂ)
15 mcubic.n . . . . 5 (𝜑𝑁 = (((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) + (27 · 𝐷)))
16 2cn 11043 . . . . . . . 8 2 ∈ ℂ
17 3nn0 11262 . . . . . . . . 9 3 ∈ ℕ0
18 expcl 12826 . . . . . . . . 9 ((𝐵 ∈ ℂ ∧ 3 ∈ ℕ0) → (𝐵↑3) ∈ ℂ)
192, 17, 18sylancl 693 . . . . . . . 8 (𝜑 → (𝐵↑3) ∈ ℂ)
20 mulcl 9972 . . . . . . . 8 ((2 ∈ ℂ ∧ (𝐵↑3) ∈ ℂ) → (2 · (𝐵↑3)) ∈ ℂ)
2116, 19, 20sylancr 694 . . . . . . 7 (𝜑 → (2 · (𝐵↑3)) ∈ ℂ)
22 9cn 11060 . . . . . . . 8 9 ∈ ℂ
232, 5mulcld 10012 . . . . . . . 8 (𝜑 → (𝐵 · 𝐶) ∈ ℂ)
24 mulcl 9972 . . . . . . . 8 ((9 ∈ ℂ ∧ (𝐵 · 𝐶) ∈ ℂ) → (9 · (𝐵 · 𝐶)) ∈ ℂ)
2522, 23, 24sylancr 694 . . . . . . 7 (𝜑 → (9 · (𝐵 · 𝐶)) ∈ ℂ)
2621, 25subcld 10344 . . . . . 6 (𝜑 → ((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) ∈ ℂ)
27 2nn0 11261 . . . . . . . . 9 2 ∈ ℕ0
28 7nn 11142 . . . . . . . . 9 7 ∈ ℕ
2927, 28decnncl 11470 . . . . . . . 8 27 ∈ ℕ
3029nncni 10982 . . . . . . 7 27 ∈ ℂ
31 mcubic.d . . . . . . 7 (𝜑𝐷 ∈ ℂ)
32 mulcl 9972 . . . . . . 7 ((27 ∈ ℂ ∧ 𝐷 ∈ ℂ) → (27 · 𝐷) ∈ ℂ)
3330, 31, 32sylancr 694 . . . . . 6 (𝜑 → (27 · 𝐷) ∈ ℂ)
3426, 33addcld 10011 . . . . 5 (𝜑 → (((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) + (27 · 𝐷)) ∈ ℂ)
3515, 34eqeltrd 2698 . . . 4 (𝜑𝑁 ∈ ℂ)
3630a1i 11 . . . 4 (𝜑27 ∈ ℂ)
3729nnne0i 11007 . . . . 5 27 ≠ 0
3837a1i 11 . . . 4 (𝜑27 ≠ 0)
3935, 36, 38divcld 10753 . . 3 (𝜑 → (𝑁 / 27) ∈ ℂ)
40 mcubic.x . . . 4 (𝜑𝑋 ∈ ℂ)
412, 10, 12divcld 10753 . . . 4 (𝜑 → (𝐵 / 3) ∈ ℂ)
4240, 41addcld 10011 . . 3 (𝜑 → (𝑋 + (𝐵 / 3)) ∈ ℂ)
43 mcubic.t . . . . 5 (𝜑𝑇 ∈ ℂ)
4443, 10, 12divcld 10753 . . . 4 (𝜑 → (𝑇 / 3) ∈ ℂ)
4544negcld 10331 . . 3 (𝜑 → -(𝑇 / 3) ∈ ℂ)
46 3nn 11138 . . . . . 6 3 ∈ ℕ
4746a1i 11 . . . . 5 (𝜑 → 3 ∈ ℕ)
48 2nn 11137 . . . . . . 7 2 ∈ ℕ
49 1nn0 11260 . . . . . . 7 1 ∈ ℕ0
50 1nn 10983 . . . . . . 7 1 ∈ ℕ
51 2t1e2 11128 . . . . . . . . 9 (2 · 1) = 2
5251oveq1i 6620 . . . . . . . 8 ((2 · 1) + 1) = (2 + 1)
53 2p1e3 11103 . . . . . . . 8 (2 + 1) = 3
5452, 53eqtri 2643 . . . . . . 7 ((2 · 1) + 1) = 3
55 1lt2 11146 . . . . . . 7 1 < 2
5648, 49, 50, 54, 55ndvdsi 15071 . . . . . 6 ¬ 2 ∥ 3
5756a1i 11 . . . . 5 (𝜑 → ¬ 2 ∥ 3)
58 oexpneg 15004 . . . . 5 (((𝑇 / 3) ∈ ℂ ∧ 3 ∈ ℕ ∧ ¬ 2 ∥ 3) → (-(𝑇 / 3)↑3) = -((𝑇 / 3)↑3))
5944, 47, 57, 58syl3anc 1323 . . . 4 (𝜑 → (-(𝑇 / 3)↑3) = -((𝑇 / 3)↑3))
6017a1i 11 . . . . . . 7 (𝜑 → 3 ∈ ℕ0)
6143, 10, 12, 60expdivd 12970 . . . . . 6 (𝜑 → ((𝑇 / 3)↑3) = ((𝑇↑3) / (3↑3)))
62 mcubic.3 . . . . . . 7 (𝜑 → (𝑇↑3) = ((𝑁 + 𝐺) / 2))
63 3exp3 15733 . . . . . . . 8 (3↑3) = 27
6463a1i 11 . . . . . . 7 (𝜑 → (3↑3) = 27)
6562, 64oveq12d 6628 . . . . . 6 (𝜑 → ((𝑇↑3) / (3↑3)) = (((𝑁 + 𝐺) / 2) / 27))
66 mcubic.g . . . . . . . . 9 (𝜑𝐺 ∈ ℂ)
6735, 66addcld 10011 . . . . . . . 8 (𝜑 → (𝑁 + 𝐺) ∈ ℂ)
68 2cnd 11045 . . . . . . . 8 (𝜑 → 2 ∈ ℂ)
69 2ne0 11065 . . . . . . . . 9 2 ≠ 0
7069a1i 11 . . . . . . . 8 (𝜑 → 2 ≠ 0)
7167, 68, 36, 70, 38divdiv32d 10778 . . . . . . 7 (𝜑 → (((𝑁 + 𝐺) / 2) / 27) = (((𝑁 + 𝐺) / 27) / 2))
7235, 66addcomd 10190 . . . . . . . . . 10 (𝜑 → (𝑁 + 𝐺) = (𝐺 + 𝑁))
7372oveq1d 6625 . . . . . . . . 9 (𝜑 → ((𝑁 + 𝐺) / 27) = ((𝐺 + 𝑁) / 27))
7466, 35, 36, 38divdird 10791 . . . . . . . . 9 (𝜑 → ((𝐺 + 𝑁) / 27) = ((𝐺 / 27) + (𝑁 / 27)))
7573, 74eqtrd 2655 . . . . . . . 8 (𝜑 → ((𝑁 + 𝐺) / 27) = ((𝐺 / 27) + (𝑁 / 27)))
7675oveq1d 6625 . . . . . . 7 (𝜑 → (((𝑁 + 𝐺) / 27) / 2) = (((𝐺 / 27) + (𝑁 / 27)) / 2))
7766, 36, 38divcld 10753 . . . . . . . 8 (𝜑 → (𝐺 / 27) ∈ ℂ)
7877, 39, 68, 70divdird 10791 . . . . . . 7 (𝜑 → (((𝐺 / 27) + (𝑁 / 27)) / 2) = (((𝐺 / 27) / 2) + ((𝑁 / 27) / 2)))
7971, 76, 783eqtrd 2659 . . . . . 6 (𝜑 → (((𝑁 + 𝐺) / 2) / 27) = (((𝐺 / 27) / 2) + ((𝑁 / 27) / 2)))
8061, 65, 793eqtrd 2659 . . . . 5 (𝜑 → ((𝑇 / 3)↑3) = (((𝐺 / 27) / 2) + ((𝑁 / 27) / 2)))
8180negeqd 10227 . . . 4 (𝜑 → -((𝑇 / 3)↑3) = -(((𝐺 / 27) / 2) + ((𝑁 / 27) / 2)))
8277halfcld 11229 . . . . 5 (𝜑 → ((𝐺 / 27) / 2) ∈ ℂ)
8339halfcld 11229 . . . . 5 (𝜑 → ((𝑁 / 27) / 2) ∈ ℂ)
8482, 83negdi2d 10358 . . . 4 (𝜑 → -(((𝐺 / 27) / 2) + ((𝑁 / 27) / 2)) = (-((𝐺 / 27) / 2) − ((𝑁 / 27) / 2)))
8559, 81, 843eqtrd 2659 . . 3 (𝜑 → (-(𝑇 / 3)↑3) = (-((𝐺 / 27) / 2) − ((𝑁 / 27) / 2)))
8682negcld 10331 . . 3 (𝜑 → -((𝐺 / 27) / 2) ∈ ℂ)
87 sqneg 12871 . . . . 5 (((𝐺 / 27) / 2) ∈ ℂ → (-((𝐺 / 27) / 2)↑2) = (((𝐺 / 27) / 2)↑2))
8882, 87syl 17 . . . 4 (𝜑 → (-((𝐺 / 27) / 2)↑2) = (((𝐺 / 27) / 2)↑2))
8977, 68, 70sqdivd 12969 . . . 4 (𝜑 → (((𝐺 / 27) / 2)↑2) = (((𝐺 / 27)↑2) / (2↑2)))
9039, 68, 70sqdivd 12969 . . . . . . . 8 (𝜑 → (((𝑁 / 27) / 2)↑2) = (((𝑁 / 27)↑2) / (2↑2)))
9135, 36, 38sqdivd 12969 . . . . . . . . 9 (𝜑 → ((𝑁 / 27)↑2) = ((𝑁↑2) / (27↑2)))
9291oveq1d 6625 . . . . . . . 8 (𝜑 → (((𝑁 / 27)↑2) / (2↑2)) = (((𝑁↑2) / (27↑2)) / (2↑2)))
9390, 92eqtr2d 2656 . . . . . . 7 (𝜑 → (((𝑁↑2) / (27↑2)) / (2↑2)) = (((𝑁 / 27) / 2)↑2))
94 4cn 11050 . . . . . . . . . . . 12 4 ∈ ℂ
9594a1i 11 . . . . . . . . . . 11 (𝜑 → 4 ∈ ℂ)
96 expcl 12826 . . . . . . . . . . . 12 ((𝑀 ∈ ℂ ∧ 3 ∈ ℕ0) → (𝑀↑3) ∈ ℂ)
979, 17, 96sylancl 693 . . . . . . . . . . 11 (𝜑 → (𝑀↑3) ∈ ℂ)
9830sqcli 12892 . . . . . . . . . . . 12 (27↑2) ∈ ℂ
9998a1i 11 . . . . . . . . . . 11 (𝜑 → (27↑2) ∈ ℂ)
100 sqne0 12878 . . . . . . . . . . . . 13 (27 ∈ ℂ → ((27↑2) ≠ 0 ↔ 27 ≠ 0))
10136, 100syl 17 . . . . . . . . . . . 12 (𝜑 → ((27↑2) ≠ 0 ↔ 27 ≠ 0))
10238, 101mpbird 247 . . . . . . . . . . 11 (𝜑 → (27↑2) ≠ 0)
10395, 97, 99, 102divassd 10788 . . . . . . . . . 10 (𝜑 → ((4 · (𝑀↑3)) / (27↑2)) = (4 · ((𝑀↑3) / (27↑2))))
10422a1i 11 . . . . . . . . . . . . 13 (𝜑 → 9 ∈ ℂ)
105 9nn 11144 . . . . . . . . . . . . . . 15 9 ∈ ℕ
106105nnne0i 11007 . . . . . . . . . . . . . 14 9 ≠ 0
107106a1i 11 . . . . . . . . . . . . 13 (𝜑 → 9 ≠ 0)
1089, 104, 107, 60expdivd 12970 . . . . . . . . . . . 12 (𝜑 → ((𝑀 / 9)↑3) = ((𝑀↑3) / (9↑3)))
10916, 4mulcomi 9998 . . . . . . . . . . . . . . . 16 (2 · 3) = (3 · 2)
110109oveq2i 6621 . . . . . . . . . . . . . . 15 (3↑(2 · 3)) = (3↑(3 · 2))
111 expmul 12853 . . . . . . . . . . . . . . . 16 ((3 ∈ ℂ ∧ 2 ∈ ℕ0 ∧ 3 ∈ ℕ0) → (3↑(2 · 3)) = ((3↑2)↑3))
1124, 27, 17, 111mp3an 1421 . . . . . . . . . . . . . . 15 (3↑(2 · 3)) = ((3↑2)↑3)
113 expmul 12853 . . . . . . . . . . . . . . . 16 ((3 ∈ ℂ ∧ 3 ∈ ℕ0 ∧ 2 ∈ ℕ0) → (3↑(3 · 2)) = ((3↑3)↑2))
1144, 17, 27, 113mp3an 1421 . . . . . . . . . . . . . . 15 (3↑(3 · 2)) = ((3↑3)↑2)
115110, 112, 1143eqtr3i 2651 . . . . . . . . . . . . . 14 ((3↑2)↑3) = ((3↑3)↑2)
116 sq3 12909 . . . . . . . . . . . . . . 15 (3↑2) = 9
117116oveq1i 6620 . . . . . . . . . . . . . 14 ((3↑2)↑3) = (9↑3)
11863oveq1i 6620 . . . . . . . . . . . . . 14 ((3↑3)↑2) = (27↑2)
119115, 117, 1183eqtr3i 2651 . . . . . . . . . . . . 13 (9↑3) = (27↑2)
120119oveq2i 6621 . . . . . . . . . . . 12 ((𝑀↑3) / (9↑3)) = ((𝑀↑3) / (27↑2))
121108, 120syl6eq 2671 . . . . . . . . . . 11 (𝜑 → ((𝑀 / 9)↑3) = ((𝑀↑3) / (27↑2)))
122121oveq2d 6626 . . . . . . . . . 10 (𝜑 → (4 · ((𝑀 / 9)↑3)) = (4 · ((𝑀↑3) / (27↑2))))
123103, 122eqtr4d 2658 . . . . . . . . 9 (𝜑 → ((4 · (𝑀↑3)) / (27↑2)) = (4 · ((𝑀 / 9)↑3)))
124123oveq1d 6625 . . . . . . . 8 (𝜑 → (((4 · (𝑀↑3)) / (27↑2)) / (2↑2)) = ((4 · ((𝑀 / 9)↑3)) / (2↑2)))
125 sq2 12908 . . . . . . . . . 10 (2↑2) = 4
126125oveq2i 6621 . . . . . . . . 9 ((4 · ((𝑀 / 9)↑3)) / (2↑2)) = ((4 · ((𝑀 / 9)↑3)) / 4)
1279, 104, 107divcld 10753 . . . . . . . . . . 11 (𝜑 → (𝑀 / 9) ∈ ℂ)
128 expcl 12826 . . . . . . . . . . 11 (((𝑀 / 9) ∈ ℂ ∧ 3 ∈ ℕ0) → ((𝑀 / 9)↑3) ∈ ℂ)
129127, 17, 128sylancl 693 . . . . . . . . . 10 (𝜑 → ((𝑀 / 9)↑3) ∈ ℂ)
130 4ne0 11069 . . . . . . . . . . 11 4 ≠ 0
131130a1i 11 . . . . . . . . . 10 (𝜑 → 4 ≠ 0)
132129, 95, 131divcan3d 10758 . . . . . . . . 9 (𝜑 → ((4 · ((𝑀 / 9)↑3)) / 4) = ((𝑀 / 9)↑3))
133126, 132syl5eq 2667 . . . . . . . 8 (𝜑 → ((4 · ((𝑀 / 9)↑3)) / (2↑2)) = ((𝑀 / 9)↑3))
134124, 133eqtrd 2655 . . . . . . 7 (𝜑 → (((4 · (𝑀↑3)) / (27↑2)) / (2↑2)) = ((𝑀 / 9)↑3))
13593, 134oveq12d 6628 . . . . . 6 (𝜑 → ((((𝑁↑2) / (27↑2)) / (2↑2)) − (((4 · (𝑀↑3)) / (27↑2)) / (2↑2))) = ((((𝑁 / 27) / 2)↑2) − ((𝑀 / 9)↑3)))
13635sqcld 12954 . . . . . . . 8 (𝜑 → (𝑁↑2) ∈ ℂ)
137136, 99, 102divcld 10753 . . . . . . 7 (𝜑 → ((𝑁↑2) / (27↑2)) ∈ ℂ)
138 mulcl 9972 . . . . . . . . 9 ((4 ∈ ℂ ∧ (𝑀↑3) ∈ ℂ) → (4 · (𝑀↑3)) ∈ ℂ)
13994, 97, 138sylancr 694 . . . . . . . 8 (𝜑 → (4 · (𝑀↑3)) ∈ ℂ)
140139, 99, 102divcld 10753 . . . . . . 7 (𝜑 → ((4 · (𝑀↑3)) / (27↑2)) ∈ ℂ)
14116sqcli 12892 . . . . . . . 8 (2↑2) ∈ ℂ
142141a1i 11 . . . . . . 7 (𝜑 → (2↑2) ∈ ℂ)
143125, 130eqnetri 2860 . . . . . . . 8 (2↑2) ≠ 0
144143a1i 11 . . . . . . 7 (𝜑 → (2↑2) ≠ 0)
145137, 140, 142, 144divsubdird 10792 . . . . . 6 (𝜑 → ((((𝑁↑2) / (27↑2)) − ((4 · (𝑀↑3)) / (27↑2))) / (2↑2)) = ((((𝑁↑2) / (27↑2)) / (2↑2)) − (((4 · (𝑀↑3)) / (27↑2)) / (2↑2))))
14683sqcld 12954 . . . . . . 7 (𝜑 → (((𝑁 / 27) / 2)↑2) ∈ ℂ)
147146, 129negsubd 10350 . . . . . 6 (𝜑 → ((((𝑁 / 27) / 2)↑2) + -((𝑀 / 9)↑3)) = ((((𝑁 / 27) / 2)↑2) − ((𝑀 / 9)↑3)))
148135, 145, 1473eqtr4d 2665 . . . . 5 (𝜑 → ((((𝑁↑2) / (27↑2)) − ((4 · (𝑀↑3)) / (27↑2))) / (2↑2)) = ((((𝑁 / 27) / 2)↑2) + -((𝑀 / 9)↑3)))
14966, 36, 38sqdivd 12969 . . . . . . 7 (𝜑 → ((𝐺 / 27)↑2) = ((𝐺↑2) / (27↑2)))
150 mcubic.2 . . . . . . . 8 (𝜑 → (𝐺↑2) = ((𝑁↑2) − (4 · (𝑀↑3))))
151150oveq1d 6625 . . . . . . 7 (𝜑 → ((𝐺↑2) / (27↑2)) = (((𝑁↑2) − (4 · (𝑀↑3))) / (27↑2)))
152136, 139, 99, 102divsubdird 10792 . . . . . . 7 (𝜑 → (((𝑁↑2) − (4 · (𝑀↑3))) / (27↑2)) = (((𝑁↑2) / (27↑2)) − ((4 · (𝑀↑3)) / (27↑2))))
153149, 151, 1523eqtrd 2659 . . . . . 6 (𝜑 → ((𝐺 / 27)↑2) = (((𝑁↑2) / (27↑2)) − ((4 · (𝑀↑3)) / (27↑2))))
154153oveq1d 6625 . . . . 5 (𝜑 → (((𝐺 / 27)↑2) / (2↑2)) = ((((𝑁↑2) / (27↑2)) − ((4 · (𝑀↑3)) / (27↑2))) / (2↑2)))
155 oexpneg 15004 . . . . . . 7 (((𝑀 / 9) ∈ ℂ ∧ 3 ∈ ℕ ∧ ¬ 2 ∥ 3) → (-(𝑀 / 9)↑3) = -((𝑀 / 9)↑3))
156127, 47, 57, 155syl3anc 1323 . . . . . 6 (𝜑 → (-(𝑀 / 9)↑3) = -((𝑀 / 9)↑3))
157156oveq2d 6626 . . . . 5 (𝜑 → ((((𝑁 / 27) / 2)↑2) + (-(𝑀 / 9)↑3)) = ((((𝑁 / 27) / 2)↑2) + -((𝑀 / 9)↑3)))
158148, 154, 1573eqtr4d 2665 . . . 4 (𝜑 → (((𝐺 / 27)↑2) / (2↑2)) = ((((𝑁 / 27) / 2)↑2) + (-(𝑀 / 9)↑3)))
15988, 89, 1583eqtrd 2659 . . 3 (𝜑 → (-((𝐺 / 27) / 2)↑2) = ((((𝑁 / 27) / 2)↑2) + (-(𝑀 / 9)↑3)))
1609, 10, 10, 12, 12divdiv1d 10784 . . . . . 6 (𝜑 → ((𝑀 / 3) / 3) = (𝑀 / (3 · 3)))
161 3t3e9 11132 . . . . . . 7 (3 · 3) = 9
162161oveq2i 6621 . . . . . 6 (𝑀 / (3 · 3)) = (𝑀 / 9)
163160, 162syl6eq 2671 . . . . 5 (𝜑 → ((𝑀 / 3) / 3) = (𝑀 / 9))
164163negeqd 10227 . . . 4 (𝜑 → -((𝑀 / 3) / 3) = -(𝑀 / 9))
16513, 10, 12divnegd 10766 . . . 4 (𝜑 → -((𝑀 / 3) / 3) = (-(𝑀 / 3) / 3))
166164, 165eqtr3d 2657 . . 3 (𝜑 → -(𝑀 / 9) = (-(𝑀 / 3) / 3))
167 eqidd 2622 . . 3 (𝜑 → ((𝑁 / 27) / 2) = ((𝑁 / 27) / 2))
168 mcubic.0 . . . . 5 (𝜑𝑇 ≠ 0)
16943, 10, 168, 12divne0d 10769 . . . 4 (𝜑 → (𝑇 / 3) ≠ 0)
17044, 169negne0d 10342 . . 3 (𝜑 → -(𝑇 / 3) ≠ 0)
17114, 39, 42, 45, 85, 86, 159, 166, 167, 170dcubic 24490 . 2 (𝜑 → ((((𝑋 + (𝐵 / 3))↑3) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27))) = 0 ↔ ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ (𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))))))
172 binom3 12933 . . . . . . 7 ((𝑋 ∈ ℂ ∧ (𝐵 / 3) ∈ ℂ) → ((𝑋 + (𝐵 / 3))↑3) = (((𝑋↑3) + (3 · ((𝑋↑2) · (𝐵 / 3)))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))))
17340, 41, 172syl2anc 692 . . . . . 6 (𝜑 → ((𝑋 + (𝐵 / 3))↑3) = (((𝑋↑3) + (3 · ((𝑋↑2) · (𝐵 / 3)))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))))
17440sqcld 12954 . . . . . . . . . 10 (𝜑 → (𝑋↑2) ∈ ℂ)
17510, 174, 41mul12d 10197 . . . . . . . . 9 (𝜑 → (3 · ((𝑋↑2) · (𝐵 / 3))) = ((𝑋↑2) · (3 · (𝐵 / 3))))
1762, 10, 12divcan2d 10755 . . . . . . . . . 10 (𝜑 → (3 · (𝐵 / 3)) = 𝐵)
177176oveq2d 6626 . . . . . . . . 9 (𝜑 → ((𝑋↑2) · (3 · (𝐵 / 3))) = ((𝑋↑2) · 𝐵))
178174, 2mulcomd 10013 . . . . . . . . 9 (𝜑 → ((𝑋↑2) · 𝐵) = (𝐵 · (𝑋↑2)))
179175, 177, 1783eqtrd 2659 . . . . . . . 8 (𝜑 → (3 · ((𝑋↑2) · (𝐵 / 3))) = (𝐵 · (𝑋↑2)))
180179oveq2d 6626 . . . . . . 7 (𝜑 → ((𝑋↑3) + (3 · ((𝑋↑2) · (𝐵 / 3)))) = ((𝑋↑3) + (𝐵 · (𝑋↑2))))
181180oveq1d 6625 . . . . . 6 (𝜑 → (((𝑋↑3) + (3 · ((𝑋↑2) · (𝐵 / 3)))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))) = (((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))))
182173, 181eqtrd 2655 . . . . 5 (𝜑 → ((𝑋 + (𝐵 / 3))↑3) = (((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))))
183182oveq1d 6625 . . . 4 (𝜑 → (((𝑋 + (𝐵 / 3))↑3) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27))) = ((((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27))))
184 expcl 12826 . . . . . . 7 ((𝑋 ∈ ℂ ∧ 3 ∈ ℕ0) → (𝑋↑3) ∈ ℂ)
18540, 17, 184sylancl 693 . . . . . 6 (𝜑 → (𝑋↑3) ∈ ℂ)
1862, 174mulcld 10012 . . . . . 6 (𝜑 → (𝐵 · (𝑋↑2)) ∈ ℂ)
187185, 186addcld 10011 . . . . 5 (𝜑 → ((𝑋↑3) + (𝐵 · (𝑋↑2))) ∈ ℂ)
18841sqcld 12954 . . . . . . . 8 (𝜑 → ((𝐵 / 3)↑2) ∈ ℂ)
18940, 188mulcld 10012 . . . . . . 7 (𝜑 → (𝑋 · ((𝐵 / 3)↑2)) ∈ ℂ)
19010, 189mulcld 10012 . . . . . 6 (𝜑 → (3 · (𝑋 · ((𝐵 / 3)↑2))) ∈ ℂ)
191 expcl 12826 . . . . . . 7 (((𝐵 / 3) ∈ ℂ ∧ 3 ∈ ℕ0) → ((𝐵 / 3)↑3) ∈ ℂ)
19241, 17, 191sylancl 693 . . . . . 6 (𝜑 → ((𝐵 / 3)↑3) ∈ ℂ)
193190, 192addcld 10011 . . . . 5 (𝜑 → ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) ∈ ℂ)
19414, 42mulcld 10012 . . . . . 6 (𝜑 → (-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) ∈ ℂ)
195194, 39addcld 10011 . . . . 5 (𝜑 → ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27)) ∈ ℂ)
196187, 193, 195addassd 10014 . . . 4 (𝜑 → ((((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27))) = (((𝑋↑3) + (𝐵 · (𝑋↑2))) + (((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27)))))
19714, 40, 41adddid 10016 . . . . . . . . . 10 (𝜑 → (-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) = ((-(𝑀 / 3) · 𝑋) + (-(𝑀 / 3) · (𝐵 / 3))))
198197oveq1d 6625 . . . . . . . . 9 (𝜑 → ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27)) = (((-(𝑀 / 3) · 𝑋) + (-(𝑀 / 3) · (𝐵 / 3))) + (𝑁 / 27)))
19914, 40mulcld 10012 . . . . . . . . . 10 (𝜑 → (-(𝑀 / 3) · 𝑋) ∈ ℂ)
20014, 41mulcld 10012 . . . . . . . . . 10 (𝜑 → (-(𝑀 / 3) · (𝐵 / 3)) ∈ ℂ)
201199, 200, 39addassd 10014 . . . . . . . . 9 (𝜑 → (((-(𝑀 / 3) · 𝑋) + (-(𝑀 / 3) · (𝐵 / 3))) + (𝑁 / 27)) = ((-(𝑀 / 3) · 𝑋) + ((-(𝑀 / 3) · (𝐵 / 3)) + (𝑁 / 27))))
2021oveq1d 6625 . . . . . . . . . . . . . . 15 (𝜑 → (𝑀 / 3) = (((𝐵↑2) − (3 · 𝐶)) / 3))
2033, 7, 10, 12divsubdird 10792 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐵↑2) − (3 · 𝐶)) / 3) = (((𝐵↑2) / 3) − ((3 · 𝐶) / 3)))
2045, 10, 12divcan3d 10758 . . . . . . . . . . . . . . . 16 (𝜑 → ((3 · 𝐶) / 3) = 𝐶)
205204oveq2d 6626 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐵↑2) / 3) − ((3 · 𝐶) / 3)) = (((𝐵↑2) / 3) − 𝐶))
206202, 203, 2053eqtrd 2659 . . . . . . . . . . . . . 14 (𝜑 → (𝑀 / 3) = (((𝐵↑2) / 3) − 𝐶))
207206negeqd 10227 . . . . . . . . . . . . 13 (𝜑 → -(𝑀 / 3) = -(((𝐵↑2) / 3) − 𝐶))
2083, 10, 12divcld 10753 . . . . . . . . . . . . . 14 (𝜑 → ((𝐵↑2) / 3) ∈ ℂ)
209208, 5negsubdi2d 10360 . . . . . . . . . . . . 13 (𝜑 → -(((𝐵↑2) / 3) − 𝐶) = (𝐶 − ((𝐵↑2) / 3)))
210207, 209eqtrd 2655 . . . . . . . . . . . 12 (𝜑 → -(𝑀 / 3) = (𝐶 − ((𝐵↑2) / 3)))
211210oveq1d 6625 . . . . . . . . . . 11 (𝜑 → (-(𝑀 / 3) · 𝑋) = ((𝐶 − ((𝐵↑2) / 3)) · 𝑋))
2125, 208, 40subdird 10439 . . . . . . . . . . 11 (𝜑 → ((𝐶 − ((𝐵↑2) / 3)) · 𝑋) = ((𝐶 · 𝑋) − (((𝐵↑2) / 3) · 𝑋)))
213208, 40mulcomd 10013 . . . . . . . . . . . . 13 (𝜑 → (((𝐵↑2) / 3) · 𝑋) = (𝑋 · ((𝐵↑2) / 3)))
2144sqvali 12891 . . . . . . . . . . . . . . . . . 18 (3↑2) = (3 · 3)
215214oveq2i 6621 . . . . . . . . . . . . . . . . 17 ((𝐵↑2) / (3↑2)) = ((𝐵↑2) / (3 · 3))
2162, 10, 12sqdivd 12969 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐵 / 3)↑2) = ((𝐵↑2) / (3↑2)))
2173, 10, 10, 12, 12divdiv1d 10784 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝐵↑2) / 3) / 3) = ((𝐵↑2) / (3 · 3)))
218215, 216, 2173eqtr4a 2681 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐵 / 3)↑2) = (((𝐵↑2) / 3) / 3))
219218oveq2d 6626 . . . . . . . . . . . . . . 15 (𝜑 → (3 · ((𝐵 / 3)↑2)) = (3 · (((𝐵↑2) / 3) / 3)))
220208, 10, 12divcan2d 10755 . . . . . . . . . . . . . . 15 (𝜑 → (3 · (((𝐵↑2) / 3) / 3)) = ((𝐵↑2) / 3))
221219, 220eqtrd 2655 . . . . . . . . . . . . . 14 (𝜑 → (3 · ((𝐵 / 3)↑2)) = ((𝐵↑2) / 3))
222221oveq2d 6626 . . . . . . . . . . . . 13 (𝜑 → (𝑋 · (3 · ((𝐵 / 3)↑2))) = (𝑋 · ((𝐵↑2) / 3)))
22340, 10, 188mul12d 10197 . . . . . . . . . . . . 13 (𝜑 → (𝑋 · (3 · ((𝐵 / 3)↑2))) = (3 · (𝑋 · ((𝐵 / 3)↑2))))
224213, 222, 2233eqtr2d 2661 . . . . . . . . . . . 12 (𝜑 → (((𝐵↑2) / 3) · 𝑋) = (3 · (𝑋 · ((𝐵 / 3)↑2))))
225224oveq2d 6626 . . . . . . . . . . 11 (𝜑 → ((𝐶 · 𝑋) − (((𝐵↑2) / 3) · 𝑋)) = ((𝐶 · 𝑋) − (3 · (𝑋 · ((𝐵 / 3)↑2)))))
226211, 212, 2253eqtrd 2659 . . . . . . . . . 10 (𝜑 → (-(𝑀 / 3) · 𝑋) = ((𝐶 · 𝑋) − (3 · (𝑋 · ((𝐵 / 3)↑2)))))
227210oveq1d 6625 . . . . . . . . . . . . 13 (𝜑 → (-(𝑀 / 3) · (𝐵 / 3)) = ((𝐶 − ((𝐵↑2) / 3)) · (𝐵 / 3)))
2285, 208, 41subdird 10439 . . . . . . . . . . . . 13 (𝜑 → ((𝐶 − ((𝐵↑2) / 3)) · (𝐵 / 3)) = ((𝐶 · (𝐵 / 3)) − (((𝐵↑2) / 3) · (𝐵 / 3))))
2295, 2, 10, 12divassd 10788 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐶 · 𝐵) / 3) = (𝐶 · (𝐵 / 3)))
2305, 2mulcomd 10013 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐶 · 𝐵) = (𝐵 · 𝐶))
231230oveq1d 6625 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐶 · 𝐵) / 3) = ((𝐵 · 𝐶) / 3))
232229, 231eqtr3d 2657 . . . . . . . . . . . . . 14 (𝜑 → (𝐶 · (𝐵 / 3)) = ((𝐵 · 𝐶) / 3))
2333, 10, 2, 10, 12, 12divmuldivd 10794 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐵↑2) / 3) · (𝐵 / 3)) = (((𝐵↑2) · 𝐵) / (3 · 3)))
234 df-3 11032 . . . . . . . . . . . . . . . . . 18 3 = (2 + 1)
235234oveq2i 6621 . . . . . . . . . . . . . . . . 17 (𝐵↑3) = (𝐵↑(2 + 1))
236 expp1 12815 . . . . . . . . . . . . . . . . . 18 ((𝐵 ∈ ℂ ∧ 2 ∈ ℕ0) → (𝐵↑(2 + 1)) = ((𝐵↑2) · 𝐵))
2372, 27, 236sylancl 693 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵↑(2 + 1)) = ((𝐵↑2) · 𝐵))
238235, 237syl5req 2668 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐵↑2) · 𝐵) = (𝐵↑3))
239161a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → (3 · 3) = 9)
240238, 239oveq12d 6628 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐵↑2) · 𝐵) / (3 · 3)) = ((𝐵↑3) / 9))
241233, 240eqtrd 2655 . . . . . . . . . . . . . 14 (𝜑 → (((𝐵↑2) / 3) · (𝐵 / 3)) = ((𝐵↑3) / 9))
242232, 241oveq12d 6628 . . . . . . . . . . . . 13 (𝜑 → ((𝐶 · (𝐵 / 3)) − (((𝐵↑2) / 3) · (𝐵 / 3))) = (((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)))
243227, 228, 2423eqtrd 2659 . . . . . . . . . . . 12 (𝜑 → (-(𝑀 / 3) · (𝐵 / 3)) = (((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)))
24415oveq1d 6625 . . . . . . . . . . . . 13 (𝜑 → (𝑁 / 27) = ((((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) + (27 · 𝐷)) / 27))
24526, 33, 36, 38divdird 10791 . . . . . . . . . . . . 13 (𝜑 → ((((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) + (27 · 𝐷)) / 27) = ((((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) / 27) + ((27 · 𝐷) / 27)))
24621, 25, 36, 38divsubdird 10792 . . . . . . . . . . . . . . 15 (𝜑 → (((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) / 27) = (((2 · (𝐵↑3)) / 27) − ((9 · (𝐵 · 𝐶)) / 27)))
247 9t3e27 11616 . . . . . . . . . . . . . . . . . 18 (9 · 3) = 27
248247oveq2i 6621 . . . . . . . . . . . . . . . . 17 ((9 · (𝐵 · 𝐶)) / (9 · 3)) = ((9 · (𝐵 · 𝐶)) / 27)
24923, 10, 104, 12, 107divcan5d 10779 . . . . . . . . . . . . . . . . 17 (𝜑 → ((9 · (𝐵 · 𝐶)) / (9 · 3)) = ((𝐵 · 𝐶) / 3))
250248, 249syl5eqr 2669 . . . . . . . . . . . . . . . 16 (𝜑 → ((9 · (𝐵 · 𝐶)) / 27) = ((𝐵 · 𝐶) / 3))
251250oveq2d 6626 . . . . . . . . . . . . . . 15 (𝜑 → (((2 · (𝐵↑3)) / 27) − ((9 · (𝐵 · 𝐶)) / 27)) = (((2 · (𝐵↑3)) / 27) − ((𝐵 · 𝐶) / 3)))
252246, 251eqtrd 2655 . . . . . . . . . . . . . 14 (𝜑 → (((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) / 27) = (((2 · (𝐵↑3)) / 27) − ((𝐵 · 𝐶) / 3)))
25331, 36, 38divcan3d 10758 . . . . . . . . . . . . . 14 (𝜑 → ((27 · 𝐷) / 27) = 𝐷)
254252, 253oveq12d 6628 . . . . . . . . . . . . 13 (𝜑 → ((((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) / 27) + ((27 · 𝐷) / 27)) = ((((2 · (𝐵↑3)) / 27) − ((𝐵 · 𝐶) / 3)) + 𝐷))
255244, 245, 2543eqtrd 2659 . . . . . . . . . . . 12 (𝜑 → (𝑁 / 27) = ((((2 · (𝐵↑3)) / 27) − ((𝐵 · 𝐶) / 3)) + 𝐷))
256243, 255oveq12d 6628 . . . . . . . . . . 11 (𝜑 → ((-(𝑀 / 3) · (𝐵 / 3)) + (𝑁 / 27)) = ((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + ((((2 · (𝐵↑3)) / 27) − ((𝐵 · 𝐶) / 3)) + 𝐷)))
25719, 104, 107divcld 10753 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐵↑3) / 9) ∈ ℂ)
25821, 36, 38divcld 10753 . . . . . . . . . . . . . . 15 (𝜑 → ((2 · (𝐵↑3)) / 27) ∈ ℂ)
259257, 258negsubdi2d 10360 . . . . . . . . . . . . . 14 (𝜑 → -(((𝐵↑3) / 9) − ((2 · (𝐵↑3)) / 27)) = (((2 · (𝐵↑3)) / 27) − ((𝐵↑3) / 9)))
2602, 10, 12, 60expdivd 12970 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐵 / 3)↑3) = ((𝐵↑3) / (3↑3)))
26163oveq2i 6621 . . . . . . . . . . . . . . . . 17 ((𝐵↑3) / (3↑3)) = ((𝐵↑3) / 27)
262 ax-1cn 9946 . . . . . . . . . . . . . . . . . . . . . . 23 1 ∈ ℂ
2634, 16, 262, 53subaddrii 10322 . . . . . . . . . . . . . . . . . . . . . 22 (3 − 2) = 1
264263oveq1i 6620 . . . . . . . . . . . . . . . . . . . . 21 ((3 − 2) · (𝐵↑3)) = (1 · (𝐵↑3))
26519mulid2d 10010 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (1 · (𝐵↑3)) = (𝐵↑3))
266264, 265syl5eq 2667 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((3 − 2) · (𝐵↑3)) = (𝐵↑3))
26710, 68, 19subdird 10439 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((3 − 2) · (𝐵↑3)) = ((3 · (𝐵↑3)) − (2 · (𝐵↑3))))
268266, 267eqtr3d 2657 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐵↑3) = ((3 · (𝐵↑3)) − (2 · (𝐵↑3))))
269268oveq1d 6625 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐵↑3) / 27) = (((3 · (𝐵↑3)) − (2 · (𝐵↑3))) / 27))
270 mulcl 9972 . . . . . . . . . . . . . . . . . . . 20 ((3 ∈ ℂ ∧ (𝐵↑3) ∈ ℂ) → (3 · (𝐵↑3)) ∈ ℂ)
2714, 19, 270sylancr 694 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (3 · (𝐵↑3)) ∈ ℂ)
272271, 21, 36, 38divsubdird 10792 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((3 · (𝐵↑3)) − (2 · (𝐵↑3))) / 27) = (((3 · (𝐵↑3)) / 27) − ((2 · (𝐵↑3)) / 27)))
273269, 272eqtrd 2655 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐵↑3) / 27) = (((3 · (𝐵↑3)) / 27) − ((2 · (𝐵↑3)) / 27)))
274261, 273syl5eq 2667 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐵↑3) / (3↑3)) = (((3 · (𝐵↑3)) / 27) − ((2 · (𝐵↑3)) / 27)))
27522, 4, 247mulcomli 9999 . . . . . . . . . . . . . . . . . . 19 (3 · 9) = 27
276275oveq2i 6621 . . . . . . . . . . . . . . . . . 18 ((3 · (𝐵↑3)) / (3 · 9)) = ((3 · (𝐵↑3)) / 27)
27719, 104, 10, 107, 12divcan5d 10779 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((3 · (𝐵↑3)) / (3 · 9)) = ((𝐵↑3) / 9))
278276, 277syl5eqr 2669 . . . . . . . . . . . . . . . . 17 (𝜑 → ((3 · (𝐵↑3)) / 27) = ((𝐵↑3) / 9))
279278oveq1d 6625 . . . . . . . . . . . . . . . 16 (𝜑 → (((3 · (𝐵↑3)) / 27) − ((2 · (𝐵↑3)) / 27)) = (((𝐵↑3) / 9) − ((2 · (𝐵↑3)) / 27)))
280260, 274, 2793eqtrd 2659 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐵 / 3)↑3) = (((𝐵↑3) / 9) − ((2 · (𝐵↑3)) / 27)))
281280negeqd 10227 . . . . . . . . . . . . . 14 (𝜑 → -((𝐵 / 3)↑3) = -(((𝐵↑3) / 9) − ((2 · (𝐵↑3)) / 27)))
28223, 10, 12divcld 10753 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐵 · 𝐶) / 3) ∈ ℂ)
283282, 257, 258npncan3d 10380 . . . . . . . . . . . . . 14 (𝜑 → ((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + (((2 · (𝐵↑3)) / 27) − ((𝐵 · 𝐶) / 3))) = (((2 · (𝐵↑3)) / 27) − ((𝐵↑3) / 9)))
284259, 281, 2833eqtr4d 2665 . . . . . . . . . . . . 13 (𝜑 → -((𝐵 / 3)↑3) = ((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + (((2 · (𝐵↑3)) / 27) − ((𝐵 · 𝐶) / 3))))
285284oveq1d 6625 . . . . . . . . . . . 12 (𝜑 → (-((𝐵 / 3)↑3) + 𝐷) = (((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + (((2 · (𝐵↑3)) / 27) − ((𝐵 · 𝐶) / 3))) + 𝐷))
286192negcld 10331 . . . . . . . . . . . . 13 (𝜑 → -((𝐵 / 3)↑3) ∈ ℂ)
287286, 31addcomd 10190 . . . . . . . . . . . 12 (𝜑 → (-((𝐵 / 3)↑3) + 𝐷) = (𝐷 + -((𝐵 / 3)↑3)))
288243, 200eqeltrrd 2699 . . . . . . . . . . . . 13 (𝜑 → (((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) ∈ ℂ)
289258, 282subcld 10344 . . . . . . . . . . . . 13 (𝜑 → (((2 · (𝐵↑3)) / 27) − ((𝐵 · 𝐶) / 3)) ∈ ℂ)
290288, 289, 31addassd 10014 . . . . . . . . . . . 12 (𝜑 → (((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + (((2 · (𝐵↑3)) / 27) − ((𝐵 · 𝐶) / 3))) + 𝐷) = ((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + ((((2 · (𝐵↑3)) / 27) − ((𝐵 · 𝐶) / 3)) + 𝐷)))
291285, 287, 2903eqtr3d 2663 . . . . . . . . . . 11 (𝜑 → (𝐷 + -((𝐵 / 3)↑3)) = ((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + ((((2 · (𝐵↑3)) / 27) − ((𝐵 · 𝐶) / 3)) + 𝐷)))
29231, 192negsubd 10350 . . . . . . . . . . 11 (𝜑 → (𝐷 + -((𝐵 / 3)↑3)) = (𝐷 − ((𝐵 / 3)↑3)))
293256, 291, 2923eqtr2d 2661 . . . . . . . . . 10 (𝜑 → ((-(𝑀 / 3) · (𝐵 / 3)) + (𝑁 / 27)) = (𝐷 − ((𝐵 / 3)↑3)))
294226, 293oveq12d 6628 . . . . . . . . 9 (𝜑 → ((-(𝑀 / 3) · 𝑋) + ((-(𝑀 / 3) · (𝐵 / 3)) + (𝑁 / 27))) = (((𝐶 · 𝑋) − (3 · (𝑋 · ((𝐵 / 3)↑2)))) + (𝐷 − ((𝐵 / 3)↑3))))
295198, 201, 2943eqtrd 2659 . . . . . . . 8 (𝜑 → ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27)) = (((𝐶 · 𝑋) − (3 · (𝑋 · ((𝐵 / 3)↑2)))) + (𝐷 − ((𝐵 / 3)↑3))))
2965, 40mulcld 10012 . . . . . . . . 9 (𝜑 → (𝐶 · 𝑋) ∈ ℂ)
297296, 31, 190, 192addsub4d 10391 . . . . . . . 8 (𝜑 → (((𝐶 · 𝑋) + 𝐷) − ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))) = (((𝐶 · 𝑋) − (3 · (𝑋 · ((𝐵 / 3)↑2)))) + (𝐷 − ((𝐵 / 3)↑3))))
298295, 297eqtr4d 2658 . . . . . . 7 (𝜑 → ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27)) = (((𝐶 · 𝑋) + 𝐷) − ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))))
299298oveq2d 6626 . . . . . 6 (𝜑 → (((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27))) = (((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) + (((𝐶 · 𝑋) + 𝐷) − ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)))))
300296, 31addcld 10011 . . . . . . 7 (𝜑 → ((𝐶 · 𝑋) + 𝐷) ∈ ℂ)
301193, 300pncan3d 10347 . . . . . 6 (𝜑 → (((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) + (((𝐶 · 𝑋) + 𝐷) − ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)))) = ((𝐶 · 𝑋) + 𝐷))
302299, 301eqtrd 2655 . . . . 5 (𝜑 → (((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27))) = ((𝐶 · 𝑋) + 𝐷))
303302oveq2d 6626 . . . 4 (𝜑 → (((𝑋↑3) + (𝐵 · (𝑋↑2))) + (((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27)))) = (((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((𝐶 · 𝑋) + 𝐷)))
304183, 196, 3033eqtrd 2659 . . 3 (𝜑 → (((𝑋 + (𝐵 / 3))↑3) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27))) = (((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((𝐶 · 𝑋) + 𝐷)))
305304eqeq1d 2623 . 2 (𝜑 → ((((𝑋 + (𝐵 / 3))↑3) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27))) = 0 ↔ (((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((𝐶 · 𝑋) + 𝐷)) = 0))
306 oveq1 6617 . . . . . . . 8 (𝑟 = 0 → (𝑟↑3) = (0↑3))
307 0exp 12843 . . . . . . . . 9 (3 ∈ ℕ → (0↑3) = 0)
30846, 307ax-mp 5 . . . . . . . 8 (0↑3) = 0
309306, 308syl6eq 2671 . . . . . . 7 (𝑟 = 0 → (𝑟↑3) = 0)
310 0ne1 11040 . . . . . . . 8 0 ≠ 1
311310a1i 11 . . . . . . 7 (𝑟 = 0 → 0 ≠ 1)
312309, 311eqnetrd 2857 . . . . . 6 (𝑟 = 0 → (𝑟↑3) ≠ 1)
313312necon2i 2824 . . . . 5 ((𝑟↑3) = 1 → 𝑟 ≠ 0)
314 eqcom 2628 . . . . . . . 8 (𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) ↔ -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = 𝑋)
3152adantr 481 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝐵 ∈ ℂ)
316 simprl 793 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑟 ∈ ℂ)
31743adantr 481 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑇 ∈ ℂ)
318316, 317mulcld 10012 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑟 · 𝑇) ∈ ℂ)
3199adantr 481 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑀 ∈ ℂ)
320 simprr 795 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑟 ≠ 0)
321168adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑇 ≠ 0)
322316, 317, 320, 321mulne0d 10631 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑟 · 𝑇) ≠ 0)
323319, 318, 322divcld 10753 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑀 / (𝑟 · 𝑇)) ∈ ℂ)
324318, 323addcld 10011 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) ∈ ℂ)
3254a1i 11 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 3 ∈ ℂ)
32611a1i 11 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 3 ≠ 0)
327315, 324, 325, 326divdird 10791 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝐵 + ((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇)))) / 3) = ((𝐵 / 3) + (((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)))
328315, 318, 323addassd 10014 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) = (𝐵 + ((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇)))))
329328oveq1d 6625 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = ((𝐵 + ((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇)))) / 3))
33041adantr 481 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝐵 / 3) ∈ ℂ)
331324, 325, 326divcld 10753 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) ∈ ℂ)
332330, 331subnegd 10351 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝐵 / 3) − -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)) = ((𝐵 / 3) + (((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)))
333327, 329, 3323eqtr4d 2665 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = ((𝐵 / 3) − -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)))
334333negeqd 10227 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = -((𝐵 / 3) − -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)))
335331negcld 10331 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) ∈ ℂ)
336330, 335negsubdi2d 10360 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -((𝐵 / 3) − -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)) = (-(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) − (𝐵 / 3)))
337334, 336eqtrd 2655 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = (-(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) − (𝐵 / 3)))
338337eqeq1d 2623 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (-(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = 𝑋 ↔ (-(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) − (𝐵 / 3)) = 𝑋))
339314, 338syl5bb 272 . . . . . . 7 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) ↔ (-(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) − (𝐵 / 3)) = 𝑋))
34040adantr 481 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑋 ∈ ℂ)
341335, 330, 340subadd2d 10363 . . . . . . 7 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((-(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) − (𝐵 / 3)) = 𝑋 ↔ (𝑋 + (𝐵 / 3)) = -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)))
342318, 323, 325, 326divdird 10791 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) = (((𝑟 · 𝑇) / 3) + ((𝑀 / (𝑟 · 𝑇)) / 3)))
343342negeqd 10227 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) = -(((𝑟 · 𝑇) / 3) + ((𝑀 / (𝑟 · 𝑇)) / 3)))
344318, 325, 326divcld 10753 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑟 · 𝑇) / 3) ∈ ℂ)
345323, 325, 326divcld 10753 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑀 / (𝑟 · 𝑇)) / 3) ∈ ℂ)
346344, 345negdi2d 10358 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝑟 · 𝑇) / 3) + ((𝑀 / (𝑟 · 𝑇)) / 3)) = (-((𝑟 · 𝑇) / 3) − ((𝑀 / (𝑟 · 𝑇)) / 3)))
347316, 317, 325, 326divassd 10788 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑟 · 𝑇) / 3) = (𝑟 · (𝑇 / 3)))
348347negeqd 10227 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -((𝑟 · 𝑇) / 3) = -(𝑟 · (𝑇 / 3)))
34944adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑇 / 3) ∈ ℂ)
350316, 349mulneg2d 10436 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑟 · -(𝑇 / 3)) = -(𝑟 · (𝑇 / 3)))
351348, 350eqtr4d 2658 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -((𝑟 · 𝑇) / 3) = (𝑟 · -(𝑇 / 3)))
352319, 318, 325, 322, 326divdiv32d 10778 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑀 / (𝑟 · 𝑇)) / 3) = ((𝑀 / 3) / (𝑟 · 𝑇)))
35313adantr 481 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑀 / 3) ∈ ℂ)
354353, 318, 325, 322, 326divcan7d 10781 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝑀 / 3) / 3) / ((𝑟 · 𝑇) / 3)) = ((𝑀 / 3) / (𝑟 · 𝑇)))
355163oveq1d 6625 . . . . . . . . . . . . 13 (𝜑 → (((𝑀 / 3) / 3) / ((𝑟 · 𝑇) / 3)) = ((𝑀 / 9) / ((𝑟 · 𝑇) / 3)))
356355adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝑀 / 3) / 3) / ((𝑟 · 𝑇) / 3)) = ((𝑀 / 9) / ((𝑟 · 𝑇) / 3)))
357352, 354, 3563eqtr2d 2661 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑀 / (𝑟 · 𝑇)) / 3) = ((𝑀 / 9) / ((𝑟 · 𝑇) / 3)))
358127adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑀 / 9) ∈ ℂ)
359318, 325, 322, 326divne0d 10769 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑟 · 𝑇) / 3) ≠ 0)
360358, 344, 359div2negd 10768 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (-(𝑀 / 9) / -((𝑟 · 𝑇) / 3)) = ((𝑀 / 9) / ((𝑟 · 𝑇) / 3)))
361351oveq2d 6626 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (-(𝑀 / 9) / -((𝑟 · 𝑇) / 3)) = (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3))))
362357, 360, 3613eqtr2d 2661 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑀 / (𝑟 · 𝑇)) / 3) = (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3))))
363351, 362oveq12d 6628 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (-((𝑟 · 𝑇) / 3) − ((𝑀 / (𝑟 · 𝑇)) / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))))
364343, 346, 3633eqtrd 2659 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))))
365364eqeq2d 2631 . . . . . . 7 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑋 + (𝐵 / 3)) = -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) ↔ (𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3))))))
366339, 341, 3653bitrrd 295 . . . . . 6 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))) ↔ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3)))
367366anassrs 679 . . . . 5 (((𝜑𝑟 ∈ ℂ) ∧ 𝑟 ≠ 0) → ((𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))) ↔ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3)))
368313, 367sylan2 491 . . . 4 (((𝜑𝑟 ∈ ℂ) ∧ (𝑟↑3) = 1) → ((𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))) ↔ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3)))
369368pm5.32da 672 . . 3 ((𝜑𝑟 ∈ ℂ) → (((𝑟↑3) = 1 ∧ (𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3))))) ↔ ((𝑟↑3) = 1 ∧ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3))))
370369rexbidva 3043 . 2 (𝜑 → (∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ (𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3))))) ↔ ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3))))
371171, 305, 3703bitr3d 298 1 (𝜑 → ((((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((𝐶 · 𝑋) + 𝐷)) = 0 ↔ ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384   = wceq 1480  wcel 1987  wne 2790  wrex 2908   class class class wbr 4618  (class class class)co 6610  cc 9886  0cc0 9888  1c1 9889   + caddc 9891   · cmul 9893  cmin 10218  -cneg 10219   / cdiv 10636  cn 10972  2c2 11022  3c3 11023  4c4 11024  7c7 11027  9c9 11029  0cn0 11244  cdc 11445  cexp 12808  cdvds 14918
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-cnex 9944  ax-resscn 9945  ax-1cn 9946  ax-icn 9947  ax-addcl 9948  ax-addrcl 9949  ax-mulcl 9950  ax-mulrcl 9951  ax-mulcom 9952  ax-addass 9953  ax-mulass 9954  ax-distr 9955  ax-i2m1 9956  ax-1ne0 9957  ax-1rid 9958  ax-rnegex 9959  ax-rrecex 9960  ax-cnre 9961  ax-pre-lttri 9962  ax-pre-lttrn 9963  ax-pre-ltadd 9964  ax-pre-mulgt0 9965  ax-pre-sup 9966
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-om 7020  df-1st 7120  df-2nd 7121  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-er 7694  df-en 7908  df-dom 7909  df-sdom 7910  df-sup 8300  df-inf 8301  df-pnf 10028  df-mnf 10029  df-xr 10030  df-ltxr 10031  df-le 10032  df-sub 10220  df-neg 10221  df-div 10637  df-nn 10973  df-2 11031  df-3 11032  df-4 11033  df-5 11034  df-6 11035  df-7 11036  df-8 11037  df-9 11038  df-n0 11245  df-z 11330  df-dec 11446  df-uz 11640  df-rp 11785  df-fz 12277  df-seq 12750  df-exp 12809  df-cj 13781  df-re 13782  df-im 13783  df-sqrt 13917  df-abs 13918  df-dvds 14919
This theorem is referenced by:  cubic2  24492  quart  24505
  Copyright terms: Public domain W3C validator