dcubic - Metamath Proof Explorer

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

Theorem dcubic 26835

Description: Solutions to the depressed cubic, a special case of cubic 26838. (The definitions of 𝑀, 𝑁, 𝐺, 𝑇 here differ from mcubic 26836 by scale factors of -9, 54, 54 and -27 respectively, to simplify the algebra and presentation.) (Contributed by Mario Carneiro, 26-Apr-2015.)

**Hypotheses**
Ref	Expression
dcubic.c	⊢ (𝜑 → 𝑃 ∈ ℂ)
dcubic.d	⊢ (𝜑 → 𝑄 ∈ ℂ)
dcubic.x	⊢ (𝜑 → 𝑋 ∈ ℂ)
dcubic.t	⊢ (𝜑 → 𝑇 ∈ ℂ)
dcubic.3	⊢ (𝜑 → (𝑇↑3) = (𝐺 − 𝑁))
dcubic.g	⊢ (𝜑 → 𝐺 ∈ ℂ)
dcubic.2	⊢ (𝜑 → (𝐺↑2) = ((𝑁↑2) + (𝑀↑3)))
dcubic.m	⊢ (𝜑 → 𝑀 = (𝑃 / 3))
dcubic.n	⊢ (𝜑 → 𝑁 = (𝑄 / 2))
dcubic.0	⊢ (𝜑 → 𝑇 ≠ 0)

**Assertion**
Ref	Expression
dcubic	⊢ (𝜑 → (((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0 ↔ ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))))

Distinct variable groups: 𝑀,𝑟 𝑃,𝑟 𝜑,𝑟 𝑄,𝑟 𝑇,𝑟 𝑋,𝑟 Allowed substitution hints: 𝐺(𝑟) 𝑁(𝑟)

