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

Theorem mcubic 26197
Description: Solutions to a monic cubic equation, a special case of cubic 26199. (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 14049 . . . . . . 7 (𝜑 → (𝐵↑2) ∈ ℂ)
4 3cn 12234 . . . . . . . 8 3 ∈ ℂ
5 mcubic.c . . . . . . . 8 (𝜑𝐶 ∈ ℂ)
6 mulcl 11135 . . . . . . . 8 ((3 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (3 · 𝐶) ∈ ℂ)
74, 5, 6sylancr 587 . . . . . . 7 (𝜑 → (3 · 𝐶) ∈ ℂ)
83, 7subcld 11512 . . . . . 6 (𝜑 → ((𝐵↑2) − (3 · 𝐶)) ∈ ℂ)
91, 8eqeltrd 2838 . . . . 5 (𝜑𝑀 ∈ ℂ)
104a1i 11 . . . . 5 (𝜑 → 3 ∈ ℂ)
11 3ne0 12259 . . . . . 6 3 ≠ 0
1211a1i 11 . . . . 5 (𝜑 → 3 ≠ 0)
139, 10, 12divcld 11931 . . . 4 (𝜑 → (𝑀 / 3) ∈ ℂ)
1413negcld 11499 . . 3 (𝜑 → -(𝑀 / 3) ∈ ℂ)
15 mcubic.n . . . . 5 (𝜑𝑁 = (((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) + (27 · 𝐷)))
16 2cn 12228 . . . . . . . 8 2 ∈ ℂ
17 3nn0 12431 . . . . . . . . 9 3 ∈ ℕ0
18 expcl 13985 . . . . . . . . 9 ((𝐵 ∈ ℂ ∧ 3 ∈ ℕ0) → (𝐵↑3) ∈ ℂ)
192, 17, 18sylancl 586 . . . . . . . 8 (𝜑 → (𝐵↑3) ∈ ℂ)
20 mulcl 11135 . . . . . . . 8 ((2 ∈ ℂ ∧ (𝐵↑3) ∈ ℂ) → (2 · (𝐵↑3)) ∈ ℂ)
2116, 19, 20sylancr 587 . . . . . . 7 (𝜑 → (2 · (𝐵↑3)) ∈ ℂ)
22 9cn 12253 . . . . . . . 8 9 ∈ ℂ
232, 5mulcld 11175 . . . . . . . 8 (𝜑 → (𝐵 · 𝐶) ∈ ℂ)
24 mulcl 11135 . . . . . . . 8 ((9 ∈ ℂ ∧ (𝐵 · 𝐶) ∈ ℂ) → (9 · (𝐵 · 𝐶)) ∈ ℂ)
2522, 23, 24sylancr 587 . . . . . . 7 (𝜑 → (9 · (𝐵 · 𝐶)) ∈ ℂ)
2621, 25subcld 11512 . . . . . 6 (𝜑 → ((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) ∈ ℂ)
27 2nn0 12430 . . . . . . . . 9 2 ∈ ℕ0
28 7nn 12245 . . . . . . . . 9 7 ∈ ℕ
2927, 28decnncl 12638 . . . . . . . 8 27 ∈ ℕ
3029nncni 12163 . . . . . . 7 27 ∈ ℂ
31 mcubic.d . . . . . . 7 (𝜑𝐷 ∈ ℂ)
32 mulcl 11135 . . . . . . 7 ((27 ∈ ℂ ∧ 𝐷 ∈ ℂ) → (27 · 𝐷) ∈ ℂ)
3330, 31, 32sylancr 587 . . . . . 6 (𝜑 → (27 · 𝐷) ∈ ℂ)
3426, 33addcld 11174 . . . . 5 (𝜑 → (((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) + (27 · 𝐷)) ∈ ℂ)
3515, 34eqeltrd 2838 . . . 4 (𝜑𝑁 ∈ ℂ)
3630a1i 11 . . . 4 (𝜑27 ∈ ℂ)
3729nnne0i 12193 . . . . 5 27 ≠ 0
3837a1i 11 . . . 4 (𝜑27 ≠ 0)
3935, 36, 38divcld 11931 . . 3 (𝜑 → (𝑁 / 27) ∈ ℂ)
40 mcubic.x . . . 4 (𝜑𝑋 ∈ ℂ)
412, 10, 12divcld 11931 . . . 4 (𝜑 → (𝐵 / 3) ∈ ℂ)
4240, 41addcld 11174 . . 3 (𝜑 → (𝑋 + (𝐵 / 3)) ∈ ℂ)
43 mcubic.t . . . . 5 (𝜑𝑇 ∈ ℂ)
4443, 10, 12divcld 11931 . . . 4 (𝜑 → (𝑇 / 3) ∈ ℂ)
4544negcld 11499 . . 3 (𝜑 → -(𝑇 / 3) ∈ ℂ)
46 3nn 12232 . . . . . 6 3 ∈ ℕ
4746a1i 11 . . . . 5 (𝜑 → 3 ∈ ℕ)
48 n2dvds3 16253 . . . . . 6 ¬ 2 ∥ 3
4948a1i 11 . . . . 5 (𝜑 → ¬ 2 ∥ 3)
50 oexpneg 16227 . . . . 5 (((𝑇 / 3) ∈ ℂ ∧ 3 ∈ ℕ ∧ ¬ 2 ∥ 3) → (-(𝑇 / 3)↑3) = -((𝑇 / 3)↑3))
5144, 47, 49, 50syl3anc 1371 . . . 4 (𝜑 → (-(𝑇 / 3)↑3) = -((𝑇 / 3)↑3))
5217a1i 11 . . . . . . 7 (𝜑 → 3 ∈ ℕ0)
5343, 10, 12, 52expdivd 14065 . . . . . 6 (𝜑 → ((𝑇 / 3)↑3) = ((𝑇↑3) / (3↑3)))
54 mcubic.3 . . . . . . 7 (𝜑 → (𝑇↑3) = ((𝑁 + 𝐺) / 2))
55 3exp3 16964 . . . . . . . 8 (3↑3) = 27
5655a1i 11 . . . . . . 7 (𝜑 → (3↑3) = 27)
5754, 56oveq12d 7375 . . . . . 6 (𝜑 → ((𝑇↑3) / (3↑3)) = (((𝑁 + 𝐺) / 2) / 27))
58 mcubic.g . . . . . . . . 9 (𝜑𝐺 ∈ ℂ)
5935, 58addcld 11174 . . . . . . . 8 (𝜑 → (𝑁 + 𝐺) ∈ ℂ)
60 2cnd 12231 . . . . . . . 8 (𝜑 → 2 ∈ ℂ)
61 2ne0 12257 . . . . . . . . 9 2 ≠ 0
6261a1i 11 . . . . . . . 8 (𝜑 → 2 ≠ 0)
6359, 60, 36, 62, 38divdiv32d 11956 . . . . . . 7 (𝜑 → (((𝑁 + 𝐺) / 2) / 27) = (((𝑁 + 𝐺) / 27) / 2))
6435, 58addcomd 11357 . . . . . . . . . 10 (𝜑 → (𝑁 + 𝐺) = (𝐺 + 𝑁))
6564oveq1d 7372 . . . . . . . . 9 (𝜑 → ((𝑁 + 𝐺) / 27) = ((𝐺 + 𝑁) / 27))
6658, 35, 36, 38divdird 11969 . . . . . . . . 9 (𝜑 → ((𝐺 + 𝑁) / 27) = ((𝐺 / 27) + (𝑁 / 27)))
6765, 66eqtrd 2776 . . . . . . . 8 (𝜑 → ((𝑁 + 𝐺) / 27) = ((𝐺 / 27) + (𝑁 / 27)))
6867oveq1d 7372 . . . . . . 7 (𝜑 → (((𝑁 + 𝐺) / 27) / 2) = (((𝐺 / 27) + (𝑁 / 27)) / 2))
6958, 36, 38divcld 11931 . . . . . . . 8 (𝜑 → (𝐺 / 27) ∈ ℂ)
7069, 39, 60, 62divdird 11969 . . . . . . 7 (𝜑 → (((𝐺 / 27) + (𝑁 / 27)) / 2) = (((𝐺 / 27) / 2) + ((𝑁 / 27) / 2)))
7163, 68, 703eqtrd 2780 . . . . . 6 (𝜑 → (((𝑁 + 𝐺) / 2) / 27) = (((𝐺 / 27) / 2) + ((𝑁 / 27) / 2)))
7253, 57, 713eqtrd 2780 . . . . 5 (𝜑 → ((𝑇 / 3)↑3) = (((𝐺 / 27) / 2) + ((𝑁 / 27) / 2)))
7372negeqd 11395 . . . 4 (𝜑 → -((𝑇 / 3)↑3) = -(((𝐺 / 27) / 2) + ((𝑁 / 27) / 2)))
7469halfcld 12398 . . . . 5 (𝜑 → ((𝐺 / 27) / 2) ∈ ℂ)
7539halfcld 12398 . . . . 5 (𝜑 → ((𝑁 / 27) / 2) ∈ ℂ)
7674, 75negdi2d 11526 . . . 4 (𝜑 → -(((𝐺 / 27) / 2) + ((𝑁 / 27) / 2)) = (-((𝐺 / 27) / 2) − ((𝑁 / 27) / 2)))
7751, 73, 763eqtrd 2780 . . 3 (𝜑 → (-(𝑇 / 3)↑3) = (-((𝐺 / 27) / 2) − ((𝑁 / 27) / 2)))
7874negcld 11499 . . 3 (𝜑 → -((𝐺 / 27) / 2) ∈ ℂ)
79 sqneg 14021 . . . . 5 (((𝐺 / 27) / 2) ∈ ℂ → (-((𝐺 / 27) / 2)↑2) = (((𝐺 / 27) / 2)↑2))
8074, 79syl 17 . . . 4 (𝜑 → (-((𝐺 / 27) / 2)↑2) = (((𝐺 / 27) / 2)↑2))
8169, 60, 62sqdivd 14064 . . . 4 (𝜑 → (((𝐺 / 27) / 2)↑2) = (((𝐺 / 27)↑2) / (2↑2)))
8239, 60, 62sqdivd 14064 . . . . . . . 8 (𝜑 → (((𝑁 / 27) / 2)↑2) = (((𝑁 / 27)↑2) / (2↑2)))
8335, 36, 38sqdivd 14064 . . . . . . . . 9 (𝜑 → ((𝑁 / 27)↑2) = ((𝑁↑2) / (27↑2)))
8483oveq1d 7372 . . . . . . . 8 (𝜑 → (((𝑁 / 27)↑2) / (2↑2)) = (((𝑁↑2) / (27↑2)) / (2↑2)))
8582, 84eqtr2d 2777 . . . . . . 7 (𝜑 → (((𝑁↑2) / (27↑2)) / (2↑2)) = (((𝑁 / 27) / 2)↑2))
86 4cn 12238 . . . . . . . . . . . 12 4 ∈ ℂ
8786a1i 11 . . . . . . . . . . 11 (𝜑 → 4 ∈ ℂ)
88 expcl 13985 . . . . . . . . . . . 12 ((𝑀 ∈ ℂ ∧ 3 ∈ ℕ0) → (𝑀↑3) ∈ ℂ)
899, 17, 88sylancl 586 . . . . . . . . . . 11 (𝜑 → (𝑀↑3) ∈ ℂ)
9030sqcli 14085 . . . . . . . . . . . 12 (27↑2) ∈ ℂ
9190a1i 11 . . . . . . . . . . 11 (𝜑 → (27↑2) ∈ ℂ)
92 sqne0 14028 . . . . . . . . . . . . 13 (27 ∈ ℂ → ((27↑2) ≠ 0 ↔ 27 ≠ 0))
9336, 92syl 17 . . . . . . . . . . . 12 (𝜑 → ((27↑2) ≠ 0 ↔ 27 ≠ 0))
9438, 93mpbird 256 . . . . . . . . . . 11 (𝜑 → (27↑2) ≠ 0)
9587, 89, 91, 94divassd 11966 . . . . . . . . . 10 (𝜑 → ((4 · (𝑀↑3)) / (27↑2)) = (4 · ((𝑀↑3) / (27↑2))))
9622a1i 11 . . . . . . . . . . . . 13 (𝜑 → 9 ∈ ℂ)
97 9nn 12251 . . . . . . . . . . . . . . 15 9 ∈ ℕ
9897nnne0i 12193 . . . . . . . . . . . . . 14 9 ≠ 0
9998a1i 11 . . . . . . . . . . . . 13 (𝜑 → 9 ≠ 0)
1009, 96, 99, 52expdivd 14065 . . . . . . . . . . . 12 (𝜑 → ((𝑀 / 9)↑3) = ((𝑀↑3) / (9↑3)))
10116, 4mulcomi 11163 . . . . . . . . . . . . . . . 16 (2 · 3) = (3 · 2)
102101oveq2i 7368 . . . . . . . . . . . . . . 15 (3↑(2 · 3)) = (3↑(3 · 2))
103 expmul 14013 . . . . . . . . . . . . . . . 16 ((3 ∈ ℂ ∧ 2 ∈ ℕ0 ∧ 3 ∈ ℕ0) → (3↑(2 · 3)) = ((3↑2)↑3))
1044, 27, 17, 103mp3an 1461 . . . . . . . . . . . . . . 15 (3↑(2 · 3)) = ((3↑2)↑3)
105 expmul 14013 . . . . . . . . . . . . . . . 16 ((3 ∈ ℂ ∧ 3 ∈ ℕ0 ∧ 2 ∈ ℕ0) → (3↑(3 · 2)) = ((3↑3)↑2))
1064, 17, 27, 105mp3an 1461 . . . . . . . . . . . . . . 15 (3↑(3 · 2)) = ((3↑3)↑2)
107102, 104, 1063eqtr3i 2772 . . . . . . . . . . . . . 14 ((3↑2)↑3) = ((3↑3)↑2)
108 sq3 14102 . . . . . . . . . . . . . . 15 (3↑2) = 9
109108oveq1i 7367 . . . . . . . . . . . . . 14 ((3↑2)↑3) = (9↑3)
11055oveq1i 7367 . . . . . . . . . . . . . 14 ((3↑3)↑2) = (27↑2)
111107, 109, 1103eqtr3i 2772 . . . . . . . . . . . . 13 (9↑3) = (27↑2)
112111oveq2i 7368 . . . . . . . . . . . 12 ((𝑀↑3) / (9↑3)) = ((𝑀↑3) / (27↑2))
113100, 112eqtrdi 2792 . . . . . . . . . . 11 (𝜑 → ((𝑀 / 9)↑3) = ((𝑀↑3) / (27↑2)))
114113oveq2d 7373 . . . . . . . . . 10 (𝜑 → (4 · ((𝑀 / 9)↑3)) = (4 · ((𝑀↑3) / (27↑2))))
11595, 114eqtr4d 2779 . . . . . . . . 9 (𝜑 → ((4 · (𝑀↑3)) / (27↑2)) = (4 · ((𝑀 / 9)↑3)))
116115oveq1d 7372 . . . . . . . 8 (𝜑 → (((4 · (𝑀↑3)) / (27↑2)) / (2↑2)) = ((4 · ((𝑀 / 9)↑3)) / (2↑2)))
117 sq2 14101 . . . . . . . . . 10 (2↑2) = 4
118117oveq2i 7368 . . . . . . . . 9 ((4 · ((𝑀 / 9)↑3)) / (2↑2)) = ((4 · ((𝑀 / 9)↑3)) / 4)
1199, 96, 99divcld 11931 . . . . . . . . . . 11 (𝜑 → (𝑀 / 9) ∈ ℂ)
120 expcl 13985 . . . . . . . . . . 11 (((𝑀 / 9) ∈ ℂ ∧ 3 ∈ ℕ0) → ((𝑀 / 9)↑3) ∈ ℂ)
121119, 17, 120sylancl 586 . . . . . . . . . 10 (𝜑 → ((𝑀 / 9)↑3) ∈ ℂ)
122 4ne0 12261 . . . . . . . . . . 11 4 ≠ 0
123122a1i 11 . . . . . . . . . 10 (𝜑 → 4 ≠ 0)
124121, 87, 123divcan3d 11936 . . . . . . . . 9 (𝜑 → ((4 · ((𝑀 / 9)↑3)) / 4) = ((𝑀 / 9)↑3))
125118, 124eqtrid 2788 . . . . . . . 8 (𝜑 → ((4 · ((𝑀 / 9)↑3)) / (2↑2)) = ((𝑀 / 9)↑3))
126116, 125eqtrd 2776 . . . . . . 7 (𝜑 → (((4 · (𝑀↑3)) / (27↑2)) / (2↑2)) = ((𝑀 / 9)↑3))
12785, 126oveq12d 7375 . . . . . 6 (𝜑 → ((((𝑁↑2) / (27↑2)) / (2↑2)) − (((4 · (𝑀↑3)) / (27↑2)) / (2↑2))) = ((((𝑁 / 27) / 2)↑2) − ((𝑀 / 9)↑3)))
12835sqcld 14049 . . . . . . . 8 (𝜑 → (𝑁↑2) ∈ ℂ)
129128, 91, 94divcld 11931 . . . . . . 7 (𝜑 → ((𝑁↑2) / (27↑2)) ∈ ℂ)
130 mulcl 11135 . . . . . . . . 9 ((4 ∈ ℂ ∧ (𝑀↑3) ∈ ℂ) → (4 · (𝑀↑3)) ∈ ℂ)
13186, 89, 130sylancr 587 . . . . . . . 8 (𝜑 → (4 · (𝑀↑3)) ∈ ℂ)
132131, 91, 94divcld 11931 . . . . . . 7 (𝜑 → ((4 · (𝑀↑3)) / (27↑2)) ∈ ℂ)
13316sqcli 14085 . . . . . . . 8 (2↑2) ∈ ℂ
134133a1i 11 . . . . . . 7 (𝜑 → (2↑2) ∈ ℂ)
135117, 122eqnetri 3014 . . . . . . . 8 (2↑2) ≠ 0
136135a1i 11 . . . . . . 7 (𝜑 → (2↑2) ≠ 0)
137129, 132, 134, 136divsubdird 11970 . . . . . 6 (𝜑 → ((((𝑁↑2) / (27↑2)) − ((4 · (𝑀↑3)) / (27↑2))) / (2↑2)) = ((((𝑁↑2) / (27↑2)) / (2↑2)) − (((4 · (𝑀↑3)) / (27↑2)) / (2↑2))))
13875sqcld 14049 . . . . . . 7 (𝜑 → (((𝑁 / 27) / 2)↑2) ∈ ℂ)
139138, 121negsubd 11518 . . . . . 6 (𝜑 → ((((𝑁 / 27) / 2)↑2) + -((𝑀 / 9)↑3)) = ((((𝑁 / 27) / 2)↑2) − ((𝑀 / 9)↑3)))
140127, 137, 1393eqtr4d 2786 . . . . 5 (𝜑 → ((((𝑁↑2) / (27↑2)) − ((4 · (𝑀↑3)) / (27↑2))) / (2↑2)) = ((((𝑁 / 27) / 2)↑2) + -((𝑀 / 9)↑3)))
14158, 36, 38sqdivd 14064 . . . . . . 7 (𝜑 → ((𝐺 / 27)↑2) = ((𝐺↑2) / (27↑2)))
142 mcubic.2 . . . . . . . 8 (𝜑 → (𝐺↑2) = ((𝑁↑2) − (4 · (𝑀↑3))))
143142oveq1d 7372 . . . . . . 7 (𝜑 → ((𝐺↑2) / (27↑2)) = (((𝑁↑2) − (4 · (𝑀↑3))) / (27↑2)))
144128, 131, 91, 94divsubdird 11970 . . . . . . 7 (𝜑 → (((𝑁↑2) − (4 · (𝑀↑3))) / (27↑2)) = (((𝑁↑2) / (27↑2)) − ((4 · (𝑀↑3)) / (27↑2))))
145141, 143, 1443eqtrd 2780 . . . . . 6 (𝜑 → ((𝐺 / 27)↑2) = (((𝑁↑2) / (27↑2)) − ((4 · (𝑀↑3)) / (27↑2))))
146145oveq1d 7372 . . . . 5 (𝜑 → (((𝐺 / 27)↑2) / (2↑2)) = ((((𝑁↑2) / (27↑2)) − ((4 · (𝑀↑3)) / (27↑2))) / (2↑2)))
147 oexpneg 16227 . . . . . . 7 (((𝑀 / 9) ∈ ℂ ∧ 3 ∈ ℕ ∧ ¬ 2 ∥ 3) → (-(𝑀 / 9)↑3) = -((𝑀 / 9)↑3))
148119, 47, 49, 147syl3anc 1371 . . . . . 6 (𝜑 → (-(𝑀 / 9)↑3) = -((𝑀 / 9)↑3))
149148oveq2d 7373 . . . . 5 (𝜑 → ((((𝑁 / 27) / 2)↑2) + (-(𝑀 / 9)↑3)) = ((((𝑁 / 27) / 2)↑2) + -((𝑀 / 9)↑3)))
150140, 146, 1493eqtr4d 2786 . . . 4 (𝜑 → (((𝐺 / 27)↑2) / (2↑2)) = ((((𝑁 / 27) / 2)↑2) + (-(𝑀 / 9)↑3)))
15180, 81, 1503eqtrd 2780 . . 3 (𝜑 → (-((𝐺 / 27) / 2)↑2) = ((((𝑁 / 27) / 2)↑2) + (-(𝑀 / 9)↑3)))
1529, 10, 10, 12, 12divdiv1d 11962 . . . . . 6 (𝜑 → ((𝑀 / 3) / 3) = (𝑀 / (3 · 3)))
153 3t3e9 12320 . . . . . . 7 (3 · 3) = 9
154153oveq2i 7368 . . . . . 6 (𝑀 / (3 · 3)) = (𝑀 / 9)
155152, 154eqtrdi 2792 . . . . 5 (𝜑 → ((𝑀 / 3) / 3) = (𝑀 / 9))
156155negeqd 11395 . . . 4 (𝜑 → -((𝑀 / 3) / 3) = -(𝑀 / 9))
15713, 10, 12divnegd 11944 . . . 4 (𝜑 → -((𝑀 / 3) / 3) = (-(𝑀 / 3) / 3))
158156, 157eqtr3d 2778 . . 3 (𝜑 → -(𝑀 / 9) = (-(𝑀 / 3) / 3))
159 eqidd 2737 . . 3 (𝜑 → ((𝑁 / 27) / 2) = ((𝑁 / 27) / 2))
160 mcubic.0 . . . . 5 (𝜑𝑇 ≠ 0)
16143, 10, 160, 12divne0d 11947 . . . 4 (𝜑 → (𝑇 / 3) ≠ 0)
16244, 161negne0d 11510 . . 3 (𝜑 → -(𝑇 / 3) ≠ 0)
16314, 39, 42, 45, 77, 78, 151, 158, 159, 162dcubic 26196 . 2 (𝜑 → ((((𝑋 + (𝐵 / 3))↑3) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27))) = 0 ↔ ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ (𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))))))
164 binom3 14127 . . . . . . 7 ((𝑋 ∈ ℂ ∧ (𝐵 / 3) ∈ ℂ) → ((𝑋 + (𝐵 / 3))↑3) = (((𝑋↑3) + (3 · ((𝑋↑2) · (𝐵 / 3)))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))))
16540, 41, 164syl2anc 584 . . . . . 6 (𝜑 → ((𝑋 + (𝐵 / 3))↑3) = (((𝑋↑3) + (3 · ((𝑋↑2) · (𝐵 / 3)))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))))
16640sqcld 14049 . . . . . . . . . 10 (𝜑 → (𝑋↑2) ∈ ℂ)
16710, 166, 41mul12d 11364 . . . . . . . . 9 (𝜑 → (3 · ((𝑋↑2) · (𝐵 / 3))) = ((𝑋↑2) · (3 · (𝐵 / 3))))
1682, 10, 12divcan2d 11933 . . . . . . . . . 10 (𝜑 → (3 · (𝐵 / 3)) = 𝐵)
169168oveq2d 7373 . . . . . . . . 9 (𝜑 → ((𝑋↑2) · (3 · (𝐵 / 3))) = ((𝑋↑2) · 𝐵))
170166, 2mulcomd 11176 . . . . . . . . 9 (𝜑 → ((𝑋↑2) · 𝐵) = (𝐵 · (𝑋↑2)))
171167, 169, 1703eqtrd 2780 . . . . . . . 8 (𝜑 → (3 · ((𝑋↑2) · (𝐵 / 3))) = (𝐵 · (𝑋↑2)))
172171oveq2d 7373 . . . . . . 7 (𝜑 → ((𝑋↑3) + (3 · ((𝑋↑2) · (𝐵 / 3)))) = ((𝑋↑3) + (𝐵 · (𝑋↑2))))
173172oveq1d 7372 . . . . . 6 (𝜑 → (((𝑋↑3) + (3 · ((𝑋↑2) · (𝐵 / 3)))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))) = (((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))))
174165, 173eqtrd 2776 . . . . 5 (𝜑 → ((𝑋 + (𝐵 / 3))↑3) = (((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))))
175174oveq1d 7372 . . . 4 (𝜑 → (((𝑋 + (𝐵 / 3))↑3) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27))) = ((((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27))))
176 expcl 13985 . . . . . . 7 ((𝑋 ∈ ℂ ∧ 3 ∈ ℕ0) → (𝑋↑3) ∈ ℂ)
17740, 17, 176sylancl 586 . . . . . 6 (𝜑 → (𝑋↑3) ∈ ℂ)
1782, 166mulcld 11175 . . . . . 6 (𝜑 → (𝐵 · (𝑋↑2)) ∈ ℂ)
179177, 178addcld 11174 . . . . 5 (𝜑 → ((𝑋↑3) + (𝐵 · (𝑋↑2))) ∈ ℂ)
18041sqcld 14049 . . . . . . . 8 (𝜑 → ((𝐵 / 3)↑2) ∈ ℂ)
18140, 180mulcld 11175 . . . . . . 7 (𝜑 → (𝑋 · ((𝐵 / 3)↑2)) ∈ ℂ)
18210, 181mulcld 11175 . . . . . 6 (𝜑 → (3 · (𝑋 · ((𝐵 / 3)↑2))) ∈ ℂ)
183 expcl 13985 . . . . . . 7 (((𝐵 / 3) ∈ ℂ ∧ 3 ∈ ℕ0) → ((𝐵 / 3)↑3) ∈ ℂ)
18441, 17, 183sylancl 586 . . . . . 6 (𝜑 → ((𝐵 / 3)↑3) ∈ ℂ)
185182, 184addcld 11174 . . . . 5 (𝜑 → ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) ∈ ℂ)
18614, 42mulcld 11175 . . . . . 6 (𝜑 → (-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) ∈ ℂ)
187186, 39addcld 11174 . . . . 5 (𝜑 → ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27)) ∈ ℂ)
188179, 185, 187addassd 11177 . . . 4 (𝜑 → ((((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27))) = (((𝑋↑3) + (𝐵 · (𝑋↑2))) + (((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27)))))
18914, 40, 41adddid 11179 . . . . . . . . . 10 (𝜑 → (-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) = ((-(𝑀 / 3) · 𝑋) + (-(𝑀 / 3) · (𝐵 / 3))))
190189oveq1d 7372 . . . . . . . . 9 (𝜑 → ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27)) = (((-(𝑀 / 3) · 𝑋) + (-(𝑀 / 3) · (𝐵 / 3))) + (𝑁 / 27)))
19114, 40mulcld 11175 . . . . . . . . . 10 (𝜑 → (-(𝑀 / 3) · 𝑋) ∈ ℂ)
19214, 41mulcld 11175 . . . . . . . . . 10 (𝜑 → (-(𝑀 / 3) · (𝐵 / 3)) ∈ ℂ)
193191, 192, 39addassd 11177 . . . . . . . . 9 (𝜑 → (((-(𝑀 / 3) · 𝑋) + (-(𝑀 / 3) · (𝐵 / 3))) + (𝑁 / 27)) = ((-(𝑀 / 3) · 𝑋) + ((-(𝑀 / 3) · (𝐵 / 3)) + (𝑁 / 27))))
1941oveq1d 7372 . . . . . . . . . . . . . . 15 (𝜑 → (𝑀 / 3) = (((𝐵↑2) − (3 · 𝐶)) / 3))
1953, 7, 10, 12divsubdird 11970 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐵↑2) − (3 · 𝐶)) / 3) = (((𝐵↑2) / 3) − ((3 · 𝐶) / 3)))
1965, 10, 12divcan3d 11936 . . . . . . . . . . . . . . . 16 (𝜑 → ((3 · 𝐶) / 3) = 𝐶)
197196oveq2d 7373 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐵↑2) / 3) − ((3 · 𝐶) / 3)) = (((𝐵↑2) / 3) − 𝐶))
198194, 195, 1973eqtrd 2780 . . . . . . . . . . . . . 14 (𝜑 → (𝑀 / 3) = (((𝐵↑2) / 3) − 𝐶))
199198negeqd 11395 . . . . . . . . . . . . 13 (𝜑 → -(𝑀 / 3) = -(((𝐵↑2) / 3) − 𝐶))
2003, 10, 12divcld 11931 . . . . . . . . . . . . . 14 (𝜑 → ((𝐵↑2) / 3) ∈ ℂ)
201200, 5negsubdi2d 11528 . . . . . . . . . . . . 13 (𝜑 → -(((𝐵↑2) / 3) − 𝐶) = (𝐶 − ((𝐵↑2) / 3)))
202199, 201eqtrd 2776 . . . . . . . . . . . 12 (𝜑 → -(𝑀 / 3) = (𝐶 − ((𝐵↑2) / 3)))
203202oveq1d 7372 . . . . . . . . . . 11 (𝜑 → (-(𝑀 / 3) · 𝑋) = ((𝐶 − ((𝐵↑2) / 3)) · 𝑋))
2045, 200, 40subdird 11612 . . . . . . . . . . 11 (𝜑 → ((𝐶 − ((𝐵↑2) / 3)) · 𝑋) = ((𝐶 · 𝑋) − (((𝐵↑2) / 3) · 𝑋)))
205200, 40mulcomd 11176 . . . . . . . . . . . . 13 (𝜑 → (((𝐵↑2) / 3) · 𝑋) = (𝑋 · ((𝐵↑2) / 3)))
2064sqvali 14084 . . . . . . . . . . . . . . . . . 18 (3↑2) = (3 · 3)
207206oveq2i 7368 . . . . . . . . . . . . . . . . 17 ((𝐵↑2) / (3↑2)) = ((𝐵↑2) / (3 · 3))
2082, 10, 12sqdivd 14064 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐵 / 3)↑2) = ((𝐵↑2) / (3↑2)))
2093, 10, 10, 12, 12divdiv1d 11962 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝐵↑2) / 3) / 3) = ((𝐵↑2) / (3 · 3)))
210207, 208, 2093eqtr4a 2802 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐵 / 3)↑2) = (((𝐵↑2) / 3) / 3))
211210oveq2d 7373 . . . . . . . . . . . . . . 15 (𝜑 → (3 · ((𝐵 / 3)↑2)) = (3 · (((𝐵↑2) / 3) / 3)))
212200, 10, 12divcan2d 11933 . . . . . . . . . . . . . . 15 (𝜑 → (3 · (((𝐵↑2) / 3) / 3)) = ((𝐵↑2) / 3))
213211, 212eqtrd 2776 . . . . . . . . . . . . . 14 (𝜑 → (3 · ((𝐵 / 3)↑2)) = ((𝐵↑2) / 3))
214213oveq2d 7373 . . . . . . . . . . . . 13 (𝜑 → (𝑋 · (3 · ((𝐵 / 3)↑2))) = (𝑋 · ((𝐵↑2) / 3)))
21540, 10, 180mul12d 11364 . . . . . . . . . . . . 13 (𝜑 → (𝑋 · (3 · ((𝐵 / 3)↑2))) = (3 · (𝑋 · ((𝐵 / 3)↑2))))
216205, 214, 2153eqtr2d 2782 . . . . . . . . . . . 12 (𝜑 → (((𝐵↑2) / 3) · 𝑋) = (3 · (𝑋 · ((𝐵 / 3)↑2))))
217216oveq2d 7373 . . . . . . . . . . 11 (𝜑 → ((𝐶 · 𝑋) − (((𝐵↑2) / 3) · 𝑋)) = ((𝐶 · 𝑋) − (3 · (𝑋 · ((𝐵 / 3)↑2)))))
218203, 204, 2173eqtrd 2780 . . . . . . . . . 10 (𝜑 → (-(𝑀 / 3) · 𝑋) = ((𝐶 · 𝑋) − (3 · (𝑋 · ((𝐵 / 3)↑2)))))
219202oveq1d 7372 . . . . . . . . . . . . 13 (𝜑 → (-(𝑀 / 3) · (𝐵 / 3)) = ((𝐶 − ((𝐵↑2) / 3)) · (𝐵 / 3)))
2205, 200, 41subdird 11612 . . . . . . . . . . . . 13 (𝜑 → ((𝐶 − ((𝐵↑2) / 3)) · (𝐵 / 3)) = ((𝐶 · (𝐵 / 3)) − (((𝐵↑2) / 3) · (𝐵 / 3))))
2215, 2, 10, 12divassd 11966 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐶 · 𝐵) / 3) = (𝐶 · (𝐵 / 3)))
2225, 2mulcomd 11176 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐶 · 𝐵) = (𝐵 · 𝐶))
223222oveq1d 7372 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐶 · 𝐵) / 3) = ((𝐵 · 𝐶) / 3))
224221, 223eqtr3d 2778 . . . . . . . . . . . . . 14 (𝜑 → (𝐶 · (𝐵 / 3)) = ((𝐵 · 𝐶) / 3))
2253, 10, 2, 10, 12, 12divmuldivd 11972 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐵↑2) / 3) · (𝐵 / 3)) = (((𝐵↑2) · 𝐵) / (3 · 3)))
226 df-3 12217 . . . . . . . . . . . . . . . . . 18 3 = (2 + 1)
227226oveq2i 7368 . . . . . . . . . . . . . . . . 17 (𝐵↑3) = (𝐵↑(2 + 1))
228 expp1 13974 . . . . . . . . . . . . . . . . . 18 ((𝐵 ∈ ℂ ∧ 2 ∈ ℕ0) → (𝐵↑(2 + 1)) = ((𝐵↑2) · 𝐵))
2292, 27, 228sylancl 586 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵↑(2 + 1)) = ((𝐵↑2) · 𝐵))
230227, 229eqtr2id 2789 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐵↑2) · 𝐵) = (𝐵↑3))
231153a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → (3 · 3) = 9)
232230, 231oveq12d 7375 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐵↑2) · 𝐵) / (3 · 3)) = ((𝐵↑3) / 9))
233225, 232eqtrd 2776 . . . . . . . . . . . . . 14 (𝜑 → (((𝐵↑2) / 3) · (𝐵 / 3)) = ((𝐵↑3) / 9))
234224, 233oveq12d 7375 . . . . . . . . . . . . 13 (𝜑 → ((𝐶 · (𝐵 / 3)) − (((𝐵↑2) / 3) · (𝐵 / 3))) = (((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)))
235219, 220, 2343eqtrd 2780 . . . . . . . . . . . 12 (𝜑 → (-(𝑀 / 3) · (𝐵 / 3)) = (((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)))
23615oveq1d 7372 . . . . . . . . . . . . 13 (𝜑 → (𝑁 / 27) = ((((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) + (27 · 𝐷)) / 27))
23726, 33, 36, 38divdird 11969 . . . . . . . . . . . . 13 (𝜑 → ((((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) + (27 · 𝐷)) / 27) = ((((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) / 27) + ((27 · 𝐷) / 27)))
23821, 25, 36, 38divsubdird 11970 . . . . . . . . . . . . . . 15 (𝜑 → (((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) / 27) = (((2 · (𝐵↑3)) / 27) − ((9 · (𝐵 · 𝐶)) / 27)))
239 9t3e27 12741 . . . . . . . . . . . . . . . . . 18 (9 · 3) = 27
240239oveq2i 7368 . . . . . . . . . . . . . . . . 17 ((9 · (𝐵 · 𝐶)) / (9 · 3)) = ((9 · (𝐵 · 𝐶)) / 27)
24123, 10, 96, 12, 99divcan5d 11957 . . . . . . . . . . . . . . . . 17 (𝜑 → ((9 · (𝐵 · 𝐶)) / (9 · 3)) = ((𝐵 · 𝐶) / 3))
242240, 241eqtr3id 2790 . . . . . . . . . . . . . . . 16 (𝜑 → ((9 · (𝐵 · 𝐶)) / 27) = ((𝐵 · 𝐶) / 3))
243242oveq2d 7373 . . . . . . . . . . . . . . 15 (𝜑 → (((2 · (𝐵↑3)) / 27) − ((9 · (𝐵 · 𝐶)) / 27)) = (((2 · (𝐵↑3)) / 27) − ((𝐵 · 𝐶) / 3)))
244238, 243eqtrd 2776 . . . . . . . . . . . . . 14 (𝜑 → (((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) / 27) = (((2 · (𝐵↑3)) / 27) − ((𝐵 · 𝐶) / 3)))
24531, 36, 38divcan3d 11936 . . . . . . . . . . . . . 14 (𝜑 → ((27 · 𝐷) / 27) = 𝐷)
246244, 245oveq12d 7375 . . . . . . . . . . . . 13 (𝜑 → ((((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) / 27) + ((27 · 𝐷) / 27)) = ((((2 · (𝐵↑3)) / 27) − ((𝐵 · 𝐶) / 3)) + 𝐷))
247236, 237, 2463eqtrd 2780 . . . . . . . . . . . 12 (𝜑 → (𝑁 / 27) = ((((2 · (𝐵↑3)) / 27) − ((𝐵 · 𝐶) / 3)) + 𝐷))
248235, 247oveq12d 7375 . . . . . . . . . . 11 (𝜑 → ((-(𝑀 / 3) · (𝐵 / 3)) + (𝑁 / 27)) = ((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + ((((2 · (𝐵↑3)) / 27) − ((𝐵 · 𝐶) / 3)) + 𝐷)))
24919, 96, 99divcld 11931 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐵↑3) / 9) ∈ ℂ)
25021, 36, 38divcld 11931 . . . . . . . . . . . . . . 15 (𝜑 → ((2 · (𝐵↑3)) / 27) ∈ ℂ)
251249, 250negsubdi2d 11528 . . . . . . . . . . . . . 14 (𝜑 → -(((𝐵↑3) / 9) − ((2 · (𝐵↑3)) / 27)) = (((2 · (𝐵↑3)) / 27) − ((𝐵↑3) / 9)))
2522, 10, 12, 52expdivd 14065 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐵 / 3)↑3) = ((𝐵↑3) / (3↑3)))
25355oveq2i 7368 . . . . . . . . . . . . . . . . 17 ((𝐵↑3) / (3↑3)) = ((𝐵↑3) / 27)
254 ax-1cn 11109 . . . . . . . . . . . . . . . . . . . . . . 23 1 ∈ ℂ
255 2p1e3 12295 . . . . . . . . . . . . . . . . . . . . . . 23 (2 + 1) = 3
2564, 16, 254, 255subaddrii 11490 . . . . . . . . . . . . . . . . . . . . . 22 (3 − 2) = 1
257256oveq1i 7367 . . . . . . . . . . . . . . . . . . . . 21 ((3 − 2) · (𝐵↑3)) = (1 · (𝐵↑3))
25819mulid2d 11173 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (1 · (𝐵↑3)) = (𝐵↑3))
259257, 258eqtrid 2788 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((3 − 2) · (𝐵↑3)) = (𝐵↑3))
26010, 60, 19subdird 11612 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((3 − 2) · (𝐵↑3)) = ((3 · (𝐵↑3)) − (2 · (𝐵↑3))))
261259, 260eqtr3d 2778 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐵↑3) = ((3 · (𝐵↑3)) − (2 · (𝐵↑3))))
262261oveq1d 7372 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐵↑3) / 27) = (((3 · (𝐵↑3)) − (2 · (𝐵↑3))) / 27))
263 mulcl 11135 . . . . . . . . . . . . . . . . . . . 20 ((3 ∈ ℂ ∧ (𝐵↑3) ∈ ℂ) → (3 · (𝐵↑3)) ∈ ℂ)
2644, 19, 263sylancr 587 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (3 · (𝐵↑3)) ∈ ℂ)
265264, 21, 36, 38divsubdird 11970 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((3 · (𝐵↑3)) − (2 · (𝐵↑3))) / 27) = (((3 · (𝐵↑3)) / 27) − ((2 · (𝐵↑3)) / 27)))
266262, 265eqtrd 2776 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐵↑3) / 27) = (((3 · (𝐵↑3)) / 27) − ((2 · (𝐵↑3)) / 27)))
267253, 266eqtrid 2788 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐵↑3) / (3↑3)) = (((3 · (𝐵↑3)) / 27) − ((2 · (𝐵↑3)) / 27)))
26822, 4, 239mulcomli 11164 . . . . . . . . . . . . . . . . . . 19 (3 · 9) = 27
269268oveq2i 7368 . . . . . . . . . . . . . . . . . 18 ((3 · (𝐵↑3)) / (3 · 9)) = ((3 · (𝐵↑3)) / 27)
27019, 96, 10, 99, 12divcan5d 11957 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((3 · (𝐵↑3)) / (3 · 9)) = ((𝐵↑3) / 9))
271269, 270eqtr3id 2790 . . . . . . . . . . . . . . . . 17 (𝜑 → ((3 · (𝐵↑3)) / 27) = ((𝐵↑3) / 9))
272271oveq1d 7372 . . . . . . . . . . . . . . . 16 (𝜑 → (((3 · (𝐵↑3)) / 27) − ((2 · (𝐵↑3)) / 27)) = (((𝐵↑3) / 9) − ((2 · (𝐵↑3)) / 27)))
273252, 267, 2723eqtrd 2780 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐵 / 3)↑3) = (((𝐵↑3) / 9) − ((2 · (𝐵↑3)) / 27)))
274273negeqd 11395 . . . . . . . . . . . . . 14 (𝜑 → -((𝐵 / 3)↑3) = -(((𝐵↑3) / 9) − ((2 · (𝐵↑3)) / 27)))
27523, 10, 12divcld 11931 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐵 · 𝐶) / 3) ∈ ℂ)
276275, 249, 250npncan3d 11548 . . . . . . . . . . . . . 14 (𝜑 → ((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + (((2 · (𝐵↑3)) / 27) − ((𝐵 · 𝐶) / 3))) = (((2 · (𝐵↑3)) / 27) − ((𝐵↑3) / 9)))
277251, 274, 2763eqtr4d 2786 . . . . . . . . . . . . 13 (𝜑 → -((𝐵 / 3)↑3) = ((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + (((2 · (𝐵↑3)) / 27) − ((𝐵 · 𝐶) / 3))))
278277oveq1d 7372 . . . . . . . . . . . 12 (𝜑 → (-((𝐵 / 3)↑3) + 𝐷) = (((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + (((2 · (𝐵↑3)) / 27) − ((𝐵 · 𝐶) / 3))) + 𝐷))
279184negcld 11499 . . . . . . . . . . . . 13 (𝜑 → -((𝐵 / 3)↑3) ∈ ℂ)
280279, 31addcomd 11357 . . . . . . . . . . . 12 (𝜑 → (-((𝐵 / 3)↑3) + 𝐷) = (𝐷 + -((𝐵 / 3)↑3)))
281235, 192eqeltrrd 2839 . . . . . . . . . . . . 13 (𝜑 → (((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) ∈ ℂ)
282250, 275subcld 11512 . . . . . . . . . . . . 13 (𝜑 → (((2 · (𝐵↑3)) / 27) − ((𝐵 · 𝐶) / 3)) ∈ ℂ)
283281, 282, 31addassd 11177 . . . . . . . . . . . 12 (𝜑 → (((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + (((2 · (𝐵↑3)) / 27) − ((𝐵 · 𝐶) / 3))) + 𝐷) = ((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + ((((2 · (𝐵↑3)) / 27) − ((𝐵 · 𝐶) / 3)) + 𝐷)))
284278, 280, 2833eqtr3d 2784 . . . . . . . . . . 11 (𝜑 → (𝐷 + -((𝐵 / 3)↑3)) = ((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + ((((2 · (𝐵↑3)) / 27) − ((𝐵 · 𝐶) / 3)) + 𝐷)))
28531, 184negsubd 11518 . . . . . . . . . . 11 (𝜑 → (𝐷 + -((𝐵 / 3)↑3)) = (𝐷 − ((𝐵 / 3)↑3)))
286248, 284, 2853eqtr2d 2782 . . . . . . . . . 10 (𝜑 → ((-(𝑀 / 3) · (𝐵 / 3)) + (𝑁 / 27)) = (𝐷 − ((𝐵 / 3)↑3)))
287218, 286oveq12d 7375 . . . . . . . . 9 (𝜑 → ((-(𝑀 / 3) · 𝑋) + ((-(𝑀 / 3) · (𝐵 / 3)) + (𝑁 / 27))) = (((𝐶 · 𝑋) − (3 · (𝑋 · ((𝐵 / 3)↑2)))) + (𝐷 − ((𝐵 / 3)↑3))))
288190, 193, 2873eqtrd 2780 . . . . . . . 8 (𝜑 → ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27)) = (((𝐶 · 𝑋) − (3 · (𝑋 · ((𝐵 / 3)↑2)))) + (𝐷 − ((𝐵 / 3)↑3))))
2895, 40mulcld 11175 . . . . . . . . 9 (𝜑 → (𝐶 · 𝑋) ∈ ℂ)
290289, 31, 182, 184addsub4d 11559 . . . . . . . 8 (𝜑 → (((𝐶 · 𝑋) + 𝐷) − ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))) = (((𝐶 · 𝑋) − (3 · (𝑋 · ((𝐵 / 3)↑2)))) + (𝐷 − ((𝐵 / 3)↑3))))
291288, 290eqtr4d 2779 . . . . . . 7 (𝜑 → ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27)) = (((𝐶 · 𝑋) + 𝐷) − ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))))
292291oveq2d 7373 . . . . . 6 (𝜑 → (((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27))) = (((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) + (((𝐶 · 𝑋) + 𝐷) − ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)))))
293289, 31addcld 11174 . . . . . . 7 (𝜑 → ((𝐶 · 𝑋) + 𝐷) ∈ ℂ)
294185, 293pncan3d 11515 . . . . . 6 (𝜑 → (((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) + (((𝐶 · 𝑋) + 𝐷) − ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)))) = ((𝐶 · 𝑋) + 𝐷))
295292, 294eqtrd 2776 . . . . 5 (𝜑 → (((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27))) = ((𝐶 · 𝑋) + 𝐷))
296295oveq2d 7373 . . . 4 (𝜑 → (((𝑋↑3) + (𝐵 · (𝑋↑2))) + (((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27)))) = (((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((𝐶 · 𝑋) + 𝐷)))
297175, 188, 2963eqtrd 2780 . . 3 (𝜑 → (((𝑋 + (𝐵 / 3))↑3) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27))) = (((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((𝐶 · 𝑋) + 𝐷)))
298297eqeq1d 2738 . 2 (𝜑 → ((((𝑋 + (𝐵 / 3))↑3) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / 27))) = 0 ↔ (((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((𝐶 · 𝑋) + 𝐷)) = 0))
299 oveq1 7364 . . . . . . . 8 (𝑟 = 0 → (𝑟↑3) = (0↑3))
300 0exp 14003 . . . . . . . . 9 (3 ∈ ℕ → (0↑3) = 0)
30146, 300ax-mp 5 . . . . . . . 8 (0↑3) = 0
302299, 301eqtrdi 2792 . . . . . . 7 (𝑟 = 0 → (𝑟↑3) = 0)
303 0ne1 12224 . . . . . . . 8 0 ≠ 1
304303a1i 11 . . . . . . 7 (𝑟 = 0 → 0 ≠ 1)
305302, 304eqnetrd 3011 . . . . . 6 (𝑟 = 0 → (𝑟↑3) ≠ 1)
306305necon2i 2978 . . . . 5 ((𝑟↑3) = 1 → 𝑟 ≠ 0)
307 eqcom 2743 . . . . . . . 8 (𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) ↔ -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = 𝑋)
3082adantr 481 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝐵 ∈ ℂ)
309 simprl 769 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑟 ∈ ℂ)
31043adantr 481 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑇 ∈ ℂ)
311309, 310mulcld 11175 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑟 · 𝑇) ∈ ℂ)
3129adantr 481 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑀 ∈ ℂ)
313 simprr 771 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑟 ≠ 0)
314160adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑇 ≠ 0)
315309, 310, 313, 314mulne0d 11807 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑟 · 𝑇) ≠ 0)
316312, 311, 315divcld 11931 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑀 / (𝑟 · 𝑇)) ∈ ℂ)
317311, 316addcld 11174 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) ∈ ℂ)
3184a1i 11 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 3 ∈ ℂ)
31911a1i 11 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 3 ≠ 0)
320308, 317, 318, 319divdird 11969 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝐵 + ((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇)))) / 3) = ((𝐵 / 3) + (((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)))
321308, 311, 316addassd 11177 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) = (𝐵 + ((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇)))))
322321oveq1d 7372 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = ((𝐵 + ((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇)))) / 3))
32341adantr 481 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝐵 / 3) ∈ ℂ)
324317, 318, 319divcld 11931 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) ∈ ℂ)
325323, 324subnegd 11519 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝐵 / 3) − -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)) = ((𝐵 / 3) + (((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)))
326320, 322, 3253eqtr4d 2786 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = ((𝐵 / 3) − -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)))
327326negeqd 11395 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = -((𝐵 / 3) − -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)))
328324negcld 11499 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) ∈ ℂ)
329323, 328negsubdi2d 11528 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -((𝐵 / 3) − -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)) = (-(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) − (𝐵 / 3)))
330327, 329eqtrd 2776 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = (-(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) − (𝐵 / 3)))
331330eqeq1d 2738 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (-(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = 𝑋 ↔ (-(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) − (𝐵 / 3)) = 𝑋))
332307, 331bitrid 282 . . . . . . 7 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) ↔ (-(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) − (𝐵 / 3)) = 𝑋))
33340adantr 481 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑋 ∈ ℂ)
334328, 323, 333subadd2d 11531 . . . . . . 7 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((-(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) − (𝐵 / 3)) = 𝑋 ↔ (𝑋 + (𝐵 / 3)) = -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)))
335311, 316, 318, 319divdird 11969 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) = (((𝑟 · 𝑇) / 3) + ((𝑀 / (𝑟 · 𝑇)) / 3)))
336335negeqd 11395 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) = -(((𝑟 · 𝑇) / 3) + ((𝑀 / (𝑟 · 𝑇)) / 3)))
337311, 318, 319divcld 11931 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑟 · 𝑇) / 3) ∈ ℂ)
338316, 318, 319divcld 11931 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑀 / (𝑟 · 𝑇)) / 3) ∈ ℂ)
339337, 338negdi2d 11526 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝑟 · 𝑇) / 3) + ((𝑀 / (𝑟 · 𝑇)) / 3)) = (-((𝑟 · 𝑇) / 3) − ((𝑀 / (𝑟 · 𝑇)) / 3)))
340309, 310, 318, 319divassd 11966 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑟 · 𝑇) / 3) = (𝑟 · (𝑇 / 3)))
341340negeqd 11395 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -((𝑟 · 𝑇) / 3) = -(𝑟 · (𝑇 / 3)))
34244adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑇 / 3) ∈ ℂ)
343309, 342mulneg2d 11609 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑟 · -(𝑇 / 3)) = -(𝑟 · (𝑇 / 3)))
344341, 343eqtr4d 2779 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -((𝑟 · 𝑇) / 3) = (𝑟 · -(𝑇 / 3)))
345312, 311, 318, 315, 319divdiv32d 11956 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑀 / (𝑟 · 𝑇)) / 3) = ((𝑀 / 3) / (𝑟 · 𝑇)))
34613adantr 481 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑀 / 3) ∈ ℂ)
347346, 311, 318, 315, 319divcan7d 11959 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝑀 / 3) / 3) / ((𝑟 · 𝑇) / 3)) = ((𝑀 / 3) / (𝑟 · 𝑇)))
348155oveq1d 7372 . . . . . . . . . . . . 13 (𝜑 → (((𝑀 / 3) / 3) / ((𝑟 · 𝑇) / 3)) = ((𝑀 / 9) / ((𝑟 · 𝑇) / 3)))
349348adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝑀 / 3) / 3) / ((𝑟 · 𝑇) / 3)) = ((𝑀 / 9) / ((𝑟 · 𝑇) / 3)))
350345, 347, 3493eqtr2d 2782 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑀 / (𝑟 · 𝑇)) / 3) = ((𝑀 / 9) / ((𝑟 · 𝑇) / 3)))
351119adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑀 / 9) ∈ ℂ)
352311, 318, 315, 319divne0d 11947 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑟 · 𝑇) / 3) ≠ 0)
353351, 337, 352div2negd 11946 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (-(𝑀 / 9) / -((𝑟 · 𝑇) / 3)) = ((𝑀 / 9) / ((𝑟 · 𝑇) / 3)))
354344oveq2d 7373 . . . . . . . . . . 11 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (-(𝑀 / 9) / -((𝑟 · 𝑇) / 3)) = (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3))))
355350, 353, 3543eqtr2d 2782 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑀 / (𝑟 · 𝑇)) / 3) = (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3))))
356344, 355oveq12d 7375 . . . . . . . . 9 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (-((𝑟 · 𝑇) / 3) − ((𝑀 / (𝑟 · 𝑇)) / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))))
357336, 339, 3563eqtrd 2780 . . . . . . . 8 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))))
358357eqeq2d 2747 . . . . . . 7 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑋 + (𝐵 / 3)) = -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) ↔ (𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3))))))
359332, 334, 3583bitrrd 305 . . . . . 6 ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))) ↔ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3)))
360359anassrs 468 . . . . 5 (((𝜑𝑟 ∈ ℂ) ∧ 𝑟 ≠ 0) → ((𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))) ↔ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3)))
361306, 360sylan2 593 . . . 4 (((𝜑𝑟 ∈ ℂ) ∧ (𝑟↑3) = 1) → ((𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))) ↔ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3)))
362361pm5.32da 579 . . 3 ((𝜑𝑟 ∈ ℂ) → (((𝑟↑3) = 1 ∧ (𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3))))) ↔ ((𝑟↑3) = 1 ∧ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3))))
363362rexbidva 3173 . 2 (𝜑 → (∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ (𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3))))) ↔ ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3))))
364163, 298, 3633bitr3d 308 1 (𝜑 → ((((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((𝐶 · 𝑋) + 𝐷)) = 0 ↔ ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396   = wceq 1541  wcel 2106  wne 2943  wrex 3073   class class class wbr 5105  (class class class)co 7357  cc 11049  0cc0 11051  1c1 11052   + caddc 11054   · cmul 11056  cmin 11385  -cneg 11386   / cdiv 11812  cn 12153  2c2 12208  3c3 12209  4c4 12210  7c7 12213  9c9 12215  0cn0 12413  cdc 12618  cexp 13967  cdvds 16136
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-er 8648  df-en 8884  df-dom 8885  df-sdom 8886  df-sup 9378  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-5 12219  df-6 12220  df-7 12221  df-8 12222  df-9 12223  df-n0 12414  df-z 12500  df-dec 12619  df-uz 12764  df-rp 12916  df-seq 13907  df-exp 13968  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121  df-dvds 16137
This theorem is referenced by:  cubic2  26198  quart  26211
  Copyright terms: Public domain W3C validator