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 25730

Description: Solutions to a monic cubic equation, a special case of cubic 25732. (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 13714	. . . . . . 7 ⊢ (𝜑 → (𝐵↑2) ∈ ℂ)
4		3cn 11911	. . . . . . . 8 ⊢ 3 ∈ ℂ
5		mcubic.c	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ ℂ)
6		mulcl 10813	. . . . . . . 8 ⊢ ((3 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (3 · 𝐶) ∈ ℂ)
7	4, 5, 6	sylancr 590	. . . . . . 7 ⊢ (𝜑 → (3 · 𝐶) ∈ ℂ)
8	3, 7	subcld 11189	. . . . . 6 ⊢ (𝜑 → ((𝐵↑2) − (3 · 𝐶)) ∈ ℂ)
9	1, 8	eqeltrd 2838	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ ℂ)
10	4	a1i 11	. . . . 5 ⊢ (𝜑 → 3 ∈ ℂ)
11		3ne0 11936	. . . . . 6 ⊢ 3 ≠ 0
12	11	a1i 11	. . . . 5 ⊢ (𝜑 → 3 ≠ 0)
13	9, 10, 12	divcld 11608	. . . 4 ⊢ (𝜑 → (𝑀 / 3) ∈ ℂ)
14	13	negcld 11176	. . 3 ⊢ (𝜑 → -(𝑀 / 3) ∈ ℂ)
15		mcubic.n	. . . . 5 ⊢ (𝜑 → 𝑁 = (((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) + (;27 · 𝐷)))
16		2cn 11905	. . . . . . . 8 ⊢ 2 ∈ ℂ
17		3nn0 12108	. . . . . . . . 9 ⊢ 3 ∈ ℕ₀
18		expcl 13653	. . . . . . . . 9 ⊢ ((𝐵 ∈ ℂ ∧ 3 ∈ ℕ₀) → (𝐵↑3) ∈ ℂ)
19	2, 17, 18	sylancl 589	. . . . . . . 8 ⊢ (𝜑 → (𝐵↑3) ∈ ℂ)
20		mulcl 10813	. . . . . . . 8 ⊢ ((2 ∈ ℂ ∧ (𝐵↑3) ∈ ℂ) → (2 · (𝐵↑3)) ∈ ℂ)
21	16, 19, 20	sylancr 590	. . . . . . 7 ⊢ (𝜑 → (2 · (𝐵↑3)) ∈ ℂ)
22		9cn 11930	. . . . . . . 8 ⊢ 9 ∈ ℂ
23	2, 5	mulcld 10853	. . . . . . . 8 ⊢ (𝜑 → (𝐵 · 𝐶) ∈ ℂ)
24		mulcl 10813	. . . . . . . 8 ⊢ ((9 ∈ ℂ ∧ (𝐵 · 𝐶) ∈ ℂ) → (9 · (𝐵 · 𝐶)) ∈ ℂ)
25	22, 23, 24	sylancr 590	. . . . . . 7 ⊢ (𝜑 → (9 · (𝐵 · 𝐶)) ∈ ℂ)
26	21, 25	subcld 11189	. . . . . 6 ⊢ (𝜑 → ((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) ∈ ℂ)
27		2nn0 12107	. . . . . . . . 9 ⊢ 2 ∈ ℕ₀
28		7nn 11922	. . . . . . . . 9 ⊢ 7 ∈ ℕ
29	27, 28	decnncl 12313	. . . . . . . 8 ⊢ ;27 ∈ ℕ
30	29	nncni 11840	. . . . . . 7 ⊢ ;27 ∈ ℂ
31		mcubic.d	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ ℂ)
32		mulcl 10813	. . . . . . 7 ⊢ ((;27 ∈ ℂ ∧ 𝐷 ∈ ℂ) → (;27 · 𝐷) ∈ ℂ)
33	30, 31, 32	sylancr 590	. . . . . 6 ⊢ (𝜑 → (;27 · 𝐷) ∈ ℂ)
34	26, 33	addcld 10852	. . . . 5 ⊢ (𝜑 → (((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) + (;27 · 𝐷)) ∈ ℂ)
35	15, 34	eqeltrd 2838	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ℂ)
36	30	a1i 11	. . . 4 ⊢ (𝜑 → ;27 ∈ ℂ)
37	29	nnne0i 11870	. . . . 5 ⊢ ;27 ≠ 0
38	37	a1i 11	. . . 4 ⊢ (𝜑 → ;27 ≠ 0)
39	35, 36, 38	divcld 11608	. . 3 ⊢ (𝜑 → (𝑁 / ;27) ∈ ℂ)
40		mcubic.x	. . . 4 ⊢ (𝜑 → 𝑋 ∈ ℂ)
41	2, 10, 12	divcld 11608	. . . 4 ⊢ (𝜑 → (𝐵 / 3) ∈ ℂ)
42	40, 41	addcld 10852	. . 3 ⊢ (𝜑 → (𝑋 + (𝐵 / 3)) ∈ ℂ)
43		mcubic.t	. . . . 5 ⊢ (𝜑 → 𝑇 ∈ ℂ)
44	43, 10, 12	divcld 11608	. . . 4 ⊢ (𝜑 → (𝑇 / 3) ∈ ℂ)
45	44	negcld 11176	. . 3 ⊢ (𝜑 → -(𝑇 / 3) ∈ ℂ)
46		3nn 11909	. . . . . 6 ⊢ 3 ∈ ℕ
47	46	a1i 11	. . . . 5 ⊢ (𝜑 → 3 ∈ ℕ)
48		n2dvds3 15932	. . . . . 6 ⊢ ¬ 2 ∥ 3
49	48	a1i 11	. . . . 5 ⊢ (𝜑 → ¬ 2 ∥ 3)
50		oexpneg 15906	. . . . 5 ⊢ (((𝑇 / 3) ∈ ℂ ∧ 3 ∈ ℕ ∧ ¬ 2 ∥ 3) → (-(𝑇 / 3)↑3) = -((𝑇 / 3)↑3))
51	44, 47, 49, 50	syl3anc 1373	. . . 4 ⊢ (𝜑 → (-(𝑇 / 3)↑3) = -((𝑇 / 3)↑3))
52	17	a1i 11	. . . . . . 7 ⊢ (𝜑 → 3 ∈ ℕ₀)
53	43, 10, 12, 52	expdivd 13730	. . . . . 6 ⊢ (𝜑 → ((𝑇 / 3)↑3) = ((𝑇↑3) / (3↑3)))
54		mcubic.3	. . . . . . 7 ⊢ (𝜑 → (𝑇↑3) = ((𝑁 + 𝐺) / 2))
55		3exp3 16645	. . . . . . . 8 ⊢ (3↑3) = ;27
56	55	a1i 11	. . . . . . 7 ⊢ (𝜑 → (3↑3) = ;27)
57	54, 56	oveq12d 7231	. . . . . 6 ⊢ (𝜑 → ((𝑇↑3) / (3↑3)) = (((𝑁 + 𝐺) / 2) / ;27))
58		mcubic.g	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 ∈ ℂ)
59	35, 58	addcld 10852	. . . . . . . 8 ⊢ (𝜑 → (𝑁 + 𝐺) ∈ ℂ)
60		2cnd 11908	. . . . . . . 8 ⊢ (𝜑 → 2 ∈ ℂ)
61		2ne0 11934	. . . . . . . . 9 ⊢ 2 ≠ 0
62	61	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 2 ≠ 0)
63	59, 60, 36, 62, 38	divdiv32d 11633	. . . . . . 7 ⊢ (𝜑 → (((𝑁 + 𝐺) / 2) / ;27) = (((𝑁 + 𝐺) / ;27) / 2))
64	35, 58	addcomd 11034	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 + 𝐺) = (𝐺 + 𝑁))
65	64	oveq1d 7228	. . . . . . . . 9 ⊢ (𝜑 → ((𝑁 + 𝐺) / ;27) = ((𝐺 + 𝑁) / ;27))
66	58, 35, 36, 38	divdird 11646	. . . . . . . . 9 ⊢ (𝜑 → ((𝐺 + 𝑁) / ;27) = ((𝐺 / ;27) + (𝑁 / ;27)))
67	65, 66	eqtrd 2777	. . . . . . . 8 ⊢ (𝜑 → ((𝑁 + 𝐺) / ;27) = ((𝐺 / ;27) + (𝑁 / ;27)))
68	67	oveq1d 7228	. . . . . . 7 ⊢ (𝜑 → (((𝑁 + 𝐺) / ;27) / 2) = (((𝐺 / ;27) + (𝑁 / ;27)) / 2))
69	58, 36, 38	divcld 11608	. . . . . . . 8 ⊢ (𝜑 → (𝐺 / ;27) ∈ ℂ)
70	69, 39, 60, 62	divdird 11646	. . . . . . 7 ⊢ (𝜑 → (((𝐺 / ;27) + (𝑁 / ;27)) / 2) = (((𝐺 / ;27) / 2) + ((𝑁 / ;27) / 2)))
71	63, 68, 70	3eqtrd 2781	. . . . . 6 ⊢ (𝜑 → (((𝑁 + 𝐺) / 2) / ;27) = (((𝐺 / ;27) / 2) + ((𝑁 / ;27) / 2)))
72	53, 57, 71	3eqtrd 2781	. . . . 5 ⊢ (𝜑 → ((𝑇 / 3)↑3) = (((𝐺 / ;27) / 2) + ((𝑁 / ;27) / 2)))
73	72	negeqd 11072	. . . 4 ⊢ (𝜑 → -((𝑇 / 3)↑3) = -(((𝐺 / ;27) / 2) + ((𝑁 / ;27) / 2)))
74	69	halfcld 12075	. . . . 5 ⊢ (𝜑 → ((𝐺 / ;27) / 2) ∈ ℂ)
75	39	halfcld 12075	. . . . 5 ⊢ (𝜑 → ((𝑁 / ;27) / 2) ∈ ℂ)
76	74, 75	negdi2d 11203	. . . 4 ⊢ (𝜑 → -(((𝐺 / ;27) / 2) + ((𝑁 / ;27) / 2)) = (-((𝐺 / ;27) / 2) − ((𝑁 / ;27) / 2)))
77	51, 73, 76	3eqtrd 2781	. . 3 ⊢ (𝜑 → (-(𝑇 / 3)↑3) = (-((𝐺 / ;27) / 2) − ((𝑁 / ;27) / 2)))
78	74	negcld 11176	. . 3 ⊢ (𝜑 → -((𝐺 / ;27) / 2) ∈ ℂ)
79		sqneg 13688	. . . . 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 13729	. . . 4 ⊢ (𝜑 → (((𝐺 / ;27) / 2)↑2) = (((𝐺 / ;27)↑2) / (2↑2)))
82	39, 60, 62	sqdivd 13729	. . . . . . . 8 ⊢ (𝜑 → (((𝑁 / ;27) / 2)↑2) = (((𝑁 / ;27)↑2) / (2↑2)))
83	35, 36, 38	sqdivd 13729	. . . . . . . . 9 ⊢ (𝜑 → ((𝑁 / ;27)↑2) = ((𝑁↑2) / (;27↑2)))
84	83	oveq1d 7228	. . . . . . . 8 ⊢ (𝜑 → (((𝑁 / ;27)↑2) / (2↑2)) = (((𝑁↑2) / (;27↑2)) / (2↑2)))
85	82, 84	eqtr2d 2778	. . . . . . 7 ⊢ (𝜑 → (((𝑁↑2) / (;27↑2)) / (2↑2)) = (((𝑁 / ;27) / 2)↑2))
86		4cn 11915	. . . . . . . . . . . 12 ⊢ 4 ∈ ℂ
87	86	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 4 ∈ ℂ)
88		expcl 13653	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℂ ∧ 3 ∈ ℕ₀) → (𝑀↑3) ∈ ℂ)
89	9, 17, 88	sylancl 589	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀↑3) ∈ ℂ)
90	30	sqcli 13750	. . . . . . . . . . . 12 ⊢ (;27↑2) ∈ ℂ
91	90	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (;27↑2) ∈ ℂ)
92		sqne0 13695	. . . . . . . . . . . . 13 ⊢ (;27 ∈ ℂ → ((;27↑2) ≠ 0 ↔ ;27 ≠ 0))
93	36, 92	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → ((;27↑2) ≠ 0 ↔ ;27 ≠ 0))
94	38, 93	mpbird 260	. . . . . . . . . . 11 ⊢ (𝜑 → (;27↑2) ≠ 0)
95	87, 89, 91, 94	divassd 11643	. . . . . . . . . 10 ⊢ (𝜑 → ((4 · (𝑀↑3)) / (;27↑2)) = (4 · ((𝑀↑3) / (;27↑2))))
96	22	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 9 ∈ ℂ)
97		9nn 11928	. . . . . . . . . . . . . . 15 ⊢ 9 ∈ ℕ
98	97	nnne0i 11870	. . . . . . . . . . . . . 14 ⊢ 9 ≠ 0
99	98	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 9 ≠ 0)
100	9, 96, 99, 52	expdivd 13730	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑀 / 9)↑3) = ((𝑀↑3) / (9↑3)))
101	16, 4	mulcomi 10841	. . . . . . . . . . . . . . . 16 ⊢ (2 · 3) = (3 · 2)
102	101	oveq2i 7224	. . . . . . . . . . . . . . 15 ⊢ (3↑(2 · 3)) = (3↑(3 · 2))
103		expmul 13680	. . . . . . . . . . . . . . . 16 ⊢ ((3 ∈ ℂ ∧ 2 ∈ ℕ₀ ∧ 3 ∈ ℕ₀) → (3↑(2 · 3)) = ((3↑2)↑3))
104	4, 27, 17, 103	mp3an 1463	. . . . . . . . . . . . . . 15 ⊢ (3↑(2 · 3)) = ((3↑2)↑3)
105		expmul 13680	. . . . . . . . . . . . . . . 16 ⊢ ((3 ∈ ℂ ∧ 3 ∈ ℕ₀ ∧ 2 ∈ ℕ₀) → (3↑(3 · 2)) = ((3↑3)↑2))
106	4, 17, 27, 105	mp3an 1463	. . . . . . . . . . . . . . 15 ⊢ (3↑(3 · 2)) = ((3↑3)↑2)
107	102, 104, 106	3eqtr3i 2773	. . . . . . . . . . . . . 14 ⊢ ((3↑2)↑3) = ((3↑3)↑2)
108		sq3 13767	. . . . . . . . . . . . . . 15 ⊢ (3↑2) = 9
109	108	oveq1i 7223	. . . . . . . . . . . . . 14 ⊢ ((3↑2)↑3) = (9↑3)
110	55	oveq1i 7223	. . . . . . . . . . . . . 14 ⊢ ((3↑3)↑2) = (;27↑2)
111	107, 109, 110	3eqtr3i 2773	. . . . . . . . . . . . 13 ⊢ (9↑3) = (;27↑2)
112	111	oveq2i 7224	. . . . . . . . . . . 12 ⊢ ((𝑀↑3) / (9↑3)) = ((𝑀↑3) / (;27↑2))
113	100, 112	eqtrdi 2794	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑀 / 9)↑3) = ((𝑀↑3) / (;27↑2)))
114	113	oveq2d 7229	. . . . . . . . . 10 ⊢ (𝜑 → (4 · ((𝑀 / 9)↑3)) = (4 · ((𝑀↑3) / (;27↑2))))
115	95, 114	eqtr4d 2780	. . . . . . . . 9 ⊢ (𝜑 → ((4 · (𝑀↑3)) / (;27↑2)) = (4 · ((𝑀 / 9)↑3)))
116	115	oveq1d 7228	. . . . . . . 8 ⊢ (𝜑 → (((4 · (𝑀↑3)) / (;27↑2)) / (2↑2)) = ((4 · ((𝑀 / 9)↑3)) / (2↑2)))
117		sq2 13766	. . . . . . . . . 10 ⊢ (2↑2) = 4
118	117	oveq2i 7224	. . . . . . . . 9 ⊢ ((4 · ((𝑀 / 9)↑3)) / (2↑2)) = ((4 · ((𝑀 / 9)↑3)) / 4)
119	9, 96, 99	divcld 11608	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀 / 9) ∈ ℂ)
120		expcl 13653	. . . . . . . . . . 11 ⊢ (((𝑀 / 9) ∈ ℂ ∧ 3 ∈ ℕ₀) → ((𝑀 / 9)↑3) ∈ ℂ)
121	119, 17, 120	sylancl 589	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑀 / 9)↑3) ∈ ℂ)
122		4ne0 11938	. . . . . . . . . . 11 ⊢ 4 ≠ 0
123	122	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 4 ≠ 0)
124	121, 87, 123	divcan3d 11613	. . . . . . . . 9 ⊢ (𝜑 → ((4 · ((𝑀 / 9)↑3)) / 4) = ((𝑀 / 9)↑3))
125	118, 124	syl5eq 2790	. . . . . . . 8 ⊢ (𝜑 → ((4 · ((𝑀 / 9)↑3)) / (2↑2)) = ((𝑀 / 9)↑3))
126	116, 125	eqtrd 2777	. . . . . . 7 ⊢ (𝜑 → (((4 · (𝑀↑3)) / (;27↑2)) / (2↑2)) = ((𝑀 / 9)↑3))
127	85, 126	oveq12d 7231	. . . . . 6 ⊢ (𝜑 → ((((𝑁↑2) / (;27↑2)) / (2↑2)) − (((4 · (𝑀↑3)) / (;27↑2)) / (2↑2))) = ((((𝑁 / ;27) / 2)↑2) − ((𝑀 / 9)↑3)))
128	35	sqcld 13714	. . . . . . . 8 ⊢ (𝜑 → (𝑁↑2) ∈ ℂ)
129	128, 91, 94	divcld 11608	. . . . . . 7 ⊢ (𝜑 → ((𝑁↑2) / (;27↑2)) ∈ ℂ)
130		mulcl 10813	. . . . . . . . 9 ⊢ ((4 ∈ ℂ ∧ (𝑀↑3) ∈ ℂ) → (4 · (𝑀↑3)) ∈ ℂ)
131	86, 89, 130	sylancr 590	. . . . . . . 8 ⊢ (𝜑 → (4 · (𝑀↑3)) ∈ ℂ)
132	131, 91, 94	divcld 11608	. . . . . . 7 ⊢ (𝜑 → ((4 · (𝑀↑3)) / (;27↑2)) ∈ ℂ)
133	16	sqcli 13750	. . . . . . . 8 ⊢ (2↑2) ∈ ℂ
134	133	a1i 11	. . . . . . 7 ⊢ (𝜑 → (2↑2) ∈ ℂ)
135	117, 122	eqnetri 3011	. . . . . . . 8 ⊢ (2↑2) ≠ 0
136	135	a1i 11	. . . . . . 7 ⊢ (𝜑 → (2↑2) ≠ 0)
137	129, 132, 134, 136	divsubdird 11647	. . . . . 6 ⊢ (𝜑 → ((((𝑁↑2) / (;27↑2)) − ((4 · (𝑀↑3)) / (;27↑2))) / (2↑2)) = ((((𝑁↑2) / (;27↑2)) / (2↑2)) − (((4 · (𝑀↑3)) / (;27↑2)) / (2↑2))))
138	75	sqcld 13714	. . . . . . 7 ⊢ (𝜑 → (((𝑁 / ;27) / 2)↑2) ∈ ℂ)
139	138, 121	negsubd 11195	. . . . . 6 ⊢ (𝜑 → ((((𝑁 / ;27) / 2)↑2) + -((𝑀 / 9)↑3)) = ((((𝑁 / ;27) / 2)↑2) − ((𝑀 / 9)↑3)))
140	127, 137, 139	3eqtr4d 2787	. . . . 5 ⊢ (𝜑 → ((((𝑁↑2) / (;27↑2)) − ((4 · (𝑀↑3)) / (;27↑2))) / (2↑2)) = ((((𝑁 / ;27) / 2)↑2) + -((𝑀 / 9)↑3)))
141	58, 36, 38	sqdivd 13729	. . . . . . 7 ⊢ (𝜑 → ((𝐺 / ;27)↑2) = ((𝐺↑2) / (;27↑2)))
142		mcubic.2	. . . . . . . 8 ⊢ (𝜑 → (𝐺↑2) = ((𝑁↑2) − (4 · (𝑀↑3))))
143	142	oveq1d 7228	. . . . . . 7 ⊢ (𝜑 → ((𝐺↑2) / (;27↑2)) = (((𝑁↑2) − (4 · (𝑀↑3))) / (;27↑2)))
144	128, 131, 91, 94	divsubdird 11647	. . . . . . 7 ⊢ (𝜑 → (((𝑁↑2) − (4 · (𝑀↑3))) / (;27↑2)) = (((𝑁↑2) / (;27↑2)) − ((4 · (𝑀↑3)) / (;27↑2))))
145	141, 143, 144	3eqtrd 2781	. . . . . 6 ⊢ (𝜑 → ((𝐺 / ;27)↑2) = (((𝑁↑2) / (;27↑2)) − ((4 · (𝑀↑3)) / (;27↑2))))
146	145	oveq1d 7228	. . . . 5 ⊢ (𝜑 → (((𝐺 / ;27)↑2) / (2↑2)) = ((((𝑁↑2) / (;27↑2)) − ((4 · (𝑀↑3)) / (;27↑2))) / (2↑2)))
147		oexpneg 15906	. . . . . . 7 ⊢ (((𝑀 / 9) ∈ ℂ ∧ 3 ∈ ℕ ∧ ¬ 2 ∥ 3) → (-(𝑀 / 9)↑3) = -((𝑀 / 9)↑3))
148	119, 47, 49, 147	syl3anc 1373	. . . . . 6 ⊢ (𝜑 → (-(𝑀 / 9)↑3) = -((𝑀 / 9)↑3))
149	148	oveq2d 7229	. . . . 5 ⊢ (𝜑 → ((((𝑁 / ;27) / 2)↑2) + (-(𝑀 / 9)↑3)) = ((((𝑁 / ;27) / 2)↑2) + -((𝑀 / 9)↑3)))
150	140, 146, 149	3eqtr4d 2787	. . . 4 ⊢ (𝜑 → (((𝐺 / ;27)↑2) / (2↑2)) = ((((𝑁 / ;27) / 2)↑2) + (-(𝑀 / 9)↑3)))
151	80, 81, 150	3eqtrd 2781	. . 3 ⊢ (𝜑 → (-((𝐺 / ;27) / 2)↑2) = ((((𝑁 / ;27) / 2)↑2) + (-(𝑀 / 9)↑3)))
152	9, 10, 10, 12, 12	divdiv1d 11639	. . . . . 6 ⊢ (𝜑 → ((𝑀 / 3) / 3) = (𝑀 / (3 · 3)))
153		3t3e9 11997	. . . . . . 7 ⊢ (3 · 3) = 9
154	153	oveq2i 7224	. . . . . 6 ⊢ (𝑀 / (3 · 3)) = (𝑀 / 9)
155	152, 154	eqtrdi 2794	. . . . 5 ⊢ (𝜑 → ((𝑀 / 3) / 3) = (𝑀 / 9))
156	155	negeqd 11072	. . . 4 ⊢ (𝜑 → -((𝑀 / 3) / 3) = -(𝑀 / 9))
157	13, 10, 12	divnegd 11621	. . . 4 ⊢ (𝜑 → -((𝑀 / 3) / 3) = (-(𝑀 / 3) / 3))
158	156, 157	eqtr3d 2779	. . 3 ⊢ (𝜑 → -(𝑀 / 9) = (-(𝑀 / 3) / 3))
159		eqidd 2738	. . 3 ⊢ (𝜑 → ((𝑁 / ;27) / 2) = ((𝑁 / ;27) / 2))
160		mcubic.0	. . . . 5 ⊢ (𝜑 → 𝑇 ≠ 0)
161	43, 10, 160, 12	divne0d 11624	. . . 4 ⊢ (𝜑 → (𝑇 / 3) ≠ 0)
162	44, 161	negne0d 11187	. . 3 ⊢ (𝜑 → -(𝑇 / 3) ≠ 0)
163	14, 39, 42, 45, 77, 78, 151, 158, 159, 162	dcubic 25729	. 2 ⊢ (𝜑 → ((((𝑋 + (𝐵 / 3))↑3) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27))) = 0 ↔ ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ (𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))))))
164		binom3 13791	. . . . . . 7 ⊢ ((𝑋 ∈ ℂ ∧ (𝐵 / 3) ∈ ℂ) → ((𝑋 + (𝐵 / 3))↑3) = (((𝑋↑3) + (3 · ((𝑋↑2) · (𝐵 / 3)))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))))
165	40, 41, 164	syl2anc 587	. . . . . 6 ⊢ (𝜑 → ((𝑋 + (𝐵 / 3))↑3) = (((𝑋↑3) + (3 · ((𝑋↑2) · (𝐵 / 3)))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))))
166	40	sqcld 13714	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋↑2) ∈ ℂ)
167	10, 166, 41	mul12d 11041	. . . . . . . . 9 ⊢ (𝜑 → (3 · ((𝑋↑2) · (𝐵 / 3))) = ((𝑋↑2) · (3 · (𝐵 / 3))))
168	2, 10, 12	divcan2d 11610	. . . . . . . . . 10 ⊢ (𝜑 → (3 · (𝐵 / 3)) = 𝐵)
169	168	oveq2d 7229	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋↑2) · (3 · (𝐵 / 3))) = ((𝑋↑2) · 𝐵))
170	166, 2	mulcomd 10854	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋↑2) · 𝐵) = (𝐵 · (𝑋↑2)))
171	167, 169, 170	3eqtrd 2781	. . . . . . . 8 ⊢ (𝜑 → (3 · ((𝑋↑2) · (𝐵 / 3))) = (𝐵 · (𝑋↑2)))
172	171	oveq2d 7229	. . . . . . 7 ⊢ (𝜑 → ((𝑋↑3) + (3 · ((𝑋↑2) · (𝐵 / 3)))) = ((𝑋↑3) + (𝐵 · (𝑋↑2))))
173	172	oveq1d 7228	. . . . . 6 ⊢ (𝜑 → (((𝑋↑3) + (3 · ((𝑋↑2) · (𝐵 / 3)))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))) = (((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))))
174	165, 173	eqtrd 2777	. . . . 5 ⊢ (𝜑 → ((𝑋 + (𝐵 / 3))↑3) = (((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))))
175	174	oveq1d 7228	. . . 4 ⊢ (𝜑 → (((𝑋 + (𝐵 / 3))↑3) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27))) = ((((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27))))
176		expcl 13653	. . . . . . 7 ⊢ ((𝑋 ∈ ℂ ∧ 3 ∈ ℕ₀) → (𝑋↑3) ∈ ℂ)
177	40, 17, 176	sylancl 589	. . . . . 6 ⊢ (𝜑 → (𝑋↑3) ∈ ℂ)
178	2, 166	mulcld 10853	. . . . . 6 ⊢ (𝜑 → (𝐵 · (𝑋↑2)) ∈ ℂ)
179	177, 178	addcld 10852	. . . . 5 ⊢ (𝜑 → ((𝑋↑3) + (𝐵 · (𝑋↑2))) ∈ ℂ)
180	41	sqcld 13714	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 / 3)↑2) ∈ ℂ)
181	40, 180	mulcld 10853	. . . . . . 7 ⊢ (𝜑 → (𝑋 · ((𝐵 / 3)↑2)) ∈ ℂ)
182	10, 181	mulcld 10853	. . . . . 6 ⊢ (𝜑 → (3 · (𝑋 · ((𝐵 / 3)↑2))) ∈ ℂ)
183		expcl 13653	. . . . . . 7 ⊢ (((𝐵 / 3) ∈ ℂ ∧ 3 ∈ ℕ₀) → ((𝐵 / 3)↑3) ∈ ℂ)
184	41, 17, 183	sylancl 589	. . . . . 6 ⊢ (𝜑 → ((𝐵 / 3)↑3) ∈ ℂ)
185	182, 184	addcld 10852	. . . . 5 ⊢ (𝜑 → ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) ∈ ℂ)
186	14, 42	mulcld 10853	. . . . . 6 ⊢ (𝜑 → (-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) ∈ ℂ)
187	186, 39	addcld 10852	. . . . 5 ⊢ (𝜑 → ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27)) ∈ ℂ)
188	179, 185, 187	addassd 10855	. . . 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 10857	. . . . . . . . . 10 ⊢ (𝜑 → (-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) = ((-(𝑀 / 3) · 𝑋) + (-(𝑀 / 3) · (𝐵 / 3))))
190	189	oveq1d 7228	. . . . . . . . 9 ⊢ (𝜑 → ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27)) = (((-(𝑀 / 3) · 𝑋) + (-(𝑀 / 3) · (𝐵 / 3))) + (𝑁 / ;27)))
191	14, 40	mulcld 10853	. . . . . . . . . 10 ⊢ (𝜑 → (-(𝑀 / 3) · 𝑋) ∈ ℂ)
192	14, 41	mulcld 10853	. . . . . . . . . 10 ⊢ (𝜑 → (-(𝑀 / 3) · (𝐵 / 3)) ∈ ℂ)
193	191, 192, 39	addassd 10855	. . . . . . . . 9 ⊢ (𝜑 → (((-(𝑀 / 3) · 𝑋) + (-(𝑀 / 3) · (𝐵 / 3))) + (𝑁 / ;27)) = ((-(𝑀 / 3) · 𝑋) + ((-(𝑀 / 3) · (𝐵 / 3)) + (𝑁 / ;27))))
194	1	oveq1d 7228	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀 / 3) = (((𝐵↑2) − (3 · 𝐶)) / 3))
195	3, 7, 10, 12	divsubdird 11647	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐵↑2) − (3 · 𝐶)) / 3) = (((𝐵↑2) / 3) − ((3 · 𝐶) / 3)))
196	5, 10, 12	divcan3d 11613	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((3 · 𝐶) / 3) = 𝐶)
197	196	oveq2d 7229	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐵↑2) / 3) − ((3 · 𝐶) / 3)) = (((𝐵↑2) / 3) − 𝐶))
198	194, 195, 197	3eqtrd 2781	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀 / 3) = (((𝐵↑2) / 3) − 𝐶))
199	198	negeqd 11072	. . . . . . . . . . . . 13 ⊢ (𝜑 → -(𝑀 / 3) = -(((𝐵↑2) / 3) − 𝐶))
200	3, 10, 12	divcld 11608	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐵↑2) / 3) ∈ ℂ)
201	200, 5	negsubdi2d 11205	. . . . . . . . . . . . 13 ⊢ (𝜑 → -(((𝐵↑2) / 3) − 𝐶) = (𝐶 − ((𝐵↑2) / 3)))
202	199, 201	eqtrd 2777	. . . . . . . . . . . 12 ⊢ (𝜑 → -(𝑀 / 3) = (𝐶 − ((𝐵↑2) / 3)))
203	202	oveq1d 7228	. . . . . . . . . . 11 ⊢ (𝜑 → (-(𝑀 / 3) · 𝑋) = ((𝐶 − ((𝐵↑2) / 3)) · 𝑋))
204	5, 200, 40	subdird 11289	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐶 − ((𝐵↑2) / 3)) · 𝑋) = ((𝐶 · 𝑋) − (((𝐵↑2) / 3) · 𝑋)))
205	200, 40	mulcomd 10854	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐵↑2) / 3) · 𝑋) = (𝑋 · ((𝐵↑2) / 3)))
206	4	sqvali 13749	. . . . . . . . . . . . . . . . . 18 ⊢ (3↑2) = (3 · 3)
207	206	oveq2i 7224	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵↑2) / (3↑2)) = ((𝐵↑2) / (3 · 3))
208	2, 10, 12	sqdivd 13729	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐵 / 3)↑2) = ((𝐵↑2) / (3↑2)))
209	3, 10, 10, 12, 12	divdiv1d 11639	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝐵↑2) / 3) / 3) = ((𝐵↑2) / (3 · 3)))
210	207, 208, 209	3eqtr4a 2804	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐵 / 3)↑2) = (((𝐵↑2) / 3) / 3))
211	210	oveq2d 7229	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (3 · ((𝐵 / 3)↑2)) = (3 · (((𝐵↑2) / 3) / 3)))
212	200, 10, 12	divcan2d 11610	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (3 · (((𝐵↑2) / 3) / 3)) = ((𝐵↑2) / 3))
213	211, 212	eqtrd 2777	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (3 · ((𝐵 / 3)↑2)) = ((𝐵↑2) / 3))
214	213	oveq2d 7229	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 · (3 · ((𝐵 / 3)↑2))) = (𝑋 · ((𝐵↑2) / 3)))
215	40, 10, 180	mul12d 11041	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 · (3 · ((𝐵 / 3)↑2))) = (3 · (𝑋 · ((𝐵 / 3)↑2))))
216	205, 214, 215	3eqtr2d 2783	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐵↑2) / 3) · 𝑋) = (3 · (𝑋 · ((𝐵 / 3)↑2))))
217	216	oveq2d 7229	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐶 · 𝑋) − (((𝐵↑2) / 3) · 𝑋)) = ((𝐶 · 𝑋) − (3 · (𝑋 · ((𝐵 / 3)↑2)))))
218	203, 204, 217	3eqtrd 2781	. . . . . . . . . 10 ⊢ (𝜑 → (-(𝑀 / 3) · 𝑋) = ((𝐶 · 𝑋) − (3 · (𝑋 · ((𝐵 / 3)↑2)))))
219	202	oveq1d 7228	. . . . . . . . . . . . 13 ⊢ (𝜑 → (-(𝑀 / 3) · (𝐵 / 3)) = ((𝐶 − ((𝐵↑2) / 3)) · (𝐵 / 3)))
220	5, 200, 41	subdird 11289	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐶 − ((𝐵↑2) / 3)) · (𝐵 / 3)) = ((𝐶 · (𝐵 / 3)) − (((𝐵↑2) / 3) · (𝐵 / 3))))
221	5, 2, 10, 12	divassd 11643	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐶 · 𝐵) / 3) = (𝐶 · (𝐵 / 3)))
222	5, 2	mulcomd 10854	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐶 · 𝐵) = (𝐵 · 𝐶))
223	222	oveq1d 7228	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐶 · 𝐵) / 3) = ((𝐵 · 𝐶) / 3))
224	221, 223	eqtr3d 2779	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐶 · (𝐵 / 3)) = ((𝐵 · 𝐶) / 3))
225	3, 10, 2, 10, 12, 12	divmuldivd 11649	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐵↑2) / 3) · (𝐵 / 3)) = (((𝐵↑2) · 𝐵) / (3 · 3)))
226		df-3 11894	. . . . . . . . . . . . . . . . . 18 ⊢ 3 = (2 + 1)
227	226	oveq2i 7224	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵↑3) = (𝐵↑(2 + 1))
228		expp1 13642	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ∈ ℂ ∧ 2 ∈ ℕ₀) → (𝐵↑(2 + 1)) = ((𝐵↑2) · 𝐵))
229	2, 27, 228	sylancl 589	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵↑(2 + 1)) = ((𝐵↑2) · 𝐵))
230	227, 229	eqtr2id 2791	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐵↑2) · 𝐵) = (𝐵↑3))
231	153	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (3 · 3) = 9)
232	230, 231	oveq12d 7231	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐵↑2) · 𝐵) / (3 · 3)) = ((𝐵↑3) / 9))
233	225, 232	eqtrd 2777	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐵↑2) / 3) · (𝐵 / 3)) = ((𝐵↑3) / 9))
234	224, 233	oveq12d 7231	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐶 · (𝐵 / 3)) − (((𝐵↑2) / 3) · (𝐵 / 3))) = (((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)))
235	219, 220, 234	3eqtrd 2781	. . . . . . . . . . . 12 ⊢ (𝜑 → (-(𝑀 / 3) · (𝐵 / 3)) = (((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)))
236	15	oveq1d 7228	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 / ;27) = ((((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) + (;27 · 𝐷)) / ;27))
237	26, 33, 36, 38	divdird 11646	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) + (;27 · 𝐷)) / ;27) = ((((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) / ;27) + ((;27 · 𝐷) / ;27)))
238	21, 25, 36, 38	divsubdird 11647	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) / ;27) = (((2 · (𝐵↑3)) / ;27) − ((9 · (𝐵 · 𝐶)) / ;27)))
239		9t3e27 12416	. . . . . . . . . . . . . . . . . 18 ⊢ (9 · 3) = ;27
240	239	oveq2i 7224	. . . . . . . . . . . . . . . . 17 ⊢ ((9 · (𝐵 · 𝐶)) / (9 · 3)) = ((9 · (𝐵 · 𝐶)) / ;27)
241	23, 10, 96, 12, 99	divcan5d 11634	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((9 · (𝐵 · 𝐶)) / (9 · 3)) = ((𝐵 · 𝐶) / 3))
242	240, 241	eqtr3id 2792	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((9 · (𝐵 · 𝐶)) / ;27) = ((𝐵 · 𝐶) / 3))
243	242	oveq2d 7229	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((2 · (𝐵↑3)) / ;27) − ((9 · (𝐵 · 𝐶)) / ;27)) = (((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3)))
244	238, 243	eqtrd 2777	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) / ;27) = (((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3)))
245	31, 36, 38	divcan3d 11613	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((;27 · 𝐷) / ;27) = 𝐷)
246	244, 245	oveq12d 7231	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((2 · (𝐵↑3)) − (9 · (𝐵 · 𝐶))) / ;27) + ((;27 · 𝐷) / ;27)) = ((((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3)) + 𝐷))
247	236, 237, 246	3eqtrd 2781	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁 / ;27) = ((((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3)) + 𝐷))
248	235, 247	oveq12d 7231	. . . . . . . . . . 11 ⊢ (𝜑 → ((-(𝑀 / 3) · (𝐵 / 3)) + (𝑁 / ;27)) = ((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + ((((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3)) + 𝐷)))
249	19, 96, 99	divcld 11608	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐵↑3) / 9) ∈ ℂ)
250	21, 36, 38	divcld 11608	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((2 · (𝐵↑3)) / ;27) ∈ ℂ)
251	249, 250	negsubdi2d 11205	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -(((𝐵↑3) / 9) − ((2 · (𝐵↑3)) / ;27)) = (((2 · (𝐵↑3)) / ;27) − ((𝐵↑3) / 9)))
252	2, 10, 12, 52	expdivd 13730	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐵 / 3)↑3) = ((𝐵↑3) / (3↑3)))
253	55	oveq2i 7224	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵↑3) / (3↑3)) = ((𝐵↑3) / ;27)
254		ax-1cn 10787	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 ∈ ℂ
255		2p1e3 11972	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (2 + 1) = 3
256	4, 16, 254, 255	subaddrii 11167	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (3 − 2) = 1
257	256	oveq1i 7223	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((3 − 2) · (𝐵↑3)) = (1 · (𝐵↑3))
258	19	mulid2d 10851	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (1 · (𝐵↑3)) = (𝐵↑3))
259	257, 258	syl5eq 2790	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((3 − 2) · (𝐵↑3)) = (𝐵↑3))
260	10, 60, 19	subdird 11289	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((3 − 2) · (𝐵↑3)) = ((3 · (𝐵↑3)) − (2 · (𝐵↑3))))
261	259, 260	eqtr3d 2779	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐵↑3) = ((3 · (𝐵↑3)) − (2 · (𝐵↑3))))
262	261	oveq1d 7228	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐵↑3) / ;27) = (((3 · (𝐵↑3)) − (2 · (𝐵↑3))) / ;27))
263		mulcl 10813	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((3 ∈ ℂ ∧ (𝐵↑3) ∈ ℂ) → (3 · (𝐵↑3)) ∈ ℂ)
264	4, 19, 263	sylancr 590	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (3 · (𝐵↑3)) ∈ ℂ)
265	264, 21, 36, 38	divsubdird 11647	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((3 · (𝐵↑3)) − (2 · (𝐵↑3))) / ;27) = (((3 · (𝐵↑3)) / ;27) − ((2 · (𝐵↑3)) / ;27)))
266	262, 265	eqtrd 2777	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐵↑3) / ;27) = (((3 · (𝐵↑3)) / ;27) − ((2 · (𝐵↑3)) / ;27)))
267	253, 266	syl5eq 2790	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐵↑3) / (3↑3)) = (((3 · (𝐵↑3)) / ;27) − ((2 · (𝐵↑3)) / ;27)))
268	22, 4, 239	mulcomli 10842	. . . . . . . . . . . . . . . . . . 19 ⊢ (3 · 9) = ;27
269	268	oveq2i 7224	. . . . . . . . . . . . . . . . . 18 ⊢ ((3 · (𝐵↑3)) / (3 · 9)) = ((3 · (𝐵↑3)) / ;27)
270	19, 96, 10, 99, 12	divcan5d 11634	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((3 · (𝐵↑3)) / (3 · 9)) = ((𝐵↑3) / 9))
271	269, 270	eqtr3id 2792	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((3 · (𝐵↑3)) / ;27) = ((𝐵↑3) / 9))
272	271	oveq1d 7228	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((3 · (𝐵↑3)) / ;27) − ((2 · (𝐵↑3)) / ;27)) = (((𝐵↑3) / 9) − ((2 · (𝐵↑3)) / ;27)))
273	252, 267, 272	3eqtrd 2781	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐵 / 3)↑3) = (((𝐵↑3) / 9) − ((2 · (𝐵↑3)) / ;27)))
274	273	negeqd 11072	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -((𝐵 / 3)↑3) = -(((𝐵↑3) / 9) − ((2 · (𝐵↑3)) / ;27)))
275	23, 10, 12	divcld 11608	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐵 · 𝐶) / 3) ∈ ℂ)
276	275, 249, 250	npncan3d 11225	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + (((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3))) = (((2 · (𝐵↑3)) / ;27) − ((𝐵↑3) / 9)))
277	251, 274, 276	3eqtr4d 2787	. . . . . . . . . . . . 13 ⊢ (𝜑 → -((𝐵 / 3)↑3) = ((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + (((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3))))
278	277	oveq1d 7228	. . . . . . . . . . . 12 ⊢ (𝜑 → (-((𝐵 / 3)↑3) + 𝐷) = (((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + (((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3))) + 𝐷))
279	184	negcld 11176	. . . . . . . . . . . . 13 ⊢ (𝜑 → -((𝐵 / 3)↑3) ∈ ℂ)
280	279, 31	addcomd 11034	. . . . . . . . . . . 12 ⊢ (𝜑 → (-((𝐵 / 3)↑3) + 𝐷) = (𝐷 + -((𝐵 / 3)↑3)))
281	235, 192	eqeltrrd 2839	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) ∈ ℂ)
282	250, 275	subcld 11189	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3)) ∈ ℂ)
283	281, 282, 31	addassd 10855	. . . . . . . . . . . 12 ⊢ (𝜑 → (((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + (((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3))) + 𝐷) = ((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + ((((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3)) + 𝐷)))
284	278, 280, 283	3eqtr3d 2785	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐷 + -((𝐵 / 3)↑3)) = ((((𝐵 · 𝐶) / 3) − ((𝐵↑3) / 9)) + ((((2 · (𝐵↑3)) / ;27) − ((𝐵 · 𝐶) / 3)) + 𝐷)))
285	31, 184	negsubd 11195	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐷 + -((𝐵 / 3)↑3)) = (𝐷 − ((𝐵 / 3)↑3)))
286	248, 284, 285	3eqtr2d 2783	. . . . . . . . . 10 ⊢ (𝜑 → ((-(𝑀 / 3) · (𝐵 / 3)) + (𝑁 / ;27)) = (𝐷 − ((𝐵 / 3)↑3)))
287	218, 286	oveq12d 7231	. . . . . . . . 9 ⊢ (𝜑 → ((-(𝑀 / 3) · 𝑋) + ((-(𝑀 / 3) · (𝐵 / 3)) + (𝑁 / ;27))) = (((𝐶 · 𝑋) − (3 · (𝑋 · ((𝐵 / 3)↑2)))) + (𝐷 − ((𝐵 / 3)↑3))))
288	190, 193, 287	3eqtrd 2781	. . . . . . . 8 ⊢ (𝜑 → ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27)) = (((𝐶 · 𝑋) − (3 · (𝑋 · ((𝐵 / 3)↑2)))) + (𝐷 − ((𝐵 / 3)↑3))))
289	5, 40	mulcld 10853	. . . . . . . . 9 ⊢ (𝜑 → (𝐶 · 𝑋) ∈ ℂ)
290	289, 31, 182, 184	addsub4d 11236	. . . . . . . 8 ⊢ (𝜑 → (((𝐶 · 𝑋) + 𝐷) − ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))) = (((𝐶 · 𝑋) − (3 · (𝑋 · ((𝐵 / 3)↑2)))) + (𝐷 − ((𝐵 / 3)↑3))))
291	288, 290	eqtr4d 2780	. . . . . . 7 ⊢ (𝜑 → ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27)) = (((𝐶 · 𝑋) + 𝐷) − ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3))))
292	291	oveq2d 7229	. . . . . 6 ⊢ (𝜑 → (((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27))) = (((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) + (((𝐶 · 𝑋) + 𝐷) − ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)))))
293	289, 31	addcld 10852	. . . . . . 7 ⊢ (𝜑 → ((𝐶 · 𝑋) + 𝐷) ∈ ℂ)
294	185, 293	pncan3d 11192	. . . . . 6 ⊢ (𝜑 → (((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) + (((𝐶 · 𝑋) + 𝐷) − ((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)))) = ((𝐶 · 𝑋) + 𝐷))
295	292, 294	eqtrd 2777	. . . . 5 ⊢ (𝜑 → (((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27))) = ((𝐶 · 𝑋) + 𝐷))
296	295	oveq2d 7229	. . . 4 ⊢ (𝜑 → (((𝑋↑3) + (𝐵 · (𝑋↑2))) + (((3 · (𝑋 · ((𝐵 / 3)↑2))) + ((𝐵 / 3)↑3)) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27)))) = (((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((𝐶 · 𝑋) + 𝐷)))
297	175, 188, 296	3eqtrd 2781	. . 3 ⊢ (𝜑 → (((𝑋 + (𝐵 / 3))↑3) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27))) = (((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((𝐶 · 𝑋) + 𝐷)))
298	297	eqeq1d 2739	. 2 ⊢ (𝜑 → ((((𝑋 + (𝐵 / 3))↑3) + ((-(𝑀 / 3) · (𝑋 + (𝐵 / 3))) + (𝑁 / ;27))) = 0 ↔ (((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((𝐶 · 𝑋) + 𝐷)) = 0))
299		oveq1 7220	. . . . . . . 8 ⊢ (𝑟 = 0 → (𝑟↑3) = (0↑3))
300		0exp 13670	. . . . . . . . 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 11901	. . . . . . . 8 ⊢ 0 ≠ 1
304	303	a1i 11	. . . . . . 7 ⊢ (𝑟 = 0 → 0 ≠ 1)
305	302, 304	eqnetrd 3008	. . . . . 6 ⊢ (𝑟 = 0 → (𝑟↑3) ≠ 1)
306	305	necon2i 2975	. . . . 5 ⊢ ((𝑟↑3) = 1 → 𝑟 ≠ 0)
307		eqcom 2744	. . . . . . . 8 ⊢ (𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) ↔ -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = 𝑋)
308	2	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝐵 ∈ ℂ)
309		simprl 771	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑟 ∈ ℂ)
310	43	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑇 ∈ ℂ)
311	309, 310	mulcld 10853	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑟 · 𝑇) ∈ ℂ)
312	9	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑀 ∈ ℂ)
313		simprr 773	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑟 ≠ 0)
314	160	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑇 ≠ 0)
315	309, 310, 313, 314	mulne0d 11484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑟 · 𝑇) ≠ 0)
316	312, 311, 315	divcld 11608	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑀 / (𝑟 · 𝑇)) ∈ ℂ)
317	311, 316	addcld 10852	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) ∈ ℂ)
318	4	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 3 ∈ ℂ)
319	11	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 3 ≠ 0)
320	308, 317, 318, 319	divdird 11646	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝐵 + ((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇)))) / 3) = ((𝐵 / 3) + (((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)))
321	308, 311, 316	addassd 10855	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) = (𝐵 + ((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇)))))
322	321	oveq1d 7228	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = ((𝐵 + ((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇)))) / 3))
323	41	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝐵 / 3) ∈ ℂ)
324	317, 318, 319	divcld 11608	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) ∈ ℂ)
325	323, 324	subnegd 11196	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝐵 / 3) − -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)) = ((𝐵 / 3) + (((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)))
326	320, 322, 325	3eqtr4d 2787	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = ((𝐵 / 3) − -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)))
327	326	negeqd 11072	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = -((𝐵 / 3) − -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)))
328	324	negcld 11176	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) ∈ ℂ)
329	323, 328	negsubdi2d 11205	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -((𝐵 / 3) − -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)) = (-(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) − (𝐵 / 3)))
330	327, 329	eqtrd 2777	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = (-(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) − (𝐵 / 3)))
331	330	eqeq1d 2739	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (-(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) = 𝑋 ↔ (-(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) − (𝐵 / 3)) = 𝑋))
332	307, 331	syl5bb 286	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3) ↔ (-(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) − (𝐵 / 3)) = 𝑋))
333	40	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → 𝑋 ∈ ℂ)
334	328, 323, 333	subadd2d 11208	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((-(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) − (𝐵 / 3)) = 𝑋 ↔ (𝑋 + (𝐵 / 3)) = -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3)))
335	311, 316, 318, 319	divdird 11646	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) = (((𝑟 · 𝑇) / 3) + ((𝑀 / (𝑟 · 𝑇)) / 3)))
336	335	negeqd 11072	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) = -(((𝑟 · 𝑇) / 3) + ((𝑀 / (𝑟 · 𝑇)) / 3)))
337	311, 318, 319	divcld 11608	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑟 · 𝑇) / 3) ∈ ℂ)
338	316, 318, 319	divcld 11608	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑀 / (𝑟 · 𝑇)) / 3) ∈ ℂ)
339	337, 338	negdi2d 11203	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝑟 · 𝑇) / 3) + ((𝑀 / (𝑟 · 𝑇)) / 3)) = (-((𝑟 · 𝑇) / 3) − ((𝑀 / (𝑟 · 𝑇)) / 3)))
340	309, 310, 318, 319	divassd 11643	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑟 · 𝑇) / 3) = (𝑟 · (𝑇 / 3)))
341	340	negeqd 11072	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -((𝑟 · 𝑇) / 3) = -(𝑟 · (𝑇 / 3)))
342	44	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑇 / 3) ∈ ℂ)
343	309, 342	mulneg2d 11286	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑟 · -(𝑇 / 3)) = -(𝑟 · (𝑇 / 3)))
344	341, 343	eqtr4d 2780	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -((𝑟 · 𝑇) / 3) = (𝑟 · -(𝑇 / 3)))
345	312, 311, 318, 315, 319	divdiv32d 11633	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑀 / (𝑟 · 𝑇)) / 3) = ((𝑀 / 3) / (𝑟 · 𝑇)))
346	13	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑀 / 3) ∈ ℂ)
347	346, 311, 318, 315, 319	divcan7d 11636	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝑀 / 3) / 3) / ((𝑟 · 𝑇) / 3)) = ((𝑀 / 3) / (𝑟 · 𝑇)))
348	155	oveq1d 7228	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝑀 / 3) / 3) / ((𝑟 · 𝑇) / 3)) = ((𝑀 / 9) / ((𝑟 · 𝑇) / 3)))
349	348	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (((𝑀 / 3) / 3) / ((𝑟 · 𝑇) / 3)) = ((𝑀 / 9) / ((𝑟 · 𝑇) / 3)))
350	345, 347, 349	3eqtr2d 2783	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑀 / (𝑟 · 𝑇)) / 3) = ((𝑀 / 9) / ((𝑟 · 𝑇) / 3)))
351	119	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (𝑀 / 9) ∈ ℂ)
352	311, 318, 315, 319	divne0d 11624	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑟 · 𝑇) / 3) ≠ 0)
353	351, 337, 352	div2negd 11623	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (-(𝑀 / 9) / -((𝑟 · 𝑇) / 3)) = ((𝑀 / 9) / ((𝑟 · 𝑇) / 3)))
354	344	oveq2d 7229	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (-(𝑀 / 9) / -((𝑟 · 𝑇) / 3)) = (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3))))
355	350, 353, 354	3eqtr2d 2783	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑀 / (𝑟 · 𝑇)) / 3) = (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3))))
356	344, 355	oveq12d 7231	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → (-((𝑟 · 𝑇) / 3) − ((𝑀 / (𝑟 · 𝑇)) / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))))
357	336, 339, 356	3eqtrd 2781	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))))
358	357	eqeq2d 2748	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑋 + (𝐵 / 3)) = -(((𝑟 · 𝑇) + (𝑀 / (𝑟 · 𝑇))) / 3) ↔ (𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3))))))
359	332, 334, 358	3bitrrd 309	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℂ ∧ 𝑟 ≠ 0)) → ((𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))) ↔ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3)))
360	359	anassrs 471	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ 𝑟 ≠ 0) → ((𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))) ↔ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3)))
361	306, 360	sylan2 596	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ (𝑟↑3) = 1) → ((𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3)))) ↔ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3)))
362	361	pm5.32da 582	. . 3 ⊢ ((𝜑 ∧ 𝑟 ∈ ℂ) → (((𝑟↑3) = 1 ∧ (𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3))))) ↔ ((𝑟↑3) = 1 ∧ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3))))
363	362	rexbidva 3215	. 2 ⊢ (𝜑 → (∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ (𝑋 + (𝐵 / 3)) = ((𝑟 · -(𝑇 / 3)) − (-(𝑀 / 9) / (𝑟 · -(𝑇 / 3))))) ↔ ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3))))
364	163, 298, 363	3bitr3d 312	1 ⊢ (𝜑 → ((((𝑋↑3) + (𝐵 · (𝑋↑2))) + ((𝐶 · 𝑋) + 𝐷)) = 0 ↔ ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = -(((𝐵 + (𝑟 · 𝑇)) + (𝑀 / (𝑟 · 𝑇))) / 3))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 399 = wceq 1543 ∈ wcel 2110 ≠ wne 2940 ∃wrex 3062 class class class wbr 5053 (class class class)co 7213 ℂcc 10727 0cc0 10729 1c1 10730 + caddc 10732 · cmul 10734 − cmin 11062 -cneg 11063 / cdiv 11489 ℕcn 11830 2c2 11885 3c3 11886 4c4 11887 7c7 11890 9c9 11892 ℕ₀cn0 12090 cdc 12293 ↑cexp 13635 ∥ cdvds 15815

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2708 ax-sep 5192 ax-nul 5199 ax-pow 5258 ax-pr 5322 ax-un 7523 ax-cnex 10785 ax-resscn 10786 ax-1cn 10787 ax-icn 10788 ax-addcl 10789 ax-addrcl 10790 ax-mulcl 10791 ax-mulrcl 10792 ax-mulcom 10793 ax-addass 10794 ax-mulass 10795 ax-distr 10796 ax-i2m1 10797 ax-1ne0 10798 ax-1rid 10799 ax-rnegex 10800 ax-rrecex 10801 ax-cnre 10802 ax-pre-lttri 10803 ax-pre-lttrn 10804 ax-pre-ltadd 10805 ax-pre-mulgt0 10806 ax-pre-sup 10807

This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2071 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2886 df-ne 2941 df-nel 3047 df-ral 3066 df-rex 3067 df-reu 3068 df-rmo 3069 df-rab 3070 df-v 3410 df-sbc 3695 df-csb 3812 df-dif 3869 df-un 3871 df-in 3873 df-ss 3883 df-pss 3885 df-nul 4238 df-if 4440 df-pw 4515 df-sn 4542 df-pr 4544 df-tp 4546 df-op 4548 df-uni 4820 df-iun 4906 df-br 5054 df-opab 5116 df-mpt 5136 df-tr 5162 df-id 5455 df-eprel 5460 df-po 5468 df-so 5469 df-fr 5509 df-we 5511 df-xp 5557 df-rel 5558 df-cnv 5559 df-co 5560 df-dm 5561 df-rn 5562 df-res 5563 df-ima 5564 df-pred 6160 df-ord 6216 df-on 6217 df-lim 6218 df-suc 6219 df-iota 6338 df-fun 6382 df-fn 6383 df-f 6384 df-f1 6385 df-fo 6386 df-f1o 6387 df-fv 6388 df-riota 7170 df-ov 7216 df-oprab 7217 df-mpo 7218 df-om 7645 df-2nd 7762 df-wrecs 8047 df-recs 8108 df-rdg 8146 df-er 8391 df-en 8627 df-dom 8628 df-sdom 8629 df-sup 9058 df-pnf 10869 df-mnf 10870 df-xr 10871 df-ltxr 10872 df-le 10873 df-sub 11064 df-neg 11065 df-div 11490 df-nn 11831 df-2 11893 df-3 11894 df-4 11895 df-5 11896 df-6 11897 df-7 11898 df-8 11899 df-9 11900 df-n0 12091 df-z 12177 df-dec 12294 df-uz 12439 df-rp 12587 df-seq 13575 df-exp 13636 df-cj 14662 df-re 14663 df-im 14664 df-sqrt 14798 df-abs 14799 df-dvds 15816

This theorem is referenced by: cubic2 25731 quart 25744

W3C validator