mcubic - Metamath Proof Explorer

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

Theorem mcubic 25902

Description: Solutions to a monic cubic equation, a special case of cubic 25904. (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**
Step	Hyp	Ref	Expression
1		mcubic.m	. . . . . 6 ⊢ (𝜑 → 𝑀 = ((𝐵↑2) − (3 · 𝐶)))
2		mcubic.b	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3	2	sqcld 13790	. . . . . . 7 ⊢ (𝜑 → (𝐵↑2) ∈ ℂ)
4		3cn 11984	. . . . . . . 8 ⊢ 3 ∈ ℂ
5		mcubic.c	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ ℂ)
6		mulcl 10886	. . . . . . . 8 ⊢ ((3 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (3 · 𝐶) ∈ ℂ)
7	4, 5, 6	sylancr 586	. . . . . . 7 ⊢ (𝜑 → (3 · 𝐶) ∈ ℂ)
8	3, 7	subcld 11262	. . . . . 6 ⊢ (𝜑 → ((𝐵↑2) − (3 · 𝐶)) ∈ ℂ)
9	1, 8	eqeltrd 2839	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ ℂ)
10	4	a1i 11	. . . . 5 ⊢ (𝜑 → 3 ∈ ℂ)
11		3ne0 12009	. . . . . 6 ⊢ 3 ≠ 0
12	11	a1i 11	. . . . 5 ⊢ (𝜑 → 3 ≠ 0)
13	9, 10, 12	divcld 11681	. . . 4 ⊢ (𝜑 → (𝑀 / 3) ∈ ℂ)
14	13	negcld 11249	. . 3 ⊢ (𝜑 → -(𝑀 / 3) ∈ ℂ)
15		mcubic.n	. . . . 5 ⊢ (𝜑 → 𝑁 = (((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) + (;27 · 𝐷)))
16		2cn 11978	. . . . . . . 8 ⊢ 2 ∈ ℂ
17		3nn0 12181	. . . . . . . . 9 ⊢ 3 ∈ ℕ₀
18		expcl 13728	. . . . . . . . 9 ⊢ ((𝐵 ∈ ℂ ∧ 3 ∈ ℕ₀) → (𝐵↑3) ∈ ℂ)
19	2, 17, 18	sylancl 585	. . . . . . . 8 ⊢ (𝜑 → (𝐵↑3) ∈ ℂ)
20		mulcl 10886	. . . . . . . 8 ⊢ ((2 ∈ ℂ ∧ (𝐵↑3) ∈ ℂ) → (2 · (𝐵↑3)) ∈ ℂ)
21	16, 19, 20	sylancr 586	. . . . . . 7 ⊢ (𝜑 → (2 · (𝐵↑3)) ∈ ℂ)
22		9cn 12003	. . . . . . . 8 ⊢ 9 ∈ ℂ
23	2, 5	mulcld 10926	. . . . . . . 8 ⊢ (𝜑 → (𝐵 · 𝐶) ∈ ℂ)
24		mulcl 10886	. . . . . . . 8 ⊢ ((9 ∈ ℂ ∧ (𝐵 · 𝐶) ∈ ℂ) → (9 · (𝐵 · 𝐶)) ∈ ℂ)
25	22, 23, 24	sylancr 586	. . . . . . 7 ⊢ (𝜑 → (9 · (𝐵 · 𝐶)) ∈ ℂ)
26	21, 25	subcld 11262	. . . . . 6 ⊢ (𝜑 → ((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) ∈ ℂ)
27		2nn0 12180	. . . . . . . . 9 ⊢ 2 ∈ ℕ₀
28		7nn 11995	. . . . . . . . 9 ⊢ 7 ∈ ℕ
29	27, 28	decnncl 12386	. . . . . . . 8 ⊢ ;27 ∈ ℕ
30	29	nncni 11913	. . . . . . 7 ⊢ ;27 ∈ ℂ
31		mcubic.d	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ ℂ)
32		mulcl 10886	. . . . . . 7 ⊢ ((;27 ∈ ℂ ∧ 𝐷 ∈ ℂ) → (;27 · 𝐷) ∈ ℂ)
33	30, 31, 32	sylancr 586	. . . . . 6 ⊢ (𝜑 → (;27 · 𝐷) ∈ ℂ)
34	26, 33	addcld 10925	. . . . 5 ⊢ (𝜑 → (((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) + (;27 · 𝐷)) ∈ ℂ)
35	15, 34	eqeltrd 2839	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ℂ)
36	30	a1i 11	. . . 4 ⊢ (𝜑 → ;27 ∈ ℂ)
37	29	nnne0i 11943	. . . . 5 ⊢ ;27 ≠ 0
38	37	a1i 11	. . . 4 ⊢ (𝜑 → ;27 ≠ 0)
39	35, 36, 38	divcld 11681	. . 3 ⊢ (𝜑 → (𝑁 / ;27) ∈ ℂ)
40		mcubic.x	. . . 4 ⊢ (𝜑 → 𝑋 ∈ ℂ)
41	2, 10, 12	divcld 11681	. . . 4 ⊢ (𝜑 → (𝐵 / 3) ∈ ℂ)
42	40, 41	addcld 10925	. . 3 ⊢ (𝜑 → (𝑋 + (𝐵 / 3)) ∈ ℂ)
43		mcubic.t	. . . . 5 ⊢ (𝜑 → 𝑇 ∈ ℂ)
44	43, 10, 12	divcld 11681	. . . 4 ⊢ (𝜑 → (𝑇 / 3) ∈ ℂ)
45	44	negcld 11249	. . 3 ⊢ (𝜑 → -(𝑇 / 3) ∈ ℂ)
46		3nn 11982	. . . . . 6 ⊢ 3 ∈ ℕ
47	46	a1i 11	. . . . 5 ⊢ (𝜑 → 3 ∈ ℕ)
48		n2dvds3 16008	. . . . . 6 ⊢ ¬ 2 ∥ 3
49	48	a1i 11	. . . . 5 ⊢ (𝜑 → ¬ 2 ∥ 3)
50		oexpneg 15982	. . . . 5 ⊢ (((𝑇 / 3) ∈ ℂ ∧ 3 ∈ ℕ ∧ ¬ 2 ∥ 3) → (-(𝑇 / 3)↑3) = -((𝑇 / 3)↑3))
51	44, 47, 49, 50	syl3anc 1369	. . . 4 ⊢ (𝜑 → (-(𝑇 / 3)↑3) = -((𝑇 / 3)↑3))
52	17	a1i 11	. . . . . . 7 ⊢ (𝜑 → 3 ∈ ℕ₀)
53	43, 10, 12, 52	expdivd 13806	. . . . . 6 ⊢ (𝜑 → ((𝑇 / 3)↑3) = ((𝑇↑3) / (3↑3)))
54		mcubic.3	. . . . . . 7 ⊢ (𝜑 → (𝑇↑3) = ((𝑁 + 𝐺) / 2))
55		3exp3 16721	. . . . . . . 8 ⊢ (3↑3) = ;27
56	55	a1i 11	. . . . . . 7 ⊢ (𝜑 → (3↑3) = ;27)
57	54, 56	oveq12d 7273	. . . . . 6 ⊢ (𝜑 → ((𝑇↑3) / (3↑3)) = (((𝑁 + 𝐺) / 2) / ;27))
58		mcubic.g	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 ∈ ℂ)
59	35, 58	addcld 10925	. . . . . . . 8 ⊢ (𝜑 → (𝑁 + 𝐺) ∈ ℂ)
60		2cnd 11981	. . . . . . . 8 ⊢ (𝜑 → 2 ∈ ℂ)
61		2ne0 12007	. . . . . . . . 9 ⊢ 2 ≠ 0
62	61	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 2 ≠ 0)
63	59, 60, 36, 62, 38	divdiv32d 11706	. . . . . . 7 ⊢ (𝜑 → (((𝑁 + 𝐺) / 2) / ;27) = (((𝑁 + 𝐺) / ;27) / 2))
64	35, 58	addcomd 11107	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 + 𝐺) = (𝐺 + 𝑁))
65	64	oveq1d 7270	. . . . . . . . 9 ⊢ (𝜑 → ((𝑁 + 𝐺) / ;27) = ((𝐺 + 𝑁) / ;27))
66	58, 35, 36, 38	divdird 11719	. . . . . . . . 9 ⊢ (𝜑 → ((𝐺 + 𝑁) / ;27) = ((𝐺 / ;27) + (𝑁 / ;27)))
67	65, 66	eqtrd 2778	. . . . . . . 8 ⊢ (𝜑 → ((𝑁 + 𝐺) / ;27) = ((𝐺 / ;27) + (𝑁 / ;27)))
68	67	oveq1d 7270	. . . . . . 7 ⊢ (𝜑 → (((𝑁 + 𝐺) / ;27) / 2) = (((𝐺 / ;27) + (𝑁 / ;27)) / 2))
69	58, 36, 38	divcld 11681	. . . . . . . 8 ⊢ (𝜑 → (𝐺 / ;27) ∈ ℂ)
70	69, 39, 60, 62	divdird 11719	. . . . . . 7 ⊢ (𝜑 → (((𝐺 / ;27) + (𝑁 / ;27)) / 2) = (((𝐺 / ;27) / 2) + ((𝑁 / ;27) / 2)))
71	63, 68, 70	3eqtrd 2782	. . . . . 6 ⊢ (𝜑 → (((𝑁 + 𝐺) / 2) / ;27) = (((𝐺 / ;27) / 2) + ((𝑁 / ;27) / 2)))
72	53, 57, 71	3eqtrd 2782	. . . . 5 ⊢ (𝜑 → ((𝑇 / 3)↑3) = (((𝐺 / ;27) / 2) + ((𝑁 / ;27) / 2)))
73	72	negeqd 11145	. . . 4 ⊢ (𝜑 → -((𝑇 / 3)↑3) = -(((𝐺 / ;27) / 2) + ((𝑁 / ;27) / 2)))
74	69	halfcld 12148	. . . . 5 ⊢ (𝜑 → ((𝐺 / ;27) / 2) ∈ ℂ)
75	39	halfcld 12148	. . . . 5 ⊢ (𝜑 → ((𝑁 / ;27) / 2) ∈ ℂ)
76	74, 75	negdi2d 11276	. . . 4 ⊢ (𝜑 → -(((𝐺 / ;27) / 2) + ((𝑁 / ;27) / 2)) = (-((𝐺 / ;27) / 2) − ((𝑁 / ;27) / 2)))
77	51, 73, 76	3eqtrd 2782	. . 3 ⊢ (𝜑 → (-(𝑇 / 3)↑3) = (-((𝐺 / ;27) / 2) − ((𝑁 / ;27) / 2)))
78	74	negcld 11249	. . 3 ⊢ (𝜑 → -((𝐺 / ;27) / 2) ∈ ℂ)
79		sqneg 13764	. . . . 5 ⊢ (((𝐺 / ;27) / 2) ∈ ℂ → (-((𝐺 / ;27) / 2)↑2) = (((𝐺 / ;27) / 2)↑2))
80	74, 79	syl 17	. . . 4 ⊢ (𝜑 → (-((𝐺 / ;27) / 2)↑2) = (((𝐺 / ;27) / 2)↑2))
81	69, 60, 62	sqdivd 13805	. . . 4 ⊢ (𝜑 → (((𝐺 / ;27) / 2)↑2) = (((𝐺 / ;27)↑2) / (2↑2)))
82	39, 60, 62	sqdivd 13805	. . . . . . . 8 ⊢ (𝜑 → (((𝑁 / ;27) / 2)↑2) = (((𝑁 / ;27)↑2) / (2↑2)))
83	35, 36, 38	sqdivd 13805	. . . . . . . . 9 ⊢ (𝜑 → ((𝑁 / ;27)↑2) = ((𝑁↑2) / (;27↑2)))
84	83	oveq1d 7270	. . . . . . . 8 ⊢ (𝜑 → (((𝑁 / ;27)↑2) / (2↑2)) = (((𝑁↑2) / (;27↑2)) / (2↑2)))
85	82, 84	eqtr2d 2779	. . . . . . 7 ⊢ (𝜑 → (((𝑁↑2) / (;27↑2)) / (2↑2)) = (((𝑁 / ;27) / 2)↑2))
86		4cn 11988	. . . . . . . . . . . 12 ⊢ 4 ∈ ℂ
87	86	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 4 ∈ ℂ)
88		expcl 13728	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℂ ∧ 3 ∈ ℕ₀) → (𝑀↑3) ∈ ℂ)
89	9, 17, 88	sylancl 585	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀↑3) ∈ ℂ)
90	30	sqcli 13826	. . . . . . . . . . . 12 ⊢ (;27↑2) ∈ ℂ
91	90	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (;27↑2) ∈ ℂ)
92		sqne0 13771	. . . . . . . . . . . . 13 ⊢ (;27 ∈ ℂ → ((;27↑2) ≠ 0 ↔ ;27 ≠ 0))
93	36, 92	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → ((;27↑2) ≠ 0 ↔ ;27 ≠ 0))
94	38, 93	mpbird 256	. . . . . . . . . . 11 ⊢ (𝜑 → (;27↑2) ≠ 0)
95	87, 89, 91, 94	divassd 11716	. . . . . . . . . 10 ⊢ (𝜑 → ((4 · (𝑀↑3)) / (;27↑2)) = (4 · ((𝑀↑3) / (;27↑2))))
96	22	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 9 ∈ ℂ)
97		9nn 12001	. . . . . . . . . . . . . . 15 ⊢ 9 ∈ ℕ
98	97	nnne0i 11943	. . . . . . . . . . . . . 14 ⊢ 9 ≠ 0
99	98	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 9 ≠ 0)
100	9, 96, 99, 52	expdivd 13806	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑀 / 9)↑3) = ((𝑀↑3) / (9↑3)))
101	16, 4	mulcomi 10914	. . . . . . . . . . . . . . . 16 ⊢ (2 · 3) = (3 · 2)
102	101	oveq2i 7266	. . . . . . . . . . . . . . 15 ⊢ (3↑(2 · 3)) = (3↑(3 · 2))
103		expmul 13756	. . . . . . . . . . . . . . . 16 ⊢ ((3 ∈ ℂ ∧ 2 ∈ ℕ₀ ∧ 3 ∈ ℕ₀) → (3↑(2 · 3)) = ((3↑2)↑3))
104	4, 27, 17, 103	mp3an 1459	. . . . . . . . . . . . . . 15 ⊢ (3↑(2 · 3)) = ((3↑2)↑3)
105		expmul 13756	. . . . . . . . . . . . . . . 16 ⊢ ((3 ∈ ℂ ∧ 3 ∈ ℕ₀ ∧ 2 ∈ ℕ₀) → (3↑(3 · 2)) = ((3↑3)↑2))
106	4, 17, 27, 105	mp3an 1459	. . . . . . . . . . . . . . 15 ⊢ (3↑(3 · 2)) = ((3↑3)↑2)
107	102, 104, 106	3eqtr3i 2774	. . . . . . . . . . . . . 14 ⊢ ((3↑2)↑3) = ((3↑3)↑2)
108		sq3 13843	. . . . . . . . . . . . . . 15 ⊢ (3↑2) = 9
109	108	oveq1i 7265	. . . . . . . . . . . . . 14 ⊢ ((3↑2)↑3) = (9↑3)
110	55	oveq1i 7265	. . . . . . . . . . . . . 14 ⊢ ((3↑3)↑2) = (;27↑2)
111	107, 109, 110	3eqtr3i 2774	. . . . . . . . . . . . 13 ⊢ (9↑3) = (;27↑2)
112	111	oveq2i 7266	. . . . . . . . . . . 12 ⊢ ((𝑀↑3) / (9↑3)) = ((𝑀↑3) / (;27↑2))
113	100, 112	eqtrdi 2795	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑀 / 9)↑3) = ((𝑀↑3) / (;27↑2)))
114	113	oveq2d 7271	. . . . . . . . . 10 ⊢ (𝜑 → (4 · ((𝑀 / 9)↑3)) = (4 · ((𝑀↑3) / (;27↑2))))
115	95, 114	eqtr4d 2781	. . . . . . . . 9 ⊢ (𝜑 → ((4 · (𝑀↑3)) / (;27↑2)) = (4 · ((𝑀 / 9)↑3)))
116	115	oveq1d 7270	. . . . . . . 8 ⊢ (𝜑 → (((4 · (𝑀↑3)) / (;27↑2)) / (2↑2)) = ((4 · ((𝑀 / 9)↑3)) / (2↑2)))
117		sq2 13842	. . . . . . . . . 10 ⊢ (2↑2) = 4
118	117	oveq2i 7266	. . . . . . . . 9 ⊢ ((4 · ((𝑀 / 9)↑3)) / (2↑2)) = ((4 · ((𝑀 / 9)↑3)) / 4)
119	9, 96, 99	divcld 11681	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀 / 9) ∈ ℂ)
120		expcl 13728	. . . . . . . . . . 11 ⊢ (((𝑀 / 9) ∈ ℂ ∧ 3 ∈ ℕ₀) → ((𝑀 / 9)↑3) ∈ ℂ)
121	119, 17, 120	sylancl 585	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑀 / 9)↑3) ∈ ℂ)
122		4ne0 12011	. . . . . . . . . . 11 ⊢ 4 ≠ 0
123	122	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 4 ≠ 0)
124	121, 87, 123	divcan3d 11686	. . . . . . . . 9 ⊢ (𝜑 → ((4 · ((𝑀 / 9)↑3)) / 4) = ((𝑀 / 9)↑3))
125	118, 124	syl5eq 2791	. . . . . . . 8 ⊢ (𝜑 → ((4 · ((𝑀 / 9)↑3)) / (2↑2)) = ((𝑀 / 9)↑3))
126	116, 125	eqtrd 2778	. . . . . . 7 ⊢ (𝜑 → (((4 · (𝑀↑3)) / (;27↑2)) / (2↑2)) = ((𝑀 / 9)↑3))
127	85, 126	oveq12d 7273	. . . . . 6 ⊢ (𝜑 → ((((𝑁↑2) / (;27↑2)) / (2↑2)) − (((4 · (𝑀↑3)) / (;27↑2)) / (2↑2))) = ((((𝑁 / ;27) / 2)↑2) − ((𝑀 / 9)↑3)))
128	35	sqcld 13790	. . . . . . . 8 ⊢ (𝜑 → (𝑁↑2) ∈ ℂ)
129	128, 91, 94	divcld 11681	. . . . . . 7 ⊢ (𝜑 → ((𝑁↑2) / (;27↑2)) ∈ ℂ)
130		mulcl 10886	. . . . . . . . 9 ⊢ ((4 ∈ ℂ ∧ (𝑀↑3) ∈ ℂ) → (4 · (𝑀↑3)) ∈ ℂ)
131	86, 89, 130	sylancr 586	. . . . . . . 8 ⊢ (𝜑 → (4 · (𝑀↑3)) ∈ ℂ)
132	131, 91, 94	divcld 11681	. . . . . . 7 ⊢ (𝜑 → ((4 · (𝑀↑3)) / (;27↑2)) ∈ ℂ)
133	16	sqcli 13826	. . . . . . . 8 ⊢ (2↑2) ∈ ℂ
134	133	a1i 11	. . . . . . 7 ⊢ (𝜑 → (2↑2) ∈ ℂ)
135	117, 122	eqnetri 3013	. . . . . . . 8 ⊢ (2↑2) ≠ 0
136	135	a1i 11	. . . . . . 7 ⊢ (𝜑 → (2↑2) ≠ 0)
137	129, 132, 134, 136	divsubdird 11720	. . . . . 6 ⊢ (𝜑 → ((((𝑁↑2) / (;27↑2)) − ((4 · (𝑀↑3)) / (;27↑2))) / (2↑2)) = ((((𝑁↑2) / (;27↑2)) / (2↑2)) − (((4 · (𝑀↑3)) / (;27↑2)) / (2↑2))))
138	75	sqcld 13790	. . . . . . 7 ⊢ (𝜑 → (((𝑁 / ;27) / 2)↑2) ∈ ℂ)
139	138, 121	negsubd 11268	. . . . . 6 ⊢ (𝜑 → ((((𝑁 / ;27) / 2)↑2) + -((𝑀 / 9)↑3)) = ((((𝑁 / ;27) / 2)↑2) − ((𝑀 / 9)↑3)))
140	127, 137, 139	3eqtr4d 2788	. . . . 5 ⊢ (𝜑 → ((((𝑁↑2) / (;27↑2)) − ((4 · (𝑀↑3)) / (;27↑2))) / (2↑2)) = ((((𝑁 / ;27) / 2)↑2) + -((𝑀 / 9)↑3)))
141	58, 36, 38	sqdivd 13805	. . . . . . 7 ⊢ (𝜑 → ((𝐺 / ;27)↑2) = ((𝐺↑2) / (;27↑2)))
142		mcubic.2	. . . . . . . 8 ⊢ (𝜑 → (𝐺↑2) = ((𝑁↑2) − (4 · (𝑀↑3))))
143	142	oveq1d 7270	. . . . . . 7 ⊢ (𝜑 → ((𝐺↑2) / (;27↑2)) = (((𝑁↑2) − (4 · (𝑀↑3))) / (;27↑2)))
144	128, 131, 91, 94	divsubdird 11720	. . . . . . 7 ⊢ (𝜑 → (((𝑁↑2) − (4 · (𝑀↑3))) / (;27↑2)) = (((𝑁↑2) / (;27↑2)) − ((4 · (𝑀↑3)) / (;27↑2))))
145	141, 143, 144	3eqtrd 2782	. . . . . 6 ⊢ (𝜑 → ((𝐺 / ;27)↑2) = (((𝑁↑2) / (;27↑2)) − ((4 · (𝑀↑3)) / (;27↑2))))
146	145	oveq1d 7270	. . . . 5 ⊢ (𝜑 → (((𝐺 / ;27)↑2) / (2↑2)) = ((((𝑁↑2) / (;27↑2)) − ((4 · (𝑀↑3)) / (;27↑2))) / (2↑2)))
147		oexpneg 15982	. . . . . . 7 ⊢ (((𝑀 / 9) ∈ ℂ ∧ 3 ∈ ℕ ∧ ¬ 2 ∥ 3) → (-(𝑀 / 9)↑3) = -((𝑀 / 9)↑3))
148	119, 47, 49, 147	syl3anc 1369	. . . . . 6 ⊢ (𝜑 → (-(𝑀 / 9)↑3) = -((𝑀 / 9)↑3))
149	148	oveq2d 7271	. . . . 5 ⊢ (𝜑 → ((((𝑁 / ;27) / 2)↑2) + (-(𝑀 / 9)↑3)) = ((((𝑁 / ;27) / 2)↑2) + -((𝑀 / 9)↑3)))
150	140, 146, 149	3eqtr4d 2788	. . . 4 ⊢ (𝜑 → (((𝐺 / ;27)↑2) / (2↑2)) = ((((𝑁 / ;27) / 2)↑2) + (-(𝑀 / 9)↑3)))
151	80, 81, 150	3eqtrd 2782	. . 3 ⊢ (𝜑 → (-((𝐺 / ;27) / 2)↑2) = ((((𝑁 / ;27) / 2)↑2) + (-(𝑀 / 9)↑3)))
152	9, 10, 10, 12, 12	divdiv1d 11712	. . . . . 6 ⊢ (𝜑 → ((𝑀 / 3) / 3) = (𝑀 / (3 · 3)))
153		3t3e9 12070	. . . . . . 7 ⊢ (3 · 3) = 9
154	153	oveq2i 7266	. . . . . 6 ⊢ (𝑀 / (3 · 3)) = (𝑀 / 9)
155	152, 154	eqtrdi 2795	. . . . 5 ⊢ (𝜑 → ((𝑀 / 3) / 3) = (𝑀 / 9))
156	155	negeqd 11145	. . . 4 ⊢ (𝜑 → -((𝑀 / 3) / 3) = -(𝑀 / 9))
157	13, 10, 12	divnegd 11694	. . . 4 ⊢ (𝜑 → -((𝑀 / 3) / 3) = (-(𝑀 / 3) / 3))
158	156, 157	eqtr3d 2780	. . 3 ⊢ (𝜑 → -(𝑀 / 9) = (-(𝑀 / 3) / 3))
159		eqidd 2739	. . 3 ⊢ (𝜑 → ((𝑁 / ;27) / 2) = ((𝑁 / ;27) / 2))
160		mcubic.0	. . . . 5 ⊢ (𝜑 → 𝑇 ≠ 0)
161	43, 10, 160, 12	divne0d 11697	. . . 4 ⊢ (𝜑 → (𝑇 / 3) ≠ 0)
162	44, 161	negne0d 11260	. . 3 ⊢ (𝜑 → -(𝑇 / 3) ≠ 0)
163	14, 39, 42, 45, 77, 78, 151, 158, 159, 162	dcubic 25901	. 2 ⊢ (𝜑 → ((((𝑋 + (𝐵 / 3))↑3) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27))) = 0 ↔ ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ (𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))))))
164		binom3 13867	. . . . . . 7 ⊢ ((𝑋 ∈ ℂ ∧ (𝐵 / 3) ∈ ℂ) → ((𝑋 + (𝐵 / 3))↑3) = (((𝑋↑3) + (3 · ((𝑋↑2) · (𝐵 / 3)))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))))
165	40, 41, 164	syl2anc 583	. . . . . 6 ⊢ (𝜑 → ((𝑋 + (𝐵 / 3))↑3) = (((𝑋↑3) + (3 · ((𝑋↑2) · (𝐵 / 3)))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))))
166	40	sqcld 13790	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋↑2) ∈ ℂ)
167	10, 166, 41	mul12d 11114	. . . . . . . . 9 ⊢ (𝜑 → (3 · ((𝑋↑2) · (𝐵 / 3))) = ((𝑋↑2) · (3 · (𝐵 / 3))))
168	2, 10, 12	divcan2d 11683	. . . . . . . . . 10 ⊢ (𝜑 → (3 · (𝐵 / 3)) = 𝐵)
169	168	oveq2d 7271	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋↑2) · (3 · (𝐵 / 3))) = ((𝑋↑2) · 𝐵))
170	166, 2	mulcomd 10927	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋↑2) · 𝐵) = (𝐵 · (𝑋↑2)))
171	167, 169, 170	3eqtrd 2782	. . . . . . . 8 ⊢ (𝜑 → (3 · ((𝑋↑2) · (𝐵 / 3))) = (𝐵 · (𝑋↑2)))
172	171	oveq2d 7271	. . . . . . 7 ⊢ (𝜑 → ((𝑋↑3) + (3 · ((𝑋↑2) · (𝐵 / 3)))) = ((𝑋↑3) + (𝐵 · (𝑋↑2))))
173	172	oveq1d 7270	. . . . . 6 ⊢ (𝜑 → (((𝑋↑3) + (3 · ((𝑋↑2) · (𝐵 / 3)))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))) = (((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))))
174	165, 173	eqtrd 2778	. . . . 5 ⊢ (𝜑 → ((𝑋 + (𝐵 / 3))↑3) = (((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))))
175	174	oveq1d 7270	. . . 4 ⊢ (𝜑 → (((𝑋 + (𝐵 / 3))↑3) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27))) = ((((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27))))
176		expcl 13728	. . . . . . 7 ⊢ ((𝑋 ∈ ℂ ∧ 3 ∈ ℕ₀) → (𝑋↑3) ∈ ℂ)
177	40, 17, 176	sylancl 585	. . . . . 6 ⊢ (𝜑 → (𝑋↑3) ∈ ℂ)
178	2, 166	mulcld 10926	. . . . . 6 ⊢ (𝜑 → (𝐵 · (𝑋↑2)) ∈ ℂ)
179	177, 178	addcld 10925	. . . . 5 ⊢ (𝜑 → ((𝑋↑3) + (𝐵 · (𝑋↑2))) ∈ ℂ)
180	41	sqcld 13790	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 / 3)↑2) ∈ ℂ)
181	40, 180	mulcld 10926	. . . . . . 7 ⊢ (𝜑 → (𝑋 · ((𝐵 / 3)↑2)) ∈ ℂ)
182	10, 181	mulcld 10926	. . . . . 6 ⊢ (𝜑 → (3 · (𝑋 · ((𝐵 / 3)↑2))) ∈ ℂ)
183		expcl 13728	. . . . . . 7 ⊢ (((𝐵 / 3) ∈ ℂ ∧ 3 ∈ ℕ₀) → ((𝐵 / 3)↑3) ∈ ℂ)
184	41, 17, 183	sylancl 585	. . . . . 6 ⊢ (𝜑 → ((𝐵 / 3)↑3) ∈ ℂ)
185	182, 184	addcld 10925	. . . . 5 ⊢ (𝜑 → ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) ∈ ℂ)
186	14, 42	mulcld 10926	. . . . . 6 ⊢ (𝜑 → (-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) ∈ ℂ)
187	186, 39	addcld 10925	. . . . 5 ⊢ (𝜑 → ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27)) ∈ ℂ)
188	179, 185, 187	addassd 10928	. . . 4 ⊢ (𝜑 → ((((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27))) = (((𝑋↑3) + (𝐵 · (𝑋↑2))) + (((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27)))))
189	14, 40, 41	adddid 10930	. . . . . . . . . 10 ⊢ (𝜑 → (-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) = ((-(𝑀 / 3) · 𝑋) + (-(𝑀 / 3) · (𝐵 / 3))))
190	189	oveq1d 7270	. . . . . . . . 9 ⊢ (𝜑 → ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27)) = (((-(𝑀 / 3) · 𝑋) + (-(𝑀 / 3) · (𝐵 / 3))) + (𝑁 / ;27)))
191	14, 40	mulcld 10926	. . . . . . . . . 10 ⊢ (𝜑 → (-(𝑀 / 3) · 𝑋) ∈ ℂ)
192	14, 41	mulcld 10926	. . . . . . . . . 10 ⊢ (𝜑 → (-(𝑀 / 3) · (𝐵 / 3)) ∈ ℂ)
193	191, 192, 39	addassd 10928	. . . . . . . . 9 ⊢ (𝜑 → (((-(𝑀 / 3) · 𝑋) + (-(𝑀 / 3) · (𝐵 / 3))) + (𝑁 / ;27)) = ((-(𝑀 / 3) · 𝑋) + ((-(𝑀 / 3) · (𝐵 / 3)) + (𝑁 / ;27))))
194	1	oveq1d 7270	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀 / 3) = (((𝐵↑2) − (3 · 𝐶)) / 3))
195	3, 7, 10, 12	divsubdird 11720	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐵↑2) − (3 · 𝐶)) / 3) = (((𝐵↑2) / 3) − ((3 · 𝐶) / 3)))
196	5, 10, 12	divcan3d 11686	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((3 · 𝐶) / 3) = 𝐶)
197	196	oveq2d 7271	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐵↑2) / 3) − ((3 · 𝐶) / 3)) = (((𝐵↑2) / 3) − 𝐶))
198	194, 195, 197	3eqtrd 2782	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀 / 3) = (((𝐵↑2) / 3) − 𝐶))
199	198	negeqd 11145	. . . . . . . . . . . . 13 ⊢ (𝜑 → -(𝑀 / 3) = -(((𝐵↑2) / 3) − 𝐶))
200	3, 10, 12	divcld 11681	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵↑2) / 3) ∈ ℂ)
201	200, 5	negsubdi2d 11278	. . . . . . . . . . . . 13 ⊢ (𝜑 → -(((𝐵↑2) / 3) − 𝐶) = (𝐶 − ((𝐵↑2) / 3)))
202	199, 201	eqtrd 2778	. . . . . . . . . . . 12 ⊢ (𝜑 → -(𝑀 / 3) = (𝐶 − ((𝐵↑2) / 3)))
203	202	oveq1d 7270	. . . . . . . . . . 11 ⊢ (𝜑 → (-(𝑀 / 3) · 𝑋) = ((𝐶 − ((𝐵↑2) / 3)) · 𝑋))
204	5, 200, 40	subdird 11362	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐶 − ((𝐵↑2) / 3)) · 𝑋) = ((𝐶 · 𝑋) − (((𝐵↑2) / 3) · 𝑋)))
205	200, 40	mulcomd 10927	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐵↑2) / 3) · 𝑋) = (𝑋 · ((𝐵↑2) / 3)))
206	4	sqvali 13825	. . . . . . . . . . . . . . . . . 18 ⊢ (3↑2) = (3 · 3)
207	206	oveq2i 7266	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵↑2) / (3↑2)) = ((𝐵↑2) / (3 · 3))
208	2, 10, 12	sqdivd 13805	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐵 / 3)↑2) = ((𝐵↑2) / (3↑2)))
209	3, 10, 10, 12, 12	divdiv1d 11712	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝐵↑2) / 3) / 3) = ((𝐵↑2) / (3 · 3)))
210	207, 208, 209	3eqtr4a 2805	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐵 / 3)↑2) = (((𝐵↑2) / 3) / 3))
211	210	oveq2d 7271	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (3 · ((𝐵 / 3)↑2)) = (3 · (((𝐵↑2) / 3) / 3)))
212	200, 10, 12	divcan2d 11683	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (3 · (((𝐵↑2) / 3) / 3)) = ((𝐵↑2) / 3))
213	211, 212	eqtrd 2778	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (3 · ((𝐵 / 3)↑2)) = ((𝐵↑2) / 3))
214	213	oveq2d 7271	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 · (3 · ((𝐵 / 3)↑2))) = (𝑋 · ((𝐵↑2) / 3)))
215	40, 10, 180	mul12d 11114	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 · (3 · ((𝐵 / 3)↑2))) = (3 · (𝑋 · ((𝐵 / 3)↑2))))
216	205, 214, 215	3eqtr2d 2784	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐵↑2) / 3) · 𝑋) = (3 · (𝑋 · ((𝐵 / 3)↑2))))
217	216	oveq2d 7271	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐶 · 𝑋) − (((𝐵↑2) / 3) · 𝑋)) = ((𝐶 · 𝑋) − (3 · (𝑋 · ((𝐵 / 3)↑2)))))
218	203, 204, 217	3eqtrd 2782	. . . . . . . . . 10 ⊢ (𝜑 → (-(𝑀 / 3) · 𝑋) = ((𝐶 · 𝑋) − (3 · (𝑋 · ((𝐵 / 3)↑2)))))
219	202	oveq1d 7270	. . . . . . . . . . . . 13 ⊢ (𝜑 → (-(𝑀 / 3) · (𝐵 / 3)) = ((𝐶 − ((𝐵↑2) / 3)) · (𝐵 / 3)))
220	5, 200, 41	subdird 11362	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐶 − ((𝐵↑2) / 3)) · (𝐵 / 3)) = ((𝐶 · (𝐵 / 3)) − (((𝐵↑2) / 3) · (𝐵 / 3))))
221	5, 2, 10, 12	divassd 11716	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐶 · 𝐵) / 3) = (𝐶 · (𝐵 / 3)))
222	5, 2	mulcomd 10927	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐶 · 𝐵) = (𝐵 · 𝐶))
223	222	oveq1d 7270	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐶 · 𝐵) / 3) = ((𝐵 · 𝐶) / 3))
224	221, 223	eqtr3d 2780	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐶 · (𝐵 / 3)) = ((𝐵 · 𝐶) / 3))
225	3, 10, 2, 10, 12, 12	divmuldivd 11722	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐵↑2) / 3) · (𝐵 / 3)) = (((𝐵↑2) · 𝐵) / (3 · 3)))
226		df-3 11967	. . . . . . . . . . . . . . . . . 18 ⊢ 3 = (2 + 1)
227	226	oveq2i 7266	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵↑3) = (𝐵↑(2 + 1))
228		expp1 13717	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ∈ ℂ ∧ 2 ∈ ℕ₀) → (𝐵↑(2 + 1)) = ((𝐵↑2) · 𝐵))
229	2, 27, 228	sylancl 585	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵↑(2 + 1)) = ((𝐵↑2) · 𝐵))
230	227, 229	eqtr2id 2792	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐵↑2) · 𝐵) = (𝐵↑3))
231	153	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (3 · 3) = 9)
232	230, 231	oveq12d 7273	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐵↑2) · 𝐵) / (3 · 3)) = ((𝐵↑3) / 9))
233	225, 232	eqtrd 2778	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐵↑2) / 3) · (𝐵 / 3)) = ((𝐵↑3) / 9))
234	224, 233	oveq12d 7273	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐶 · (𝐵 / 3)) − (((𝐵↑2) / 3) · (𝐵 / 3))) = (((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)))
235	219, 220, 234	3eqtrd 2782	. . . . . . . . . . . 12 ⊢ (𝜑 → (-(𝑀 / 3) · (𝐵 / 3)) = (((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)))
236	15	oveq1d 7270	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 / ;27) = ((((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) + (;27 · 𝐷)) / ;27))
237	26, 33, 36, 38	divdird 11719	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) + (;27 · 𝐷)) / ;27) = ((((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) / ;27) + ((;27 · 𝐷) / ;27)))
238	21, 25, 36, 38	divsubdird 11720	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) / ;27) = (((2 · (𝐵↑3)) / ;27) − ((9 · (𝐵 · 𝐶)) / ;27)))
239		9t3e27 12489	. . . . . . . . . . . . . . . . . 18 ⊢ (9 · 3) = ;27
240	239	oveq2i 7266	. . . . . . . . . . . . . . . . 17 ⊢ ((9 · (𝐵 · 𝐶)) / (9 · 3)) = ((9 · (𝐵 · 𝐶)) / ;27)
241	23, 10, 96, 12, 99	divcan5d 11707	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((9 · (𝐵 · 𝐶)) / (9 · 3)) = ((𝐵 · 𝐶) / 3))
242	240, 241	eqtr3id 2793	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((9 · (𝐵 · 𝐶)) / ;27) = ((𝐵 · 𝐶) / 3))
243	242	oveq2d 7271	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((2 · (𝐵↑3)) / ;27) − ((9 · (𝐵 · 𝐶)) / ;27)) = (((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3)))
244	238, 243	eqtrd 2778	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) / ;27) = (((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3)))
245	31, 36, 38	divcan3d 11686	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((;27 · 𝐷) / ;27) = 𝐷)
246	244, 245	oveq12d 7273	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) / ;27) + ((;27 · 𝐷) / ;27)) = ((((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3)) + 𝐷))
247	236, 237, 246	3eqtrd 2782	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁 / ;27) = ((((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3)) + 𝐷))
248	235, 247	oveq12d 7273	. . . . . . . . . . 11 ⊢ (𝜑 → ((-(𝑀 / 3) · (𝐵 / 3)) + (𝑁 / ;27)) = ((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + ((((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3)) + 𝐷)))
249	19, 96, 99	divcld 11681	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐵↑3) / 9) ∈ ℂ)
250	21, 36, 38	divcld 11681	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((2 · (𝐵↑3)) / ;27) ∈ ℂ)
251	249, 250	negsubdi2d 11278	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -(((𝐵↑3) / 9) − ((2 · (𝐵↑3)) / ;27)) = (((2 · (𝐵↑3)) / ;27) − ((𝐵↑3) / 9)))
252	2, 10, 12, 52	expdivd 13806	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐵 / 3)↑3) = ((𝐵↑3) / (3↑3)))
253	55	oveq2i 7266	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵↑3) / (3↑3)) = ((𝐵↑3) / ;27)
254		ax-1cn 10860	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 ∈ ℂ
255		2p1e3 12045	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (2 + 1) = 3
256	4, 16, 254, 255	subaddrii 11240	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (3 − 2) = 1
257	256	oveq1i 7265	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((3 − 2) · (𝐵↑3)) = (1 · (𝐵↑3))
258	19	mulid2d 10924	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (1 · (𝐵↑3)) = (𝐵↑3))
259	257, 258	syl5eq 2791	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((3 − 2) · (𝐵↑3)) = (𝐵↑3))
260	10, 60, 19	subdird 11362	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((3 − 2) · (𝐵↑3)) = ((3 · (𝐵↑3)) − (2 · (𝐵↑3))))
261	259, 260	eqtr3d 2780	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐵↑3) = ((3 · (𝐵↑3)) − (2 · (𝐵↑3))))
262	261	oveq1d 7270	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐵↑3) / ;27) = (((3 · (𝐵↑3)) − (2 · (𝐵↑3))) / ;27))
263		mulcl 10886	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((3 ∈ ℂ ∧ (𝐵↑3) ∈ ℂ) → (3 · (𝐵↑3)) ∈ ℂ)
264	4, 19, 263	sylancr 586	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (3 · (𝐵↑3)) ∈ ℂ)
265	264, 21, 36, 38	divsubdird 11720	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((3 · (𝐵↑3)) − (2 · (𝐵↑3))) / ;27) = (((3 · (𝐵↑3)) / ;27) − ((2 · (𝐵↑3)) / ;27)))
266	262, 265	eqtrd 2778	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐵↑3) / ;27) = (((3 · (𝐵↑3)) / ;27) − ((2 · (𝐵↑3)) / ;27)))
267	253, 266	syl5eq 2791	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐵↑3) / (3↑3)) = (((3 · (𝐵↑3)) / ;27) − ((2 · (𝐵↑3)) / ;27)))
268	22, 4, 239	mulcomli 10915	. . . . . . . . . . . . . . . . . . 19 ⊢ (3 · 9) = ;27
269	268	oveq2i 7266	. . . . . . . . . . . . . . . . . 18 ⊢ ((3 · (𝐵↑3)) / (3 · 9)) = ((3 · (𝐵↑3)) / ;27)
270	19, 96, 10, 99, 12	divcan5d 11707	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((3 · (𝐵↑3)) / (3 · 9)) = ((𝐵↑3) / 9))
271	269, 270	eqtr3id 2793	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((3 · (𝐵↑3)) / ;27) = ((𝐵↑3) / 9))
272	271	oveq1d 7270	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((3 · (𝐵↑3)) / ;27) − ((2 · (𝐵↑3)) / ;27)) = (((𝐵↑3) / 9) − ((2 · (𝐵↑3)) / ;27)))
273	252, 267, 272	3eqtrd 2782	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐵 / 3)↑3) = (((𝐵↑3) / 9) − ((2 · (𝐵↑3)) / ;27)))
274	273	negeqd 11145	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -((𝐵 / 3)↑3) = -(((𝐵↑3) / 9) − ((2 · (𝐵↑3)) / ;27)))
275	23, 10, 12	divcld 11681	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐵 · 𝐶) / 3) ∈ ℂ)
276	275, 249, 250	npncan3d 11298	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + (((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3))) = (((2 · (𝐵↑3)) / ;27) − ((𝐵↑3) / 9)))
277	251, 274, 276	3eqtr4d 2788	. . . . . . . . . . . . 13 ⊢ (𝜑 → -((𝐵 / 3)↑3) = ((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + (((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3))))
278	277	oveq1d 7270	. . . . . . . . . . . 12 ⊢ (𝜑 → (-((𝐵 / 3)↑3) + 𝐷) = (((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + (((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3))) + 𝐷))
279	184	negcld 11249	. . . . . . . . . . . . 13 ⊢ (𝜑 → -((𝐵 / 3)↑3) ∈ ℂ)
280	279, 31	addcomd 11107	. . . . . . . . . . . 12 ⊢ (𝜑 → (-((𝐵 / 3)↑3) + 𝐷) = (𝐷 + -((𝐵 / 3)↑3)))
281	235, 192	eqeltrrd 2840	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) ∈ ℂ)
282	250, 275	subcld 11262	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3)) ∈ ℂ)
283	281, 282, 31	addassd 10928	. . . . . . . . . . . 12 ⊢ (𝜑 → (((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + (((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3))) + 𝐷) = ((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + ((((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3)) + 𝐷)))
284	278, 280, 283	3eqtr3d 2786	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐷 + -((𝐵 / 3)↑3)) = ((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + ((((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3)) + 𝐷)))
285	31, 184	negsubd 11268	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐷 + -((𝐵 / 3)↑3)) = (𝐷 − ((𝐵 / 3)↑3)))
286	248, 284, 285	3eqtr2d 2784	. . . . . . . . . 10 ⊢ (𝜑 → ((-(𝑀 / 3) · (𝐵 / 3)) + (𝑁 / ;27)) = (𝐷 − ((𝐵 / 3)↑3)))
287	218, 286	oveq12d 7273	. . . . . . . . 9 ⊢ (𝜑 → ((-(𝑀 / 3) · 𝑋) + ((-(𝑀 / 3) · (𝐵 / 3)) + (𝑁 / ;27))) = (((𝐶 · 𝑋) − (3 · (𝑋 · ((𝐵 / 3)↑2)))) + (𝐷 − ((𝐵 / 3)↑3))))
288	190, 193, 287	3eqtrd 2782	. . . . . . . 8 ⊢ (𝜑 → ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27)) = (((𝐶 · 𝑋) − (3 · (𝑋 · ((𝐵 / 3)↑2)))) + (𝐷 − ((𝐵 / 3)↑3))))
289	5, 40	mulcld 10926	. . . . . . . . 9 ⊢ (𝜑 → (𝐶 · 𝑋) ∈ ℂ)
290	289, 31, 182, 184	addsub4d 11309	. . . . . . . 8 ⊢ (𝜑 → (((𝐶 · 𝑋) + 𝐷) − ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))) = (((𝐶 · 𝑋) − (3 · (𝑋 · ((𝐵 / 3)↑2)))) + (𝐷 − ((𝐵 / 3)↑3))))
291	288, 290	eqtr4d 2781	. . . . . . 7 ⊢ (𝜑 → ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27)) = (((𝐶 · 𝑋) + 𝐷) − ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))))
292	291	oveq2d 7271	. . . . . 6 ⊢ (𝜑 → (((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27))) = (((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) + (((𝐶 · 𝑋) + 𝐷) − ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)))))
293	289, 31	addcld 10925	. . . . . . 7 ⊢ (𝜑 → ((𝐶 · 𝑋) + 𝐷) ∈ ℂ)
294	185, 293	pncan3d 11265	. . . . . 6 ⊢ (𝜑 → (((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) + (((𝐶 · 𝑋) + 𝐷) − ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)))) = ((𝐶 · 𝑋) + 𝐷))
295	292, 294	eqtrd 2778	. . . . 5 ⊢ (𝜑 → (((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27))) = ((𝐶 · 𝑋) + 𝐷))
296	295	oveq2d 7271	. . . 4 ⊢ (𝜑 → (((𝑋↑3) + (𝐵 · (𝑋↑2))) + (((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27)))) = (((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((𝐶 · 𝑋) + 𝐷)))
297	175, 188, 296	3eqtrd 2782	. . 3 ⊢ (𝜑 → (((𝑋 + (𝐵 / 3))↑3) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27))) = (((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((𝐶 · 𝑋) + 𝐷)))
298	297	eqeq1d 2740	. 2 ⊢ (𝜑 → ((((𝑋 + (𝐵 / 3))↑3) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27))) = 0 ↔ (((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((𝐶 · 𝑋) + 𝐷)) = 0))
299		oveq1 7262	. . . . . . . 8 ⊢ (𝑟 = 0 → (𝑟↑3) = (0↑3))
300		0exp 13746	. . . . . . . . 9 ⊢ (3 ∈ ℕ → (0↑3) = 0)
301	46, 300	ax-mp 5	. . . . . . . 8 ⊢ (0↑3) = 0
302	299, 301	eqtrdi 2795	. . . . . . 7 ⊢ (𝑟 = 0 → (𝑟↑3) = 0)
303		0ne1 11974	. . . . . . . 8 ⊢ 0 ≠ 1
304	303	a1i 11	. . . . . . 7 ⊢ (𝑟 = 0 → 0 ≠ 1)
305	302, 304	eqnetrd 3010	. . . . . 6 ⊢ (𝑟 = 0 → (𝑟↑3) ≠ 1)
306	305	necon2i 2977	. . . . 5 ⊢ ((𝑟↑3) = 1 → 𝑟 ≠ 0)
307		eqcom 2745	. . . . . . . 8 ⊢ (𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) ↔ -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = 𝑋)
308	2	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝐵 ∈ ℂ)
309		simprl 767	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑟 ∈ ℂ)
310	43	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑇 ∈ ℂ)
311	309, 310	mulcld 10926	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑟 · 𝑇) ∈ ℂ)
312	9	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑀 ∈ ℂ)
313		simprr 769	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑟 ≠ 0)
314	160	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑇 ≠ 0)
315	309, 310, 313, 314	mulne0d 11557	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑟 · 𝑇) ≠ 0)
316	312, 311, 315	divcld 11681	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑀 / (𝑟 · 𝑇)) ∈ ℂ)
317	311, 316	addcld 10925	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) ∈ ℂ)
318	4	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 3 ∈ ℂ)
319	11	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 3 ≠ 0)
320	308, 317, 318, 319	divdird 11719	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝐵 + ((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇)))) / 3) = ((𝐵 / 3) + (((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)))
321	308, 311, 316	addassd 10928	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) = (𝐵 + ((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇)))))
322	321	oveq1d 7270	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = ((𝐵 + ((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇)))) / 3))
323	41	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝐵 / 3) ∈ ℂ)
324	317, 318, 319	divcld 11681	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) ∈ ℂ)
325	323, 324	subnegd 11269	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝐵 / 3) − -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)) = ((𝐵 / 3) + (((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)))
326	320, 322, 325	3eqtr4d 2788	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = ((𝐵 / 3) − -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)))
327	326	negeqd 11145	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = -((𝐵 / 3) − -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)))
328	324	negcld 11249	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) ∈ ℂ)
329	323, 328	negsubdi2d 11278	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -((𝐵 / 3) − -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)) = (-(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) − (𝐵 / 3)))
330	327, 329	eqtrd 2778	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = (-(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) − (𝐵 / 3)))
331	330	eqeq1d 2740	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (-(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = 𝑋 ↔ (-(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) − (𝐵 / 3)) = 𝑋))
332	307, 331	syl5bb 282	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) ↔ (-(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) − (𝐵 / 3)) = 𝑋))
333	40	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑋 ∈ ℂ)
334	328, 323, 333	subadd2d 11281	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((-(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) − (𝐵 / 3)) = 𝑋 ↔ (𝑋 + (𝐵 / 3)) = -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)))
335	311, 316, 318, 319	divdird 11719	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) = (((𝑟 · 𝑇) / 3) + ((𝑀 / (𝑟 · 𝑇)) / 3)))
336	335	negeqd 11145	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) = -(((𝑟 · 𝑇) / 3) + ((𝑀 / (𝑟 · 𝑇)) / 3)))
337	311, 318, 319	divcld 11681	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑟 · 𝑇) / 3) ∈ ℂ)
338	316, 318, 319	divcld 11681	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑀 / (𝑟 · 𝑇)) / 3) ∈ ℂ)
339	337, 338	negdi2d 11276	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝑟 · 𝑇) / 3) + ((𝑀 / (𝑟 · 𝑇)) / 3)) = (-((𝑟 · 𝑇) / 3) − ((𝑀 / (𝑟 · 𝑇)) / 3)))
340	309, 310, 318, 319	divassd 11716	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑟 · 𝑇) / 3) = (𝑟 · (𝑇 / 3)))
341	340	negeqd 11145	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -((𝑟 · 𝑇) / 3) = -(𝑟 · (𝑇 / 3)))
342	44	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑇 / 3) ∈ ℂ)
343	309, 342	mulneg2d 11359	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑟 · -(𝑇 / 3)) = -(𝑟 · (𝑇 / 3)))
344	341, 343	eqtr4d 2781	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -((𝑟 · 𝑇) / 3) = (𝑟 · -(𝑇 / 3)))
345	312, 311, 318, 315, 319	divdiv32d 11706	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑀 / (𝑟 · 𝑇)) / 3) = ((𝑀 / 3) / (𝑟 · 𝑇)))
346	13	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑀 / 3) ∈ ℂ)
347	346, 311, 318, 315, 319	divcan7d 11709	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝑀 / 3) / 3) / ((𝑟 · 𝑇) / 3)) = ((𝑀 / 3) / (𝑟 · 𝑇)))
348	155	oveq1d 7270	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑀 / 3) / 3) / ((𝑟 · 𝑇) / 3)) = ((𝑀 / 9) / ((𝑟 · 𝑇) / 3)))
349	348	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝑀 / 3) / 3) / ((𝑟 · 𝑇) / 3)) = ((𝑀 / 9) / ((𝑟 · 𝑇) / 3)))
350	345, 347, 349	3eqtr2d 2784	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑀 / (𝑟 · 𝑇)) / 3) = ((𝑀 / 9) / ((𝑟 · 𝑇) / 3)))
351	119	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑀 / 9) ∈ ℂ)
352	311, 318, 315, 319	divne0d 11697	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑟 · 𝑇) / 3) ≠ 0)
353	351, 337, 352	div2negd 11696	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (-(𝑀 / 9) / -((𝑟 · 𝑇) / 3)) = ((𝑀 / 9) / ((𝑟 · 𝑇) / 3)))
354	344	oveq2d 7271	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (-(𝑀 / 9) / -((𝑟 · 𝑇) / 3)) = (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3))))
355	350, 353, 354	3eqtr2d 2784	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑀 / (𝑟 · 𝑇)) / 3) = (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3))))
356	344, 355	oveq12d 7273	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (-((𝑟 · 𝑇) / 3) − ((𝑀 / (𝑟 · 𝑇)) / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))))
357	336, 339, 356	3eqtrd 2782	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))))
358	357	eqeq2d 2749	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑋 + (𝐵 / 3)) = -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) ↔ (𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3))))))
359	332, 334, 358	3bitrrd 305	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))) ↔ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3)))
360	359	anassrs 467	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ 𝑟 ≠ 0) → ((𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))) ↔ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3)))
361	306, 360	sylan2 592	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ (𝑟↑3) = 1) → ((𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))) ↔ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3)))
362	361	pm5.32da 578	. . 3 ⊢ ((𝜑 ∧ 𝑟 ∈ ℂ) → (((𝑟↑3) = 1 ∧ (𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3))))) ↔ ((𝑟↑3) = 1 ∧ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3))))
363	362	rexbidva 3224	. 2 ⊢ (𝜑 → (∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ (𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3))))) ↔ ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3))))
364	163, 298, 363	3bitr3d 308	1 ⊢ (𝜑 → ((((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((𝐶 · 𝑋) + 𝐷)) = 0 ↔ ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 = wceq 1539 ∈ wcel 2108 ≠ wne 2942 ∃wrex 3064 class class class wbr 5070 (class class class)co 7255 ℂcc 10800 0cc0 10802 1c1 10803 + caddc 10805 · cmul 10807 − cmin 11135 -cneg 11136 / cdiv 11562 ℕcn 11903 2c2 11958 3c3 11959 4c4 11960 7c7 11963 9c9 11965 ℕ₀cn0 12163 cdc 12366 ↑cexp 13710 ∥ cdvds 15891

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879 ax-pre-sup 10880

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-om 7688 df-2nd 7805 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-er 8456 df-en 8692 df-dom 8693 df-sdom 8694 df-sup 9131 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-div 11563 df-nn 11904 df-2 11966 df-3 11967 df-4 11968 df-5 11969 df-6 11970 df-7 11971 df-8 11972 df-9 11973 df-n0 12164 df-z 12250 df-dec 12367 df-uz 12512 df-rp 12660 df-seq 13650 df-exp 13711 df-cj 14738 df-re 14739 df-im 14740 df-sqrt 14874 df-abs 14875 df-dvds 15892

This theorem is referenced by: cubic2 25903 quart 25916

W3C validator