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

Theorem mcubic 24374
Description: Solutions to a monic cubic equation, a special case of cubic 24376. (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 12868 . . . . . . 7 (𝜑 → (𝐵↑2) ∈ ℂ)
4 3cn 10972 . . . . . . . 8 3 ∈ ℂ
5 mcubic.c . . . . . . . 8 (𝜑𝐶 ∈ ℂ)
6 mulcl 9899 . . . . . . . 8 ((3 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (3 · 𝐶) ∈ ℂ)
74, 5, 6sylancr 694 . . . . . . 7 (𝜑 → (3 · 𝐶) ∈ ℂ)
83, 7subcld 10271 . . . . . 6 (𝜑 → ((𝐵↑2) − (3 · 𝐶)) ∈ ℂ)
91, 8eqeltrd 2688 . . . . 5 (𝜑𝑀 ∈ ℂ)
104a1i 11 . . . . 5 (𝜑 → 3 ∈ ℂ)
11 3ne0 10992 . . . . . 6 3 ≠ 0
1211a1i 11 . . . . 5 (𝜑 → 3 ≠ 0)
139, 10, 12divcld 10680 . . . 4 (𝜑 → (𝑀 / 3) ∈ ℂ)
1413negcld 10258 . . 3 (𝜑 → -(𝑀 / 3) ∈ ℂ)
15 mcubic.n . . . . 5 (𝜑𝑁 = (((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) + (27 · 𝐷)))
16 2cn 10968 . . . . . . . 8 2 ∈ ℂ
17 3nn0 11187 . . . . . . . . 9 3 ∈ ℕ0
18 expcl 12740 . . . . . . . . 9 ((𝐵 ∈ ℂ ∧ 3 ∈ ℕ0) → (𝐵↑3) ∈ ℂ)
192, 17, 18sylancl 693 . . . . . . . 8 (𝜑 → (𝐵↑3) ∈ ℂ)
20 mulcl 9899 . . . . . . . 8 ((2 ∈ ℂ ∧ (𝐵↑3) ∈ ℂ) → (2 · (𝐵↑3)) ∈ ℂ)
2116, 19, 20sylancr 694 . . . . . . 7 (𝜑 → (2 · (𝐵↑3)) ∈ ℂ)
22 9cn 10985 . . . . . . . 8 9 ∈ ℂ
232, 5mulcld 9939 . . . . . . . 8 (𝜑 → (𝐵 · 𝐶) ∈ ℂ)
24 mulcl 9899 . . . . . . . 8 ((9 ∈ ℂ ∧ (𝐵 · 𝐶) ∈ ℂ) → (9 · (𝐵 · 𝐶)) ∈ ℂ)
2522, 23, 24sylancr 694 . . . . . . 7 (𝜑 → (9 · (𝐵 · 𝐶)) ∈ ℂ)
2621, 25subcld 10271 . . . . . 6 (𝜑 → ((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) ∈ ℂ)
27 2nn0 11186 . . . . . . . . 9 2 ∈ ℕ0
28 7nn 11067 . . . . . . . . 9 7 ∈ ℕ
2927, 28decnncl 11394 . . . . . . . 8 27 ∈ ℕ
3029nncni 10907 . . . . . . 7 27 ∈ ℂ
31 mcubic.d . . . . . . 7 (𝜑𝐷 ∈ ℂ)
32 mulcl 9899 . . . . . . 7 ((27 ∈ ℂ ∧ 𝐷 ∈ ℂ) → (27 · 𝐷) ∈ ℂ)
3330, 31, 32sylancr 694 . . . . . 6 (𝜑 → (27 · 𝐷) ∈ ℂ)
3426, 33addcld 9938 . . . . 5 (𝜑 → (((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) + (27 · 𝐷)) ∈ ℂ)
3515, 34eqeltrd 2688 . . . 4 (𝜑𝑁 ∈ ℂ)
3630a1i 11 . . . 4 (𝜑27 ∈ ℂ)
3729nnne0i 10932 . . . . 5 27 ≠ 0
3837a1i 11 . . . 4 (𝜑27 ≠ 0)
3935, 36, 38divcld 10680 . . 3 (𝜑 → (𝑁 / 27) ∈ ℂ)
40 mcubic.x . . . 4 (𝜑𝑋 ∈ ℂ)
412, 10, 12divcld 10680 . . . 4 (𝜑 → (𝐵 / 3) ∈ ℂ)
4240, 41addcld 9938 . . 3 (𝜑 → (𝑋 + (𝐵 / 3)) ∈ ℂ)
43 mcubic.t . . . . 5 (𝜑𝑇 ∈ ℂ)
4443, 10, 12divcld 10680 . . . 4 (𝜑 → (𝑇 / 3) ∈ ℂ)
4544negcld 10258 . . 3 (𝜑 → -(𝑇 / 3) ∈ ℂ)
46 3nn 11063 . . . . . 6 3 ∈ ℕ
4746a1i 11 . . . . 5 (𝜑 → 3 ∈ ℕ)
48 2nn 11062 . . . . . . 7 2 ∈ ℕ
49 1nn0 11185 . . . . . . 7 1 ∈ ℕ0
50 1nn 10908 . . . . . . 7 1 ∈ ℕ
51 2t1e2 11053 . . . . . . . . 9 (2 · 1) = 2
5251oveq1i 6559 . . . . . . . 8 ((2 · 1) + 1) = (2 + 1)
53 2p1e3 11028 . . . . . . . 8 (2 + 1) = 3
5452, 53eqtri 2632 . . . . . . 7 ((2 · 1) + 1) = 3
55 1lt2 11071 . . . . . . 7 1 < 2
5648, 49, 50, 54, 55ndvdsi 14974 . . . . . 6 ¬ 2 ∥ 3
5756a1i 11 . . . . 5 (𝜑 → ¬ 2 ∥ 3)
58 oexpneg 14907 . . . . 5 (((𝑇 / 3) ∈ ℂ ∧ 3 ∈ ℕ ∧ ¬ 2 ∥ 3) → (-(𝑇 / 3)↑3) = -((𝑇 / 3)↑3))
5944, 47, 57, 58syl3anc 1318 . . . 4 (𝜑 → (-(𝑇 / 3)↑3) = -((𝑇 / 3)↑3))
6017a1i 11 . . . . . . 7 (𝜑 → 3 ∈ ℕ0)
6143, 10, 12, 60expdivd 12884 . . . . . 6 (𝜑 → ((𝑇 / 3)↑3) = ((𝑇↑3) / (3↑3)))
62 mcubic.3 . . . . . . 7 (𝜑 → (𝑇↑3) = ((𝑁 + 𝐺) / 2))
63 3exp3 15636 . . . . . . . 8 (3↑3) = 27
6463a1i 11 . . . . . . 7 (𝜑 → (3↑3) = 27)
6562, 64oveq12d 6567 . . . . . 6 (𝜑 → ((𝑇↑3) / (3↑3)) = (((𝑁 + 𝐺) / 2) / 27))
66 mcubic.g . . . . . . . . 9 (𝜑𝐺 ∈ ℂ)
6735, 66addcld 9938 . . . . . . . 8 (𝜑 → (𝑁 + 𝐺) ∈ ℂ)
68 2cnd 10970 . . . . . . . 8 (𝜑 → 2 ∈ ℂ)
69 2ne0 10990 . . . . . . . . 9 2 ≠ 0
7069a1i 11 . . . . . . . 8 (𝜑 → 2 ≠ 0)
7167, 68, 36, 70, 38divdiv32d 10705 . . . . . . 7 (𝜑 → (((𝑁 + 𝐺) / 2) / 27) = (((𝑁 + 𝐺) / 27) / 2))
7235, 66addcomd 10117 . . . . . . . . . 10 (𝜑 → (𝑁 + 𝐺) = (𝐺 + 𝑁))
7372oveq1d 6564 . . . . . . . . 9 (𝜑 → ((𝑁 + 𝐺) / 27) = ((𝐺 + 𝑁) / 27))
7466, 35, 36, 38divdird 10718 . . . . . . . . 9 (𝜑 → ((𝐺 + 𝑁) / 27) = ((𝐺 / 27) + (𝑁 / 27)))
7573, 74eqtrd 2644 . . . . . . . 8 (𝜑 → ((𝑁 + 𝐺) / 27) = ((𝐺 / 27) + (𝑁 / 27)))
7675oveq1d 6564 . . . . . . 7 (𝜑 → (((𝑁 + 𝐺) / 27) / 2) = (((𝐺 / 27) + (𝑁 / 27)) / 2))
7766, 36, 38divcld 10680 . . . . . . . 8 (𝜑 → (𝐺 / 27) ∈ ℂ)
7877, 39, 68, 70divdird 10718 . . . . . . 7 (𝜑 → (((𝐺 / 27) + (𝑁 / 27)) / 2) = (((𝐺 / 27) / 2) + ((𝑁 / 27) / 2)))
7971, 76, 783eqtrd 2648 . . . . . 6 (𝜑 → (((𝑁 + 𝐺) / 2) / 27) = (((𝐺 / 27) / 2) + ((𝑁 / 27) / 2)))
8061, 65, 793eqtrd 2648 . . . . 5 (𝜑 → ((𝑇 / 3)↑3) = (((𝐺 / 27) / 2) + ((𝑁 / 27) / 2)))
8180negeqd 10154 . . . 4 (𝜑 → -((𝑇 / 3)↑3) = -(((𝐺 / 27) / 2) + ((𝑁 / 27) / 2)))
8277halfcld 11154 . . . . 5 (𝜑 → ((𝐺 / 27) / 2) ∈ ℂ)
8339halfcld 11154 . . . . 5 (𝜑 → ((𝑁 / 27) / 2) ∈ ℂ)
8482, 83negdi2d 10285 . . . 4 (𝜑 → -(((𝐺 / 27) / 2) + ((𝑁 / 27) / 2)) = (-((𝐺 / 27) / 2) − ((𝑁 / 27) / 2)))
8559, 81, 843eqtrd 2648 . . 3 (𝜑 → (-(𝑇 / 3)↑3) = (-((𝐺 / 27) / 2) − ((𝑁 / 27) / 2)))
8682negcld 10258 . . 3 (𝜑 → -((𝐺 / 27) / 2) ∈ ℂ)
87 sqneg 12785 . . . . 5 (((𝐺 / 27) / 2) ∈ ℂ → (-((𝐺 / 27) / 2)↑2) = (((𝐺 / 27) / 2)↑2))
8882, 87syl 17 . . . 4 (𝜑 → (-((𝐺 / 27) / 2)↑2) = (((𝐺 / 27) / 2)↑2))
8977, 68, 70sqdivd 12883 . . . 4 (𝜑 → (((𝐺 / 27) / 2)↑2) = (((𝐺 / 27)↑2) / (2↑2)))
9039, 68, 70sqdivd 12883 . . . . . . . 8 (𝜑 → (((𝑁 / 27) / 2)↑2) = (((𝑁 / 27)↑2) / (2↑2)))
9135, 36, 38sqdivd 12883 . . . . . . . . 9 (𝜑 → ((𝑁 / 27)↑2) = ((𝑁↑2) / (27↑2)))
9291oveq1d 6564 . . . . . . . 8 (𝜑 → (((𝑁 / 27)↑2) / (2↑2)) = (((𝑁↑2) / (27↑2)) / (2↑2)))
9390, 92eqtr2d 2645 . . . . . . 7 (𝜑 → (((𝑁↑2) / (27↑2)) / (2↑2)) = (((𝑁 / 27) / 2)↑2))
94 4cn 10975 . . . . . . . . . . . 12 4 ∈ ℂ
9594a1i 11 . . . . . . . . . . 11 (𝜑 → 4 ∈ ℂ)
96 expcl 12740 . . . . . . . . . . . 12 ((𝑀 ∈ ℂ ∧ 3 ∈ ℕ0) → (𝑀↑3) ∈ ℂ)
979, 17, 96sylancl 693 . . . . . . . . . . 11 (𝜑 → (𝑀↑3) ∈ ℂ)
9830sqcli 12806 . . . . . . . . . . . 12 (27↑2) ∈ ℂ
9998a1i 11 . . . . . . . . . . 11 (𝜑 → (27↑2) ∈ ℂ)
100 sqne0 12792 . . . . . . . . . . . . 13 (27 ∈ ℂ → ((27↑2) ≠ 0 ↔ 27 ≠ 0))
10136, 100syl 17 . . . . . . . . . . . 12 (𝜑 → ((27↑2) ≠ 0 ↔ 27 ≠ 0))
10238, 101mpbird 246 . . . . . . . . . . 11 (𝜑 → (27↑2) ≠ 0)
10395, 97, 99, 102divassd 10715 . . . . . . . . . 10 (𝜑 → ((4 · (𝑀↑3)) / (27↑2)) = (4 · ((𝑀↑3) / (27↑2))))
10422a1i 11 . . . . . . . . . . . . 13 (𝜑 → 9 ∈ ℂ)
105 9nn 11069 . . . . . . . . . . . . . . 15 9 ∈ ℕ
106105nnne0i 10932 . . . . . . . . . . . . . 14 9 ≠ 0
107106a1i 11 . . . . . . . . . . . . 13 (𝜑 → 9 ≠ 0)
1089, 104, 107, 60expdivd 12884 . . . . . . . . . . . 12 (𝜑 → ((𝑀 / 9)↑3) = ((𝑀↑3) / (9↑3)))
10916, 4mulcomi 9925 . . . . . . . . . . . . . . . 16 (2 · 3) = (3 · 2)
110109oveq2i 6560 . . . . . . . . . . . . . . 15 (3↑(2 · 3)) = (3↑(3 · 2))
111 expmul 12767 . . . . . . . . . . . . . . . 16 ((3 ∈ ℂ ∧ 2 ∈ ℕ0 ∧ 3 ∈ ℕ0) → (3↑(2 · 3)) = ((3↑2)↑3))
1124, 27, 17, 111mp3an 1416 . . . . . . . . . . . . . . 15 (3↑(2 · 3)) = ((3↑2)↑3)
113 expmul 12767 . . . . . . . . . . . . . . . 16 ((3 ∈ ℂ ∧ 3 ∈ ℕ0 ∧ 2 ∈ ℕ0) → (3↑(3 · 2)) = ((3↑3)↑2))
1144, 17, 27, 113mp3an 1416 . . . . . . . . . . . . . . 15 (3↑(3 · 2)) = ((3↑3)↑2)
115110, 112, 1143eqtr3i 2640 . . . . . . . . . . . . . 14 ((3↑2)↑3) = ((3↑3)↑2)
116 sq3 12823 . . . . . . . . . . . . . . 15 (3↑2) = 9
117116oveq1i 6559 . . . . . . . . . . . . . 14 ((3↑2)↑3) = (9↑3)
11863oveq1i 6559 . . . . . . . . . . . . . 14 ((3↑3)↑2) = (27↑2)
119115, 117, 1183eqtr3i 2640 . . . . . . . . . . . . 13 (9↑3) = (27↑2)
120119oveq2i 6560 . . . . . . . . . . . 12 ((𝑀↑3) / (9↑3)) = ((𝑀↑3) / (27↑2))
121108, 120syl6eq 2660 . . . . . . . . . . 11 (𝜑 → ((𝑀 / 9)↑3) = ((𝑀↑3) / (27↑2)))
122121oveq2d 6565 . . . . . . . . . 10 (𝜑 → (4 · ((𝑀 / 9)↑3)) = (4 · ((𝑀↑3) / (27↑2))))
123103, 122eqtr4d 2647 . . . . . . . . 9 (𝜑 → ((4 · (𝑀↑3)) / (27↑2)) = (4 · ((𝑀 / 9)↑3)))
124123oveq1d 6564 . . . . . . . 8 (𝜑 → (((4 · (𝑀↑3)) / (27↑2)) / (2↑2)) = ((4 · ((𝑀 / 9)↑3)) / (2↑2)))
125 sq2 12822 . . . . . . . . . 10 (2↑2) = 4
126125oveq2i 6560 . . . . . . . . 9 ((4 · ((𝑀 / 9)↑3)) / (2↑2)) = ((4 · ((𝑀 / 9)↑3)) / 4)
1279, 104, 107divcld 10680 . . . . . . . . . . 11 (𝜑 → (𝑀 / 9) ∈ ℂ)
128 expcl 12740 . . . . . . . . . . 11 (((𝑀 / 9) ∈ ℂ ∧ 3 ∈ ℕ0) → ((𝑀 / 9)↑3) ∈ ℂ)
129127, 17, 128sylancl 693 . . . . . . . . . 10 (𝜑 → ((𝑀 / 9)↑3) ∈ ℂ)
130 4ne0 10994 . . . . . . . . . . 11 4 ≠ 0
131130a1i 11 . . . . . . . . . 10 (𝜑 → 4 ≠ 0)
132129, 95, 131divcan3d 10685 . . . . . . . . 9 (𝜑 → ((4 · ((𝑀 / 9)↑3)) / 4) = ((𝑀 / 9)↑3))
133126, 132syl5eq 2656 . . . . . . . 8 (𝜑 → ((4 · ((𝑀 / 9)↑3)) / (2↑2)) = ((𝑀 / 9)↑3))
134124, 133eqtrd 2644 . . . . . . 7 (𝜑 → (((4 · (𝑀↑3)) / (27↑2)) / (2↑2)) = ((𝑀 / 9)↑3))
13593, 134oveq12d 6567 . . . . . 6 (𝜑 → ((((𝑁↑2) / (27↑2)) / (2↑2)) − (((4 · (𝑀↑3)) / (27↑2)) / (2↑2))) = ((((𝑁 / 27) / 2)↑2) − ((𝑀 / 9)↑3)))
13635sqcld 12868 . . . . . . . 8 (𝜑 → (𝑁↑2) ∈ ℂ)
137136, 99, 102divcld 10680 . . . . . . 7 (𝜑 → ((𝑁↑2) / (27↑2)) ∈ ℂ)
138 mulcl 9899 . . . . . . . . 9 ((4 ∈ ℂ ∧ (𝑀↑3) ∈ ℂ) → (4 · (𝑀↑3)) ∈ ℂ)
13994, 97, 138sylancr 694 . . . . . . . 8 (𝜑 → (4 · (𝑀↑3)) ∈ ℂ)
140139, 99, 102divcld 10680 . . . . . . 7 (𝜑 → ((4 · (𝑀↑3)) / (27↑2)) ∈ ℂ)
14116sqcli 12806 . . . . . . . 8 (2↑2) ∈ ℂ
142141a1i 11 . . . . . . 7 (𝜑 → (2↑2) ∈ ℂ)
143125, 130eqnetri 2852 . . . . . . . 8 (2↑2) ≠ 0
144143a1i 11 . . . . . . 7 (𝜑 → (2↑2) ≠ 0)
145137, 140, 142, 144divsubdird 10719 . . . . . 6 (𝜑 → ((((𝑁↑2) / (27↑2)) − ((4 · (𝑀↑3)) / (27↑2))) / (2↑2)) = ((((𝑁↑2) / (27↑2)) / (2↑2)) − (((4 · (𝑀↑3)) / (27↑2)) / (2↑2))))
14683sqcld 12868 . . . . . . 7 (𝜑 → (((𝑁 / 27) / 2)↑2) ∈ ℂ)
147146, 129negsubd 10277 . . . . . 6 (𝜑 → ((((𝑁 / 27) / 2)↑2) + -((𝑀 / 9)↑3)) = ((((𝑁 / 27) / 2)↑2) − ((𝑀 / 9)↑3)))
148135, 145, 1473eqtr4d 2654 . . . . 5 (𝜑 → ((((𝑁↑2) / (27↑2)) − ((4 · (𝑀↑3)) / (27↑2))) / (2↑2)) = ((((𝑁 / 27) / 2)↑2) + -((𝑀 / 9)↑3)))
14966, 36, 38sqdivd 12883 . . . . . . 7 (𝜑 → ((𝐺 / 27)↑2) = ((𝐺↑2) / (27↑2)))
150 mcubic.2 . . . . . . . 8 (𝜑 → (𝐺↑2) = ((𝑁↑2) − (4 · (𝑀↑3))))
151150oveq1d 6564 . . . . . . 7 (𝜑 → ((𝐺↑2) / (27↑2)) = (((𝑁↑2) − (4 · (𝑀↑3))) / (27↑2)))
152136, 139, 99, 102divsubdird 10719 . . . . . . 7 (𝜑 → (((𝑁↑2) − (4 · (𝑀↑3))) / (27↑2)) = (((𝑁↑2) / (27↑2)) − ((4 · (𝑀↑3)) / (27↑2))))
153149, 151, 1523eqtrd 2648 . . . . . 6 (𝜑 → ((𝐺 / 27)↑2) = (((𝑁↑2) / (27↑2)) − ((4 · (𝑀↑3)) / (27↑2))))
154153oveq1d 6564 . . . . 5 (𝜑 → (((𝐺 / 27)↑2) / (2↑2)) = ((((𝑁↑2) / (27↑2)) − ((4 · (𝑀↑3)) / (27↑2))) / (2↑2)))
155 oexpneg 14907 . . . . . . 7 (((𝑀 / 9) ∈ ℂ ∧ 3 ∈ ℕ ∧ ¬ 2 ∥ 3) → (-(𝑀 / 9)↑3) = -((𝑀 / 9)↑3))
156127, 47, 57, 155syl3anc 1318 . . . . . 6 (𝜑 → (-(𝑀 / 9)↑3) = -((𝑀 / 9)↑3))
157156oveq2d 6565 . . . . 5 (𝜑 → ((((𝑁 / 27) / 2)↑2) + (-(𝑀 / 9)↑3)) = ((((𝑁 / 27) / 2)↑2) + -((𝑀 / 9)↑3)))
158148, 154, 1573eqtr4d 2654 . . . 4 (𝜑 → (((𝐺 / 27)↑2) / (2↑2)) = ((((𝑁 / 27) / 2)↑2) + (-(𝑀 / 9)↑3)))
15988, 89, 1583eqtrd 2648 . . 3 (𝜑 → (-((𝐺 / 27) / 2)↑2) = ((((𝑁 / 27) / 2)↑2) + (-(𝑀 / 9)↑3)))
1609, 10, 10, 12, 12divdiv1d 10711 . . . . . 6 (𝜑 → ((𝑀 / 3) / 3) = (𝑀 / (3 · 3)))
161 3t3e9 11057 . . . . . . 7 (3 · 3) = 9
162161oveq2i 6560 . . . . . 6 (𝑀 / (3 · 3)) = (𝑀 / 9)
163160, 162syl6eq 2660 . . . . 5 (𝜑 → ((𝑀 / 3) / 3) = (𝑀 / 9))
164163negeqd 10154 . . . 4 (𝜑 → -((𝑀 / 3) / 3) = -(𝑀 / 9))
16513, 10, 12divnegd 10693 . . . 4 (𝜑 → -((𝑀 / 3) / 3) = (-(𝑀 / 3) / 3))
166164, 165eqtr3d 2646 . . 3 (𝜑 → -(𝑀 / 9) = (-(𝑀 / 3) / 3))
167 eqidd 2611 . . 3 (𝜑 → ((𝑁 / 27) / 2) = ((𝑁 / 27) / 2))
168 mcubic.0 . . . . 5 (𝜑𝑇 ≠ 0)
16943, 10, 168, 12divne0d 10696 . . . 4 (𝜑 → (𝑇 / 3) ≠ 0)
17044, 169negne0d 10269 . . 3 (𝜑 → -(𝑇 / 3) ≠ 0)
17114, 39, 42, 45, 85, 86, 159, 166, 167, 170dcubic 24373 . 2 (𝜑 → ((((𝑋 + (𝐵 / 3))↑3) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27))) = 0 ↔ ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ (𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))))))
172 binom3 12847 . . . . . . 7 ((𝑋 ∈ ℂ ∧ (𝐵 / 3) ∈ ℂ) → ((𝑋 + (𝐵 / 3))↑3) = (((𝑋↑3) + (3 · ((𝑋↑2) · (𝐵 / 3)))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))))
17340, 41, 172syl2anc 691 . . . . . 6 (𝜑 → ((𝑋 + (𝐵 / 3))↑3) = (((𝑋↑3) + (3 · ((𝑋↑2) · (𝐵 / 3)))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))))
17440sqcld 12868 . . . . . . . . . 10 (𝜑 → (𝑋↑2) ∈ ℂ)
17510, 174, 41mul12d 10124 . . . . . . . . 9 (𝜑 → (3 · ((𝑋↑2) · (𝐵 / 3))) = ((𝑋↑2) · (3 · (𝐵 / 3))))
1762, 10, 12divcan2d 10682 . . . . . . . . . 10 (𝜑 → (3 · (𝐵 / 3)) = 𝐵)
177176oveq2d 6565 . . . . . . . . 9 (𝜑 → ((𝑋↑2) · (3 · (𝐵 / 3))) = ((𝑋↑2) · 𝐵))
178174, 2mulcomd 9940 . . . . . . . . 9 (𝜑 → ((𝑋↑2) · 𝐵) = (𝐵 · (𝑋↑2)))
179175, 177, 1783eqtrd 2648 . . . . . . . 8 (𝜑 → (3 · ((𝑋↑2) · (𝐵 / 3))) = (𝐵 · (𝑋↑2)))
180179oveq2d 6565 . . . . . . 7 (𝜑 → ((𝑋↑3) + (3 · ((𝑋↑2) · (𝐵 / 3)))) = ((𝑋↑3) + (𝐵 · (𝑋↑2))))
181180oveq1d 6564 . . . . . 6 (𝜑 → (((𝑋↑3) + (3 · ((𝑋↑2) · (𝐵 / 3)))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))) = (((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))))
182173, 181eqtrd 2644 . . . . 5 (𝜑 → ((𝑋 + (𝐵 / 3))↑3) = (((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))))
183182oveq1d 6564 . . . 4 (𝜑 → (((𝑋 + (𝐵 / 3))↑3) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27))) = ((((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27))))
184 expcl 12740 . . . . . . 7 ((𝑋 ∈ ℂ ∧ 3 ∈ ℕ0) → (𝑋↑3) ∈ ℂ)
18540, 17, 184sylancl 693 . . . . . 6 (𝜑 → (𝑋↑3) ∈ ℂ)
1862, 174mulcld 9939 . . . . . 6 (𝜑 → (𝐵 · (𝑋↑2)) ∈ ℂ)
187185, 186addcld 9938 . . . . 5 (𝜑 → ((𝑋↑3) + (𝐵 · (𝑋↑2))) ∈ ℂ)
18841sqcld 12868 . . . . . . . 8 (𝜑 → ((𝐵 / 3)↑2) ∈ ℂ)
18940, 188mulcld 9939 . . . . . . 7 (𝜑 → (𝑋 · ((𝐵 / 3)↑2)) ∈ ℂ)
19010, 189mulcld 9939 . . . . . 6 (𝜑 → (3 · (𝑋 · ((𝐵 / 3)↑2))) ∈ ℂ)
191 expcl 12740 . . . . . . 7 (((𝐵 / 3) ∈ ℂ ∧ 3 ∈ ℕ0) → ((𝐵 / 3)↑3) ∈ ℂ)
19241, 17, 191sylancl 693 . . . . . 6 (𝜑 → ((𝐵 / 3)↑3) ∈ ℂ)
193190, 192addcld 9938 . . . . 5 (𝜑 → ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) ∈ ℂ)
19414, 42mulcld 9939 . . . . . 6 (𝜑 → (-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) ∈ ℂ)
195194, 39addcld 9938 . . . . 5 (𝜑 → ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27)) ∈ ℂ)
196187, 193, 195addassd 9941 . . . 4 (𝜑 → ((((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27))) = (((𝑋↑3) + (𝐵 · (𝑋↑2))) + (((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27)))))
19714, 40, 41adddid 9943 . . . . . . . . . 10 (𝜑 → (-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) = ((-(𝑀 / 3) · 𝑋) + (-(𝑀 / 3) · (𝐵 / 3))))
198197oveq1d 6564 . . . . . . . . 9 (𝜑 → ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27)) = (((-(𝑀 / 3) · 𝑋) + (-(𝑀 / 3) · (𝐵 / 3))) + (𝑁 / 27)))
19914, 40mulcld 9939 . . . . . . . . . 10 (𝜑 → (-(𝑀 / 3) · 𝑋) ∈ ℂ)
20014, 41mulcld 9939 . . . . . . . . . 10 (𝜑 → (-(𝑀 / 3) · (𝐵 / 3)) ∈ ℂ)
201199, 200, 39addassd 9941 . . . . . . . . 9 (𝜑 → (((-(𝑀 / 3) · 𝑋) + (-(𝑀 / 3) · (𝐵 / 3))) + (𝑁 / 27)) = ((-(𝑀 / 3) · 𝑋) + ((-(𝑀 / 3) · (𝐵 / 3)) + (𝑁 / 27))))
2021oveq1d 6564 . . . . . . . . . . . . . . 15 (𝜑 → (𝑀 / 3) = (((𝐵↑2) − (3 · 𝐶)) / 3))
2033, 7, 10, 12divsubdird 10719 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐵↑2) − (3 · 𝐶)) / 3) = (((𝐵↑2) / 3) − ((3 · 𝐶) / 3)))
2045, 10, 12divcan3d 10685 . . . . . . . . . . . . . . . 16 (𝜑 → ((3 · 𝐶) / 3) = 𝐶)
205204oveq2d 6565 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐵↑2) / 3) − ((3 · 𝐶) / 3)) = (((𝐵↑2) / 3) − 𝐶))
206202, 203, 2053eqtrd 2648 . . . . . . . . . . . . . 14 (𝜑 → (𝑀 / 3) = (((𝐵↑2) / 3) − 𝐶))
207206negeqd 10154 . . . . . . . . . . . . 13 (𝜑 → -(𝑀 / 3) = -(((𝐵↑2) / 3) − 𝐶))
2083, 10, 12divcld 10680 . . . . . . . . . . . . . 14 (𝜑 → ((𝐵↑2) / 3) ∈ ℂ)
209208, 5negsubdi2d 10287 . . . . . . . . . . . . 13 (𝜑 → -(((𝐵↑2) / 3) − 𝐶) = (𝐶 − ((𝐵↑2) / 3)))
210207, 209eqtrd 2644 . . . . . . . . . . . 12 (𝜑 → -(𝑀 / 3) = (𝐶 − ((𝐵↑2) / 3)))
211210oveq1d 6564 . . . . . . . . . . 11 (𝜑 → (-(𝑀 / 3) · 𝑋) = ((𝐶 − ((𝐵↑2) / 3)) · 𝑋))
2125, 208, 40subdird 10366 . . . . . . . . . . 11 (𝜑 → ((𝐶 − ((𝐵↑2) / 3)) · 𝑋) = ((𝐶 · 𝑋) − (((𝐵↑2) / 3) · 𝑋)))
213208, 40mulcomd 9940 . . . . . . . . . . . . 13 (𝜑 → (((𝐵↑2) / 3) · 𝑋) = (𝑋 · ((𝐵↑2) / 3)))
2144sqvali 12805 . . . . . . . . . . . . . . . . . 18 (3↑2) = (3 · 3)
215214oveq2i 6560 . . . . . . . . . . . . . . . . 17 ((𝐵↑2) / (3↑2)) = ((𝐵↑2) / (3 · 3))
2162, 10, 12sqdivd 12883 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐵 / 3)↑2) = ((𝐵↑2) / (3↑2)))
2173, 10, 10, 12, 12divdiv1d 10711 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝐵↑2) / 3) / 3) = ((𝐵↑2) / (3 · 3)))
218215, 216, 2173eqtr4a 2670 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐵 / 3)↑2) = (((𝐵↑2) / 3) / 3))
219218oveq2d 6565 . . . . . . . . . . . . . . 15 (𝜑 → (3 · ((𝐵 / 3)↑2)) = (3 · (((𝐵↑2) / 3) / 3)))
220208, 10, 12divcan2d 10682 . . . . . . . . . . . . . . 15 (𝜑 → (3 · (((𝐵↑2) / 3) / 3)) = ((𝐵↑2) / 3))
221219, 220eqtrd 2644 . . . . . . . . . . . . . 14 (𝜑 → (3 · ((𝐵 / 3)↑2)) = ((𝐵↑2) / 3))
222221oveq2d 6565 . . . . . . . . . . . . 13 (𝜑 → (𝑋 · (3 · ((𝐵 / 3)↑2))) = (𝑋 · ((𝐵↑2) / 3)))
22340, 10, 188mul12d 10124 . . . . . . . . . . . . 13 (𝜑 → (𝑋 · (3 · ((𝐵 / 3)↑2))) = (3 · (𝑋 · ((𝐵 / 3)↑2))))
224213, 222, 2233eqtr2d 2650 . . . . . . . . . . . 12 (𝜑 → (((𝐵↑2) / 3) · 𝑋) = (3 · (𝑋 · ((𝐵 / 3)↑2))))
225224oveq2d 6565 . . . . . . . . . . 11 (𝜑 → ((𝐶 · 𝑋) − (((𝐵↑2) / 3) · 𝑋)) = ((𝐶 · 𝑋) − (3 · (𝑋 · ((𝐵 / 3)↑2)))))
226211, 212, 2253eqtrd 2648 . . . . . . . . . 10 (𝜑 → (-(𝑀 / 3) · 𝑋) = ((𝐶 · 𝑋) − (3 · (𝑋 · ((𝐵 / 3)↑2)))))
227210oveq1d 6564 . . . . . . . . . . . . 13 (𝜑 → (-(𝑀 / 3) · (𝐵 / 3)) = ((𝐶 − ((𝐵↑2) / 3)) · (𝐵 / 3)))
2285, 208, 41subdird 10366 . . . . . . . . . . . . 13 (𝜑 → ((𝐶 − ((𝐵↑2) / 3)) · (𝐵 / 3)) = ((𝐶 · (𝐵 / 3)) − (((𝐵↑2) / 3) · (𝐵 / 3))))
2295, 2, 10, 12divassd 10715 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐶 · 𝐵) / 3) = (𝐶 · (𝐵 / 3)))
2305, 2mulcomd 9940 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐶 · 𝐵) = (𝐵 · 𝐶))
231230oveq1d 6564 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐶 · 𝐵) / 3) = ((𝐵 · 𝐶) / 3))
232229, 231eqtr3d 2646 . . . . . . . . . . . . . 14 (𝜑 → (𝐶 · (𝐵 / 3)) = ((𝐵 · 𝐶) / 3))
2333, 10, 2, 10, 12, 12divmuldivd 10721 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐵↑2) / 3) · (𝐵 / 3)) = (((𝐵↑2) · 𝐵) / (3 · 3)))
234 df-3 10957 . . . . . . . . . . . . . . . . . 18 3 = (2 + 1)
235234oveq2i 6560 . . . . . . . . . . . . . . . . 17 (𝐵↑3) = (𝐵↑(2 + 1))
236 expp1 12729 . . . . . . . . . . . . . . . . . 18 ((𝐵 ∈ ℂ ∧ 2 ∈ ℕ0) → (𝐵↑(2 + 1)) = ((𝐵↑2) · 𝐵))
2372, 27, 236sylancl 693 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵↑(2 + 1)) = ((𝐵↑2) · 𝐵))
238235, 237syl5req 2657 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐵↑2) · 𝐵) = (𝐵↑3))
239161a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → (3 · 3) = 9)
240238, 239oveq12d 6567 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐵↑2) · 𝐵) / (3 · 3)) = ((𝐵↑3) / 9))
241233, 240eqtrd 2644 . . . . . . . . . . . . . 14 (𝜑 → (((𝐵↑2) / 3) · (𝐵 / 3)) = ((𝐵↑3) / 9))
242232, 241oveq12d 6567 . . . . . . . . . . . . 13 (𝜑 → ((𝐶 · (𝐵 / 3)) − (((𝐵↑2) / 3) · (𝐵 / 3))) = (((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)))
243227, 228, 2423eqtrd 2648 . . . . . . . . . . . 12 (𝜑 → (-(𝑀 / 3) · (𝐵 / 3)) = (((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)))
24415oveq1d 6564 . . . . . . . . . . . . 13 (𝜑 → (𝑁 / 27) = ((((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) + (27 · 𝐷)) / 27))
24526, 33, 36, 38divdird 10718 . . . . . . . . . . . . 13 (𝜑 → ((((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) + (27 · 𝐷)) / 27) = ((((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) / 27) + ((27 · 𝐷) / 27)))
24621, 25, 36, 38divsubdird 10719 . . . . . . . . . . . . . . 15 (𝜑 → (((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) / 27) = (((2 · (𝐵↑3)) / 27) − ((9 · (𝐵 · 𝐶)) / 27)))
247 9t3e27 11540 . . . . . . . . . . . . . . . . . 18 (9 · 3) = 27
248247oveq2i 6560 . . . . . . . . . . . . . . . . 17 ((9 · (𝐵 · 𝐶)) / (9 · 3)) = ((9 · (𝐵 · 𝐶)) / 27)
24923, 10, 104, 12, 107divcan5d 10706 . . . . . . . . . . . . . . . . 17 (𝜑 → ((9 · (𝐵 · 𝐶)) / (9 · 3)) = ((𝐵 · 𝐶) / 3))
250248, 249syl5eqr 2658 . . . . . . . . . . . . . . . 16 (𝜑 → ((9 · (𝐵 · 𝐶)) / 27) = ((𝐵 · 𝐶) / 3))
251250oveq2d 6565 . . . . . . . . . . . . . . 15 (𝜑 → (((2 · (𝐵↑3)) / 27) − ((9 · (𝐵 · 𝐶)) / 27)) = (((2 · (𝐵↑3)) / 27) − ((𝐵 · 𝐶) / 3)))
252246, 251eqtrd 2644 . . . . . . . . . . . . . 14 (𝜑 → (((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) / 27) = (((2 · (𝐵↑3)) / 27) − ((𝐵 · 𝐶) / 3)))
25331, 36, 38divcan3d 10685 . . . . . . . . . . . . . 14 (𝜑 → ((27 · 𝐷) / 27) = 𝐷)
254252, 253oveq12d 6567 . . . . . . . . . . . . 13 (𝜑 → ((((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) / 27) + ((27 · 𝐷) / 27)) = ((((2 · (𝐵↑3)) / 27) − ((𝐵 · 𝐶) / 3)) + 𝐷))
255244, 245, 2543eqtrd 2648 . . . . . . . . . . . 12 (𝜑 → (𝑁 / 27) = ((((2 · (𝐵↑3)) / 27) − ((𝐵 · 𝐶) / 3)) + 𝐷))
256243, 255oveq12d 6567 . . . . . . . . . . 11 (𝜑 → ((-(𝑀 / 3) · (𝐵 / 3)) + (𝑁 / 27)) = ((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + ((((2 · (𝐵↑3)) / 27) − ((𝐵 · 𝐶) / 3)) + 𝐷)))
25719, 104, 107divcld 10680 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐵↑3) / 9) ∈ ℂ)
25821, 36, 38divcld 10680 . . . . . . . . . . . . . . 15 (𝜑 → ((2 · (𝐵↑3)) / 27) ∈ ℂ)
259257, 258negsubdi2d 10287 . . . . . . . . . . . . . 14 (𝜑 → -(((𝐵↑3) / 9) − ((2 · (𝐵↑3)) / 27)) = (((2 · (𝐵↑3)) / 27) − ((𝐵↑3) / 9)))
2602, 10, 12, 60expdivd 12884 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐵 / 3)↑3) = ((𝐵↑3) / (3↑3)))
26163oveq2i 6560 . . . . . . . . . . . . . . . . 17 ((𝐵↑3) / (3↑3)) = ((𝐵↑3) / 27)
262 ax-1cn 9873 . . . . . . . . . . . . . . . . . . . . . . 23 1 ∈ ℂ
2634, 16, 262, 53subaddrii 10249 . . . . . . . . . . . . . . . . . . . . . 22 (3 − 2) = 1
264263oveq1i 6559 . . . . . . . . . . . . . . . . . . . . 21 ((3 − 2) · (𝐵↑3)) = (1 · (𝐵↑3))
26519mulid2d 9937 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (1 · (𝐵↑3)) = (𝐵↑3))
266264, 265syl5eq 2656 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((3 − 2) · (𝐵↑3)) = (𝐵↑3))
26710, 68, 19subdird 10366 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((3 − 2) · (𝐵↑3)) = ((3 · (𝐵↑3)) − (2 · (𝐵↑3))))
268266, 267eqtr3d 2646 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐵↑3) = ((3 · (𝐵↑3)) − (2 · (𝐵↑3))))
269268oveq1d 6564 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐵↑3) / 27) = (((3 · (𝐵↑3)) − (2 · (𝐵↑3))) / 27))
270 mulcl 9899 . . . . . . . . . . . . . . . . . . . 20 ((3 ∈ ℂ ∧ (𝐵↑3) ∈ ℂ) → (3 · (𝐵↑3)) ∈ ℂ)
2714, 19, 270sylancr 694 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (3 · (𝐵↑3)) ∈ ℂ)
272271, 21, 36, 38divsubdird 10719 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((3 · (𝐵↑3)) − (2 · (𝐵↑3))) / 27) = (((3 · (𝐵↑3)) / 27) − ((2 · (𝐵↑3)) / 27)))
273269, 272eqtrd 2644 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐵↑3) / 27) = (((3 · (𝐵↑3)) / 27) − ((2 · (𝐵↑3)) / 27)))
274261, 273syl5eq 2656 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐵↑3) / (3↑3)) = (((3 · (𝐵↑3)) / 27) − ((2 · (𝐵↑3)) / 27)))
27522, 4, 247mulcomli 9926 . . . . . . . . . . . . . . . . . . 19 (3 · 9) = 27
276275oveq2i 6560 . . . . . . . . . . . . . . . . . 18 ((3 · (𝐵↑3)) / (3 · 9)) = ((3 · (𝐵↑3)) / 27)
27719, 104, 10, 107, 12divcan5d 10706 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((3 · (𝐵↑3)) / (3 · 9)) = ((𝐵↑3) / 9))
278276, 277syl5eqr 2658 . . . . . . . . . . . . . . . . 17 (𝜑 → ((3 · (𝐵↑3)) / 27) = ((𝐵↑3) / 9))
279278oveq1d 6564 . . . . . . . . . . . . . . . 16 (𝜑 → (((3 · (𝐵↑3)) / 27) − ((2 · (𝐵↑3)) / 27)) = (((𝐵↑3) / 9) − ((2 · (𝐵↑3)) / 27)))
280260, 274, 2793eqtrd 2648 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐵 / 3)↑3) = (((𝐵↑3) / 9) − ((2 · (𝐵↑3)) / 27)))
281280negeqd 10154 . . . . . . . . . . . . . 14 (𝜑 → -((𝐵 / 3)↑3) = -(((𝐵↑3) / 9) − ((2 · (𝐵↑3)) / 27)))
28223, 10, 12divcld 10680 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐵 · 𝐶) / 3) ∈ ℂ)
283282, 257, 258npncan3d 10307 . . . . . . . . . . . . . 14 (𝜑 → ((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + (((2 · (𝐵↑3)) / 27) − ((𝐵 · 𝐶) / 3))) = (((2 · (𝐵↑3)) / 27) − ((𝐵↑3) / 9)))
284259, 281, 2833eqtr4d 2654 . . . . . . . . . . . . 13 (𝜑 → -((𝐵 / 3)↑3) = ((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + (((2 · (𝐵↑3)) / 27) − ((𝐵 · 𝐶) / 3))))
285284oveq1d 6564 . . . . . . . . . . . 12 (𝜑 → (-((𝐵 / 3)↑3) + 𝐷) = (((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + (((2 · (𝐵↑3)) / 27) − ((𝐵 · 𝐶) / 3))) + 𝐷))
286192negcld 10258 . . . . . . . . . . . . 13 (𝜑 → -((𝐵 / 3)↑3) ∈ ℂ)
287286, 31addcomd 10117 . . . . . . . . . . . 12 (𝜑 → (-((𝐵 / 3)↑3) + 𝐷) = (𝐷 + -((𝐵 / 3)↑3)))
288243, 200eqeltrrd 2689 . . . . . . . . . . . . 13 (𝜑 → (((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) ∈ ℂ)
289258, 282subcld 10271 . . . . . . . . . . . . 13 (𝜑 → (((2 · (𝐵↑3)) / 27) − ((𝐵 · 𝐶) / 3)) ∈ ℂ)
290288, 289, 31addassd 9941 . . . . . . . . . . . 12 (𝜑 → (((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + (((2 · (𝐵↑3)) / 27) − ((𝐵 · 𝐶) / 3))) + 𝐷) = ((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + ((((2 · (𝐵↑3)) / 27) − ((𝐵 · 𝐶) / 3)) + 𝐷)))
291285, 287, 2903eqtr3d 2652 . . . . . . . . . . 11 (𝜑 → (𝐷 + -((𝐵 / 3)↑3)) = ((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + ((((2 · (𝐵↑3)) / 27) − ((𝐵 · 𝐶) / 3)) + 𝐷)))
29231, 192negsubd 10277 . . . . . . . . . . 11 (𝜑 → (𝐷 + -((𝐵 / 3)↑3)) = (𝐷 − ((𝐵 / 3)↑3)))
293256, 291, 2923eqtr2d 2650 . . . . . . . . . 10 (𝜑 → ((-(𝑀 / 3) · (𝐵 / 3)) + (𝑁 / 27)) = (𝐷 − ((𝐵 / 3)↑3)))
294226, 293oveq12d 6567 . . . . . . . . 9 (𝜑 → ((-(𝑀 / 3) · 𝑋) + ((-(𝑀 / 3) · (𝐵 / 3)) + (𝑁 / 27))) = (((𝐶 · 𝑋) − (3 · (𝑋 · ((𝐵 / 3)↑2)))) + (𝐷 − ((𝐵 / 3)↑3))))
295198, 201, 2943eqtrd 2648 . . . . . . . 8 (𝜑 → ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27)) = (((𝐶 · 𝑋) − (3 · (𝑋 · ((𝐵 / 3)↑2)))) + (𝐷 − ((𝐵 / 3)↑3))))
2965, 40mulcld 9939 . . . . . . . . 9 (𝜑 → (𝐶 · 𝑋) ∈ ℂ)
297296, 31, 190, 192addsub4d 10318 . . . . . . . 8 (𝜑 → (((𝐶 · 𝑋) + 𝐷) − ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))) = (((𝐶 · 𝑋) − (3 · (𝑋 · ((𝐵 / 3)↑2)))) + (𝐷 − ((𝐵 / 3)↑3))))
298295, 297eqtr4d 2647 . . . . . . 7 (𝜑 → ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27)) = (((𝐶 · 𝑋) + 𝐷) − ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))))
299298oveq2d 6565 . . . . . 6 (𝜑 → (((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27))) = (((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) + (((𝐶 · 𝑋) + 𝐷) − ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)))))
300296, 31addcld 9938 . . . . . . 7 (𝜑 → ((𝐶 · 𝑋) + 𝐷) ∈ ℂ)
301193, 300pncan3d 10274 . . . . . 6 (𝜑 → (((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) + (((𝐶 · 𝑋) + 𝐷) − ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)))) = ((𝐶 · 𝑋) + 𝐷))
302299, 301eqtrd 2644 . . . . 5 (𝜑 → (((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27))) = ((𝐶 · 𝑋) + 𝐷))
303302oveq2d 6565 . . . 4 (𝜑 → (((𝑋↑3) + (𝐵 · (𝑋↑2))) + (((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27)))) = (((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((𝐶 · 𝑋) + 𝐷)))
304183, 196, 3033eqtrd 2648 . . 3 (𝜑 → (((𝑋 + (𝐵 / 3))↑3) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27))) = (((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((𝐶 · 𝑋) + 𝐷)))
305304eqeq1d 2612 . 2 (𝜑 → ((((𝑋 + (𝐵 / 3))↑3) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27))) = 0 ↔ (((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((𝐶 · 𝑋) + 𝐷)) = 0))
306 oveq1 6556 . . . . . . . 8 (𝑟 = 0 → (𝑟↑3) = (0↑3))
307 0exp 12757 . . . . . . . . 9 (3 ∈ ℕ → (0↑3) = 0)
30846, 307ax-mp 5 . . . . . . . 8 (0↑3) = 0
309306, 308syl6eq 2660 . . . . . . 7 (𝑟 = 0 → (𝑟↑3) = 0)
310 0ne1 10965 . . . . . . . 8 0 ≠ 1
311310a1i 11 . . . . . . 7 (𝑟 = 0 → 0 ≠ 1)
312309, 311eqnetrd 2849 . . . . . 6 (𝑟 = 0 → (𝑟↑3) ≠ 1)
313312necon2i 2816 . . . . 5 ((𝑟↑3) = 1 → 𝑟 ≠ 0)
314 eqcom 2617 . . . . . . . 8 (𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) ↔ -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = 𝑋)
3152adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝐵 ∈ ℂ)
316 simprl 790 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑟 ∈ ℂ)
31743adantr 480 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑇 ∈ ℂ)
318316, 317mulcld 9939 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑟 · 𝑇) ∈ ℂ)
3199adantr 480 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑀 ∈ ℂ)
320 simprr 792 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑟 ≠ 0)
321168adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑇 ≠ 0)
322316, 317, 320, 321mulne0d 10558 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑟 · 𝑇) ≠ 0)
323319, 318, 322divcld 10680 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑀 / (𝑟 · 𝑇)) ∈ ℂ)
324318, 323addcld 9938 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) ∈ ℂ)
3254a1i 11 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 3 ∈ ℂ)
32611a1i 11 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 3 ≠ 0)
327315, 324, 325, 326divdird 10718 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝐵 + ((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇)))) / 3) = ((𝐵 / 3) + (((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)))
328315, 318, 323addassd 9941 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) = (𝐵 + ((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇)))))
329328oveq1d 6564 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = ((𝐵 + ((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇)))) / 3))
33041adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝐵 / 3) ∈ ℂ)
331324, 325, 326divcld 10680 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) ∈ ℂ)
332330, 331subnegd 10278 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝐵 / 3) − -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)) = ((𝐵 / 3) + (((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)))
333327, 329, 3323eqtr4d 2654 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = ((𝐵 / 3) − -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)))
334333negeqd 10154 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = -((𝐵 / 3) − -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)))
335331negcld 10258 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) ∈ ℂ)
336330, 335negsubdi2d 10287 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -((𝐵 / 3) − -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)) = (-(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) − (𝐵 / 3)))
337334, 336eqtrd 2644 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = (-(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) − (𝐵 / 3)))
338337eqeq1d 2612 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (-(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = 𝑋 ↔ (-(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) − (𝐵 / 3)) = 𝑋))
339314, 338syl5bb 271 . . . . . . 7 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) ↔ (-(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) − (𝐵 / 3)) = 𝑋))
34040adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑋 ∈ ℂ)
341335, 330, 340subadd2d 10290 . . . . . . 7 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((-(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) − (𝐵 / 3)) = 𝑋 ↔ (𝑋 + (𝐵 / 3)) = -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)))
342318, 323, 325, 326divdird 10718 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) = (((𝑟 · 𝑇) / 3) + ((𝑀 / (𝑟 · 𝑇)) / 3)))
343342negeqd 10154 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) = -(((𝑟 · 𝑇) / 3) + ((𝑀 / (𝑟 · 𝑇)) / 3)))
344318, 325, 326divcld 10680 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑟 · 𝑇) / 3) ∈ ℂ)
345323, 325, 326divcld 10680 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑀 / (𝑟 · 𝑇)) / 3) ∈ ℂ)
346344, 345negdi2d 10285 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝑟 · 𝑇) / 3) + ((𝑀 / (𝑟 · 𝑇)) / 3)) = (-((𝑟 · 𝑇) / 3) − ((𝑀 / (𝑟 · 𝑇)) / 3)))
347316, 317, 325, 326divassd 10715 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑟 · 𝑇) / 3) = (𝑟 · (𝑇 / 3)))
348347negeqd 10154 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -((𝑟 · 𝑇) / 3) = -(𝑟 · (𝑇 / 3)))
34944adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑇 / 3) ∈ ℂ)
350316, 349mulneg2d 10363 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑟 · -(𝑇 / 3)) = -(𝑟 · (𝑇 / 3)))
351348, 350eqtr4d 2647 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -((𝑟 · 𝑇) / 3) = (𝑟 · -(𝑇 / 3)))
352319, 318, 325, 322, 326divdiv32d 10705 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑀 / (𝑟 · 𝑇)) / 3) = ((𝑀 / 3) / (𝑟 · 𝑇)))
35313adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑀 / 3) ∈ ℂ)
354353, 318, 325, 322, 326divcan7d 10708 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝑀 / 3) / 3) / ((𝑟 · 𝑇) / 3)) = ((𝑀 / 3) / (𝑟 · 𝑇)))
355163oveq1d 6564 . . . . . . . . . . . . 13 (𝜑 → (((𝑀 / 3) / 3) / ((𝑟 · 𝑇) / 3)) = ((𝑀 / 9) / ((𝑟 · 𝑇) / 3)))
356355adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝑀 / 3) / 3) / ((𝑟 · 𝑇) / 3)) = ((𝑀 / 9) / ((𝑟 · 𝑇) / 3)))
357352, 354, 3563eqtr2d 2650 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑀 / (𝑟 · 𝑇)) / 3) = ((𝑀 / 9) / ((𝑟 · 𝑇) / 3)))
358127adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑀 / 9) ∈ ℂ)
359318, 325, 322, 326divne0d 10696 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑟 · 𝑇) / 3) ≠ 0)
360358, 344, 359div2negd 10695 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (-(𝑀 / 9) / -((𝑟 · 𝑇) / 3)) = ((𝑀 / 9) / ((𝑟 · 𝑇) / 3)))
361351oveq2d 6565 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (-(𝑀 / 9) / -((𝑟 · 𝑇) / 3)) = (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3))))
362357, 360, 3613eqtr2d 2650 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑀 / (𝑟 · 𝑇)) / 3) = (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3))))
363351, 362oveq12d 6567 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (-((𝑟 · 𝑇) / 3) − ((𝑀 / (𝑟 · 𝑇)) / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))))
364343, 346, 3633eqtrd 2648 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))))
365364eqeq2d 2620 . . . . . . 7 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑋 + (𝐵 / 3)) = -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) ↔ (𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3))))))
366339, 341, 3653bitrrd 294 . . . . . 6 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))) ↔ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3)))
367366anassrs 678 . . . . 5 (((𝜑𝑟 ∈ ℂ) ∧ 𝑟 ≠ 0) → ((𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))) ↔ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3)))
368313, 367sylan2 490 . . . 4 (((𝜑𝑟 ∈ ℂ) ∧ (𝑟↑3) = 1) → ((𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))) ↔ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3)))
369368pm5.32da 671 . . 3 ((𝜑𝑟 ∈ ℂ) → (((𝑟↑3) = 1 ∧ (𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3))))) ↔ ((𝑟↑3) = 1 ∧ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3))))
370369rexbidva 3031 . 2 (𝜑 → (∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ (𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3))))) ↔ ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3))))
371171, 305, 3703bitr3d 297 1 (𝜑 → ((((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((𝐶 · 𝑋) + 𝐷)) = 0 ↔ ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 195  wa 383   = wceq 1475  wcel 1977  wne 2780  wrex 2897   class class class wbr 4583  (class class class)co 6549  cc 9813  0cc0 9815  1c1 9816   + caddc 9818   · cmul 9820  cmin 10145  -cneg 10146   / cdiv 10563  cn 10897  2c2 10947  3c3 10948  4c4 10949  7c7 10952  9c9 10954  0cn0 11169  cdc 11369  cexp 12722  cdvds 14821
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-sup 8231  df-inf 8232  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-5 10959  df-6 10960  df-7 10961  df-8 10962  df-9 10963  df-n0 11170  df-z 11255  df-dec 11370  df-uz 11564  df-rp 11709  df-fz 12198  df-seq 12664  df-exp 12723  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-dvds 14822
This theorem is referenced by:  cubic2  24375  quart  24388
  Copyright terms: Public domain W3C validator