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 24574

Description: Solutions to a monic cubic equation, a special case of cubic 24576. (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 13006	. . . . . . 7 ⊢ (𝜑 → (𝐵↑2) ∈ ℂ)
4		3cn 11095	. . . . . . . 8 ⊢ 3 ∈ ℂ
5		mcubic.c	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ ℂ)
6		mulcl 10020	. . . . . . . 8 ⊢ ((3 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (3 · 𝐶) ∈ ℂ)
7	4, 5, 6	sylancr 695	. . . . . . 7 ⊢ (𝜑 → (3 · 𝐶) ∈ ℂ)
8	3, 7	subcld 10392	. . . . . 6 ⊢ (𝜑 → ((𝐵↑2) − (3 · 𝐶)) ∈ ℂ)
9	1, 8	eqeltrd 2701	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ ℂ)
10	4	a1i 11	. . . . 5 ⊢ (𝜑 → 3 ∈ ℂ)
11		3ne0 11115	. . . . . 6 ⊢ 3 ≠ 0
12	11	a1i 11	. . . . 5 ⊢ (𝜑 → 3 ≠ 0)
13	9, 10, 12	divcld 10801	. . . 4 ⊢ (𝜑 → (𝑀 / 3) ∈ ℂ)
14	13	negcld 10379	. . 3 ⊢ (𝜑 → -(𝑀 / 3) ∈ ℂ)
15		mcubic.n	. . . . 5 ⊢ (𝜑 → 𝑁 = (((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) + (;27 · 𝐷)))
16		2cn 11091	. . . . . . . 8 ⊢ 2 ∈ ℂ
17		3nn0 11310	. . . . . . . . 9 ⊢ 3 ∈ ℕ₀
18		expcl 12878	. . . . . . . . 9 ⊢ ((𝐵 ∈ ℂ ∧ 3 ∈ ℕ₀) → (𝐵↑3) ∈ ℂ)
19	2, 17, 18	sylancl 694	. . . . . . . 8 ⊢ (𝜑 → (𝐵↑3) ∈ ℂ)
20		mulcl 10020	. . . . . . . 8 ⊢ ((2 ∈ ℂ ∧ (𝐵↑3) ∈ ℂ) → (2 · (𝐵↑3)) ∈ ℂ)
21	16, 19, 20	sylancr 695	. . . . . . 7 ⊢ (𝜑 → (2 · (𝐵↑3)) ∈ ℂ)
22		9cn 11108	. . . . . . . 8 ⊢ 9 ∈ ℂ
23	2, 5	mulcld 10060	. . . . . . . 8 ⊢ (𝜑 → (𝐵 · 𝐶) ∈ ℂ)
24		mulcl 10020	. . . . . . . 8 ⊢ ((9 ∈ ℂ ∧ (𝐵 · 𝐶) ∈ ℂ) → (9 · (𝐵 · 𝐶)) ∈ ℂ)
25	22, 23, 24	sylancr 695	. . . . . . 7 ⊢ (𝜑 → (9 · (𝐵 · 𝐶)) ∈ ℂ)
26	21, 25	subcld 10392	. . . . . 6 ⊢ (𝜑 → ((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) ∈ ℂ)
27		2nn0 11309	. . . . . . . . 9 ⊢ 2 ∈ ℕ₀
28		7nn 11190	. . . . . . . . 9 ⊢ 7 ∈ ℕ
29	27, 28	decnncl 11518	. . . . . . . 8 ⊢ ;27 ∈ ℕ
30	29	nncni 11030	. . . . . . 7 ⊢ ;27 ∈ ℂ
31		mcubic.d	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ ℂ)
32		mulcl 10020	. . . . . . 7 ⊢ ((;27 ∈ ℂ ∧ 𝐷 ∈ ℂ) → (;27 · 𝐷) ∈ ℂ)
33	30, 31, 32	sylancr 695	. . . . . 6 ⊢ (𝜑 → (;27 · 𝐷) ∈ ℂ)
34	26, 33	addcld 10059	. . . . 5 ⊢ (𝜑 → (((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) + (;27 · 𝐷)) ∈ ℂ)
35	15, 34	eqeltrd 2701	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ℂ)
36	30	a1i 11	. . . 4 ⊢ (𝜑 → ;27 ∈ ℂ)
37	29	nnne0i 11055	. . . . 5 ⊢ ;27 ≠ 0
38	37	a1i 11	. . . 4 ⊢ (𝜑 → ;27 ≠ 0)
39	35, 36, 38	divcld 10801	. . 3 ⊢ (𝜑 → (𝑁 / ;27) ∈ ℂ)
40		mcubic.x	. . . 4 ⊢ (𝜑 → 𝑋 ∈ ℂ)
41	2, 10, 12	divcld 10801	. . . 4 ⊢ (𝜑 → (𝐵 / 3) ∈ ℂ)
42	40, 41	addcld 10059	. . 3 ⊢ (𝜑 → (𝑋 + (𝐵 / 3)) ∈ ℂ)
43		mcubic.t	. . . . 5 ⊢ (𝜑 → 𝑇 ∈ ℂ)
44	43, 10, 12	divcld 10801	. . . 4 ⊢ (𝜑 → (𝑇 / 3) ∈ ℂ)
45	44	negcld 10379	. . 3 ⊢ (𝜑 → -(𝑇 / 3) ∈ ℂ)
46		3nn 11186	. . . . . 6 ⊢ 3 ∈ ℕ
47	46	a1i 11	. . . . 5 ⊢ (𝜑 → 3 ∈ ℕ)
48		2nn 11185	. . . . . . 7 ⊢ 2 ∈ ℕ
49		1nn0 11308	. . . . . . 7 ⊢ 1 ∈ ℕ₀
50		1nn 11031	. . . . . . 7 ⊢ 1 ∈ ℕ
51		2t1e2 11176	. . . . . . . . 9 ⊢ (2 · 1) = 2
52	51	oveq1i 6660	. . . . . . . 8 ⊢ ((2 · 1) + 1) = (2 + 1)
53		2p1e3 11151	. . . . . . . 8 ⊢ (2 + 1) = 3
54	52, 53	eqtri 2644	. . . . . . 7 ⊢ ((2 · 1) + 1) = 3
55		1lt2 11194	. . . . . . 7 ⊢ 1 < 2
56	48, 49, 50, 54, 55	ndvdsi 15136	. . . . . 6 ⊢ ¬ 2 ∥ 3
57	56	a1i 11	. . . . 5 ⊢ (𝜑 → ¬ 2 ∥ 3)
58		oexpneg 15069	. . . . 5 ⊢ (((𝑇 / 3) ∈ ℂ ∧ 3 ∈ ℕ ∧ ¬ 2 ∥ 3) → (-(𝑇 / 3)↑3) = -((𝑇 / 3)↑3))
59	44, 47, 57, 58	syl3anc 1326	. . . 4 ⊢ (𝜑 → (-(𝑇 / 3)↑3) = -((𝑇 / 3)↑3))
60	17	a1i 11	. . . . . . 7 ⊢ (𝜑 → 3 ∈ ℕ₀)
61	43, 10, 12, 60	expdivd 13022	. . . . . 6 ⊢ (𝜑 → ((𝑇 / 3)↑3) = ((𝑇↑3) / (3↑3)))
62		mcubic.3	. . . . . . 7 ⊢ (𝜑 → (𝑇↑3) = ((𝑁 + 𝐺) / 2))
63		3exp3 15798	. . . . . . . 8 ⊢ (3↑3) = ;27
64	63	a1i 11	. . . . . . 7 ⊢ (𝜑 → (3↑3) = ;27)
65	62, 64	oveq12d 6668	. . . . . 6 ⊢ (𝜑 → ((𝑇↑3) / (3↑3)) = (((𝑁 + 𝐺) / 2) / ;27))
66		mcubic.g	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 ∈ ℂ)
67	35, 66	addcld 10059	. . . . . . . 8 ⊢ (𝜑 → (𝑁 + 𝐺) ∈ ℂ)
68		2cnd 11093	. . . . . . . 8 ⊢ (𝜑 → 2 ∈ ℂ)
69		2ne0 11113	. . . . . . . . 9 ⊢ 2 ≠ 0
70	69	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 2 ≠ 0)
71	67, 68, 36, 70, 38	divdiv32d 10826	. . . . . . 7 ⊢ (𝜑 → (((𝑁 + 𝐺) / 2) / ;27) = (((𝑁 + 𝐺) / ;27) / 2))
72	35, 66	addcomd 10238	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 + 𝐺) = (𝐺 + 𝑁))
73	72	oveq1d 6665	. . . . . . . . 9 ⊢ (𝜑 → ((𝑁 + 𝐺) / ;27) = ((𝐺 + 𝑁) / ;27))
74	66, 35, 36, 38	divdird 10839	. . . . . . . . 9 ⊢ (𝜑 → ((𝐺 + 𝑁) / ;27) = ((𝐺 / ;27) + (𝑁 / ;27)))
75	73, 74	eqtrd 2656	. . . . . . . 8 ⊢ (𝜑 → ((𝑁 + 𝐺) / ;27) = ((𝐺 / ;27) + (𝑁 / ;27)))
76	75	oveq1d 6665	. . . . . . 7 ⊢ (𝜑 → (((𝑁 + 𝐺) / ;27) / 2) = (((𝐺 / ;27) + (𝑁 / ;27)) / 2))
77	66, 36, 38	divcld 10801	. . . . . . . 8 ⊢ (𝜑 → (𝐺 / ;27) ∈ ℂ)
78	77, 39, 68, 70	divdird 10839	. . . . . . 7 ⊢ (𝜑 → (((𝐺 / ;27) + (𝑁 / ;27)) / 2) = (((𝐺 / ;27) / 2) + ((𝑁 / ;27) / 2)))
79	71, 76, 78	3eqtrd 2660	. . . . . 6 ⊢ (𝜑 → (((𝑁 + 𝐺) / 2) / ;27) = (((𝐺 / ;27) / 2) + ((𝑁 / ;27) / 2)))
80	61, 65, 79	3eqtrd 2660	. . . . 5 ⊢ (𝜑 → ((𝑇 / 3)↑3) = (((𝐺 / ;27) / 2) + ((𝑁 / ;27) / 2)))
81	80	negeqd 10275	. . . 4 ⊢ (𝜑 → -((𝑇 / 3)↑3) = -(((𝐺 / ;27) / 2) + ((𝑁 / ;27) / 2)))
82	77	halfcld 11277	. . . . 5 ⊢ (𝜑 → ((𝐺 / ;27) / 2) ∈ ℂ)
83	39	halfcld 11277	. . . . 5 ⊢ (𝜑 → ((𝑁 / ;27) / 2) ∈ ℂ)
84	82, 83	negdi2d 10406	. . . 4 ⊢ (𝜑 → -(((𝐺 / ;27) / 2) + ((𝑁 / ;27) / 2)) = (-((𝐺 / ;27) / 2) − ((𝑁 / ;27) / 2)))
85	59, 81, 84	3eqtrd 2660	. . 3 ⊢ (𝜑 → (-(𝑇 / 3)↑3) = (-((𝐺 / ;27) / 2) − ((𝑁 / ;27) / 2)))
86	82	negcld 10379	. . 3 ⊢ (𝜑 → -((𝐺 / ;27) / 2) ∈ ℂ)
87		sqneg 12923	. . . . 5 ⊢ (((𝐺 / ;27) / 2) ∈ ℂ → (-((𝐺 / ;27) / 2)↑2) = (((𝐺 / ;27) / 2)↑2))
88	82, 87	syl 17	. . . 4 ⊢ (𝜑 → (-((𝐺 / ;27) / 2)↑2) = (((𝐺 / ;27) / 2)↑2))
89	77, 68, 70	sqdivd 13021	. . . 4 ⊢ (𝜑 → (((𝐺 / ;27) / 2)↑2) = (((𝐺 / ;27)↑2) / (2↑2)))
90	39, 68, 70	sqdivd 13021	. . . . . . . 8 ⊢ (𝜑 → (((𝑁 / ;27) / 2)↑2) = (((𝑁 / ;27)↑2) / (2↑2)))
91	35, 36, 38	sqdivd 13021	. . . . . . . . 9 ⊢ (𝜑 → ((𝑁 / ;27)↑2) = ((𝑁↑2) / (;27↑2)))
92	91	oveq1d 6665	. . . . . . . 8 ⊢ (𝜑 → (((𝑁 / ;27)↑2) / (2↑2)) = (((𝑁↑2) / (;27↑2)) / (2↑2)))
93	90, 92	eqtr2d 2657	. . . . . . 7 ⊢ (𝜑 → (((𝑁↑2) / (;27↑2)) / (2↑2)) = (((𝑁 / ;27) / 2)↑2))
94		4cn 11098	. . . . . . . . . . . 12 ⊢ 4 ∈ ℂ
95	94	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 4 ∈ ℂ)
96		expcl 12878	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℂ ∧ 3 ∈ ℕ₀) → (𝑀↑3) ∈ ℂ)
97	9, 17, 96	sylancl 694	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀↑3) ∈ ℂ)
98	30	sqcli 12944	. . . . . . . . . . . 12 ⊢ (;27↑2) ∈ ℂ
99	98	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (;27↑2) ∈ ℂ)
100		sqne0 12930	. . . . . . . . . . . . 13 ⊢ (;27 ∈ ℂ → ((;27↑2) ≠ 0 ↔ ;27 ≠ 0))
101	36, 100	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → ((;27↑2) ≠ 0 ↔ ;27 ≠ 0))
102	38, 101	mpbird 247	. . . . . . . . . . 11 ⊢ (𝜑 → (;27↑2) ≠ 0)
103	95, 97, 99, 102	divassd 10836	. . . . . . . . . 10 ⊢ (𝜑 → ((4 · (𝑀↑3)) / (;27↑2)) = (4 · ((𝑀↑3) / (;27↑2))))
104	22	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 9 ∈ ℂ)
105		9nn 11192	. . . . . . . . . . . . . . 15 ⊢ 9 ∈ ℕ
106	105	nnne0i 11055	. . . . . . . . . . . . . 14 ⊢ 9 ≠ 0
107	106	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 9 ≠ 0)
108	9, 104, 107, 60	expdivd 13022	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑀 / 9)↑3) = ((𝑀↑3) / (9↑3)))
109	16, 4	mulcomi 10046	. . . . . . . . . . . . . . . 16 ⊢ (2 · 3) = (3 · 2)
110	109	oveq2i 6661	. . . . . . . . . . . . . . 15 ⊢ (3↑(2 · 3)) = (3↑(3 · 2))
111		expmul 12905	. . . . . . . . . . . . . . . 16 ⊢ ((3 ∈ ℂ ∧ 2 ∈ ℕ₀ ∧ 3 ∈ ℕ₀) → (3↑(2 · 3)) = ((3↑2)↑3))
112	4, 27, 17, 111	mp3an 1424	. . . . . . . . . . . . . . 15 ⊢ (3↑(2 · 3)) = ((3↑2)↑3)
113		expmul 12905	. . . . . . . . . . . . . . . 16 ⊢ ((3 ∈ ℂ ∧ 3 ∈ ℕ₀ ∧ 2 ∈ ℕ₀) → (3↑(3 · 2)) = ((3↑3)↑2))
114	4, 17, 27, 113	mp3an 1424	. . . . . . . . . . . . . . 15 ⊢ (3↑(3 · 2)) = ((3↑3)↑2)
115	110, 112, 114	3eqtr3i 2652	. . . . . . . . . . . . . 14 ⊢ ((3↑2)↑3) = ((3↑3)↑2)
116		sq3 12961	. . . . . . . . . . . . . . 15 ⊢ (3↑2) = 9
117	116	oveq1i 6660	. . . . . . . . . . . . . 14 ⊢ ((3↑2)↑3) = (9↑3)
118	63	oveq1i 6660	. . . . . . . . . . . . . 14 ⊢ ((3↑3)↑2) = (;27↑2)
119	115, 117, 118	3eqtr3i 2652	. . . . . . . . . . . . 13 ⊢ (9↑3) = (;27↑2)
120	119	oveq2i 6661	. . . . . . . . . . . 12 ⊢ ((𝑀↑3) / (9↑3)) = ((𝑀↑3) / (;27↑2))
121	108, 120	syl6eq 2672	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑀 / 9)↑3) = ((𝑀↑3) / (;27↑2)))
122	121	oveq2d 6666	. . . . . . . . . 10 ⊢ (𝜑 → (4 · ((𝑀 / 9)↑3)) = (4 · ((𝑀↑3) / (;27↑2))))
123	103, 122	eqtr4d 2659	. . . . . . . . 9 ⊢ (𝜑 → ((4 · (𝑀↑3)) / (;27↑2)) = (4 · ((𝑀 / 9)↑3)))
124	123	oveq1d 6665	. . . . . . . 8 ⊢ (𝜑 → (((4 · (𝑀↑3)) / (;27↑2)) / (2↑2)) = ((4 · ((𝑀 / 9)↑3)) / (2↑2)))
125		sq2 12960	. . . . . . . . . 10 ⊢ (2↑2) = 4
126	125	oveq2i 6661	. . . . . . . . 9 ⊢ ((4 · ((𝑀 / 9)↑3)) / (2↑2)) = ((4 · ((𝑀 / 9)↑3)) / 4)
127	9, 104, 107	divcld 10801	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀 / 9) ∈ ℂ)
128		expcl 12878	. . . . . . . . . . 11 ⊢ (((𝑀 / 9) ∈ ℂ ∧ 3 ∈ ℕ₀) → ((𝑀 / 9)↑3) ∈ ℂ)
129	127, 17, 128	sylancl 694	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑀 / 9)↑3) ∈ ℂ)
130		4ne0 11117	. . . . . . . . . . 11 ⊢ 4 ≠ 0
131	130	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 4 ≠ 0)
132	129, 95, 131	divcan3d 10806	. . . . . . . . 9 ⊢ (𝜑 → ((4 · ((𝑀 / 9)↑3)) / 4) = ((𝑀 / 9)↑3))
133	126, 132	syl5eq 2668	. . . . . . . 8 ⊢ (𝜑 → ((4 · ((𝑀 / 9)↑3)) / (2↑2)) = ((𝑀 / 9)↑3))
134	124, 133	eqtrd 2656	. . . . . . 7 ⊢ (𝜑 → (((4 · (𝑀↑3)) / (;27↑2)) / (2↑2)) = ((𝑀 / 9)↑3))
135	93, 134	oveq12d 6668	. . . . . 6 ⊢ (𝜑 → ((((𝑁↑2) / (;27↑2)) / (2↑2)) − (((4 · (𝑀↑3)) / (;27↑2)) / (2↑2))) = ((((𝑁 / ;27) / 2)↑2) − ((𝑀 / 9)↑3)))
136	35	sqcld 13006	. . . . . . . 8 ⊢ (𝜑 → (𝑁↑2) ∈ ℂ)
137	136, 99, 102	divcld 10801	. . . . . . 7 ⊢ (𝜑 → ((𝑁↑2) / (;27↑2)) ∈ ℂ)
138		mulcl 10020	. . . . . . . . 9 ⊢ ((4 ∈ ℂ ∧ (𝑀↑3) ∈ ℂ) → (4 · (𝑀↑3)) ∈ ℂ)
139	94, 97, 138	sylancr 695	. . . . . . . 8 ⊢ (𝜑 → (4 · (𝑀↑3)) ∈ ℂ)
140	139, 99, 102	divcld 10801	. . . . . . 7 ⊢ (𝜑 → ((4 · (𝑀↑3)) / (;27↑2)) ∈ ℂ)
141	16	sqcli 12944	. . . . . . . 8 ⊢ (2↑2) ∈ ℂ
142	141	a1i 11	. . . . . . 7 ⊢ (𝜑 → (2↑2) ∈ ℂ)
143	125, 130	eqnetri 2864	. . . . . . . 8 ⊢ (2↑2) ≠ 0
144	143	a1i 11	. . . . . . 7 ⊢ (𝜑 → (2↑2) ≠ 0)
145	137, 140, 142, 144	divsubdird 10840	. . . . . 6 ⊢ (𝜑 → ((((𝑁↑2) / (;27↑2)) − ((4 · (𝑀↑3)) / (;27↑2))) / (2↑2)) = ((((𝑁↑2) / (;27↑2)) / (2↑2)) − (((4 · (𝑀↑3)) / (;27↑2)) / (2↑2))))
146	83	sqcld 13006	. . . . . . 7 ⊢ (𝜑 → (((𝑁 / ;27) / 2)↑2) ∈ ℂ)
147	146, 129	negsubd 10398	. . . . . 6 ⊢ (𝜑 → ((((𝑁 / ;27) / 2)↑2) + -((𝑀 / 9)↑3)) = ((((𝑁 / ;27) / 2)↑2) − ((𝑀 / 9)↑3)))
148	135, 145, 147	3eqtr4d 2666	. . . . 5 ⊢ (𝜑 → ((((𝑁↑2) / (;27↑2)) − ((4 · (𝑀↑3)) / (;27↑2))) / (2↑2)) = ((((𝑁 / ;27) / 2)↑2) + -((𝑀 / 9)↑3)))
149	66, 36, 38	sqdivd 13021	. . . . . . 7 ⊢ (𝜑 → ((𝐺 / ;27)↑2) = ((𝐺↑2) / (;27↑2)))
150		mcubic.2	. . . . . . . 8 ⊢ (𝜑 → (𝐺↑2) = ((𝑁↑2) − (4 · (𝑀↑3))))
151	150	oveq1d 6665	. . . . . . 7 ⊢ (𝜑 → ((𝐺↑2) / (;27↑2)) = (((𝑁↑2) − (4 · (𝑀↑3))) / (;27↑2)))
152	136, 139, 99, 102	divsubdird 10840	. . . . . . 7 ⊢ (𝜑 → (((𝑁↑2) − (4 · (𝑀↑3))) / (;27↑2)) = (((𝑁↑2) / (;27↑2)) − ((4 · (𝑀↑3)) / (;27↑2))))
153	149, 151, 152	3eqtrd 2660	. . . . . 6 ⊢ (𝜑 → ((𝐺 / ;27)↑2) = (((𝑁↑2) / (;27↑2)) − ((4 · (𝑀↑3)) / (;27↑2))))
154	153	oveq1d 6665	. . . . 5 ⊢ (𝜑 → (((𝐺 / ;27)↑2) / (2↑2)) = ((((𝑁↑2) / (;27↑2)) − ((4 · (𝑀↑3)) / (;27↑2))) / (2↑2)))
155		oexpneg 15069	. . . . . . 7 ⊢ (((𝑀 / 9) ∈ ℂ ∧ 3 ∈ ℕ ∧ ¬ 2 ∥ 3) → (-(𝑀 / 9)↑3) = -((𝑀 / 9)↑3))
156	127, 47, 57, 155	syl3anc 1326	. . . . . 6 ⊢ (𝜑 → (-(𝑀 / 9)↑3) = -((𝑀 / 9)↑3))
157	156	oveq2d 6666	. . . . 5 ⊢ (𝜑 → ((((𝑁 / ;27) / 2)↑2) + (-(𝑀 / 9)↑3)) = ((((𝑁 / ;27) / 2)↑2) + -((𝑀 / 9)↑3)))
158	148, 154, 157	3eqtr4d 2666	. . . 4 ⊢ (𝜑 → (((𝐺 / ;27)↑2) / (2↑2)) = ((((𝑁 / ;27) / 2)↑2) + (-(𝑀 / 9)↑3)))
159	88, 89, 158	3eqtrd 2660	. . 3 ⊢ (𝜑 → (-((𝐺 / ;27) / 2)↑2) = ((((𝑁 / ;27) / 2)↑2) + (-(𝑀 / 9)↑3)))
160	9, 10, 10, 12, 12	divdiv1d 10832	. . . . . 6 ⊢ (𝜑 → ((𝑀 / 3) / 3) = (𝑀 / (3 · 3)))
161		3t3e9 11180	. . . . . . 7 ⊢ (3 · 3) = 9
162	161	oveq2i 6661	. . . . . 6 ⊢ (𝑀 / (3 · 3)) = (𝑀 / 9)
163	160, 162	syl6eq 2672	. . . . 5 ⊢ (𝜑 → ((𝑀 / 3) / 3) = (𝑀 / 9))
164	163	negeqd 10275	. . . 4 ⊢ (𝜑 → -((𝑀 / 3) / 3) = -(𝑀 / 9))
165	13, 10, 12	divnegd 10814	. . . 4 ⊢ (𝜑 → -((𝑀 / 3) / 3) = (-(𝑀 / 3) / 3))
166	164, 165	eqtr3d 2658	. . 3 ⊢ (𝜑 → -(𝑀 / 9) = (-(𝑀 / 3) / 3))
167		eqidd 2623	. . 3 ⊢ (𝜑 → ((𝑁 / ;27) / 2) = ((𝑁 / ;27) / 2))
168		mcubic.0	. . . . 5 ⊢ (𝜑 → 𝑇 ≠ 0)
169	43, 10, 168, 12	divne0d 10817	. . . 4 ⊢ (𝜑 → (𝑇 / 3) ≠ 0)
170	44, 169	negne0d 10390	. . 3 ⊢ (𝜑 → -(𝑇 / 3) ≠ 0)
171	14, 39, 42, 45, 85, 86, 159, 166, 167, 170	dcubic 24573	. 2 ⊢ (𝜑 → ((((𝑋 + (𝐵 / 3))↑3) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27))) = 0 ↔ ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ (𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))))))
172		binom3 12985	. . . . . . 7 ⊢ ((𝑋 ∈ ℂ ∧ (𝐵 / 3) ∈ ℂ) → ((𝑋 + (𝐵 / 3))↑3) = (((𝑋↑3) + (3 · ((𝑋↑2) · (𝐵 / 3)))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))))
173	40, 41, 172	syl2anc 693	. . . . . 6 ⊢ (𝜑 → ((𝑋 + (𝐵 / 3))↑3) = (((𝑋↑3) + (3 · ((𝑋↑2) · (𝐵 / 3)))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))))
174	40	sqcld 13006	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋↑2) ∈ ℂ)
175	10, 174, 41	mul12d 10245	. . . . . . . . 9 ⊢ (𝜑 → (3 · ((𝑋↑2) · (𝐵 / 3))) = ((𝑋↑2) · (3 · (𝐵 / 3))))
176	2, 10, 12	divcan2d 10803	. . . . . . . . . 10 ⊢ (𝜑 → (3 · (𝐵 / 3)) = 𝐵)
177	176	oveq2d 6666	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋↑2) · (3 · (𝐵 / 3))) = ((𝑋↑2) · 𝐵))
178	174, 2	mulcomd 10061	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋↑2) · 𝐵) = (𝐵 · (𝑋↑2)))
179	175, 177, 178	3eqtrd 2660	. . . . . . . 8 ⊢ (𝜑 → (3 · ((𝑋↑2) · (𝐵 / 3))) = (𝐵 · (𝑋↑2)))
180	179	oveq2d 6666	. . . . . . 7 ⊢ (𝜑 → ((𝑋↑3) + (3 · ((𝑋↑2) · (𝐵 / 3)))) = ((𝑋↑3) + (𝐵 · (𝑋↑2))))
181	180	oveq1d 6665	. . . . . 6 ⊢ (𝜑 → (((𝑋↑3) + (3 · ((𝑋↑2) · (𝐵 / 3)))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))) = (((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))))
182	173, 181	eqtrd 2656	. . . . 5 ⊢ (𝜑 → ((𝑋 + (𝐵 / 3))↑3) = (((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))))
183	182	oveq1d 6665	. . . 4 ⊢ (𝜑 → (((𝑋 + (𝐵 / 3))↑3) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27))) = ((((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27))))
184		expcl 12878	. . . . . . 7 ⊢ ((𝑋 ∈ ℂ ∧ 3 ∈ ℕ₀) → (𝑋↑3) ∈ ℂ)
185	40, 17, 184	sylancl 694	. . . . . 6 ⊢ (𝜑 → (𝑋↑3) ∈ ℂ)
186	2, 174	mulcld 10060	. . . . . 6 ⊢ (𝜑 → (𝐵 · (𝑋↑2)) ∈ ℂ)
187	185, 186	addcld 10059	. . . . 5 ⊢ (𝜑 → ((𝑋↑3) + (𝐵 · (𝑋↑2))) ∈ ℂ)
188	41	sqcld 13006	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 / 3)↑2) ∈ ℂ)
189	40, 188	mulcld 10060	. . . . . . 7 ⊢ (𝜑 → (𝑋 · ((𝐵 / 3)↑2)) ∈ ℂ)
190	10, 189	mulcld 10060	. . . . . 6 ⊢ (𝜑 → (3 · (𝑋 · ((𝐵 / 3)↑2))) ∈ ℂ)
191		expcl 12878	. . . . . . 7 ⊢ (((𝐵 / 3) ∈ ℂ ∧ 3 ∈ ℕ₀) → ((𝐵 / 3)↑3) ∈ ℂ)
192	41, 17, 191	sylancl 694	. . . . . 6 ⊢ (𝜑 → ((𝐵 / 3)↑3) ∈ ℂ)
193	190, 192	addcld 10059	. . . . 5 ⊢ (𝜑 → ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) ∈ ℂ)
194	14, 42	mulcld 10060	. . . . . 6 ⊢ (𝜑 → (-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) ∈ ℂ)
195	194, 39	addcld 10059	. . . . 5 ⊢ (𝜑 → ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27)) ∈ ℂ)
196	187, 193, 195	addassd 10062	. . . 4 ⊢ (𝜑 → ((((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27))) = (((𝑋↑3) + (𝐵 · (𝑋↑2))) + (((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27)))))
197	14, 40, 41	adddid 10064	. . . . . . . . . 10 ⊢ (𝜑 → (-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) = ((-(𝑀 / 3) · 𝑋) + (-(𝑀 / 3) · (𝐵 / 3))))
198	197	oveq1d 6665	. . . . . . . . 9 ⊢ (𝜑 → ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27)) = (((-(𝑀 / 3) · 𝑋) + (-(𝑀 / 3) · (𝐵 / 3))) + (𝑁 / ;27)))
199	14, 40	mulcld 10060	. . . . . . . . . 10 ⊢ (𝜑 → (-(𝑀 / 3) · 𝑋) ∈ ℂ)
200	14, 41	mulcld 10060	. . . . . . . . . 10 ⊢ (𝜑 → (-(𝑀 / 3) · (𝐵 / 3)) ∈ ℂ)
201	199, 200, 39	addassd 10062	. . . . . . . . 9 ⊢ (𝜑 → (((-(𝑀 / 3) · 𝑋) + (-(𝑀 / 3) · (𝐵 / 3))) + (𝑁 / ;27)) = ((-(𝑀 / 3) · 𝑋) + ((-(𝑀 / 3) · (𝐵 / 3)) + (𝑁 / ;27))))
202	1	oveq1d 6665	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀 / 3) = (((𝐵↑2) − (3 · 𝐶)) / 3))
203	3, 7, 10, 12	divsubdird 10840	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐵↑2) − (3 · 𝐶)) / 3) = (((𝐵↑2) / 3) − ((3 · 𝐶) / 3)))
204	5, 10, 12	divcan3d 10806	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((3 · 𝐶) / 3) = 𝐶)
205	204	oveq2d 6666	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐵↑2) / 3) − ((3 · 𝐶) / 3)) = (((𝐵↑2) / 3) − 𝐶))
206	202, 203, 205	3eqtrd 2660	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀 / 3) = (((𝐵↑2) / 3) − 𝐶))
207	206	negeqd 10275	. . . . . . . . . . . . 13 ⊢ (𝜑 → -(𝑀 / 3) = -(((𝐵↑2) / 3) − 𝐶))
208	3, 10, 12	divcld 10801	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵↑2) / 3) ∈ ℂ)
209	208, 5	negsubdi2d 10408	. . . . . . . . . . . . 13 ⊢ (𝜑 → -(((𝐵↑2) / 3) − 𝐶) = (𝐶 − ((𝐵↑2) / 3)))
210	207, 209	eqtrd 2656	. . . . . . . . . . . 12 ⊢ (𝜑 → -(𝑀 / 3) = (𝐶 − ((𝐵↑2) / 3)))
211	210	oveq1d 6665	. . . . . . . . . . 11 ⊢ (𝜑 → (-(𝑀 / 3) · 𝑋) = ((𝐶 − ((𝐵↑2) / 3)) · 𝑋))
212	5, 208, 40	subdird 10487	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐶 − ((𝐵↑2) / 3)) · 𝑋) = ((𝐶 · 𝑋) − (((𝐵↑2) / 3) · 𝑋)))
213	208, 40	mulcomd 10061	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐵↑2) / 3) · 𝑋) = (𝑋 · ((𝐵↑2) / 3)))
214	4	sqvali 12943	. . . . . . . . . . . . . . . . . 18 ⊢ (3↑2) = (3 · 3)
215	214	oveq2i 6661	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵↑2) / (3↑2)) = ((𝐵↑2) / (3 · 3))
216	2, 10, 12	sqdivd 13021	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐵 / 3)↑2) = ((𝐵↑2) / (3↑2)))
217	3, 10, 10, 12, 12	divdiv1d 10832	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝐵↑2) / 3) / 3) = ((𝐵↑2) / (3 · 3)))
218	215, 216, 217	3eqtr4a 2682	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐵 / 3)↑2) = (((𝐵↑2) / 3) / 3))
219	218	oveq2d 6666	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (3 · ((𝐵 / 3)↑2)) = (3 · (((𝐵↑2) / 3) / 3)))
220	208, 10, 12	divcan2d 10803	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (3 · (((𝐵↑2) / 3) / 3)) = ((𝐵↑2) / 3))
221	219, 220	eqtrd 2656	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (3 · ((𝐵 / 3)↑2)) = ((𝐵↑2) / 3))
222	221	oveq2d 6666	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 · (3 · ((𝐵 / 3)↑2))) = (𝑋 · ((𝐵↑2) / 3)))
223	40, 10, 188	mul12d 10245	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 · (3 · ((𝐵 / 3)↑2))) = (3 · (𝑋 · ((𝐵 / 3)↑2))))
224	213, 222, 223	3eqtr2d 2662	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐵↑2) / 3) · 𝑋) = (3 · (𝑋 · ((𝐵 / 3)↑2))))
225	224	oveq2d 6666	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐶 · 𝑋) − (((𝐵↑2) / 3) · 𝑋)) = ((𝐶 · 𝑋) − (3 · (𝑋 · ((𝐵 / 3)↑2)))))
226	211, 212, 225	3eqtrd 2660	. . . . . . . . . 10 ⊢ (𝜑 → (-(𝑀 / 3) · 𝑋) = ((𝐶 · 𝑋) − (3 · (𝑋 · ((𝐵 / 3)↑2)))))
227	210	oveq1d 6665	. . . . . . . . . . . . 13 ⊢ (𝜑 → (-(𝑀 / 3) · (𝐵 / 3)) = ((𝐶 − ((𝐵↑2) / 3)) · (𝐵 / 3)))
228	5, 208, 41	subdird 10487	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐶 − ((𝐵↑2) / 3)) · (𝐵 / 3)) = ((𝐶 · (𝐵 / 3)) − (((𝐵↑2) / 3) · (𝐵 / 3))))
229	5, 2, 10, 12	divassd 10836	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐶 · 𝐵) / 3) = (𝐶 · (𝐵 / 3)))
230	5, 2	mulcomd 10061	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐶 · 𝐵) = (𝐵 · 𝐶))
231	230	oveq1d 6665	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐶 · 𝐵) / 3) = ((𝐵 · 𝐶) / 3))
232	229, 231	eqtr3d 2658	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐶 · (𝐵 / 3)) = ((𝐵 · 𝐶) / 3))
233	3, 10, 2, 10, 12, 12	divmuldivd 10842	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐵↑2) / 3) · (𝐵 / 3)) = (((𝐵↑2) · 𝐵) / (3 · 3)))
234		df-3 11080	. . . . . . . . . . . . . . . . . 18 ⊢ 3 = (2 + 1)
235	234	oveq2i 6661	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵↑3) = (𝐵↑(2 + 1))
236		expp1 12867	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ∈ ℂ ∧ 2 ∈ ℕ₀) → (𝐵↑(2 + 1)) = ((𝐵↑2) · 𝐵))
237	2, 27, 236	sylancl 694	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵↑(2 + 1)) = ((𝐵↑2) · 𝐵))
238	235, 237	syl5req 2669	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐵↑2) · 𝐵) = (𝐵↑3))
239	161	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (3 · 3) = 9)
240	238, 239	oveq12d 6668	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐵↑2) · 𝐵) / (3 · 3)) = ((𝐵↑3) / 9))
241	233, 240	eqtrd 2656	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐵↑2) / 3) · (𝐵 / 3)) = ((𝐵↑3) / 9))
242	232, 241	oveq12d 6668	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐶 · (𝐵 / 3)) − (((𝐵↑2) / 3) · (𝐵 / 3))) = (((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)))
243	227, 228, 242	3eqtrd 2660	. . . . . . . . . . . 12 ⊢ (𝜑 → (-(𝑀 / 3) · (𝐵 / 3)) = (((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)))
244	15	oveq1d 6665	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 / ;27) = ((((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) + (;27 · 𝐷)) / ;27))
245	26, 33, 36, 38	divdird 10839	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) + (;27 · 𝐷)) / ;27) = ((((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) / ;27) + ((;27 · 𝐷) / ;27)))
246	21, 25, 36, 38	divsubdird 10840	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) / ;27) = (((2 · (𝐵↑3)) / ;27) − ((9 · (𝐵 · 𝐶)) / ;27)))
247		9t3e27 11664	. . . . . . . . . . . . . . . . . 18 ⊢ (9 · 3) = ;27
248	247	oveq2i 6661	. . . . . . . . . . . . . . . . 17 ⊢ ((9 · (𝐵 · 𝐶)) / (9 · 3)) = ((9 · (𝐵 · 𝐶)) / ;27)
249	23, 10, 104, 12, 107	divcan5d 10827	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((9 · (𝐵 · 𝐶)) / (9 · 3)) = ((𝐵 · 𝐶) / 3))
250	248, 249	syl5eqr 2670	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((9 · (𝐵 · 𝐶)) / ;27) = ((𝐵 · 𝐶) / 3))
251	250	oveq2d 6666	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((2 · (𝐵↑3)) / ;27) − ((9 · (𝐵 · 𝐶)) / ;27)) = (((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3)))
252	246, 251	eqtrd 2656	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) / ;27) = (((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3)))
253	31, 36, 38	divcan3d 10806	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((;27 · 𝐷) / ;27) = 𝐷)
254	252, 253	oveq12d 6668	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) / ;27) + ((;27 · 𝐷) / ;27)) = ((((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3)) + 𝐷))
255	244, 245, 254	3eqtrd 2660	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁 / ;27) = ((((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3)) + 𝐷))
256	243, 255	oveq12d 6668	. . . . . . . . . . 11 ⊢ (𝜑 → ((-(𝑀 / 3) · (𝐵 / 3)) + (𝑁 / ;27)) = ((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + ((((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3)) + 𝐷)))
257	19, 104, 107	divcld 10801	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐵↑3) / 9) ∈ ℂ)
258	21, 36, 38	divcld 10801	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((2 · (𝐵↑3)) / ;27) ∈ ℂ)
259	257, 258	negsubdi2d 10408	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -(((𝐵↑3) / 9) − ((2 · (𝐵↑3)) / ;27)) = (((2 · (𝐵↑3)) / ;27) − ((𝐵↑3) / 9)))
260	2, 10, 12, 60	expdivd 13022	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐵 / 3)↑3) = ((𝐵↑3) / (3↑3)))
261	63	oveq2i 6661	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵↑3) / (3↑3)) = ((𝐵↑3) / ;27)
262		ax-1cn 9994	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 ∈ ℂ
263	4, 16, 262, 53	subaddrii 10370	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (3 − 2) = 1
264	263	oveq1i 6660	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((3 − 2) · (𝐵↑3)) = (1 · (𝐵↑3))
265	19	mulid2d 10058	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (1 · (𝐵↑3)) = (𝐵↑3))
266	264, 265	syl5eq 2668	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((3 − 2) · (𝐵↑3)) = (𝐵↑3))
267	10, 68, 19	subdird 10487	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((3 − 2) · (𝐵↑3)) = ((3 · (𝐵↑3)) − (2 · (𝐵↑3))))
268	266, 267	eqtr3d 2658	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐵↑3) = ((3 · (𝐵↑3)) − (2 · (𝐵↑3))))
269	268	oveq1d 6665	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐵↑3) / ;27) = (((3 · (𝐵↑3)) − (2 · (𝐵↑3))) / ;27))
270		mulcl 10020	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((3 ∈ ℂ ∧ (𝐵↑3) ∈ ℂ) → (3 · (𝐵↑3)) ∈ ℂ)
271	4, 19, 270	sylancr 695	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (3 · (𝐵↑3)) ∈ ℂ)
272	271, 21, 36, 38	divsubdird 10840	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((3 · (𝐵↑3)) − (2 · (𝐵↑3))) / ;27) = (((3 · (𝐵↑3)) / ;27) − ((2 · (𝐵↑3)) / ;27)))
273	269, 272	eqtrd 2656	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐵↑3) / ;27) = (((3 · (𝐵↑3)) / ;27) − ((2 · (𝐵↑3)) / ;27)))
274	261, 273	syl5eq 2668	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐵↑3) / (3↑3)) = (((3 · (𝐵↑3)) / ;27) − ((2 · (𝐵↑3)) / ;27)))
275	22, 4, 247	mulcomli 10047	. . . . . . . . . . . . . . . . . . 19 ⊢ (3 · 9) = ;27
276	275	oveq2i 6661	. . . . . . . . . . . . . . . . . 18 ⊢ ((3 · (𝐵↑3)) / (3 · 9)) = ((3 · (𝐵↑3)) / ;27)
277	19, 104, 10, 107, 12	divcan5d 10827	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((3 · (𝐵↑3)) / (3 · 9)) = ((𝐵↑3) / 9))
278	276, 277	syl5eqr 2670	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((3 · (𝐵↑3)) / ;27) = ((𝐵↑3) / 9))
279	278	oveq1d 6665	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((3 · (𝐵↑3)) / ;27) − ((2 · (𝐵↑3)) / ;27)) = (((𝐵↑3) / 9) − ((2 · (𝐵↑3)) / ;27)))
280	260, 274, 279	3eqtrd 2660	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐵 / 3)↑3) = (((𝐵↑3) / 9) − ((2 · (𝐵↑3)) / ;27)))
281	280	negeqd 10275	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -((𝐵 / 3)↑3) = -(((𝐵↑3) / 9) − ((2 · (𝐵↑3)) / ;27)))
282	23, 10, 12	divcld 10801	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐵 · 𝐶) / 3) ∈ ℂ)
283	282, 257, 258	npncan3d 10428	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + (((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3))) = (((2 · (𝐵↑3)) / ;27) − ((𝐵↑3) / 9)))
284	259, 281, 283	3eqtr4d 2666	. . . . . . . . . . . . 13 ⊢ (𝜑 → -((𝐵 / 3)↑3) = ((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + (((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3))))
285	284	oveq1d 6665	. . . . . . . . . . . 12 ⊢ (𝜑 → (-((𝐵 / 3)↑3) + 𝐷) = (((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + (((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3))) + 𝐷))
286	192	negcld 10379	. . . . . . . . . . . . 13 ⊢ (𝜑 → -((𝐵 / 3)↑3) ∈ ℂ)
287	286, 31	addcomd 10238	. . . . . . . . . . . 12 ⊢ (𝜑 → (-((𝐵 / 3)↑3) + 𝐷) = (𝐷 + -((𝐵 / 3)↑3)))
288	243, 200	eqeltrrd 2702	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) ∈ ℂ)
289	258, 282	subcld 10392	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3)) ∈ ℂ)
290	288, 289, 31	addassd 10062	. . . . . . . . . . . 12 ⊢ (𝜑 → (((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + (((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3))) + 𝐷) = ((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + ((((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3)) + 𝐷)))
291	285, 287, 290	3eqtr3d 2664	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐷 + -((𝐵 / 3)↑3)) = ((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + ((((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3)) + 𝐷)))
292	31, 192	negsubd 10398	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐷 + -((𝐵 / 3)↑3)) = (𝐷 − ((𝐵 / 3)↑3)))
293	256, 291, 292	3eqtr2d 2662	. . . . . . . . . 10 ⊢ (𝜑 → ((-(𝑀 / 3) · (𝐵 / 3)) + (𝑁 / ;27)) = (𝐷 − ((𝐵 / 3)↑3)))
294	226, 293	oveq12d 6668	. . . . . . . . 9 ⊢ (𝜑 → ((-(𝑀 / 3) · 𝑋) + ((-(𝑀 / 3) · (𝐵 / 3)) + (𝑁 / ;27))) = (((𝐶 · 𝑋) − (3 · (𝑋 · ((𝐵 / 3)↑2)))) + (𝐷 − ((𝐵 / 3)↑3))))
295	198, 201, 294	3eqtrd 2660	. . . . . . . 8 ⊢ (𝜑 → ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27)) = (((𝐶 · 𝑋) − (3 · (𝑋 · ((𝐵 / 3)↑2)))) + (𝐷 − ((𝐵 / 3)↑3))))
296	5, 40	mulcld 10060	. . . . . . . . 9 ⊢ (𝜑 → (𝐶 · 𝑋) ∈ ℂ)
297	296, 31, 190, 192	addsub4d 10439	. . . . . . . 8 ⊢ (𝜑 → (((𝐶 · 𝑋) + 𝐷) − ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))) = (((𝐶 · 𝑋) − (3 · (𝑋 · ((𝐵 / 3)↑2)))) + (𝐷 − ((𝐵 / 3)↑3))))
298	295, 297	eqtr4d 2659	. . . . . . 7 ⊢ (𝜑 → ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27)) = (((𝐶 · 𝑋) + 𝐷) − ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))))
299	298	oveq2d 6666	. . . . . 6 ⊢ (𝜑 → (((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27))) = (((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) + (((𝐶 · 𝑋) + 𝐷) − ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)))))
300	296, 31	addcld 10059	. . . . . . 7 ⊢ (𝜑 → ((𝐶 · 𝑋) + 𝐷) ∈ ℂ)
301	193, 300	pncan3d 10395	. . . . . 6 ⊢ (𝜑 → (((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) + (((𝐶 · 𝑋) + 𝐷) − ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)))) = ((𝐶 · 𝑋) + 𝐷))
302	299, 301	eqtrd 2656	. . . . 5 ⊢ (𝜑 → (((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27))) = ((𝐶 · 𝑋) + 𝐷))
303	302	oveq2d 6666	. . . 4 ⊢ (𝜑 → (((𝑋↑3) + (𝐵 · (𝑋↑2))) + (((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27)))) = (((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((𝐶 · 𝑋) + 𝐷)))
304	183, 196, 303	3eqtrd 2660	. . 3 ⊢ (𝜑 → (((𝑋 + (𝐵 / 3))↑3) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27))) = (((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((𝐶 · 𝑋) + 𝐷)))
305	304	eqeq1d 2624	. 2 ⊢ (𝜑 → ((((𝑋 + (𝐵 / 3))↑3) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27))) = 0 ↔ (((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((𝐶 · 𝑋) + 𝐷)) = 0))
306		oveq1 6657	. . . . . . . 8 ⊢ (𝑟 = 0 → (𝑟↑3) = (0↑3))
307		0exp 12895	. . . . . . . . 9 ⊢ (3 ∈ ℕ → (0↑3) = 0)
308	46, 307	ax-mp 5	. . . . . . . 8 ⊢ (0↑3) = 0
309	306, 308	syl6eq 2672	. . . . . . 7 ⊢ (𝑟 = 0 → (𝑟↑3) = 0)
310		0ne1 11088	. . . . . . . 8 ⊢ 0 ≠ 1
311	310	a1i 11	. . . . . . 7 ⊢ (𝑟 = 0 → 0 ≠ 1)
312	309, 311	eqnetrd 2861	. . . . . 6 ⊢ (𝑟 = 0 → (𝑟↑3) ≠ 1)
313	312	necon2i 2828	. . . . 5 ⊢ ((𝑟↑3) = 1 → 𝑟 ≠ 0)
314		eqcom 2629	. . . . . . . 8 ⊢ (𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) ↔ -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = 𝑋)
315	2	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝐵 ∈ ℂ)
316		simprl 794	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑟 ∈ ℂ)
317	43	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑇 ∈ ℂ)
318	316, 317	mulcld 10060	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑟 · 𝑇) ∈ ℂ)
319	9	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑀 ∈ ℂ)
320		simprr 796	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑟 ≠ 0)
321	168	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑇 ≠ 0)
322	316, 317, 320, 321	mulne0d 10679	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑟 · 𝑇) ≠ 0)
323	319, 318, 322	divcld 10801	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑀 / (𝑟 · 𝑇)) ∈ ℂ)
324	318, 323	addcld 10059	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) ∈ ℂ)
325	4	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 3 ∈ ℂ)
326	11	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 3 ≠ 0)
327	315, 324, 325, 326	divdird 10839	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝐵 + ((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇)))) / 3) = ((𝐵 / 3) + (((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)))
328	315, 318, 323	addassd 10062	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) = (𝐵 + ((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇)))))
329	328	oveq1d 6665	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = ((𝐵 + ((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇)))) / 3))
330	41	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝐵 / 3) ∈ ℂ)
331	324, 325, 326	divcld 10801	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) ∈ ℂ)
332	330, 331	subnegd 10399	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝐵 / 3) − -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)) = ((𝐵 / 3) + (((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)))
333	327, 329, 332	3eqtr4d 2666	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = ((𝐵 / 3) − -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)))
334	333	negeqd 10275	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = -((𝐵 / 3) − -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)))
335	331	negcld 10379	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) ∈ ℂ)
336	330, 335	negsubdi2d 10408	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -((𝐵 / 3) − -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)) = (-(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) − (𝐵 / 3)))
337	334, 336	eqtrd 2656	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = (-(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) − (𝐵 / 3)))
338	337	eqeq1d 2624	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (-(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = 𝑋 ↔ (-(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) − (𝐵 / 3)) = 𝑋))
339	314, 338	syl5bb 272	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) ↔ (-(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) − (𝐵 / 3)) = 𝑋))
340	40	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑋 ∈ ℂ)
341	335, 330, 340	subadd2d 10411	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((-(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) − (𝐵 / 3)) = 𝑋 ↔ (𝑋 + (𝐵 / 3)) = -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)))
342	318, 323, 325, 326	divdird 10839	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) = (((𝑟 · 𝑇) / 3) + ((𝑀 / (𝑟 · 𝑇)) / 3)))
343	342	negeqd 10275	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) = -(((𝑟 · 𝑇) / 3) + ((𝑀 / (𝑟 · 𝑇)) / 3)))
344	318, 325, 326	divcld 10801	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑟 · 𝑇) / 3) ∈ ℂ)
345	323, 325, 326	divcld 10801	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑀 / (𝑟 · 𝑇)) / 3) ∈ ℂ)
346	344, 345	negdi2d 10406	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝑟 · 𝑇) / 3) + ((𝑀 / (𝑟 · 𝑇)) / 3)) = (-((𝑟 · 𝑇) / 3) − ((𝑀 / (𝑟 · 𝑇)) / 3)))
347	316, 317, 325, 326	divassd 10836	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑟 · 𝑇) / 3) = (𝑟 · (𝑇 / 3)))
348	347	negeqd 10275	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -((𝑟 · 𝑇) / 3) = -(𝑟 · (𝑇 / 3)))
349	44	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑇 / 3) ∈ ℂ)
350	316, 349	mulneg2d 10484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑟 · -(𝑇 / 3)) = -(𝑟 · (𝑇 / 3)))
351	348, 350	eqtr4d 2659	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -((𝑟 · 𝑇) / 3) = (𝑟 · -(𝑇 / 3)))
352	319, 318, 325, 322, 326	divdiv32d 10826	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑀 / (𝑟 · 𝑇)) / 3) = ((𝑀 / 3) / (𝑟 · 𝑇)))
353	13	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑀 / 3) ∈ ℂ)
354	353, 318, 325, 322, 326	divcan7d 10829	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝑀 / 3) / 3) / ((𝑟 · 𝑇) / 3)) = ((𝑀 / 3) / (𝑟 · 𝑇)))
355	163	oveq1d 6665	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑀 / 3) / 3) / ((𝑟 · 𝑇) / 3)) = ((𝑀 / 9) / ((𝑟 · 𝑇) / 3)))
356	355	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝑀 / 3) / 3) / ((𝑟 · 𝑇) / 3)) = ((𝑀 / 9) / ((𝑟 · 𝑇) / 3)))
357	352, 354, 356	3eqtr2d 2662	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑀 / (𝑟 · 𝑇)) / 3) = ((𝑀 / 9) / ((𝑟 · 𝑇) / 3)))
358	127	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑀 / 9) ∈ ℂ)
359	318, 325, 322, 326	divne0d 10817	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑟 · 𝑇) / 3) ≠ 0)
360	358, 344, 359	div2negd 10816	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (-(𝑀 / 9) / -((𝑟 · 𝑇) / 3)) = ((𝑀 / 9) / ((𝑟 · 𝑇) / 3)))
361	351	oveq2d 6666	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (-(𝑀 / 9) / -((𝑟 · 𝑇) / 3)) = (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3))))
362	357, 360, 361	3eqtr2d 2662	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑀 / (𝑟 · 𝑇)) / 3) = (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3))))
363	351, 362	oveq12d 6668	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (-((𝑟 · 𝑇) / 3) − ((𝑀 / (𝑟 · 𝑇)) / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))))
364	343, 346, 363	3eqtrd 2660	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))))
365	364	eqeq2d 2632	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑋 + (𝐵 / 3)) = -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) ↔ (𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3))))))
366	339, 341, 365	3bitrrd 295	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))) ↔ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3)))
367	366	anassrs 680	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ 𝑟 ≠ 0) → ((𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))) ↔ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3)))
368	313, 367	sylan2 491	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ (𝑟↑3) = 1) → ((𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))) ↔ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3)))
369	368	pm5.32da 673	. . 3 ⊢ ((𝜑 ∧ 𝑟 ∈ ℂ) → (((𝑟↑3) = 1 ∧ (𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3))))) ↔ ((𝑟↑3) = 1 ∧ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3))))
370	369	rexbidva 3049	. 2 ⊢ (𝜑 → (∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ (𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3))))) ↔ ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3))))
371	171, 305, 370	3bitr3d 298	1 ⊢ (𝜑 → ((((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((𝐶 · 𝑋) + 𝐷)) = 0 ↔ ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∧ wa 384 = wceq 1483 ∈ wcel 1990 ≠ wne 2794 ∃wrex 2913 class class class wbr 4653 (class class class)co 6650 ℂcc 9934 0cc0 9936 1c1 9937 + caddc 9939 · cmul 9941 − cmin 10266 -cneg 10267 / cdiv 10684 ℕcn 11020 2c2 11070 3c3 11071 4c4 11072 7c7 11075 9c9 11077 ℕ₀cn0 11292 cdc 11493 ↑cexp 12860 ∥ cdvds 14983

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-er 7742 df-en 7956 df-dom 7957 df-sdom 7958 df-sup 8348 df-inf 8349 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-4 11081 df-5 11082 df-6 11083 df-7 11084 df-8 11085 df-9 11086 df-n0 11293 df-z 11378 df-dec 11494 df-uz 11688 df-rp 11833 df-fz 12327 df-seq 12802 df-exp 12861 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-dvds 14984

This theorem is referenced by: cubic2 24575 quart 24588

W3C validator