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 25997

Description: Solutions to a monic cubic equation, a special case of cubic 25999. (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 13862	. . . . . . 7 ⊢ (𝜑 → (𝐵↑2) ∈ ℂ)
4		3cn 12054	. . . . . . . 8 ⊢ 3 ∈ ℂ
5		mcubic.c	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ ℂ)
6		mulcl 10955	. . . . . . . 8 ⊢ ((3 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (3 · 𝐶) ∈ ℂ)
7	4, 5, 6	sylancr 587	. . . . . . 7 ⊢ (𝜑 → (3 · 𝐶) ∈ ℂ)
8	3, 7	subcld 11332	. . . . . 6 ⊢ (𝜑 → ((𝐵↑2) − (3 · 𝐶)) ∈ ℂ)
9	1, 8	eqeltrd 2839	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ ℂ)
10	4	a1i 11	. . . . 5 ⊢ (𝜑 → 3 ∈ ℂ)
11		3ne0 12079	. . . . . 6 ⊢ 3 ≠ 0
12	11	a1i 11	. . . . 5 ⊢ (𝜑 → 3 ≠ 0)
13	9, 10, 12	divcld 11751	. . . 4 ⊢ (𝜑 → (𝑀 / 3) ∈ ℂ)
14	13	negcld 11319	. . 3 ⊢ (𝜑 → -(𝑀 / 3) ∈ ℂ)
15		mcubic.n	. . . . 5 ⊢ (𝜑 → 𝑁 = (((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) + (;27 · 𝐷)))
16		2cn 12048	. . . . . . . 8 ⊢ 2 ∈ ℂ
17		3nn0 12251	. . . . . . . . 9 ⊢ 3 ∈ ℕ₀
18		expcl 13800	. . . . . . . . 9 ⊢ ((𝐵 ∈ ℂ ∧ 3 ∈ ℕ₀) → (𝐵↑3) ∈ ℂ)
19	2, 17, 18	sylancl 586	. . . . . . . 8 ⊢ (𝜑 → (𝐵↑3) ∈ ℂ)
20		mulcl 10955	. . . . . . . 8 ⊢ ((2 ∈ ℂ ∧ (𝐵↑3) ∈ ℂ) → (2 · (𝐵↑3)) ∈ ℂ)
21	16, 19, 20	sylancr 587	. . . . . . 7 ⊢ (𝜑 → (2 · (𝐵↑3)) ∈ ℂ)
22		9cn 12073	. . . . . . . 8 ⊢ 9 ∈ ℂ
23	2, 5	mulcld 10995	. . . . . . . 8 ⊢ (𝜑 → (𝐵 · 𝐶) ∈ ℂ)
24		mulcl 10955	. . . . . . . 8 ⊢ ((9 ∈ ℂ ∧ (𝐵 · 𝐶) ∈ ℂ) → (9 · (𝐵 · 𝐶)) ∈ ℂ)
25	22, 23, 24	sylancr 587	. . . . . . 7 ⊢ (𝜑 → (9 · (𝐵 · 𝐶)) ∈ ℂ)
26	21, 25	subcld 11332	. . . . . 6 ⊢ (𝜑 → ((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) ∈ ℂ)
27		2nn0 12250	. . . . . . . . 9 ⊢ 2 ∈ ℕ₀
28		7nn 12065	. . . . . . . . 9 ⊢ 7 ∈ ℕ
29	27, 28	decnncl 12457	. . . . . . . 8 ⊢ ;27 ∈ ℕ
30	29	nncni 11983	. . . . . . 7 ⊢ ;27 ∈ ℂ
31		mcubic.d	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ ℂ)
32		mulcl 10955	. . . . . . 7 ⊢ ((;27 ∈ ℂ ∧ 𝐷 ∈ ℂ) → (;27 · 𝐷) ∈ ℂ)
33	30, 31, 32	sylancr 587	. . . . . 6 ⊢ (𝜑 → (;27 · 𝐷) ∈ ℂ)
34	26, 33	addcld 10994	. . . . 5 ⊢ (𝜑 → (((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) + (;27 · 𝐷)) ∈ ℂ)
35	15, 34	eqeltrd 2839	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ℂ)
36	30	a1i 11	. . . 4 ⊢ (𝜑 → ;27 ∈ ℂ)
37	29	nnne0i 12013	. . . . 5 ⊢ ;27 ≠ 0
38	37	a1i 11	. . . 4 ⊢ (𝜑 → ;27 ≠ 0)
39	35, 36, 38	divcld 11751	. . 3 ⊢ (𝜑 → (𝑁 / ;27) ∈ ℂ)
40		mcubic.x	. . . 4 ⊢ (𝜑 → 𝑋 ∈ ℂ)
41	2, 10, 12	divcld 11751	. . . 4 ⊢ (𝜑 → (𝐵 / 3) ∈ ℂ)
42	40, 41	addcld 10994	. . 3 ⊢ (𝜑 → (𝑋 + (𝐵 / 3)) ∈ ℂ)
43		mcubic.t	. . . . 5 ⊢ (𝜑 → 𝑇 ∈ ℂ)
44	43, 10, 12	divcld 11751	. . . 4 ⊢ (𝜑 → (𝑇 / 3) ∈ ℂ)
45	44	negcld 11319	. . 3 ⊢ (𝜑 → -(𝑇 / 3) ∈ ℂ)
46		3nn 12052	. . . . . 6 ⊢ 3 ∈ ℕ
47	46	a1i 11	. . . . 5 ⊢ (𝜑 → 3 ∈ ℕ)
48		n2dvds3 16080	. . . . . 6 ⊢ ¬ 2 ∥ 3
49	48	a1i 11	. . . . 5 ⊢ (𝜑 → ¬ 2 ∥ 3)
50		oexpneg 16054	. . . . 5 ⊢ (((𝑇 / 3) ∈ ℂ ∧ 3 ∈ ℕ ∧ ¬ 2 ∥ 3) → (-(𝑇 / 3)↑3) = -((𝑇 / 3)↑3))
51	44, 47, 49, 50	syl3anc 1370	. . . 4 ⊢ (𝜑 → (-(𝑇 / 3)↑3) = -((𝑇 / 3)↑3))
52	17	a1i 11	. . . . . . 7 ⊢ (𝜑 → 3 ∈ ℕ₀)
53	43, 10, 12, 52	expdivd 13878	. . . . . 6 ⊢ (𝜑 → ((𝑇 / 3)↑3) = ((𝑇↑3) / (3↑3)))
54		mcubic.3	. . . . . . 7 ⊢ (𝜑 → (𝑇↑3) = ((𝑁 + 𝐺) / 2))
55		3exp3 16793	. . . . . . . 8 ⊢ (3↑3) = ;27
56	55	a1i 11	. . . . . . 7 ⊢ (𝜑 → (3↑3) = ;27)
57	54, 56	oveq12d 7293	. . . . . 6 ⊢ (𝜑 → ((𝑇↑3) / (3↑3)) = (((𝑁 + 𝐺) / 2) / ;27))
58		mcubic.g	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 ∈ ℂ)
59	35, 58	addcld 10994	. . . . . . . 8 ⊢ (𝜑 → (𝑁 + 𝐺) ∈ ℂ)
60		2cnd 12051	. . . . . . . 8 ⊢ (𝜑 → 2 ∈ ℂ)
61		2ne0 12077	. . . . . . . . 9 ⊢ 2 ≠ 0
62	61	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 2 ≠ 0)
63	59, 60, 36, 62, 38	divdiv32d 11776	. . . . . . 7 ⊢ (𝜑 → (((𝑁 + 𝐺) / 2) / ;27) = (((𝑁 + 𝐺) / ;27) / 2))
64	35, 58	addcomd 11177	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 + 𝐺) = (𝐺 + 𝑁))
65	64	oveq1d 7290	. . . . . . . . 9 ⊢ (𝜑 → ((𝑁 + 𝐺) / ;27) = ((𝐺 + 𝑁) / ;27))
66	58, 35, 36, 38	divdird 11789	. . . . . . . . 9 ⊢ (𝜑 → ((𝐺 + 𝑁) / ;27) = ((𝐺 / ;27) + (𝑁 / ;27)))
67	65, 66	eqtrd 2778	. . . . . . . 8 ⊢ (𝜑 → ((𝑁 + 𝐺) / ;27) = ((𝐺 / ;27) + (𝑁 / ;27)))
68	67	oveq1d 7290	. . . . . . 7 ⊢ (𝜑 → (((𝑁 + 𝐺) / ;27) / 2) = (((𝐺 / ;27) + (𝑁 / ;27)) / 2))
69	58, 36, 38	divcld 11751	. . . . . . . 8 ⊢ (𝜑 → (𝐺 / ;27) ∈ ℂ)
70	69, 39, 60, 62	divdird 11789	. . . . . . 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 11215	. . . 4 ⊢ (𝜑 → -((𝑇 / 3)↑3) = -(((𝐺 / ;27) / 2) + ((𝑁 / ;27) / 2)))
74	69	halfcld 12218	. . . . 5 ⊢ (𝜑 → ((𝐺 / ;27) / 2) ∈ ℂ)
75	39	halfcld 12218	. . . . 5 ⊢ (𝜑 → ((𝑁 / ;27) / 2) ∈ ℂ)
76	74, 75	negdi2d 11346	. . . 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 11319	. . 3 ⊢ (𝜑 → -((𝐺 / ;27) / 2) ∈ ℂ)
79		sqneg 13836	. . . . 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 13877	. . . 4 ⊢ (𝜑 → (((𝐺 / ;27) / 2)↑2) = (((𝐺 / ;27)↑2) / (2↑2)))
82	39, 60, 62	sqdivd 13877	. . . . . . . 8 ⊢ (𝜑 → (((𝑁 / ;27) / 2)↑2) = (((𝑁 / ;27)↑2) / (2↑2)))
83	35, 36, 38	sqdivd 13877	. . . . . . . . 9 ⊢ (𝜑 → ((𝑁 / ;27)↑2) = ((𝑁↑2) / (;27↑2)))
84	83	oveq1d 7290	. . . . . . . 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 12058	. . . . . . . . . . . 12 ⊢ 4 ∈ ℂ
87	86	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 4 ∈ ℂ)
88		expcl 13800	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℂ ∧ 3 ∈ ℕ₀) → (𝑀↑3) ∈ ℂ)
89	9, 17, 88	sylancl 586	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀↑3) ∈ ℂ)
90	30	sqcli 13898	. . . . . . . . . . . 12 ⊢ (;27↑2) ∈ ℂ
91	90	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (;27↑2) ∈ ℂ)
92		sqne0 13843	. . . . . . . . . . . . 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 11786	. . . . . . . . . 10 ⊢ (𝜑 → ((4 · (𝑀↑3)) / (;27↑2)) = (4 · ((𝑀↑3) / (;27↑2))))
96	22	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 9 ∈ ℂ)
97		9nn 12071	. . . . . . . . . . . . . . 15 ⊢ 9 ∈ ℕ
98	97	nnne0i 12013	. . . . . . . . . . . . . 14 ⊢ 9 ≠ 0
99	98	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 9 ≠ 0)
100	9, 96, 99, 52	expdivd 13878	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑀 / 9)↑3) = ((𝑀↑3) / (9↑3)))
101	16, 4	mulcomi 10983	. . . . . . . . . . . . . . . 16 ⊢ (2 · 3) = (3 · 2)
102	101	oveq2i 7286	. . . . . . . . . . . . . . 15 ⊢ (3↑(2 · 3)) = (3↑(3 · 2))
103		expmul 13828	. . . . . . . . . . . . . . . 16 ⊢ ((3 ∈ ℂ ∧ 2 ∈ ℕ₀ ∧ 3 ∈ ℕ₀) → (3↑(2 · 3)) = ((3↑2)↑3))
104	4, 27, 17, 103	mp3an 1460	. . . . . . . . . . . . . . 15 ⊢ (3↑(2 · 3)) = ((3↑2)↑3)
105		expmul 13828	. . . . . . . . . . . . . . . 16 ⊢ ((3 ∈ ℂ ∧ 3 ∈ ℕ₀ ∧ 2 ∈ ℕ₀) → (3↑(3 · 2)) = ((3↑3)↑2))
106	4, 17, 27, 105	mp3an 1460	. . . . . . . . . . . . . . 15 ⊢ (3↑(3 · 2)) = ((3↑3)↑2)
107	102, 104, 106	3eqtr3i 2774	. . . . . . . . . . . . . 14 ⊢ ((3↑2)↑3) = ((3↑3)↑2)
108		sq3 13915	. . . . . . . . . . . . . . 15 ⊢ (3↑2) = 9
109	108	oveq1i 7285	. . . . . . . . . . . . . 14 ⊢ ((3↑2)↑3) = (9↑3)
110	55	oveq1i 7285	. . . . . . . . . . . . . 14 ⊢ ((3↑3)↑2) = (;27↑2)
111	107, 109, 110	3eqtr3i 2774	. . . . . . . . . . . . 13 ⊢ (9↑3) = (;27↑2)
112	111	oveq2i 7286	. . . . . . . . . . . 12 ⊢ ((𝑀↑3) / (9↑3)) = ((𝑀↑3) / (;27↑2))
113	100, 112	eqtrdi 2794	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑀 / 9)↑3) = ((𝑀↑3) / (;27↑2)))
114	113	oveq2d 7291	. . . . . . . . . 10 ⊢ (𝜑 → (4 · ((𝑀 / 9)↑3)) = (4 · ((𝑀↑3) / (;27↑2))))
115	95, 114	eqtr4d 2781	. . . . . . . . 9 ⊢ (𝜑 → ((4 · (𝑀↑3)) / (;27↑2)) = (4 · ((𝑀 / 9)↑3)))
116	115	oveq1d 7290	. . . . . . . 8 ⊢ (𝜑 → (((4 · (𝑀↑3)) / (;27↑2)) / (2↑2)) = ((4 · ((𝑀 / 9)↑3)) / (2↑2)))
117		sq2 13914	. . . . . . . . . 10 ⊢ (2↑2) = 4
118	117	oveq2i 7286	. . . . . . . . 9 ⊢ ((4 · ((𝑀 / 9)↑3)) / (2↑2)) = ((4 · ((𝑀 / 9)↑3)) / 4)
119	9, 96, 99	divcld 11751	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀 / 9) ∈ ℂ)
120		expcl 13800	. . . . . . . . . . 11 ⊢ (((𝑀 / 9) ∈ ℂ ∧ 3 ∈ ℕ₀) → ((𝑀 / 9)↑3) ∈ ℂ)
121	119, 17, 120	sylancl 586	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑀 / 9)↑3) ∈ ℂ)
122		4ne0 12081	. . . . . . . . . . 11 ⊢ 4 ≠ 0
123	122	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 4 ≠ 0)
124	121, 87, 123	divcan3d 11756	. . . . . . . . 9 ⊢ (𝜑 → ((4 · ((𝑀 / 9)↑3)) / 4) = ((𝑀 / 9)↑3))
125	118, 124	eqtrid 2790	. . . . . . . 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 7293	. . . . . 6 ⊢ (𝜑 → ((((𝑁↑2) / (;27↑2)) / (2↑2)) − (((4 · (𝑀↑3)) / (;27↑2)) / (2↑2))) = ((((𝑁 / ;27) / 2)↑2) − ((𝑀 / 9)↑3)))
128	35	sqcld 13862	. . . . . . . 8 ⊢ (𝜑 → (𝑁↑2) ∈ ℂ)
129	128, 91, 94	divcld 11751	. . . . . . 7 ⊢ (𝜑 → ((𝑁↑2) / (;27↑2)) ∈ ℂ)
130		mulcl 10955	. . . . . . . . 9 ⊢ ((4 ∈ ℂ ∧ (𝑀↑3) ∈ ℂ) → (4 · (𝑀↑3)) ∈ ℂ)
131	86, 89, 130	sylancr 587	. . . . . . . 8 ⊢ (𝜑 → (4 · (𝑀↑3)) ∈ ℂ)
132	131, 91, 94	divcld 11751	. . . . . . 7 ⊢ (𝜑 → ((4 · (𝑀↑3)) / (;27↑2)) ∈ ℂ)
133	16	sqcli 13898	. . . . . . . 8 ⊢ (2↑2) ∈ ℂ
134	133	a1i 11	. . . . . . 7 ⊢ (𝜑 → (2↑2) ∈ ℂ)
135	117, 122	eqnetri 3014	. . . . . . . 8 ⊢ (2↑2) ≠ 0
136	135	a1i 11	. . . . . . 7 ⊢ (𝜑 → (2↑2) ≠ 0)
137	129, 132, 134, 136	divsubdird 11790	. . . . . 6 ⊢ (𝜑 → ((((𝑁↑2) / (;27↑2)) − ((4 · (𝑀↑3)) / (;27↑2))) / (2↑2)) = ((((𝑁↑2) / (;27↑2)) / (2↑2)) − (((4 · (𝑀↑3)) / (;27↑2)) / (2↑2))))
138	75	sqcld 13862	. . . . . . 7 ⊢ (𝜑 → (((𝑁 / ;27) / 2)↑2) ∈ ℂ)
139	138, 121	negsubd 11338	. . . . . 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 13877	. . . . . . 7 ⊢ (𝜑 → ((𝐺 / ;27)↑2) = ((𝐺↑2) / (;27↑2)))
142		mcubic.2	. . . . . . . 8 ⊢ (𝜑 → (𝐺↑2) = ((𝑁↑2) − (4 · (𝑀↑3))))
143	142	oveq1d 7290	. . . . . . 7 ⊢ (𝜑 → ((𝐺↑2) / (;27↑2)) = (((𝑁↑2) − (4 · (𝑀↑3))) / (;27↑2)))
144	128, 131, 91, 94	divsubdird 11790	. . . . . . 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 7290	. . . . 5 ⊢ (𝜑 → (((𝐺 / ;27)↑2) / (2↑2)) = ((((𝑁↑2) / (;27↑2)) − ((4 · (𝑀↑3)) / (;27↑2))) / (2↑2)))
147		oexpneg 16054	. . . . . . 7 ⊢ (((𝑀 / 9) ∈ ℂ ∧ 3 ∈ ℕ ∧ ¬ 2 ∥ 3) → (-(𝑀 / 9)↑3) = -((𝑀 / 9)↑3))
148	119, 47, 49, 147	syl3anc 1370	. . . . . 6 ⊢ (𝜑 → (-(𝑀 / 9)↑3) = -((𝑀 / 9)↑3))
149	148	oveq2d 7291	. . . . 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 11782	. . . . . 6 ⊢ (𝜑 → ((𝑀 / 3) / 3) = (𝑀 / (3 · 3)))
153		3t3e9 12140	. . . . . . 7 ⊢ (3 · 3) = 9
154	153	oveq2i 7286	. . . . . 6 ⊢ (𝑀 / (3 · 3)) = (𝑀 / 9)
155	152, 154	eqtrdi 2794	. . . . 5 ⊢ (𝜑 → ((𝑀 / 3) / 3) = (𝑀 / 9))
156	155	negeqd 11215	. . . 4 ⊢ (𝜑 → -((𝑀 / 3) / 3) = -(𝑀 / 9))
157	13, 10, 12	divnegd 11764	. . . 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 11767	. . . 4 ⊢ (𝜑 → (𝑇 / 3) ≠ 0)
162	44, 161	negne0d 11330	. . 3 ⊢ (𝜑 → -(𝑇 / 3) ≠ 0)
163	14, 39, 42, 45, 77, 78, 151, 158, 159, 162	dcubic 25996	. 2 ⊢ (𝜑 → ((((𝑋 + (𝐵 / 3))↑3) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27))) = 0 ↔ ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ (𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))))))
164		binom3 13939	. . . . . . 7 ⊢ ((𝑋 ∈ ℂ ∧ (𝐵 / 3) ∈ ℂ) → ((𝑋 + (𝐵 / 3))↑3) = (((𝑋↑3) + (3 · ((𝑋↑2) · (𝐵 / 3)))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))))
165	40, 41, 164	syl2anc 584	. . . . . 6 ⊢ (𝜑 → ((𝑋 + (𝐵 / 3))↑3) = (((𝑋↑3) + (3 · ((𝑋↑2) · (𝐵 / 3)))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))))
166	40	sqcld 13862	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋↑2) ∈ ℂ)
167	10, 166, 41	mul12d 11184	. . . . . . . . 9 ⊢ (𝜑 → (3 · ((𝑋↑2) · (𝐵 / 3))) = ((𝑋↑2) · (3 · (𝐵 / 3))))
168	2, 10, 12	divcan2d 11753	. . . . . . . . . 10 ⊢ (𝜑 → (3 · (𝐵 / 3)) = 𝐵)
169	168	oveq2d 7291	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋↑2) · (3 · (𝐵 / 3))) = ((𝑋↑2) · 𝐵))
170	166, 2	mulcomd 10996	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋↑2) · 𝐵) = (𝐵 · (𝑋↑2)))
171	167, 169, 170	3eqtrd 2782	. . . . . . . 8 ⊢ (𝜑 → (3 · ((𝑋↑2) · (𝐵 / 3))) = (𝐵 · (𝑋↑2)))
172	171	oveq2d 7291	. . . . . . 7 ⊢ (𝜑 → ((𝑋↑3) + (3 · ((𝑋↑2) · (𝐵 / 3)))) = ((𝑋↑3) + (𝐵 · (𝑋↑2))))
173	172	oveq1d 7290	. . . . . 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 7290	. . . 4 ⊢ (𝜑 → (((𝑋 + (𝐵 / 3))↑3) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27))) = ((((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27))))
176		expcl 13800	. . . . . . 7 ⊢ ((𝑋 ∈ ℂ ∧ 3 ∈ ℕ₀) → (𝑋↑3) ∈ ℂ)
177	40, 17, 176	sylancl 586	. . . . . 6 ⊢ (𝜑 → (𝑋↑3) ∈ ℂ)
178	2, 166	mulcld 10995	. . . . . 6 ⊢ (𝜑 → (𝐵 · (𝑋↑2)) ∈ ℂ)
179	177, 178	addcld 10994	. . . . 5 ⊢ (𝜑 → ((𝑋↑3) + (𝐵 · (𝑋↑2))) ∈ ℂ)
180	41	sqcld 13862	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 / 3)↑2) ∈ ℂ)
181	40, 180	mulcld 10995	. . . . . . 7 ⊢ (𝜑 → (𝑋 · ((𝐵 / 3)↑2)) ∈ ℂ)
182	10, 181	mulcld 10995	. . . . . 6 ⊢ (𝜑 → (3 · (𝑋 · ((𝐵 / 3)↑2))) ∈ ℂ)
183		expcl 13800	. . . . . . 7 ⊢ (((𝐵 / 3) ∈ ℂ ∧ 3 ∈ ℕ₀) → ((𝐵 / 3)↑3) ∈ ℂ)
184	41, 17, 183	sylancl 586	. . . . . 6 ⊢ (𝜑 → ((𝐵 / 3)↑3) ∈ ℂ)
185	182, 184	addcld 10994	. . . . 5 ⊢ (𝜑 → ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) ∈ ℂ)
186	14, 42	mulcld 10995	. . . . . 6 ⊢ (𝜑 → (-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) ∈ ℂ)
187	186, 39	addcld 10994	. . . . 5 ⊢ (𝜑 → ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27)) ∈ ℂ)
188	179, 185, 187	addassd 10997	. . . 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 10999	. . . . . . . . . 10 ⊢ (𝜑 → (-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) = ((-(𝑀 / 3) · 𝑋) + (-(𝑀 / 3) · (𝐵 / 3))))
190	189	oveq1d 7290	. . . . . . . . 9 ⊢ (𝜑 → ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27)) = (((-(𝑀 / 3) · 𝑋) + (-(𝑀 / 3) · (𝐵 / 3))) + (𝑁 / ;27)))
191	14, 40	mulcld 10995	. . . . . . . . . 10 ⊢ (𝜑 → (-(𝑀 / 3) · 𝑋) ∈ ℂ)
192	14, 41	mulcld 10995	. . . . . . . . . 10 ⊢ (𝜑 → (-(𝑀 / 3) · (𝐵 / 3)) ∈ ℂ)
193	191, 192, 39	addassd 10997	. . . . . . . . 9 ⊢ (𝜑 → (((-(𝑀 / 3) · 𝑋) + (-(𝑀 / 3) · (𝐵 / 3))) + (𝑁 / ;27)) = ((-(𝑀 / 3) · 𝑋) + ((-(𝑀 / 3) · (𝐵 / 3)) + (𝑁 / ;27))))
194	1	oveq1d 7290	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀 / 3) = (((𝐵↑2) − (3 · 𝐶)) / 3))
195	3, 7, 10, 12	divsubdird 11790	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐵↑2) − (3 · 𝐶)) / 3) = (((𝐵↑2) / 3) − ((3 · 𝐶) / 3)))
196	5, 10, 12	divcan3d 11756	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((3 · 𝐶) / 3) = 𝐶)
197	196	oveq2d 7291	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐵↑2) / 3) − ((3 · 𝐶) / 3)) = (((𝐵↑2) / 3) − 𝐶))
198	194, 195, 197	3eqtrd 2782	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀 / 3) = (((𝐵↑2) / 3) − 𝐶))
199	198	negeqd 11215	. . . . . . . . . . . . 13 ⊢ (𝜑 → -(𝑀 / 3) = -(((𝐵↑2) / 3) − 𝐶))
200	3, 10, 12	divcld 11751	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵↑2) / 3) ∈ ℂ)
201	200, 5	negsubdi2d 11348	. . . . . . . . . . . . 13 ⊢ (𝜑 → -(((𝐵↑2) / 3) − 𝐶) = (𝐶 − ((𝐵↑2) / 3)))
202	199, 201	eqtrd 2778	. . . . . . . . . . . 12 ⊢ (𝜑 → -(𝑀 / 3) = (𝐶 − ((𝐵↑2) / 3)))
203	202	oveq1d 7290	. . . . . . . . . . 11 ⊢ (𝜑 → (-(𝑀 / 3) · 𝑋) = ((𝐶 − ((𝐵↑2) / 3)) · 𝑋))
204	5, 200, 40	subdird 11432	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐶 − ((𝐵↑2) / 3)) · 𝑋) = ((𝐶 · 𝑋) − (((𝐵↑2) / 3) · 𝑋)))
205	200, 40	mulcomd 10996	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐵↑2) / 3) · 𝑋) = (𝑋 · ((𝐵↑2) / 3)))
206	4	sqvali 13897	. . . . . . . . . . . . . . . . . 18 ⊢ (3↑2) = (3 · 3)
207	206	oveq2i 7286	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵↑2) / (3↑2)) = ((𝐵↑2) / (3 · 3))
208	2, 10, 12	sqdivd 13877	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐵 / 3)↑2) = ((𝐵↑2) / (3↑2)))
209	3, 10, 10, 12, 12	divdiv1d 11782	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝐵↑2) / 3) / 3) = ((𝐵↑2) / (3 · 3)))
210	207, 208, 209	3eqtr4a 2804	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐵 / 3)↑2) = (((𝐵↑2) / 3) / 3))
211	210	oveq2d 7291	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (3 · ((𝐵 / 3)↑2)) = (3 · (((𝐵↑2) / 3) / 3)))
212	200, 10, 12	divcan2d 11753	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (3 · (((𝐵↑2) / 3) / 3)) = ((𝐵↑2) / 3))
213	211, 212	eqtrd 2778	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (3 · ((𝐵 / 3)↑2)) = ((𝐵↑2) / 3))
214	213	oveq2d 7291	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 · (3 · ((𝐵 / 3)↑2))) = (𝑋 · ((𝐵↑2) / 3)))
215	40, 10, 180	mul12d 11184	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 · (3 · ((𝐵 / 3)↑2))) = (3 · (𝑋 · ((𝐵 / 3)↑2))))
216	205, 214, 215	3eqtr2d 2784	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐵↑2) / 3) · 𝑋) = (3 · (𝑋 · ((𝐵 / 3)↑2))))
217	216	oveq2d 7291	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐶 · 𝑋) − (((𝐵↑2) / 3) · 𝑋)) = ((𝐶 · 𝑋) − (3 · (𝑋 · ((𝐵 / 3)↑2)))))
218	203, 204, 217	3eqtrd 2782	. . . . . . . . . 10 ⊢ (𝜑 → (-(𝑀 / 3) · 𝑋) = ((𝐶 · 𝑋) − (3 · (𝑋 · ((𝐵 / 3)↑2)))))
219	202	oveq1d 7290	. . . . . . . . . . . . 13 ⊢ (𝜑 → (-(𝑀 / 3) · (𝐵 / 3)) = ((𝐶 − ((𝐵↑2) / 3)) · (𝐵 / 3)))
220	5, 200, 41	subdird 11432	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐶 − ((𝐵↑2) / 3)) · (𝐵 / 3)) = ((𝐶 · (𝐵 / 3)) − (((𝐵↑2) / 3) · (𝐵 / 3))))
221	5, 2, 10, 12	divassd 11786	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐶 · 𝐵) / 3) = (𝐶 · (𝐵 / 3)))
222	5, 2	mulcomd 10996	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐶 · 𝐵) = (𝐵 · 𝐶))
223	222	oveq1d 7290	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐶 · 𝐵) / 3) = ((𝐵 · 𝐶) / 3))
224	221, 223	eqtr3d 2780	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐶 · (𝐵 / 3)) = ((𝐵 · 𝐶) / 3))
225	3, 10, 2, 10, 12, 12	divmuldivd 11792	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐵↑2) / 3) · (𝐵 / 3)) = (((𝐵↑2) · 𝐵) / (3 · 3)))
226		df-3 12037	. . . . . . . . . . . . . . . . . 18 ⊢ 3 = (2 + 1)
227	226	oveq2i 7286	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵↑3) = (𝐵↑(2 + 1))
228		expp1 13789	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ∈ ℂ ∧ 2 ∈ ℕ₀) → (𝐵↑(2 + 1)) = ((𝐵↑2) · 𝐵))
229	2, 27, 228	sylancl 586	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵↑(2 + 1)) = ((𝐵↑2) · 𝐵))
230	227, 229	eqtr2id 2791	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐵↑2) · 𝐵) = (𝐵↑3))
231	153	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (3 · 3) = 9)
232	230, 231	oveq12d 7293	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐵↑2) · 𝐵) / (3 · 3)) = ((𝐵↑3) / 9))
233	225, 232	eqtrd 2778	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐵↑2) / 3) · (𝐵 / 3)) = ((𝐵↑3) / 9))
234	224, 233	oveq12d 7293	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐶 · (𝐵 / 3)) − (((𝐵↑2) / 3) · (𝐵 / 3))) = (((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)))
235	219, 220, 234	3eqtrd 2782	. . . . . . . . . . . 12 ⊢ (𝜑 → (-(𝑀 / 3) · (𝐵 / 3)) = (((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)))
236	15	oveq1d 7290	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 / ;27) = ((((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) + (;27 · 𝐷)) / ;27))
237	26, 33, 36, 38	divdird 11789	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) + (;27 · 𝐷)) / ;27) = ((((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) / ;27) + ((;27 · 𝐷) / ;27)))
238	21, 25, 36, 38	divsubdird 11790	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) / ;27) = (((2 · (𝐵↑3)) / ;27) − ((9 · (𝐵 · 𝐶)) / ;27)))
239		9t3e27 12560	. . . . . . . . . . . . . . . . . 18 ⊢ (9 · 3) = ;27
240	239	oveq2i 7286	. . . . . . . . . . . . . . . . 17 ⊢ ((9 · (𝐵 · 𝐶)) / (9 · 3)) = ((9 · (𝐵 · 𝐶)) / ;27)
241	23, 10, 96, 12, 99	divcan5d 11777	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((9 · (𝐵 · 𝐶)) / (9 · 3)) = ((𝐵 · 𝐶) / 3))
242	240, 241	eqtr3id 2792	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((9 · (𝐵 · 𝐶)) / ;27) = ((𝐵 · 𝐶) / 3))
243	242	oveq2d 7291	. . . . . . . . . . . . . . 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 11756	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((;27 · 𝐷) / ;27) = 𝐷)
246	244, 245	oveq12d 7293	. . . . . . . . . . . . 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 7293	. . . . . . . . . . 11 ⊢ (𝜑 → ((-(𝑀 / 3) · (𝐵 / 3)) + (𝑁 / ;27)) = ((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + ((((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3)) + 𝐷)))
249	19, 96, 99	divcld 11751	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐵↑3) / 9) ∈ ℂ)
250	21, 36, 38	divcld 11751	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((2 · (𝐵↑3)) / ;27) ∈ ℂ)
251	249, 250	negsubdi2d 11348	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -(((𝐵↑3) / 9) − ((2 · (𝐵↑3)) / ;27)) = (((2 · (𝐵↑3)) / ;27) − ((𝐵↑3) / 9)))
252	2, 10, 12, 52	expdivd 13878	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐵 / 3)↑3) = ((𝐵↑3) / (3↑3)))
253	55	oveq2i 7286	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵↑3) / (3↑3)) = ((𝐵↑3) / ;27)
254		ax-1cn 10929	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 ∈ ℂ
255		2p1e3 12115	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (2 + 1) = 3
256	4, 16, 254, 255	subaddrii 11310	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (3 − 2) = 1
257	256	oveq1i 7285	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((3 − 2) · (𝐵↑3)) = (1 · (𝐵↑3))
258	19	mulid2d 10993	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (1 · (𝐵↑3)) = (𝐵↑3))
259	257, 258	eqtrid 2790	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((3 − 2) · (𝐵↑3)) = (𝐵↑3))
260	10, 60, 19	subdird 11432	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((3 − 2) · (𝐵↑3)) = ((3 · (𝐵↑3)) − (2 · (𝐵↑3))))
261	259, 260	eqtr3d 2780	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐵↑3) = ((3 · (𝐵↑3)) − (2 · (𝐵↑3))))
262	261	oveq1d 7290	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐵↑3) / ;27) = (((3 · (𝐵↑3)) − (2 · (𝐵↑3))) / ;27))
263		mulcl 10955	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((3 ∈ ℂ ∧ (𝐵↑3) ∈ ℂ) → (3 · (𝐵↑3)) ∈ ℂ)
264	4, 19, 263	sylancr 587	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (3 · (𝐵↑3)) ∈ ℂ)
265	264, 21, 36, 38	divsubdird 11790	. . . . . . . . . . . . . . . . . 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	eqtrid 2790	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐵↑3) / (3↑3)) = (((3 · (𝐵↑3)) / ;27) − ((2 · (𝐵↑3)) / ;27)))
268	22, 4, 239	mulcomli 10984	. . . . . . . . . . . . . . . . . . 19 ⊢ (3 · 9) = ;27
269	268	oveq2i 7286	. . . . . . . . . . . . . . . . . 18 ⊢ ((3 · (𝐵↑3)) / (3 · 9)) = ((3 · (𝐵↑3)) / ;27)
270	19, 96, 10, 99, 12	divcan5d 11777	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((3 · (𝐵↑3)) / (3 · 9)) = ((𝐵↑3) / 9))
271	269, 270	eqtr3id 2792	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((3 · (𝐵↑3)) / ;27) = ((𝐵↑3) / 9))
272	271	oveq1d 7290	. . . . . . . . . . . . . . . 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 11215	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -((𝐵 / 3)↑3) = -(((𝐵↑3) / 9) − ((2 · (𝐵↑3)) / ;27)))
275	23, 10, 12	divcld 11751	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐵 · 𝐶) / 3) ∈ ℂ)
276	275, 249, 250	npncan3d 11368	. . . . . . . . . . . . . 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 7290	. . . . . . . . . . . 12 ⊢ (𝜑 → (-((𝐵 / 3)↑3) + 𝐷) = (((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + (((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3))) + 𝐷))
279	184	negcld 11319	. . . . . . . . . . . . 13 ⊢ (𝜑 → -((𝐵 / 3)↑3) ∈ ℂ)
280	279, 31	addcomd 11177	. . . . . . . . . . . 12 ⊢ (𝜑 → (-((𝐵 / 3)↑3) + 𝐷) = (𝐷 + -((𝐵 / 3)↑3)))
281	235, 192	eqeltrrd 2840	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) ∈ ℂ)
282	250, 275	subcld 11332	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3)) ∈ ℂ)
283	281, 282, 31	addassd 10997	. . . . . . . . . . . 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 11338	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐷 + -((𝐵 / 3)↑3)) = (𝐷 − ((𝐵 / 3)↑3)))
286	248, 284, 285	3eqtr2d 2784	. . . . . . . . . 10 ⊢ (𝜑 → ((-(𝑀 / 3) · (𝐵 / 3)) + (𝑁 / ;27)) = (𝐷 − ((𝐵 / 3)↑3)))
287	218, 286	oveq12d 7293	. . . . . . . . 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 10995	. . . . . . . . 9 ⊢ (𝜑 → (𝐶 · 𝑋) ∈ ℂ)
290	289, 31, 182, 184	addsub4d 11379	. . . . . . . 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 7291	. . . . . 6 ⊢ (𝜑 → (((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27))) = (((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) + (((𝐶 · 𝑋) + 𝐷) − ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)))))
293	289, 31	addcld 10994	. . . . . . 7 ⊢ (𝜑 → ((𝐶 · 𝑋) + 𝐷) ∈ ℂ)
294	185, 293	pncan3d 11335	. . . . . 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 7291	. . . 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 7282	. . . . . . . 8 ⊢ (𝑟 = 0 → (𝑟↑3) = (0↑3))
300		0exp 13818	. . . . . . . . 9 ⊢ (3 ∈ ℕ → (0↑3) = 0)
301	46, 300	ax-mp 5	. . . . . . . 8 ⊢ (0↑3) = 0
302	299, 301	eqtrdi 2794	. . . . . . 7 ⊢ (𝑟 = 0 → (𝑟↑3) = 0)
303		0ne1 12044	. . . . . . . 8 ⊢ 0 ≠ 1
304	303	a1i 11	. . . . . . 7 ⊢ (𝑟 = 0 → 0 ≠ 1)
305	302, 304	eqnetrd 3011	. . . . . 6 ⊢ (𝑟 = 0 → (𝑟↑3) ≠ 1)
306	305	necon2i 2978	. . . . 5 ⊢ ((𝑟↑3) = 1 → 𝑟 ≠ 0)
307		eqcom 2745	. . . . . . . 8 ⊢ (𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) ↔ -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = 𝑋)
308	2	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝐵 ∈ ℂ)
309		simprl 768	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑟 ∈ ℂ)
310	43	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑇 ∈ ℂ)
311	309, 310	mulcld 10995	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑟 · 𝑇) ∈ ℂ)
312	9	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑀 ∈ ℂ)
313		simprr 770	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑟 ≠ 0)
314	160	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑇 ≠ 0)
315	309, 310, 313, 314	mulne0d 11627	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑟 · 𝑇) ≠ 0)
316	312, 311, 315	divcld 11751	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑀 / (𝑟 · 𝑇)) ∈ ℂ)
317	311, 316	addcld 10994	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) ∈ ℂ)
318	4	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 3 ∈ ℂ)
319	11	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 3 ≠ 0)
320	308, 317, 318, 319	divdird 11789	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝐵 + ((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇)))) / 3) = ((𝐵 / 3) + (((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)))
321	308, 311, 316	addassd 10997	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) = (𝐵 + ((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇)))))
322	321	oveq1d 7290	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = ((𝐵 + ((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇)))) / 3))
323	41	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝐵 / 3) ∈ ℂ)
324	317, 318, 319	divcld 11751	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) ∈ ℂ)
325	323, 324	subnegd 11339	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝐵 / 3) − -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)) = ((𝐵 / 3) + (((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)))
326	320, 322, 325	3eqtr4d 2788	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = ((𝐵 / 3) − -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)))
327	326	negeqd 11215	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = -((𝐵 / 3) − -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)))
328	324	negcld 11319	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) ∈ ℂ)
329	323, 328	negsubdi2d 11348	. . . . . . . . . 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	bitrid 282	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) ↔ (-(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) − (𝐵 / 3)) = 𝑋))
333	40	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑋 ∈ ℂ)
334	328, 323, 333	subadd2d 11351	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((-(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) − (𝐵 / 3)) = 𝑋 ↔ (𝑋 + (𝐵 / 3)) = -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)))
335	311, 316, 318, 319	divdird 11789	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) = (((𝑟 · 𝑇) / 3) + ((𝑀 / (𝑟 · 𝑇)) / 3)))
336	335	negeqd 11215	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) = -(((𝑟 · 𝑇) / 3) + ((𝑀 / (𝑟 · 𝑇)) / 3)))
337	311, 318, 319	divcld 11751	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑟 · 𝑇) / 3) ∈ ℂ)
338	316, 318, 319	divcld 11751	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑀 / (𝑟 · 𝑇)) / 3) ∈ ℂ)
339	337, 338	negdi2d 11346	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝑟 · 𝑇) / 3) + ((𝑀 / (𝑟 · 𝑇)) / 3)) = (-((𝑟 · 𝑇) / 3) − ((𝑀 / (𝑟 · 𝑇)) / 3)))
340	309, 310, 318, 319	divassd 11786	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑟 · 𝑇) / 3) = (𝑟 · (𝑇 / 3)))
341	340	negeqd 11215	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -((𝑟 · 𝑇) / 3) = -(𝑟 · (𝑇 / 3)))
342	44	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑇 / 3) ∈ ℂ)
343	309, 342	mulneg2d 11429	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑟 · -(𝑇 / 3)) = -(𝑟 · (𝑇 / 3)))
344	341, 343	eqtr4d 2781	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -((𝑟 · 𝑇) / 3) = (𝑟 · -(𝑇 / 3)))
345	312, 311, 318, 315, 319	divdiv32d 11776	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑀 / (𝑟 · 𝑇)) / 3) = ((𝑀 / 3) / (𝑟 · 𝑇)))
346	13	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑀 / 3) ∈ ℂ)
347	346, 311, 318, 315, 319	divcan7d 11779	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝑀 / 3) / 3) / ((𝑟 · 𝑇) / 3)) = ((𝑀 / 3) / (𝑟 · 𝑇)))
348	155	oveq1d 7290	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑀 / 3) / 3) / ((𝑟 · 𝑇) / 3)) = ((𝑀 / 9) / ((𝑟 · 𝑇) / 3)))
349	348	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝑀 / 3) / 3) / ((𝑟 · 𝑇) / 3)) = ((𝑀 / 9) / ((𝑟 · 𝑇) / 3)))
350	345, 347, 349	3eqtr2d 2784	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑀 / (𝑟 · 𝑇)) / 3) = ((𝑀 / 9) / ((𝑟 · 𝑇) / 3)))
351	119	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑀 / 9) ∈ ℂ)
352	311, 318, 315, 319	divne0d 11767	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑟 · 𝑇) / 3) ≠ 0)
353	351, 337, 352	div2negd 11766	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (-(𝑀 / 9) / -((𝑟 · 𝑇) / 3)) = ((𝑀 / 9) / ((𝑟 · 𝑇) / 3)))
354	344	oveq2d 7291	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (-(𝑀 / 9) / -((𝑟 · 𝑇) / 3)) = (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3))))
355	350, 353, 354	3eqtr2d 2784	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑀 / (𝑟 · 𝑇)) / 3) = (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3))))
356	344, 355	oveq12d 7293	. . . . . . . . 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 306	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))) ↔ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3)))
360	359	anassrs 468	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ 𝑟 ≠ 0) → ((𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))) ↔ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3)))
361	306, 360	sylan2 593	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ (𝑟↑3) = 1) → ((𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))) ↔ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3)))
362	361	pm5.32da 579	. . 3 ⊢ ((𝜑 ∧ 𝑟 ∈ ℂ) → (((𝑟↑3) = 1 ∧ (𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3))))) ↔ ((𝑟↑3) = 1 ∧ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3))))
363	362	rexbidva 3225	. 2 ⊢ (𝜑 → (∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ (𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3))))) ↔ ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3))))
364	163, 298, 363	3bitr3d 309	1 ⊢ (𝜑 → ((((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((𝐶 · 𝑋) + 𝐷)) = 0 ↔ ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1539 ∈ wcel 2106 ≠ wne 2943 ∃wrex 3065 class class class wbr 5074 (class class class)co 7275 ℂcc 10869 0cc0 10871 1c1 10872 + caddc 10874 · cmul 10876 − cmin 11205 -cneg 11206 / cdiv 11632 ℕcn 11973 2c2 12028 3c3 12029 4c4 12030 7c7 12033 9c9 12035 ℕ₀cn0 12233 cdc 12437 ↑cexp 13782 ∥ cdvds 15963

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 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 2709 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588 ax-cnex 10927 ax-resscn 10928 ax-1cn 10929 ax-icn 10930 ax-addcl 10931 ax-addrcl 10932 ax-mulcl 10933 ax-mulrcl 10934 ax-mulcom 10935 ax-addass 10936 ax-mulass 10937 ax-distr 10938 ax-i2m1 10939 ax-1ne0 10940 ax-1rid 10941 ax-rnegex 10942 ax-rrecex 10943 ax-cnre 10944 ax-pre-lttri 10945 ax-pre-lttrn 10946 ax-pre-ltadd 10947 ax-pre-mulgt0 10948 ax-pre-sup 10949

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-rmo 3071 df-reu 3072 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-iun 4926 df-br 5075 df-opab 5137 df-mpt 5158 df-tr 5192 df-id 5489 df-eprel 5495 df-po 5503 df-so 5504 df-fr 5544 df-we 5546 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-pred 6202 df-ord 6269 df-on 6270 df-lim 6271 df-suc 6272 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440 df-fv 6441 df-riota 7232 df-ov 7278 df-oprab 7279 df-mpo 7280 df-om 7713 df-2nd 7832 df-frecs 8097 df-wrecs 8128 df-recs 8202 df-rdg 8241 df-er 8498 df-en 8734 df-dom 8735 df-sdom 8736 df-sup 9201 df-pnf 11011 df-mnf 11012 df-xr 11013 df-ltxr 11014 df-le 11015 df-sub 11207 df-neg 11208 df-div 11633 df-nn 11974 df-2 12036 df-3 12037 df-4 12038 df-5 12039 df-6 12040 df-7 12041 df-8 12042 df-9 12043 df-n0 12234 df-z 12320 df-dec 12438 df-uz 12583 df-rp 12731 df-seq 13722 df-exp 13783 df-cj 14810 df-re 14811 df-im 14812 df-sqrt 14946 df-abs 14947 df-dvds 15964

This theorem is referenced by: cubic2 25998 quart 26011

W3C validator