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 25427

Description: Solutions to a monic cubic equation, a special case of cubic 25429. (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 13511	. . . . . . 7 ⊢ (𝜑 → (𝐵↑2) ∈ ℂ)
4		3cn 11721	. . . . . . . 8 ⊢ 3 ∈ ℂ
5		mcubic.c	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ ℂ)
6		mulcl 10623	. . . . . . . 8 ⊢ ((3 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (3 · 𝐶) ∈ ℂ)
7	4, 5, 6	sylancr 589	. . . . . . 7 ⊢ (𝜑 → (3 · 𝐶) ∈ ℂ)
8	3, 7	subcld 10999	. . . . . 6 ⊢ (𝜑 → ((𝐵↑2) − (3 · 𝐶)) ∈ ℂ)
9	1, 8	eqeltrd 2915	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ ℂ)
10	4	a1i 11	. . . . 5 ⊢ (𝜑 → 3 ∈ ℂ)
11		3ne0 11746	. . . . . 6 ⊢ 3 ≠ 0
12	11	a1i 11	. . . . 5 ⊢ (𝜑 → 3 ≠ 0)
13	9, 10, 12	divcld 11418	. . . 4 ⊢ (𝜑 → (𝑀 / 3) ∈ ℂ)
14	13	negcld 10986	. . 3 ⊢ (𝜑 → -(𝑀 / 3) ∈ ℂ)
15		mcubic.n	. . . . 5 ⊢ (𝜑 → 𝑁 = (((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) + (;27 · 𝐷)))
16		2cn 11715	. . . . . . . 8 ⊢ 2 ∈ ℂ
17		3nn0 11918	. . . . . . . . 9 ⊢ 3 ∈ ℕ₀
18		expcl 13450	. . . . . . . . 9 ⊢ ((𝐵 ∈ ℂ ∧ 3 ∈ ℕ₀) → (𝐵↑3) ∈ ℂ)
19	2, 17, 18	sylancl 588	. . . . . . . 8 ⊢ (𝜑 → (𝐵↑3) ∈ ℂ)
20		mulcl 10623	. . . . . . . 8 ⊢ ((2 ∈ ℂ ∧ (𝐵↑3) ∈ ℂ) → (2 · (𝐵↑3)) ∈ ℂ)
21	16, 19, 20	sylancr 589	. . . . . . 7 ⊢ (𝜑 → (2 · (𝐵↑3)) ∈ ℂ)
22		9cn 11740	. . . . . . . 8 ⊢ 9 ∈ ℂ
23	2, 5	mulcld 10663	. . . . . . . 8 ⊢ (𝜑 → (𝐵 · 𝐶) ∈ ℂ)
24		mulcl 10623	. . . . . . . 8 ⊢ ((9 ∈ ℂ ∧ (𝐵 · 𝐶) ∈ ℂ) → (9 · (𝐵 · 𝐶)) ∈ ℂ)
25	22, 23, 24	sylancr 589	. . . . . . 7 ⊢ (𝜑 → (9 · (𝐵 · 𝐶)) ∈ ℂ)
26	21, 25	subcld 10999	. . . . . 6 ⊢ (𝜑 → ((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) ∈ ℂ)
27		2nn0 11917	. . . . . . . . 9 ⊢ 2 ∈ ℕ₀
28		7nn 11732	. . . . . . . . 9 ⊢ 7 ∈ ℕ
29	27, 28	decnncl 12121	. . . . . . . 8 ⊢ ;27 ∈ ℕ
30	29	nncni 11650	. . . . . . 7 ⊢ ;27 ∈ ℂ
31		mcubic.d	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ ℂ)
32		mulcl 10623	. . . . . . 7 ⊢ ((;27 ∈ ℂ ∧ 𝐷 ∈ ℂ) → (;27 · 𝐷) ∈ ℂ)
33	30, 31, 32	sylancr 589	. . . . . 6 ⊢ (𝜑 → (;27 · 𝐷) ∈ ℂ)
34	26, 33	addcld 10662	. . . . 5 ⊢ (𝜑 → (((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) + (;27 · 𝐷)) ∈ ℂ)
35	15, 34	eqeltrd 2915	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ℂ)
36	30	a1i 11	. . . 4 ⊢ (𝜑 → ;27 ∈ ℂ)
37	29	nnne0i 11680	. . . . 5 ⊢ ;27 ≠ 0
38	37	a1i 11	. . . 4 ⊢ (𝜑 → ;27 ≠ 0)
39	35, 36, 38	divcld 11418	. . 3 ⊢ (𝜑 → (𝑁 / ;27) ∈ ℂ)
40		mcubic.x	. . . 4 ⊢ (𝜑 → 𝑋 ∈ ℂ)
41	2, 10, 12	divcld 11418	. . . 4 ⊢ (𝜑 → (𝐵 / 3) ∈ ℂ)
42	40, 41	addcld 10662	. . 3 ⊢ (𝜑 → (𝑋 + (𝐵 / 3)) ∈ ℂ)
43		mcubic.t	. . . . 5 ⊢ (𝜑 → 𝑇 ∈ ℂ)
44	43, 10, 12	divcld 11418	. . . 4 ⊢ (𝜑 → (𝑇 / 3) ∈ ℂ)
45	44	negcld 10986	. . 3 ⊢ (𝜑 → -(𝑇 / 3) ∈ ℂ)
46		3nn 11719	. . . . . 6 ⊢ 3 ∈ ℕ
47	46	a1i 11	. . . . 5 ⊢ (𝜑 → 3 ∈ ℕ)
48		n2dvds3 15723	. . . . . 6 ⊢ ¬ 2 ∥ 3
49	48	a1i 11	. . . . 5 ⊢ (𝜑 → ¬ 2 ∥ 3)
50		oexpneg 15696	. . . . 5 ⊢ (((𝑇 / 3) ∈ ℂ ∧ 3 ∈ ℕ ∧ ¬ 2 ∥ 3) → (-(𝑇 / 3)↑3) = -((𝑇 / 3)↑3))
51	44, 47, 49, 50	syl3anc 1367	. . . 4 ⊢ (𝜑 → (-(𝑇 / 3)↑3) = -((𝑇 / 3)↑3))
52	17	a1i 11	. . . . . . 7 ⊢ (𝜑 → 3 ∈ ℕ₀)
53	43, 10, 12, 52	expdivd 13527	. . . . . 6 ⊢ (𝜑 → ((𝑇 / 3)↑3) = ((𝑇↑3) / (3↑3)))
54		mcubic.3	. . . . . . 7 ⊢ (𝜑 → (𝑇↑3) = ((𝑁 + 𝐺) / 2))
55		3exp3 16427	. . . . . . . 8 ⊢ (3↑3) = ;27
56	55	a1i 11	. . . . . . 7 ⊢ (𝜑 → (3↑3) = ;27)
57	54, 56	oveq12d 7176	. . . . . 6 ⊢ (𝜑 → ((𝑇↑3) / (3↑3)) = (((𝑁 + 𝐺) / 2) / ;27))
58		mcubic.g	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 ∈ ℂ)
59	35, 58	addcld 10662	. . . . . . . 8 ⊢ (𝜑 → (𝑁 + 𝐺) ∈ ℂ)
60		2cnd 11718	. . . . . . . 8 ⊢ (𝜑 → 2 ∈ ℂ)
61		2ne0 11744	. . . . . . . . 9 ⊢ 2 ≠ 0
62	61	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 2 ≠ 0)
63	59, 60, 36, 62, 38	divdiv32d 11443	. . . . . . 7 ⊢ (𝜑 → (((𝑁 + 𝐺) / 2) / ;27) = (((𝑁 + 𝐺) / ;27) / 2))
64	35, 58	addcomd 10844	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 + 𝐺) = (𝐺 + 𝑁))
65	64	oveq1d 7173	. . . . . . . . 9 ⊢ (𝜑 → ((𝑁 + 𝐺) / ;27) = ((𝐺 + 𝑁) / ;27))
66	58, 35, 36, 38	divdird 11456	. . . . . . . . 9 ⊢ (𝜑 → ((𝐺 + 𝑁) / ;27) = ((𝐺 / ;27) + (𝑁 / ;27)))
67	65, 66	eqtrd 2858	. . . . . . . 8 ⊢ (𝜑 → ((𝑁 + 𝐺) / ;27) = ((𝐺 / ;27) + (𝑁 / ;27)))
68	67	oveq1d 7173	. . . . . . 7 ⊢ (𝜑 → (((𝑁 + 𝐺) / ;27) / 2) = (((𝐺 / ;27) + (𝑁 / ;27)) / 2))
69	58, 36, 38	divcld 11418	. . . . . . . 8 ⊢ (𝜑 → (𝐺 / ;27) ∈ ℂ)
70	69, 39, 60, 62	divdird 11456	. . . . . . 7 ⊢ (𝜑 → (((𝐺 / ;27) + (𝑁 / ;27)) / 2) = (((𝐺 / ;27) / 2) + ((𝑁 / ;27) / 2)))
71	63, 68, 70	3eqtrd 2862	. . . . . 6 ⊢ (𝜑 → (((𝑁 + 𝐺) / 2) / ;27) = (((𝐺 / ;27) / 2) + ((𝑁 / ;27) / 2)))
72	53, 57, 71	3eqtrd 2862	. . . . 5 ⊢ (𝜑 → ((𝑇 / 3)↑3) = (((𝐺 / ;27) / 2) + ((𝑁 / ;27) / 2)))
73	72	negeqd 10882	. . . 4 ⊢ (𝜑 → -((𝑇 / 3)↑3) = -(((𝐺 / ;27) / 2) + ((𝑁 / ;27) / 2)))
74	69	halfcld 11885	. . . . 5 ⊢ (𝜑 → ((𝐺 / ;27) / 2) ∈ ℂ)
75	39	halfcld 11885	. . . . 5 ⊢ (𝜑 → ((𝑁 / ;27) / 2) ∈ ℂ)
76	74, 75	negdi2d 11013	. . . 4 ⊢ (𝜑 → -(((𝐺 / ;27) / 2) + ((𝑁 / ;27) / 2)) = (-((𝐺 / ;27) / 2) − ((𝑁 / ;27) / 2)))
77	51, 73, 76	3eqtrd 2862	. . 3 ⊢ (𝜑 → (-(𝑇 / 3)↑3) = (-((𝐺 / ;27) / 2) − ((𝑁 / ;27) / 2)))
78	74	negcld 10986	. . 3 ⊢ (𝜑 → -((𝐺 / ;27) / 2) ∈ ℂ)
79		sqneg 13485	. . . . 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 13526	. . . 4 ⊢ (𝜑 → (((𝐺 / ;27) / 2)↑2) = (((𝐺 / ;27)↑2) / (2↑2)))
82	39, 60, 62	sqdivd 13526	. . . . . . . 8 ⊢ (𝜑 → (((𝑁 / ;27) / 2)↑2) = (((𝑁 / ;27)↑2) / (2↑2)))
83	35, 36, 38	sqdivd 13526	. . . . . . . . 9 ⊢ (𝜑 → ((𝑁 / ;27)↑2) = ((𝑁↑2) / (;27↑2)))
84	83	oveq1d 7173	. . . . . . . 8 ⊢ (𝜑 → (((𝑁 / ;27)↑2) / (2↑2)) = (((𝑁↑2) / (;27↑2)) / (2↑2)))
85	82, 84	eqtr2d 2859	. . . . . . 7 ⊢ (𝜑 → (((𝑁↑2) / (;27↑2)) / (2↑2)) = (((𝑁 / ;27) / 2)↑2))
86		4cn 11725	. . . . . . . . . . . 12 ⊢ 4 ∈ ℂ
87	86	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 4 ∈ ℂ)
88		expcl 13450	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℂ ∧ 3 ∈ ℕ₀) → (𝑀↑3) ∈ ℂ)
89	9, 17, 88	sylancl 588	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀↑3) ∈ ℂ)
90	30	sqcli 13547	. . . . . . . . . . . 12 ⊢ (;27↑2) ∈ ℂ
91	90	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (;27↑2) ∈ ℂ)
92		sqne0 13492	. . . . . . . . . . . . 13 ⊢ (;27 ∈ ℂ → ((;27↑2) ≠ 0 ↔ ;27 ≠ 0))
93	36, 92	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → ((;27↑2) ≠ 0 ↔ ;27 ≠ 0))
94	38, 93	mpbird 259	. . . . . . . . . . 11 ⊢ (𝜑 → (;27↑2) ≠ 0)
95	87, 89, 91, 94	divassd 11453	. . . . . . . . . 10 ⊢ (𝜑 → ((4 · (𝑀↑3)) / (;27↑2)) = (4 · ((𝑀↑3) / (;27↑2))))
96	22	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 9 ∈ ℂ)
97		9nn 11738	. . . . . . . . . . . . . . 15 ⊢ 9 ∈ ℕ
98	97	nnne0i 11680	. . . . . . . . . . . . . 14 ⊢ 9 ≠ 0
99	98	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 9 ≠ 0)
100	9, 96, 99, 52	expdivd 13527	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑀 / 9)↑3) = ((𝑀↑3) / (9↑3)))
101	16, 4	mulcomi 10651	. . . . . . . . . . . . . . . 16 ⊢ (2 · 3) = (3 · 2)
102	101	oveq2i 7169	. . . . . . . . . . . . . . 15 ⊢ (3↑(2 · 3)) = (3↑(3 · 2))
103		expmul 13477	. . . . . . . . . . . . . . . 16 ⊢ ((3 ∈ ℂ ∧ 2 ∈ ℕ₀ ∧ 3 ∈ ℕ₀) → (3↑(2 · 3)) = ((3↑2)↑3))
104	4, 27, 17, 103	mp3an 1457	. . . . . . . . . . . . . . 15 ⊢ (3↑(2 · 3)) = ((3↑2)↑3)
105		expmul 13477	. . . . . . . . . . . . . . . 16 ⊢ ((3 ∈ ℂ ∧ 3 ∈ ℕ₀ ∧ 2 ∈ ℕ₀) → (3↑(3 · 2)) = ((3↑3)↑2))
106	4, 17, 27, 105	mp3an 1457	. . . . . . . . . . . . . . 15 ⊢ (3↑(3 · 2)) = ((3↑3)↑2)
107	102, 104, 106	3eqtr3i 2854	. . . . . . . . . . . . . 14 ⊢ ((3↑2)↑3) = ((3↑3)↑2)
108		sq3 13564	. . . . . . . . . . . . . . 15 ⊢ (3↑2) = 9
109	108	oveq1i 7168	. . . . . . . . . . . . . 14 ⊢ ((3↑2)↑3) = (9↑3)
110	55	oveq1i 7168	. . . . . . . . . . . . . 14 ⊢ ((3↑3)↑2) = (;27↑2)
111	107, 109, 110	3eqtr3i 2854	. . . . . . . . . . . . 13 ⊢ (9↑3) = (;27↑2)
112	111	oveq2i 7169	. . . . . . . . . . . 12 ⊢ ((𝑀↑3) / (9↑3)) = ((𝑀↑3) / (;27↑2))
113	100, 112	syl6eq 2874	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑀 / 9)↑3) = ((𝑀↑3) / (;27↑2)))
114	113	oveq2d 7174	. . . . . . . . . 10 ⊢ (𝜑 → (4 · ((𝑀 / 9)↑3)) = (4 · ((𝑀↑3) / (;27↑2))))
115	95, 114	eqtr4d 2861	. . . . . . . . 9 ⊢ (𝜑 → ((4 · (𝑀↑3)) / (;27↑2)) = (4 · ((𝑀 / 9)↑3)))
116	115	oveq1d 7173	. . . . . . . 8 ⊢ (𝜑 → (((4 · (𝑀↑3)) / (;27↑2)) / (2↑2)) = ((4 · ((𝑀 / 9)↑3)) / (2↑2)))
117		sq2 13563	. . . . . . . . . 10 ⊢ (2↑2) = 4
118	117	oveq2i 7169	. . . . . . . . 9 ⊢ ((4 · ((𝑀 / 9)↑3)) / (2↑2)) = ((4 · ((𝑀 / 9)↑3)) / 4)
119	9, 96, 99	divcld 11418	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀 / 9) ∈ ℂ)
120		expcl 13450	. . . . . . . . . . 11 ⊢ (((𝑀 / 9) ∈ ℂ ∧ 3 ∈ ℕ₀) → ((𝑀 / 9)↑3) ∈ ℂ)
121	119, 17, 120	sylancl 588	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑀 / 9)↑3) ∈ ℂ)
122		4ne0 11748	. . . . . . . . . . 11 ⊢ 4 ≠ 0
123	122	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 4 ≠ 0)
124	121, 87, 123	divcan3d 11423	. . . . . . . . 9 ⊢ (𝜑 → ((4 · ((𝑀 / 9)↑3)) / 4) = ((𝑀 / 9)↑3))
125	118, 124	syl5eq 2870	. . . . . . . 8 ⊢ (𝜑 → ((4 · ((𝑀 / 9)↑3)) / (2↑2)) = ((𝑀 / 9)↑3))
126	116, 125	eqtrd 2858	. . . . . . 7 ⊢ (𝜑 → (((4 · (𝑀↑3)) / (;27↑2)) / (2↑2)) = ((𝑀 / 9)↑3))
127	85, 126	oveq12d 7176	. . . . . 6 ⊢ (𝜑 → ((((𝑁↑2) / (;27↑2)) / (2↑2)) − (((4 · (𝑀↑3)) / (;27↑2)) / (2↑2))) = ((((𝑁 / ;27) / 2)↑2) − ((𝑀 / 9)↑3)))
128	35	sqcld 13511	. . . . . . . 8 ⊢ (𝜑 → (𝑁↑2) ∈ ℂ)
129	128, 91, 94	divcld 11418	. . . . . . 7 ⊢ (𝜑 → ((𝑁↑2) / (;27↑2)) ∈ ℂ)
130		mulcl 10623	. . . . . . . . 9 ⊢ ((4 ∈ ℂ ∧ (𝑀↑3) ∈ ℂ) → (4 · (𝑀↑3)) ∈ ℂ)
131	86, 89, 130	sylancr 589	. . . . . . . 8 ⊢ (𝜑 → (4 · (𝑀↑3)) ∈ ℂ)
132	131, 91, 94	divcld 11418	. . . . . . 7 ⊢ (𝜑 → ((4 · (𝑀↑3)) / (;27↑2)) ∈ ℂ)
133	16	sqcli 13547	. . . . . . . 8 ⊢ (2↑2) ∈ ℂ
134	133	a1i 11	. . . . . . 7 ⊢ (𝜑 → (2↑2) ∈ ℂ)
135	117, 122	eqnetri 3088	. . . . . . . 8 ⊢ (2↑2) ≠ 0
136	135	a1i 11	. . . . . . 7 ⊢ (𝜑 → (2↑2) ≠ 0)
137	129, 132, 134, 136	divsubdird 11457	. . . . . 6 ⊢ (𝜑 → ((((𝑁↑2) / (;27↑2)) − ((4 · (𝑀↑3)) / (;27↑2))) / (2↑2)) = ((((𝑁↑2) / (;27↑2)) / (2↑2)) − (((4 · (𝑀↑3)) / (;27↑2)) / (2↑2))))
138	75	sqcld 13511	. . . . . . 7 ⊢ (𝜑 → (((𝑁 / ;27) / 2)↑2) ∈ ℂ)
139	138, 121	negsubd 11005	. . . . . 6 ⊢ (𝜑 → ((((𝑁 / ;27) / 2)↑2) + -((𝑀 / 9)↑3)) = ((((𝑁 / ;27) / 2)↑2) − ((𝑀 / 9)↑3)))
140	127, 137, 139	3eqtr4d 2868	. . . . 5 ⊢ (𝜑 → ((((𝑁↑2) / (;27↑2)) − ((4 · (𝑀↑3)) / (;27↑2))) / (2↑2)) = ((((𝑁 / ;27) / 2)↑2) + -((𝑀 / 9)↑3)))
141	58, 36, 38	sqdivd 13526	. . . . . . 7 ⊢ (𝜑 → ((𝐺 / ;27)↑2) = ((𝐺↑2) / (;27↑2)))
142		mcubic.2	. . . . . . . 8 ⊢ (𝜑 → (𝐺↑2) = ((𝑁↑2) − (4 · (𝑀↑3))))
143	142	oveq1d 7173	. . . . . . 7 ⊢ (𝜑 → ((𝐺↑2) / (;27↑2)) = (((𝑁↑2) − (4 · (𝑀↑3))) / (;27↑2)))
144	128, 131, 91, 94	divsubdird 11457	. . . . . . 7 ⊢ (𝜑 → (((𝑁↑2) − (4 · (𝑀↑3))) / (;27↑2)) = (((𝑁↑2) / (;27↑2)) − ((4 · (𝑀↑3)) / (;27↑2))))
145	141, 143, 144	3eqtrd 2862	. . . . . 6 ⊢ (𝜑 → ((𝐺 / ;27)↑2) = (((𝑁↑2) / (;27↑2)) − ((4 · (𝑀↑3)) / (;27↑2))))
146	145	oveq1d 7173	. . . . 5 ⊢ (𝜑 → (((𝐺 / ;27)↑2) / (2↑2)) = ((((𝑁↑2) / (;27↑2)) − ((4 · (𝑀↑3)) / (;27↑2))) / (2↑2)))
147		oexpneg 15696	. . . . . . 7 ⊢ (((𝑀 / 9) ∈ ℂ ∧ 3 ∈ ℕ ∧ ¬ 2 ∥ 3) → (-(𝑀 / 9)↑3) = -((𝑀 / 9)↑3))
148	119, 47, 49, 147	syl3anc 1367	. . . . . 6 ⊢ (𝜑 → (-(𝑀 / 9)↑3) = -((𝑀 / 9)↑3))
149	148	oveq2d 7174	. . . . 5 ⊢ (𝜑 → ((((𝑁 / ;27) / 2)↑2) + (-(𝑀 / 9)↑3)) = ((((𝑁 / ;27) / 2)↑2) + -((𝑀 / 9)↑3)))
150	140, 146, 149	3eqtr4d 2868	. . . 4 ⊢ (𝜑 → (((𝐺 / ;27)↑2) / (2↑2)) = ((((𝑁 / ;27) / 2)↑2) + (-(𝑀 / 9)↑3)))
151	80, 81, 150	3eqtrd 2862	. . 3 ⊢ (𝜑 → (-((𝐺 / ;27) / 2)↑2) = ((((𝑁 / ;27) / 2)↑2) + (-(𝑀 / 9)↑3)))
152	9, 10, 10, 12, 12	divdiv1d 11449	. . . . . 6 ⊢ (𝜑 → ((𝑀 / 3) / 3) = (𝑀 / (3 · 3)))
153		3t3e9 11807	. . . . . . 7 ⊢ (3 · 3) = 9
154	153	oveq2i 7169	. . . . . 6 ⊢ (𝑀 / (3 · 3)) = (𝑀 / 9)
155	152, 154	syl6eq 2874	. . . . 5 ⊢ (𝜑 → ((𝑀 / 3) / 3) = (𝑀 / 9))
156	155	negeqd 10882	. . . 4 ⊢ (𝜑 → -((𝑀 / 3) / 3) = -(𝑀 / 9))
157	13, 10, 12	divnegd 11431	. . . 4 ⊢ (𝜑 → -((𝑀 / 3) / 3) = (-(𝑀 / 3) / 3))
158	156, 157	eqtr3d 2860	. . 3 ⊢ (𝜑 → -(𝑀 / 9) = (-(𝑀 / 3) / 3))
159		eqidd 2824	. . 3 ⊢ (𝜑 → ((𝑁 / ;27) / 2) = ((𝑁 / ;27) / 2))
160		mcubic.0	. . . . 5 ⊢ (𝜑 → 𝑇 ≠ 0)
161	43, 10, 160, 12	divne0d 11434	. . . 4 ⊢ (𝜑 → (𝑇 / 3) ≠ 0)
162	44, 161	negne0d 10997	. . 3 ⊢ (𝜑 → -(𝑇 / 3) ≠ 0)
163	14, 39, 42, 45, 77, 78, 151, 158, 159, 162	dcubic 25426	. 2 ⊢ (𝜑 → ((((𝑋 + (𝐵 / 3))↑3) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27))) = 0 ↔ ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ (𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))))))
164		binom3 13588	. . . . . . 7 ⊢ ((𝑋 ∈ ℂ ∧ (𝐵 / 3) ∈ ℂ) → ((𝑋 + (𝐵 / 3))↑3) = (((𝑋↑3) + (3 · ((𝑋↑2) · (𝐵 / 3)))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))))
165	40, 41, 164	syl2anc 586	. . . . . 6 ⊢ (𝜑 → ((𝑋 + (𝐵 / 3))↑3) = (((𝑋↑3) + (3 · ((𝑋↑2) · (𝐵 / 3)))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))))
166	40	sqcld 13511	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋↑2) ∈ ℂ)
167	10, 166, 41	mul12d 10851	. . . . . . . . 9 ⊢ (𝜑 → (3 · ((𝑋↑2) · (𝐵 / 3))) = ((𝑋↑2) · (3 · (𝐵 / 3))))
168	2, 10, 12	divcan2d 11420	. . . . . . . . . 10 ⊢ (𝜑 → (3 · (𝐵 / 3)) = 𝐵)
169	168	oveq2d 7174	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋↑2) · (3 · (𝐵 / 3))) = ((𝑋↑2) · 𝐵))
170	166, 2	mulcomd 10664	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋↑2) · 𝐵) = (𝐵 · (𝑋↑2)))
171	167, 169, 170	3eqtrd 2862	. . . . . . . 8 ⊢ (𝜑 → (3 · ((𝑋↑2) · (𝐵 / 3))) = (𝐵 · (𝑋↑2)))
172	171	oveq2d 7174	. . . . . . 7 ⊢ (𝜑 → ((𝑋↑3) + (3 · ((𝑋↑2) · (𝐵 / 3)))) = ((𝑋↑3) + (𝐵 · (𝑋↑2))))
173	172	oveq1d 7173	. . . . . 6 ⊢ (𝜑 → (((𝑋↑3) + (3 · ((𝑋↑2) · (𝐵 / 3)))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))) = (((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))))
174	165, 173	eqtrd 2858	. . . . 5 ⊢ (𝜑 → ((𝑋 + (𝐵 / 3))↑3) = (((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))))
175	174	oveq1d 7173	. . . 4 ⊢ (𝜑 → (((𝑋 + (𝐵 / 3))↑3) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27))) = ((((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27))))
176		expcl 13450	. . . . . . 7 ⊢ ((𝑋 ∈ ℂ ∧ 3 ∈ ℕ₀) → (𝑋↑3) ∈ ℂ)
177	40, 17, 176	sylancl 588	. . . . . 6 ⊢ (𝜑 → (𝑋↑3) ∈ ℂ)
178	2, 166	mulcld 10663	. . . . . 6 ⊢ (𝜑 → (𝐵 · (𝑋↑2)) ∈ ℂ)
179	177, 178	addcld 10662	. . . . 5 ⊢ (𝜑 → ((𝑋↑3) + (𝐵 · (𝑋↑2))) ∈ ℂ)
180	41	sqcld 13511	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 / 3)↑2) ∈ ℂ)
181	40, 180	mulcld 10663	. . . . . . 7 ⊢ (𝜑 → (𝑋 · ((𝐵 / 3)↑2)) ∈ ℂ)
182	10, 181	mulcld 10663	. . . . . 6 ⊢ (𝜑 → (3 · (𝑋 · ((𝐵 / 3)↑2))) ∈ ℂ)
183		expcl 13450	. . . . . . 7 ⊢ (((𝐵 / 3) ∈ ℂ ∧ 3 ∈ ℕ₀) → ((𝐵 / 3)↑3) ∈ ℂ)
184	41, 17, 183	sylancl 588	. . . . . 6 ⊢ (𝜑 → ((𝐵 / 3)↑3) ∈ ℂ)
185	182, 184	addcld 10662	. . . . 5 ⊢ (𝜑 → ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) ∈ ℂ)
186	14, 42	mulcld 10663	. . . . . 6 ⊢ (𝜑 → (-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) ∈ ℂ)
187	186, 39	addcld 10662	. . . . 5 ⊢ (𝜑 → ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27)) ∈ ℂ)
188	179, 185, 187	addassd 10665	. . . 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 10667	. . . . . . . . . 10 ⊢ (𝜑 → (-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) = ((-(𝑀 / 3) · 𝑋) + (-(𝑀 / 3) · (𝐵 / 3))))
190	189	oveq1d 7173	. . . . . . . . 9 ⊢ (𝜑 → ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27)) = (((-(𝑀 / 3) · 𝑋) + (-(𝑀 / 3) · (𝐵 / 3))) + (𝑁 / ;27)))
191	14, 40	mulcld 10663	. . . . . . . . . 10 ⊢ (𝜑 → (-(𝑀 / 3) · 𝑋) ∈ ℂ)
192	14, 41	mulcld 10663	. . . . . . . . . 10 ⊢ (𝜑 → (-(𝑀 / 3) · (𝐵 / 3)) ∈ ℂ)
193	191, 192, 39	addassd 10665	. . . . . . . . 9 ⊢ (𝜑 → (((-(𝑀 / 3) · 𝑋) + (-(𝑀 / 3) · (𝐵 / 3))) + (𝑁 / ;27)) = ((-(𝑀 / 3) · 𝑋) + ((-(𝑀 / 3) · (𝐵 / 3)) + (𝑁 / ;27))))
194	1	oveq1d 7173	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀 / 3) = (((𝐵↑2) − (3 · 𝐶)) / 3))
195	3, 7, 10, 12	divsubdird 11457	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐵↑2) − (3 · 𝐶)) / 3) = (((𝐵↑2) / 3) − ((3 · 𝐶) / 3)))
196	5, 10, 12	divcan3d 11423	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((3 · 𝐶) / 3) = 𝐶)
197	196	oveq2d 7174	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐵↑2) / 3) − ((3 · 𝐶) / 3)) = (((𝐵↑2) / 3) − 𝐶))
198	194, 195, 197	3eqtrd 2862	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀 / 3) = (((𝐵↑2) / 3) − 𝐶))
199	198	negeqd 10882	. . . . . . . . . . . . 13 ⊢ (𝜑 → -(𝑀 / 3) = -(((𝐵↑2) / 3) − 𝐶))
200	3, 10, 12	divcld 11418	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵↑2) / 3) ∈ ℂ)
201	200, 5	negsubdi2d 11015	. . . . . . . . . . . . 13 ⊢ (𝜑 → -(((𝐵↑2) / 3) − 𝐶) = (𝐶 − ((𝐵↑2) / 3)))
202	199, 201	eqtrd 2858	. . . . . . . . . . . 12 ⊢ (𝜑 → -(𝑀 / 3) = (𝐶 − ((𝐵↑2) / 3)))
203	202	oveq1d 7173	. . . . . . . . . . 11 ⊢ (𝜑 → (-(𝑀 / 3) · 𝑋) = ((𝐶 − ((𝐵↑2) / 3)) · 𝑋))
204	5, 200, 40	subdird 11099	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐶 − ((𝐵↑2) / 3)) · 𝑋) = ((𝐶 · 𝑋) − (((𝐵↑2) / 3) · 𝑋)))
205	200, 40	mulcomd 10664	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐵↑2) / 3) · 𝑋) = (𝑋 · ((𝐵↑2) / 3)))
206	4	sqvali 13546	. . . . . . . . . . . . . . . . . 18 ⊢ (3↑2) = (3 · 3)
207	206	oveq2i 7169	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵↑2) / (3↑2)) = ((𝐵↑2) / (3 · 3))
208	2, 10, 12	sqdivd 13526	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐵 / 3)↑2) = ((𝐵↑2) / (3↑2)))
209	3, 10, 10, 12, 12	divdiv1d 11449	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝐵↑2) / 3) / 3) = ((𝐵↑2) / (3 · 3)))
210	207, 208, 209	3eqtr4a 2884	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐵 / 3)↑2) = (((𝐵↑2) / 3) / 3))
211	210	oveq2d 7174	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (3 · ((𝐵 / 3)↑2)) = (3 · (((𝐵↑2) / 3) / 3)))
212	200, 10, 12	divcan2d 11420	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (3 · (((𝐵↑2) / 3) / 3)) = ((𝐵↑2) / 3))
213	211, 212	eqtrd 2858	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (3 · ((𝐵 / 3)↑2)) = ((𝐵↑2) / 3))
214	213	oveq2d 7174	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 · (3 · ((𝐵 / 3)↑2))) = (𝑋 · ((𝐵↑2) / 3)))
215	40, 10, 180	mul12d 10851	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 · (3 · ((𝐵 / 3)↑2))) = (3 · (𝑋 · ((𝐵 / 3)↑2))))
216	205, 214, 215	3eqtr2d 2864	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐵↑2) / 3) · 𝑋) = (3 · (𝑋 · ((𝐵 / 3)↑2))))
217	216	oveq2d 7174	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐶 · 𝑋) − (((𝐵↑2) / 3) · 𝑋)) = ((𝐶 · 𝑋) − (3 · (𝑋 · ((𝐵 / 3)↑2)))))
218	203, 204, 217	3eqtrd 2862	. . . . . . . . . 10 ⊢ (𝜑 → (-(𝑀 / 3) · 𝑋) = ((𝐶 · 𝑋) − (3 · (𝑋 · ((𝐵 / 3)↑2)))))
219	202	oveq1d 7173	. . . . . . . . . . . . 13 ⊢ (𝜑 → (-(𝑀 / 3) · (𝐵 / 3)) = ((𝐶 − ((𝐵↑2) / 3)) · (𝐵 / 3)))
220	5, 200, 41	subdird 11099	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐶 − ((𝐵↑2) / 3)) · (𝐵 / 3)) = ((𝐶 · (𝐵 / 3)) − (((𝐵↑2) / 3) · (𝐵 / 3))))
221	5, 2, 10, 12	divassd 11453	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐶 · 𝐵) / 3) = (𝐶 · (𝐵 / 3)))
222	5, 2	mulcomd 10664	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐶 · 𝐵) = (𝐵 · 𝐶))
223	222	oveq1d 7173	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐶 · 𝐵) / 3) = ((𝐵 · 𝐶) / 3))
224	221, 223	eqtr3d 2860	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐶 · (𝐵 / 3)) = ((𝐵 · 𝐶) / 3))
225	3, 10, 2, 10, 12, 12	divmuldivd 11459	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐵↑2) / 3) · (𝐵 / 3)) = (((𝐵↑2) · 𝐵) / (3 · 3)))
226		df-3 11704	. . . . . . . . . . . . . . . . . 18 ⊢ 3 = (2 + 1)
227	226	oveq2i 7169	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵↑3) = (𝐵↑(2 + 1))
228		expp1 13439	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ∈ ℂ ∧ 2 ∈ ℕ₀) → (𝐵↑(2 + 1)) = ((𝐵↑2) · 𝐵))
229	2, 27, 228	sylancl 588	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵↑(2 + 1)) = ((𝐵↑2) · 𝐵))
230	227, 229	syl5req 2871	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐵↑2) · 𝐵) = (𝐵↑3))
231	153	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (3 · 3) = 9)
232	230, 231	oveq12d 7176	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐵↑2) · 𝐵) / (3 · 3)) = ((𝐵↑3) / 9))
233	225, 232	eqtrd 2858	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐵↑2) / 3) · (𝐵 / 3)) = ((𝐵↑3) / 9))
234	224, 233	oveq12d 7176	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐶 · (𝐵 / 3)) − (((𝐵↑2) / 3) · (𝐵 / 3))) = (((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)))
235	219, 220, 234	3eqtrd 2862	. . . . . . . . . . . 12 ⊢ (𝜑 → (-(𝑀 / 3) · (𝐵 / 3)) = (((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)))
236	15	oveq1d 7173	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 / ;27) = ((((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) + (;27 · 𝐷)) / ;27))
237	26, 33, 36, 38	divdird 11456	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) + (;27 · 𝐷)) / ;27) = ((((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) / ;27) + ((;27 · 𝐷) / ;27)))
238	21, 25, 36, 38	divsubdird 11457	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) / ;27) = (((2 · (𝐵↑3)) / ;27) − ((9 · (𝐵 · 𝐶)) / ;27)))
239		9t3e27 12224	. . . . . . . . . . . . . . . . . 18 ⊢ (9 · 3) = ;27
240	239	oveq2i 7169	. . . . . . . . . . . . . . . . 17 ⊢ ((9 · (𝐵 · 𝐶)) / (9 · 3)) = ((9 · (𝐵 · 𝐶)) / ;27)
241	23, 10, 96, 12, 99	divcan5d 11444	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((9 · (𝐵 · 𝐶)) / (9 · 3)) = ((𝐵 · 𝐶) / 3))
242	240, 241	syl5eqr 2872	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((9 · (𝐵 · 𝐶)) / ;27) = ((𝐵 · 𝐶) / 3))
243	242	oveq2d 7174	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((2 · (𝐵↑3)) / ;27) − ((9 · (𝐵 · 𝐶)) / ;27)) = (((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3)))
244	238, 243	eqtrd 2858	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) / ;27) = (((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3)))
245	31, 36, 38	divcan3d 11423	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((;27 · 𝐷) / ;27) = 𝐷)
246	244, 245	oveq12d 7176	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) / ;27) + ((;27 · 𝐷) / ;27)) = ((((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3)) + 𝐷))
247	236, 237, 246	3eqtrd 2862	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁 / ;27) = ((((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3)) + 𝐷))
248	235, 247	oveq12d 7176	. . . . . . . . . . 11 ⊢ (𝜑 → ((-(𝑀 / 3) · (𝐵 / 3)) + (𝑁 / ;27)) = ((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + ((((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3)) + 𝐷)))
249	19, 96, 99	divcld 11418	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐵↑3) / 9) ∈ ℂ)
250	21, 36, 38	divcld 11418	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((2 · (𝐵↑3)) / ;27) ∈ ℂ)
251	249, 250	negsubdi2d 11015	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -(((𝐵↑3) / 9) − ((2 · (𝐵↑3)) / ;27)) = (((2 · (𝐵↑3)) / ;27) − ((𝐵↑3) / 9)))
252	2, 10, 12, 52	expdivd 13527	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐵 / 3)↑3) = ((𝐵↑3) / (3↑3)))
253	55	oveq2i 7169	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵↑3) / (3↑3)) = ((𝐵↑3) / ;27)
254		ax-1cn 10597	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 ∈ ℂ
255		2p1e3 11782	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (2 + 1) = 3
256	4, 16, 254, 255	subaddrii 10977	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (3 − 2) = 1
257	256	oveq1i 7168	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((3 − 2) · (𝐵↑3)) = (1 · (𝐵↑3))
258	19	mulid2d 10661	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (1 · (𝐵↑3)) = (𝐵↑3))
259	257, 258	syl5eq 2870	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((3 − 2) · (𝐵↑3)) = (𝐵↑3))
260	10, 60, 19	subdird 11099	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((3 − 2) · (𝐵↑3)) = ((3 · (𝐵↑3)) − (2 · (𝐵↑3))))
261	259, 260	eqtr3d 2860	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐵↑3) = ((3 · (𝐵↑3)) − (2 · (𝐵↑3))))
262	261	oveq1d 7173	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐵↑3) / ;27) = (((3 · (𝐵↑3)) − (2 · (𝐵↑3))) / ;27))
263		mulcl 10623	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((3 ∈ ℂ ∧ (𝐵↑3) ∈ ℂ) → (3 · (𝐵↑3)) ∈ ℂ)
264	4, 19, 263	sylancr 589	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (3 · (𝐵↑3)) ∈ ℂ)
265	264, 21, 36, 38	divsubdird 11457	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((3 · (𝐵↑3)) − (2 · (𝐵↑3))) / ;27) = (((3 · (𝐵↑3)) / ;27) − ((2 · (𝐵↑3)) / ;27)))
266	262, 265	eqtrd 2858	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐵↑3) / ;27) = (((3 · (𝐵↑3)) / ;27) − ((2 · (𝐵↑3)) / ;27)))
267	253, 266	syl5eq 2870	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐵↑3) / (3↑3)) = (((3 · (𝐵↑3)) / ;27) − ((2 · (𝐵↑3)) / ;27)))
268	22, 4, 239	mulcomli 10652	. . . . . . . . . . . . . . . . . . 19 ⊢ (3 · 9) = ;27
269	268	oveq2i 7169	. . . . . . . . . . . . . . . . . 18 ⊢ ((3 · (𝐵↑3)) / (3 · 9)) = ((3 · (𝐵↑3)) / ;27)
270	19, 96, 10, 99, 12	divcan5d 11444	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((3 · (𝐵↑3)) / (3 · 9)) = ((𝐵↑3) / 9))
271	269, 270	syl5eqr 2872	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((3 · (𝐵↑3)) / ;27) = ((𝐵↑3) / 9))
272	271	oveq1d 7173	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((3 · (𝐵↑3)) / ;27) − ((2 · (𝐵↑3)) / ;27)) = (((𝐵↑3) / 9) − ((2 · (𝐵↑3)) / ;27)))
273	252, 267, 272	3eqtrd 2862	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐵 / 3)↑3) = (((𝐵↑3) / 9) − ((2 · (𝐵↑3)) / ;27)))
274	273	negeqd 10882	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -((𝐵 / 3)↑3) = -(((𝐵↑3) / 9) − ((2 · (𝐵↑3)) / ;27)))
275	23, 10, 12	divcld 11418	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐵 · 𝐶) / 3) ∈ ℂ)
276	275, 249, 250	npncan3d 11035	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + (((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3))) = (((2 · (𝐵↑3)) / ;27) − ((𝐵↑3) / 9)))
277	251, 274, 276	3eqtr4d 2868	. . . . . . . . . . . . 13 ⊢ (𝜑 → -((𝐵 / 3)↑3) = ((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + (((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3))))
278	277	oveq1d 7173	. . . . . . . . . . . 12 ⊢ (𝜑 → (-((𝐵 / 3)↑3) + 𝐷) = (((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + (((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3))) + 𝐷))
279	184	negcld 10986	. . . . . . . . . . . . 13 ⊢ (𝜑 → -((𝐵 / 3)↑3) ∈ ℂ)
280	279, 31	addcomd 10844	. . . . . . . . . . . 12 ⊢ (𝜑 → (-((𝐵 / 3)↑3) + 𝐷) = (𝐷 + -((𝐵 / 3)↑3)))
281	235, 192	eqeltrrd 2916	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) ∈ ℂ)
282	250, 275	subcld 10999	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3)) ∈ ℂ)
283	281, 282, 31	addassd 10665	. . . . . . . . . . . 12 ⊢ (𝜑 → (((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + (((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3))) + 𝐷) = ((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + ((((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3)) + 𝐷)))
284	278, 280, 283	3eqtr3d 2866	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐷 + -((𝐵 / 3)↑3)) = ((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + ((((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3)) + 𝐷)))
285	31, 184	negsubd 11005	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐷 + -((𝐵 / 3)↑3)) = (𝐷 − ((𝐵 / 3)↑3)))
286	248, 284, 285	3eqtr2d 2864	. . . . . . . . . 10 ⊢ (𝜑 → ((-(𝑀 / 3) · (𝐵 / 3)) + (𝑁 / ;27)) = (𝐷 − ((𝐵 / 3)↑3)))
287	218, 286	oveq12d 7176	. . . . . . . . 9 ⊢ (𝜑 → ((-(𝑀 / 3) · 𝑋) + ((-(𝑀 / 3) · (𝐵 / 3)) + (𝑁 / ;27))) = (((𝐶 · 𝑋) − (3 · (𝑋 · ((𝐵 / 3)↑2)))) + (𝐷 − ((𝐵 / 3)↑3))))
288	190, 193, 287	3eqtrd 2862	. . . . . . . 8 ⊢ (𝜑 → ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27)) = (((𝐶 · 𝑋) − (3 · (𝑋 · ((𝐵 / 3)↑2)))) + (𝐷 − ((𝐵 / 3)↑3))))
289	5, 40	mulcld 10663	. . . . . . . . 9 ⊢ (𝜑 → (𝐶 · 𝑋) ∈ ℂ)
290	289, 31, 182, 184	addsub4d 11046	. . . . . . . 8 ⊢ (𝜑 → (((𝐶 · 𝑋) + 𝐷) − ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))) = (((𝐶 · 𝑋) − (3 · (𝑋 · ((𝐵 / 3)↑2)))) + (𝐷 − ((𝐵 / 3)↑3))))
291	288, 290	eqtr4d 2861	. . . . . . 7 ⊢ (𝜑 → ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27)) = (((𝐶 · 𝑋) + 𝐷) − ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))))
292	291	oveq2d 7174	. . . . . 6 ⊢ (𝜑 → (((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27))) = (((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) + (((𝐶 · 𝑋) + 𝐷) − ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)))))
293	289, 31	addcld 10662	. . . . . . 7 ⊢ (𝜑 → ((𝐶 · 𝑋) + 𝐷) ∈ ℂ)
294	185, 293	pncan3d 11002	. . . . . 6 ⊢ (𝜑 → (((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) + (((𝐶 · 𝑋) + 𝐷) − ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)))) = ((𝐶 · 𝑋) + 𝐷))
295	292, 294	eqtrd 2858	. . . . 5 ⊢ (𝜑 → (((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27))) = ((𝐶 · 𝑋) + 𝐷))
296	295	oveq2d 7174	. . . 4 ⊢ (𝜑 → (((𝑋↑3) + (𝐵 · (𝑋↑2))) + (((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27)))) = (((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((𝐶 · 𝑋) + 𝐷)))
297	175, 188, 296	3eqtrd 2862	. . 3 ⊢ (𝜑 → (((𝑋 + (𝐵 / 3))↑3) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27))) = (((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((𝐶 · 𝑋) + 𝐷)))
298	297	eqeq1d 2825	. 2 ⊢ (𝜑 → ((((𝑋 + (𝐵 / 3))↑3) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27))) = 0 ↔ (((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((𝐶 · 𝑋) + 𝐷)) = 0))
299		oveq1 7165	. . . . . . . 8 ⊢ (𝑟 = 0 → (𝑟↑3) = (0↑3))
300		0exp 13467	. . . . . . . . 9 ⊢ (3 ∈ ℕ → (0↑3) = 0)
301	46, 300	ax-mp 5	. . . . . . . 8 ⊢ (0↑3) = 0
302	299, 301	syl6eq 2874	. . . . . . 7 ⊢ (𝑟 = 0 → (𝑟↑3) = 0)
303		0ne1 11711	. . . . . . . 8 ⊢ 0 ≠ 1
304	303	a1i 11	. . . . . . 7 ⊢ (𝑟 = 0 → 0 ≠ 1)
305	302, 304	eqnetrd 3085	. . . . . 6 ⊢ (𝑟 = 0 → (𝑟↑3) ≠ 1)
306	305	necon2i 3052	. . . . 5 ⊢ ((𝑟↑3) = 1 → 𝑟 ≠ 0)
307		eqcom 2830	. . . . . . . 8 ⊢ (𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) ↔ -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = 𝑋)
308	2	adantr 483	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝐵 ∈ ℂ)
309		simprl 769	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑟 ∈ ℂ)
310	43	adantr 483	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑇 ∈ ℂ)
311	309, 310	mulcld 10663	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑟 · 𝑇) ∈ ℂ)
312	9	adantr 483	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑀 ∈ ℂ)
313		simprr 771	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑟 ≠ 0)
314	160	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑇 ≠ 0)
315	309, 310, 313, 314	mulne0d 11294	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑟 · 𝑇) ≠ 0)
316	312, 311, 315	divcld 11418	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑀 / (𝑟 · 𝑇)) ∈ ℂ)
317	311, 316	addcld 10662	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) ∈ ℂ)
318	4	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 3 ∈ ℂ)
319	11	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 3 ≠ 0)
320	308, 317, 318, 319	divdird 11456	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝐵 + ((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇)))) / 3) = ((𝐵 / 3) + (((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)))
321	308, 311, 316	addassd 10665	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) = (𝐵 + ((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇)))))
322	321	oveq1d 7173	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = ((𝐵 + ((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇)))) / 3))
323	41	adantr 483	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝐵 / 3) ∈ ℂ)
324	317, 318, 319	divcld 11418	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) ∈ ℂ)
325	323, 324	subnegd 11006	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝐵 / 3) − -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)) = ((𝐵 / 3) + (((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)))
326	320, 322, 325	3eqtr4d 2868	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = ((𝐵 / 3) − -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)))
327	326	negeqd 10882	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = -((𝐵 / 3) − -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)))
328	324	negcld 10986	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) ∈ ℂ)
329	323, 328	negsubdi2d 11015	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -((𝐵 / 3) − -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)) = (-(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) − (𝐵 / 3)))
330	327, 329	eqtrd 2858	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = (-(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) − (𝐵 / 3)))
331	330	eqeq1d 2825	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (-(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = 𝑋 ↔ (-(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) − (𝐵 / 3)) = 𝑋))
332	307, 331	syl5bb 285	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) ↔ (-(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) − (𝐵 / 3)) = 𝑋))
333	40	adantr 483	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑋 ∈ ℂ)
334	328, 323, 333	subadd2d 11018	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((-(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) − (𝐵 / 3)) = 𝑋 ↔ (𝑋 + (𝐵 / 3)) = -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)))
335	311, 316, 318, 319	divdird 11456	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) = (((𝑟 · 𝑇) / 3) + ((𝑀 / (𝑟 · 𝑇)) / 3)))
336	335	negeqd 10882	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) = -(((𝑟 · 𝑇) / 3) + ((𝑀 / (𝑟 · 𝑇)) / 3)))
337	311, 318, 319	divcld 11418	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑟 · 𝑇) / 3) ∈ ℂ)
338	316, 318, 319	divcld 11418	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑀 / (𝑟 · 𝑇)) / 3) ∈ ℂ)
339	337, 338	negdi2d 11013	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝑟 · 𝑇) / 3) + ((𝑀 / (𝑟 · 𝑇)) / 3)) = (-((𝑟 · 𝑇) / 3) − ((𝑀 / (𝑟 · 𝑇)) / 3)))
340	309, 310, 318, 319	divassd 11453	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑟 · 𝑇) / 3) = (𝑟 · (𝑇 / 3)))
341	340	negeqd 10882	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -((𝑟 · 𝑇) / 3) = -(𝑟 · (𝑇 / 3)))
342	44	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑇 / 3) ∈ ℂ)
343	309, 342	mulneg2d 11096	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑟 · -(𝑇 / 3)) = -(𝑟 · (𝑇 / 3)))
344	341, 343	eqtr4d 2861	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -((𝑟 · 𝑇) / 3) = (𝑟 · -(𝑇 / 3)))
345	312, 311, 318, 315, 319	divdiv32d 11443	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑀 / (𝑟 · 𝑇)) / 3) = ((𝑀 / 3) / (𝑟 · 𝑇)))
346	13	adantr 483	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑀 / 3) ∈ ℂ)
347	346, 311, 318, 315, 319	divcan7d 11446	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝑀 / 3) / 3) / ((𝑟 · 𝑇) / 3)) = ((𝑀 / 3) / (𝑟 · 𝑇)))
348	155	oveq1d 7173	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑀 / 3) / 3) / ((𝑟 · 𝑇) / 3)) = ((𝑀 / 9) / ((𝑟 · 𝑇) / 3)))
349	348	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝑀 / 3) / 3) / ((𝑟 · 𝑇) / 3)) = ((𝑀 / 9) / ((𝑟 · 𝑇) / 3)))
350	345, 347, 349	3eqtr2d 2864	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑀 / (𝑟 · 𝑇)) / 3) = ((𝑀 / 9) / ((𝑟 · 𝑇) / 3)))
351	119	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑀 / 9) ∈ ℂ)
352	311, 318, 315, 319	divne0d 11434	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑟 · 𝑇) / 3) ≠ 0)
353	351, 337, 352	div2negd 11433	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (-(𝑀 / 9) / -((𝑟 · 𝑇) / 3)) = ((𝑀 / 9) / ((𝑟 · 𝑇) / 3)))
354	344	oveq2d 7174	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (-(𝑀 / 9) / -((𝑟 · 𝑇) / 3)) = (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3))))
355	350, 353, 354	3eqtr2d 2864	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑀 / (𝑟 · 𝑇)) / 3) = (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3))))
356	344, 355	oveq12d 7176	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (-((𝑟 · 𝑇) / 3) − ((𝑀 / (𝑟 · 𝑇)) / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))))
357	336, 339, 356	3eqtrd 2862	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))))
358	357	eqeq2d 2834	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑋 + (𝐵 / 3)) = -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) ↔ (𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3))))))
359	332, 334, 358	3bitrrd 308	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))) ↔ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3)))
360	359	anassrs 470	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ 𝑟 ≠ 0) → ((𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))) ↔ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3)))
361	306, 360	sylan2 594	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ (𝑟↑3) = 1) → ((𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))) ↔ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3)))
362	361	pm5.32da 581	. . 3 ⊢ ((𝜑 ∧ 𝑟 ∈ ℂ) → (((𝑟↑3) = 1 ∧ (𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3))))) ↔ ((𝑟↑3) = 1 ∧ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3))))
363	362	rexbidva 3298	. 2 ⊢ (𝜑 → (∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ (𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3))))) ↔ ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3))))
364	163, 298, 363	3bitr3d 311	1 ⊢ (𝜑 → ((((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((𝐶 · 𝑋) + 𝐷)) = 0 ↔ ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 398 = wceq 1537 ∈ wcel 2114 ≠ wne 3018 ∃wrex 3141 class class class wbr 5068 (class class class)co 7158 ℂcc 10537 0cc0 10539 1c1 10540 + caddc 10542 · cmul 10544 − cmin 10872 -cneg 10873 / cdiv 11299 ℕcn 11640 2c2 11695 3c3 11696 4c4 11697 7c7 11700 9c9 11702 ℕ₀cn0 11900 cdc 12101 ↑cexp 13432 ∥ cdvds 15609

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 ax-sep 5205 ax-nul 5212 ax-pow 5268 ax-pr 5332 ax-un 7463 ax-cnex 10595 ax-resscn 10596 ax-1cn 10597 ax-icn 10598 ax-addcl 10599 ax-addrcl 10600 ax-mulcl 10601 ax-mulrcl 10602 ax-mulcom 10603 ax-addass 10604 ax-mulass 10605 ax-distr 10606 ax-i2m1 10607 ax-1ne0 10608 ax-1rid 10609 ax-rnegex 10610 ax-rrecex 10611 ax-cnre 10612 ax-pre-lttri 10613 ax-pre-lttrn 10614 ax-pre-ltadd 10615 ax-pre-mulgt0 10616 ax-pre-sup 10617

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-ne 3019 df-nel 3126 df-ral 3145 df-rex 3146 df-reu 3147 df-rmo 3148 df-rab 3149 df-v 3498 df-sbc 3775 df-csb 3886 df-dif 3941 df-un 3943 df-in 3945 df-ss 3954 df-pss 3956 df-nul 4294 df-if 4470 df-pw 4543 df-sn 4570 df-pr 4572 df-tp 4574 df-op 4576 df-uni 4841 df-iun 4923 df-br 5069 df-opab 5131 df-mpt 5149 df-tr 5175 df-id 5462 df-eprel 5467 df-po 5476 df-so 5477 df-fr 5516 df-we 5518 df-xp 5563 df-rel 5564 df-cnv 5565 df-co 5566 df-dm 5567 df-rn 5568 df-res 5569 df-ima 5570 df-pred 6150 df-ord 6196 df-on 6197 df-lim 6198 df-suc 6199 df-iota 6316 df-fun 6359 df-fn 6360 df-f 6361 df-f1 6362 df-fo 6363 df-f1o 6364 df-fv 6365 df-riota 7116 df-ov 7161 df-oprab 7162 df-mpo 7163 df-om 7583 df-2nd 7692 df-wrecs 7949 df-recs 8010 df-rdg 8048 df-er 8291 df-en 8512 df-dom 8513 df-sdom 8514 df-sup 8908 df-pnf 10679 df-mnf 10680 df-xr 10681 df-ltxr 10682 df-le 10683 df-sub 10874 df-neg 10875 df-div 11300 df-nn 11641 df-2 11703 df-3 11704 df-4 11705 df-5 11706 df-6 11707 df-7 11708 df-8 11709 df-9 11710 df-n0 11901 df-z 11985 df-dec 12102 df-uz 12247 df-rp 12393 df-seq 13373 df-exp 13433 df-cj 14460 df-re 14461 df-im 14462 df-sqrt 14596 df-abs 14597 df-dvds 15610

This theorem is referenced by: cubic2 25428 quart 25441

W3C validator