Proof of Theorem dcubic Dummy variable 𝑢 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dcubic.0	. . . . . . 7 ⊢ (𝜑 → 𝑇 ≠ 0)
2	1	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) → 𝑇 ≠ 0)
3		dcubic.t	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 ∈ ℂ)
4	3	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) → 𝑇 ∈ ℂ)
5		3z 12558	. . . . . . . . . 10 ⊢ 3 ∈ ℤ
6		expne0i 14054	. . . . . . . . . 10 ⊢ ((𝑇 ∈ ℂ ∧ 𝑇 ≠ 0 ∧ 3 ∈ ℤ) → (𝑇↑3) ≠ 0)
7	5, 6	mp3an3 1458	. . . . . . . . 9 ⊢ ((𝑇 ∈ ℂ ∧ 𝑇 ≠ 0) → (𝑇↑3) ≠ 0)
8	7	ex 413	. . . . . . . 8 ⊢ (𝑇 ∈ ℂ → (𝑇 ≠ 0 → (𝑇↑3) ≠ 0))
9	4, 8	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) → (𝑇 ≠ 0 → (𝑇↑3) ≠ 0))
10		dcubic.3	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑇↑3) = (𝐺 − 𝑁))
11	10	ad2antrr 732	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑇↑3) = (𝐺 − 𝑁))
12		dcubic.g	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐺 ∈ ℂ)
13	12	ad2antrr 732	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝐺 ∈ ℂ)
14		dcubic.2	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐺↑2) = ((𝑁↑2) + (𝑀↑3)))
15	14	ad2antrr 732	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝐺↑2) = ((𝑁↑2) + (𝑀↑3)))
16		dcubic.n	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑁 = (𝑄 / 2))
17	16	ad2antrr 732	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝑁 = (𝑄 / 2))
18		simprl 776	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝑋 = 0)
19	18	oveq2d 7379	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑃 · 𝑋) = (𝑃 · 0))
20		dcubic.c	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑃 ∈ ℂ)
21	20	ad2antrr 732	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝑃 ∈ ℂ)
22	21	mul01d 11343	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑃 · 0) = 0)
23	19, 22	eqtrd 2775	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑃 · 𝑋) = 0)
24	23	oveq1d 7378	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑃 · 𝑋) + 𝑄) = (0 + 𝑄))
25	18	oveq1d 7378	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑋↑3) = (0↑3))
26		3nn 12258	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 3 ∈ ℕ
27		0exp 14057	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (3 ∈ ℕ → (0↑3) = 0)
28	26, 27	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (0↑3) = 0
29	25, 28	eqtrdi 2791	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑋↑3) = 0)
30	29	oveq1d 7378	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = (0 + ((𝑃 · 𝑋) + 𝑄)))
31		simplr 774	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0)
32		0cnd 11135	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 0 ∈ ℂ)
33	23, 32	eqeltrd 2840	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑃 · 𝑋) ∈ ℂ)
34		dcubic.d	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑄 ∈ ℂ)
35	34	ad2antrr 732	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝑄 ∈ ℂ)
36	33, 35	addcld 11162	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑃 · 𝑋) + 𝑄) ∈ ℂ)
37	36	addlidd 11345	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (0 + ((𝑃 · 𝑋) + 𝑄)) = ((𝑃 · 𝑋) + 𝑄))
38	30, 31, 37	3eqtr3rd 2784	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑃 · 𝑋) + 𝑄) = 0)
39	35	addlidd 11345	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (0 + 𝑄) = 𝑄)
40	24, 38, 39	3eqtr3rd 2784	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝑄 = 0)
41	40	oveq1d 7378	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑄 / 2) = (0 / 2))
42		2cn 12254	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ∈ ℂ
43		2ne0 12283	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ≠ 0
44	42, 43	div0i 11887	. . . . . . . . . . . . . . . . . . 19 ⊢ (0 / 2) = 0
45	41, 44	eqtrdi 2791	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑄 / 2) = 0)
46	17, 45	eqtrd 2775	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝑁 = 0)
47	46	sq0id 14154	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑁↑2) = 0)
48		dcubic.m	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑀 = (𝑃 / 3))
49		3cn 12260	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 3 ∈ ℂ
50	49	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 3 ∈ ℂ)
51		3ne0 12285	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 3 ≠ 0
52	51	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 3 ≠ 0)
53	20, 50, 52	divcld 11929	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑃 / 3) ∈ ℂ)
54	48, 53	eqeltrd 2840	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑀 ∈ ℂ)
55	54	ad2antrr 732	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝑀 ∈ ℂ)
56		4cn 12264	. . . . . . . . . . . . . . . . . . . 20 ⊢ 4 ∈ ℂ
57	56	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 4 ∈ ℂ)
58		4ne0 12287	. . . . . . . . . . . . . . . . . . . 20 ⊢ 4 ≠ 0
59	58	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 4 ≠ 0)
60	18	sq0id 14154	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑋↑2) = 0)
61	60	oveq1d 7378	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑋↑2) + (4 · 𝑀)) = (0 + (4 · 𝑀)))
62		dcubic.x	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑋 ∈ ℂ)
63	62	sqcld 14104	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑋↑2) ∈ ℂ)
64		mulcl 11120	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((4 ∈ ℂ ∧ 𝑀 ∈ ℂ) → (4 · 𝑀) ∈ ℂ)
65	56, 54, 64	sylancr 593	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (4 · 𝑀) ∈ ℂ)
66	63, 65	addcld 11162	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝑋↑2) + (4 · 𝑀)) ∈ ℂ)
67	66	ad2antrr 732	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑋↑2) + (4 · 𝑀)) ∈ ℂ)
68		simprr 778	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (√‘((𝑋↑2) + (4 · 𝑀))) = 0)
69	67, 68	sqr00d 15404	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑋↑2) + (4 · 𝑀)) = 0)
70	65	ad2antrr 732	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (4 · 𝑀) ∈ ℂ)
71	70	addlidd 11345	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (0 + (4 · 𝑀)) = (4 · 𝑀))
72	61, 69, 71	3eqtr3rd 2784	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (4 · 𝑀) = 0)
73	56	mul01i 11334	. . . . . . . . . . . . . . . . . . . 20 ⊢ (4 · 0) = 0
74	72, 73	eqtr4di 2793	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (4 · 𝑀) = (4 · 0))
75	55, 32, 57, 59, 74	mulcanad 11783	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝑀 = 0)
76	75	oveq1d 7378	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑀↑3) = (0↑3))
77	76, 28	eqtrdi 2791	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑀↑3) = 0)
78	47, 77	oveq12d 7381	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑁↑2) + (𝑀↑3)) = (0 + 0))
79		00id 11319	. . . . . . . . . . . . . . 15 ⊢ (0 + 0) = 0
80	78, 79	eqtrdi 2791	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑁↑2) + (𝑀↑3)) = 0)
81	15, 80	eqtrd 2775	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝐺↑2) = 0)
82	13, 81	sqeq0d 14105	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝐺 = 0)
83	82, 46	oveq12d 7381	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝐺 − 𝑁) = (0 − 0))
84		0m0e0 12294	. . . . . . . . . . 11 ⊢ (0 − 0) = 0
85	83, 84	eqtrdi 2791	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝐺 − 𝑁) = 0)
86	11, 85	eqtrd 2775	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑇↑3) = 0)
87	86	ex 413	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) → ((𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0) → (𝑇↑3) = 0))
88	87	necon3ad 2948	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) → ((𝑇↑3) ≠ 0 → ¬ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)))
89	9, 88	syld 47	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) → (𝑇 ≠ 0 → ¬ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)))
90	2, 89	mpd 15	. . . . 5 ⊢ ((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) → ¬ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0))
91		oveq12 7372	. . . . . . . . . . 11 ⊢ ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0 ∧ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0) → (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) + ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = (0 + 0))
92	91, 79	eqtrdi 2791	. . . . . . . . . 10 ⊢ ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0 ∧ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0) → (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) + ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = 0)
93		oveq12 7372	. . . . . . . . . . 11 ⊢ ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0 ∧ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0) → (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) − ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = (0 − 0))
94	93, 84	eqtrdi 2791	. . . . . . . . . 10 ⊢ ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0 ∧ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0) → (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) − ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = 0)
95	92, 94	jca 516	. . . . . . . . 9 ⊢ ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0 ∧ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0) → ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) + ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = 0 ∧ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) − ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = 0))
96	66	sqrtcld 15400	. . . . . . . . . . . . 13 ⊢ (𝜑 → (√‘((𝑋↑2) + (4 · 𝑀))) ∈ ℂ)
97		halfaddsub 12408	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∈ ℂ ∧ (√‘((𝑋↑2) + (4 · 𝑀))) ∈ ℂ) → ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) + ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = 𝑋 ∧ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) − ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = (√‘((𝑋↑2) + (4 · 𝑀)))))
98	62, 96, 97	syl2anc 590	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) + ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = 𝑋 ∧ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) − ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = (√‘((𝑋↑2) + (4 · 𝑀)))))
99	98	simpld 495	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) + ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = 𝑋)
100	99	eqeq1d 2742	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) + ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = 0 ↔ 𝑋 = 0))
101	98	simprd 496	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) − ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = (√‘((𝑋↑2) + (4 · 𝑀))))
102	101	eqeq1d 2742	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) − ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = 0 ↔ (√‘((𝑋↑2) + (4 · 𝑀))) = 0))
103	100, 102	anbi12d 638	. . . . . . . . 9 ⊢ (𝜑 → (((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) + ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = 0 ∧ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) − ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = 0) ↔ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)))
104	95, 103	imbitrid 245	. . . . . . . 8 ⊢ (𝜑 → ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0 ∧ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0) → (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)))
105	104	con3d 152	. . . . . . 7 ⊢ (𝜑 → (¬ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0) → ¬ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0 ∧ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0)))
106		eldifi 4068	. . . . . . . . . . . . . 14 ⊢ (𝑢 ∈ (ℂ ∖ {0}) → 𝑢 ∈ ℂ)
107	106	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → 𝑢 ∈ ℂ)
108	54	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → 𝑀 ∈ ℂ)
109		eldifsni 4730	. . . . . . . . . . . . . . 15 ⊢ (𝑢 ∈ (ℂ ∖ {0}) → 𝑢 ≠ 0)
110	109	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → 𝑢 ≠ 0)
111	108, 107, 110	divcld 11929	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑀 / 𝑢) ∈ ℂ)
112	62	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → 𝑋 ∈ ℂ)
113	107, 111, 112	subaddd 11521	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑢 − (𝑀 / 𝑢)) = 𝑋 ↔ ((𝑀 / 𝑢) + 𝑋) = 𝑢))
114		eqcom 2747	. . . . . . . . . . . 12 ⊢ (𝑋 = (𝑢 − (𝑀 / 𝑢)) ↔ (𝑢 − (𝑀 / 𝑢)) = 𝑋)
115		eqcom 2747	. . . . . . . . . . . 12 ⊢ (𝑢 = ((𝑀 / 𝑢) + 𝑋) ↔ ((𝑀 / 𝑢) + 𝑋) = 𝑢)
116	113, 114, 115	3bitr4g 315	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑋 = (𝑢 − (𝑀 / 𝑢)) ↔ 𝑢 = ((𝑀 / 𝑢) + 𝑋)))
117	107	sqcld 14104	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑢↑2) ∈ ℂ)
118	112, 107	mulcld 11163	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑋 · 𝑢) ∈ ℂ)
119	118, 108	addcld 11162	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑋 · 𝑢) + 𝑀) ∈ ℂ)
120	117, 119	subeq0ad 11513	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (((𝑢↑2) − ((𝑋 · 𝑢) + 𝑀)) = 0 ↔ (𝑢↑2) = ((𝑋 · 𝑢) + 𝑀)))
121	107	sqvald 14103	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑢↑2) = (𝑢 · 𝑢))
122	111, 112, 107	adddird 11168	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (((𝑀 / 𝑢) + 𝑋) · 𝑢) = (((𝑀 / 𝑢) · 𝑢) + (𝑋 · 𝑢)))
123	108, 107, 110	divcan1d 11930	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑀 / 𝑢) · 𝑢) = 𝑀)
124	123	oveq1d 7378	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (((𝑀 / 𝑢) · 𝑢) + (𝑋 · 𝑢)) = (𝑀 + (𝑋 · 𝑢)))
125	108, 118	addcomd 11346	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑀 + (𝑋 · 𝑢)) = ((𝑋 · 𝑢) + 𝑀))
126	122, 124, 125	3eqtrrd 2780	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑋 · 𝑢) + 𝑀) = (((𝑀 / 𝑢) + 𝑋) · 𝑢))
127	121, 126	eqeq12d 2756	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑢↑2) = ((𝑋 · 𝑢) + 𝑀) ↔ (𝑢 · 𝑢) = (((𝑀 / 𝑢) + 𝑋) · 𝑢)))
128	111, 112	addcld 11162	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑀 / 𝑢) + 𝑋) ∈ ℂ)
129	107, 128, 107, 110	mulcan2d 11782	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑢 · 𝑢) = (((𝑀 / 𝑢) + 𝑋) · 𝑢) ↔ 𝑢 = ((𝑀 / 𝑢) + 𝑋)))
130	120, 127, 129	3bitrd 306	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (((𝑢↑2) − ((𝑋 · 𝑢) + 𝑀)) = 0 ↔ 𝑢 = ((𝑀 / 𝑢) + 𝑋)))
131		1cnd 11137	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → 1 ∈ ℂ)
132		ax-1ne0 11105	. . . . . . . . . . . . . 14 ⊢ 1 ≠ 0
133	132	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → 1 ≠ 0)
134	62	negcld 11490	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -𝑋 ∈ ℂ)
135	134	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → -𝑋 ∈ ℂ)
136	54	negcld 11490	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -𝑀 ∈ ℂ)
137	136	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → -𝑀 ∈ ℂ)
138		sqneg 14075	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 ∈ ℂ → (-𝑋↑2) = (𝑋↑2))
139	112, 138	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (-𝑋↑2) = (𝑋↑2))
140	137	mullidd 11161	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (1 · -𝑀) = -𝑀)
141	140	oveq2d 7379	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (4 · (1 · -𝑀)) = (4 · -𝑀))
142		mulneg2 11585	. . . . . . . . . . . . . . . . 17 ⊢ ((4 ∈ ℂ ∧ 𝑀 ∈ ℂ) → (4 · -𝑀) = -(4 · 𝑀))
143	56, 108, 142	sylancr 593	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (4 · -𝑀) = -(4 · 𝑀))
144	141, 143	eqtrd 2775	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (4 · (1 · -𝑀)) = -(4 · 𝑀))
145	139, 144	oveq12d 7381	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((-𝑋↑2) − (4 · (1 · -𝑀))) = ((𝑋↑2) − -(4 · 𝑀)))
146	63	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑋↑2) ∈ ℂ)
147	65	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (4 · 𝑀) ∈ ℂ)
148	146, 147	subnegd 11510	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑋↑2) − -(4 · 𝑀)) = ((𝑋↑2) + (4 · 𝑀)))
149	145, 148	eqtr2d 2776	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑋↑2) + (4 · 𝑀)) = ((-𝑋↑2) − (4 · (1 · -𝑀))))
150	131, 133, 135, 137, 107, 149	quad 26829	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (((1 · (𝑢↑2)) + ((-𝑋 · 𝑢) + -𝑀)) = 0 ↔ (𝑢 = ((--𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / (2 · 1)) ∨ 𝑢 = ((--𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / (2 · 1)))))
151	117	mullidd 11161	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (1 · (𝑢↑2)) = (𝑢↑2))
152	112, 107	mulneg1d 11601	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (-𝑋 · 𝑢) = -(𝑋 · 𝑢))
153	152	oveq1d 7378	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((-𝑋 · 𝑢) + -𝑀) = (-(𝑋 · 𝑢) + -𝑀))
154	118, 108	negdid 11516	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → -((𝑋 · 𝑢) + 𝑀) = (-(𝑋 · 𝑢) + -𝑀))
155	153, 154	eqtr4d 2778	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((-𝑋 · 𝑢) + -𝑀) = -((𝑋 · 𝑢) + 𝑀))
156	151, 155	oveq12d 7381	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((1 · (𝑢↑2)) + ((-𝑋 · 𝑢) + -𝑀)) = ((𝑢↑2) + -((𝑋 · 𝑢) + 𝑀)))
157	117, 119	negsubd 11509	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑢↑2) + -((𝑋 · 𝑢) + 𝑀)) = ((𝑢↑2) − ((𝑋 · 𝑢) + 𝑀)))
158	156, 157	eqtrd 2775	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((1 · (𝑢↑2)) + ((-𝑋 · 𝑢) + -𝑀)) = ((𝑢↑2) − ((𝑋 · 𝑢) + 𝑀)))
159	158	eqeq1d 2742	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (((1 · (𝑢↑2)) + ((-𝑋 · 𝑢) + -𝑀)) = 0 ↔ ((𝑢↑2) − ((𝑋 · 𝑢) + 𝑀)) = 0))
160	112	negnegd 11494	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → --𝑋 = 𝑋)
161	160	oveq1d 7378	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (--𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) = (𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))))
162		2t1e2 12337	. . . . . . . . . . . . . . . 16 ⊢ (2 · 1) = 2
163	162	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (2 · 1) = 2)
164	161, 163	oveq12d 7381	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((--𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / (2 · 1)) = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2))
165	164	eqeq2d 2751	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑢 = ((--𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / (2 · 1)) ↔ 𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)))
166	160	oveq1d 7378	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (--𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) = (𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))))
167	166, 163	oveq12d 7381	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((--𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / (2 · 1)) = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2))
168	167	eqeq2d 2751	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑢 = ((--𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / (2 · 1)) ↔ 𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)))
169	165, 168	orbi12d 924	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑢 = ((--𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / (2 · 1)) ∨ 𝑢 = ((--𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / (2 · 1))) ↔ (𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∨ 𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2))))
170	150, 159, 169	3bitr3d 310	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (((𝑢↑2) − ((𝑋 · 𝑢) + 𝑀)) = 0 ↔ (𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∨ 𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2))))
171	116, 130, 170	3bitr2d 308	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑋 = (𝑢 − (𝑀 / 𝑢)) ↔ (𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∨ 𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2))))
172	171	rexbidva 3162	. . . . . . . . 9 ⊢ (𝜑 → (∃𝑢 ∈ (ℂ ∖ {0})𝑋 = (𝑢 − (𝑀 / 𝑢)) ↔ ∃𝑢 ∈ (ℂ ∖ {0})(𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∨ 𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2))))
173		r19.43 3108	. . . . . . . . 9 ⊢ (∃𝑢 ∈ (ℂ ∖ {0})(𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∨ 𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) ↔ (∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∨ ∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)))
174	172, 173	bitrdi 288	. . . . . . . 8 ⊢ (𝜑 → (∃𝑢 ∈ (ℂ ∖ {0})𝑋 = (𝑢 − (𝑀 / 𝑢)) ↔ (∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∨ ∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2))))
175		risset 3215	. . . . . . . . . . 11 ⊢ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ (ℂ ∖ {0}) ↔ ∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2))
176	62, 96	addcld 11162	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) ∈ ℂ)
177	176	halfcld 12420	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ ℂ)
178		eldifsn 4726	. . . . . . . . . . . . 13 ⊢ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ (ℂ ∖ {0}) ↔ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ ℂ ∧ ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0))
179	178	baib 540	. . . . . . . . . . . 12 ⊢ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ ℂ → (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ (ℂ ∖ {0}) ↔ ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0))
180	177, 179	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ (ℂ ∖ {0}) ↔ ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0))
181	175, 180	bitr3id 286	. . . . . . . . . 10 ⊢ (𝜑 → (∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ↔ ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0))
182		risset 3215	. . . . . . . . . . 11 ⊢ (((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ (ℂ ∖ {0}) ↔ ∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2))
183	62, 96	subcld 11503	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) ∈ ℂ)
184	183	halfcld 12420	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ ℂ)
185		eldifsn 4726	. . . . . . . . . . . . 13 ⊢ (((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ (ℂ ∖ {0}) ↔ (((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ ℂ ∧ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0))
186	185	baib 540	. . . . . . . . . . . 12 ⊢ (((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ ℂ → (((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ (ℂ ∖ {0}) ↔ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0))
187	184, 186	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ (ℂ ∖ {0}) ↔ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0))
188	182, 187	bitr3id 286	. . . . . . . . . 10 ⊢ (𝜑 → (∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ↔ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0))
189	181, 188	orbi12d 924	. . . . . . . . 9 ⊢ (𝜑 → ((∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∨ ∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) ↔ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0 ∨ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0)))
190		neorian 3030	. . . . . . . . 9 ⊢ ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0 ∨ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0) ↔ ¬ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0 ∧ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0))
191	189, 190	bitrdi 288	. . . . . . . 8 ⊢ (𝜑 → ((∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∨ ∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) ↔ ¬ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0 ∧ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0)))
192	174, 191	bitrd 280	. . . . . . 7 ⊢ (𝜑 → (∃𝑢 ∈ (ℂ ∖ {0})𝑋 = (𝑢 − (𝑀 / 𝑢)) ↔ ¬ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0 ∧ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0)))
193	105, 192	sylibrd 260	. . . . . 6 ⊢ (𝜑 → (¬ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0) → ∃𝑢 ∈ (ℂ ∖ {0})𝑋 = (𝑢 − (𝑀 / 𝑢))))
194	193	imp 407	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ∃𝑢 ∈ (ℂ ∖ {0})𝑋 = (𝑢 − (𝑀 / 𝑢)))
195	90, 194	syldan 597	. . . 4 ⊢ ((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) → ∃𝑢 ∈ (ℂ ∖ {0})𝑋 = (𝑢 − (𝑀 / 𝑢)))
196	20	ad2antrr 732	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑃 ∈ ℂ)
197	34	ad2antrr 732	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑄 ∈ ℂ)
198	62	ad2antrr 732	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑋 ∈ ℂ)
199	3	ad2antrr 732	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑇 ∈ ℂ)
200	10	ad2antrr 732	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → (𝑇↑3) = (𝐺 − 𝑁))
201	12	ad2antrr 732	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝐺 ∈ ℂ)
202	14	ad2antrr 732	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → (𝐺↑2) = ((𝑁↑2) + (𝑀↑3)))
203	48	ad2antrr 732	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑀 = (𝑃 / 3))
204	16	ad2antrr 732	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑁 = (𝑄 / 2))
205	1	ad2antrr 732	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑇 ≠ 0)
206	106	ad2antrl 734	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑢 ∈ ℂ)
207	109	ad2antrl 734	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑢 ≠ 0)
208		simprr 778	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑋 = (𝑢 − (𝑀 / 𝑢)))
209		simplr 774	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0)
210	196, 197, 198, 199, 200, 201, 202, 203, 204, 205, 206, 207, 208, 209	dcubic2 26833	. . . 4 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇)))))
211	195, 210	rexlimddv 3147	. . 3 ⊢ ((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) → ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇)))))
212	211	ex 413	. 2 ⊢ (𝜑 → (((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0 → ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))))
213	20	ad2antrr 732	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑃 ∈ ℂ)
214	34	ad2antrr 732	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑄 ∈ ℂ)
215	62	ad2antrr 732	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑋 ∈ ℂ)
216		simplr 774	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑟 ∈ ℂ)
217	3	ad2antrr 732	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑇 ∈ ℂ)
218	216, 217	mulcld 11163	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → (𝑟 · 𝑇) ∈ ℂ)
219		3nn0 12453	. . . . . . 7 ⊢ 3 ∈ ℕ₀
220	219	a1i 11	. . . . . 6 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 3 ∈ ℕ₀)
221	216, 217, 220	mulexpd 14121	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → ((𝑟 · 𝑇)↑3) = ((𝑟↑3) · (𝑇↑3)))
222		simprl 776	. . . . . 6 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → (𝑟↑3) = 1)
223	222	oveq1d 7378	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → ((𝑟↑3) · (𝑇↑3)) = (1 · (𝑇↑3)))
224		expcl 14039	. . . . . . . . 9 ⊢ ((𝑇 ∈ ℂ ∧ 3 ∈ ℕ₀) → (𝑇↑3) ∈ ℂ)
225	3, 219, 224	sylancl 592	. . . . . . . 8 ⊢ (𝜑 → (𝑇↑3) ∈ ℂ)
226	225	mullidd 11161	. . . . . . 7 ⊢ (𝜑 → (1 · (𝑇↑3)) = (𝑇↑3))
227	226, 10	eqtrd 2775	. . . . . 6 ⊢ (𝜑 → (1 · (𝑇↑3)) = (𝐺 − 𝑁))
228	227	ad2antrr 732	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → (1 · (𝑇↑3)) = (𝐺 − 𝑁))
229	221, 223, 228	3eqtrd 2779	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → ((𝑟 · 𝑇)↑3) = (𝐺 − 𝑁))
230	12	ad2antrr 732	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝐺 ∈ ℂ)
231	14	ad2antrr 732	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → (𝐺↑2) = ((𝑁↑2) + (𝑀↑3)))
232	48	ad2antrr 732	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑀 = (𝑃 / 3))
233	16	ad2antrr 732	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑁 = (𝑄 / 2))
234	132	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 1 ≠ 0)
235	222, 234	eqnetrd 3002	. . . . . 6 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → (𝑟↑3) ≠ 0)
236		oveq1 7370	. . . . . . . 8 ⊢ (𝑟 = 0 → (𝑟↑3) = (0↑3))
237	236, 28	eqtrdi 2791	. . . . . . 7 ⊢ (𝑟 = 0 → (𝑟↑3) = 0)
238	237	necon3i 2967	. . . . . 6 ⊢ ((𝑟↑3) ≠ 0 → 𝑟 ≠ 0)
239	235, 238	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑟 ≠ 0)
240	1	ad2antrr 732	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑇 ≠ 0)
241	216, 217, 239, 240	mulne0d 11800	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → (𝑟 · 𝑇) ≠ 0)
242		simprr 778	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))
243	213, 214, 215, 218, 229, 230, 231, 232, 233, 241, 242	dcubic1 26834	. . 3 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0)
244	243	rexlimdva2 3143	. 2 ⊢ (𝜑 → (∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇)))) → ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0))
245	212, 244	impbid 213	1 ⊢ (𝜑 → (((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0 ↔ ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∧ wa 396 ∨ wo 853 = wceq 1547 ∈ wcel 2119 ≠ wne 2935 ∃wrex 3064 ∖ cdif 3887 {csn 4562 ‘cfv 6492 (class class class)co 7363 ℂcc 11034 0cc0 11036 1c1 11037 + caddc 11039 · cmul 11041 − cmin 11375 -cneg 11376 / cdiv 11805 ℕcn 12172 2c2 12234 3c3 12235 4c4 12236 ℕ₀cn0 12435 ℤcz 12522 ↑cexp 14021 √csqrt 15193

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2712 ax-sep 5225 ax-nul 5235 ax-pow 5301 ax-pr 5369 ax-un 7685 ax-cnex 11092 ax-resscn 11093 ax-1cn 11094 ax-icn 11095 ax-addcl 11096 ax-addrcl 11097 ax-mulcl 11098 ax-mulrcl 11099 ax-mulcom 11100 ax-addass 11101 ax-mulass 11102 ax-distr 11103 ax-i2m1 11104 ax-1ne0 11105 ax-1rid 11106 ax-rnegex 11107 ax-rrecex 11108 ax-cnre 11109 ax-pre-lttri 11110 ax-pre-lttrn 11111 ax-pre-ltadd 11112 ax-pre-mulgt0 11113 ax-pre-sup 11114

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2719 df-cleq 2732 df-clel 2815 df-nfc 2889 df-ne 2936 df-nel 3040 df-ral 3055 df-rex 3065 df-rmo 3345 df-reu 3346 df-rab 3393 df-v 3434 df-sbc 3731 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4269 df-if 4462 df-pw 4538 df-sn 4563 df-pr 4565 df-op 4569 df-uni 4846 df-iun 4930 df-br 5080 df-opab 5142 df-mpt 5161 df-tr 5187 df-id 5520 df-eprel 5525 df-po 5533 df-so 5534 df-fr 5578 df-we 5580 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-riota 7320 df-ov 7366 df-oprab 7367 df-mpo 7368 df-om 7814 df-2nd 7939 df-frecs 8228 df-wrecs 8259 df-recs 8308 df-rdg 8346 df-er 8640 df-en 8891 df-dom 8892 df-sdom 8893 df-sup 9352 df-pnf 11179 df-mnf 11180 df-xr 11181 df-ltxr 11182 df-le 11183 df-sub 11377 df-neg 11378 df-div 11806 df-nn 12173 df-2 12242 df-3 12243 df-4 12244 df-n0 12436 df-z 12523 df-uz 12787 df-rp 12941 df-seq 13962 df-exp 14022 df-cj 15059 df-re 15060 df-im 15061 df-sqrt 15195 df-abs 15196 df-dvds 16220

This theorem is referenced by: mcubic 26836

W3C validator