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 25901

Description: Solutions to the depressed cubic, a special case of cubic 25904. (The definitions of 𝑀, 𝑁, 𝐺, 𝑇 here differ from mcubic 25902 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 480	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) → 𝑇 ≠ 0)
3		dcubic.t	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 ∈ ℂ)
4	3	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) → 𝑇 ∈ ℂ)
5		3z 12283	. . . . . . . . . 10 ⊢ 3 ∈ ℤ
6		expne0i 13743	. . . . . . . . . 10 ⊢ ((𝑇 ∈ ℂ ∧ 𝑇 ≠ 0 ∧ 3 ∈ ℤ) → (𝑇↑3) ≠ 0)
7	5, 6	mp3an3 1448	. . . . . . . . 9 ⊢ ((𝑇 ∈ ℂ ∧ 𝑇 ≠ 0) → (𝑇↑3) ≠ 0)
8	7	ex 412	. . . . . . . 8 ⊢ (𝑇 ∈ ℂ → (𝑇 ≠ 0 → (𝑇↑3) ≠ 0))
9	4, 8	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) → (𝑇 ≠ 0 → (𝑇↑3) ≠ 0))
10		dcubic.3	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑇↑3) = (𝐺 − 𝑁))
11	10	ad2antrr 722	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑇↑3) = (𝐺 − 𝑁))
12		dcubic.g	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐺 ∈ ℂ)
13	12	ad2antrr 722	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝐺 ∈ ℂ)
14		dcubic.2	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐺↑2) = ((𝑁↑2) + (𝑀↑3)))
15	14	ad2antrr 722	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝐺↑2) = ((𝑁↑2) + (𝑀↑3)))
16		dcubic.n	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑁 = (𝑄 / 2))
17	16	ad2antrr 722	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝑁 = (𝑄 / 2))
18		simprl 767	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝑋 = 0)
19	18	oveq2d 7271	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑃 · 𝑋) = (𝑃 · 0))
20		dcubic.c	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑃 ∈ ℂ)
21	20	ad2antrr 722	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝑃 ∈ ℂ)
22	21	mul01d 11104	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑃 · 0) = 0)
23	19, 22	eqtrd 2778	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑃 · 𝑋) = 0)
24	23	oveq1d 7270	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑃 · 𝑋) + 𝑄) = (0 + 𝑄))
25	18	oveq1d 7270	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑋↑3) = (0↑3))
26		3nn 11982	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 3 ∈ ℕ
27		0exp 13746	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (3 ∈ ℕ → (0↑3) = 0)
28	26, 27	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (0↑3) = 0
29	25, 28	eqtrdi 2795	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑋↑3) = 0)
30	29	oveq1d 7270	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = (0 + ((𝑃 · 𝑋) + 𝑄)))
31		simplr 765	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0)
32		0cnd 10899	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 0 ∈ ℂ)
33	23, 32	eqeltrd 2839	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑃 · 𝑋) ∈ ℂ)
34		dcubic.d	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑄 ∈ ℂ)
35	34	ad2antrr 722	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝑄 ∈ ℂ)
36	33, 35	addcld 10925	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑃 · 𝑋) + 𝑄) ∈ ℂ)
37	36	addid2d 11106	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (0 + ((𝑃 · 𝑋) + 𝑄)) = ((𝑃 · 𝑋) + 𝑄))
38	30, 31, 37	3eqtr3rd 2787	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑃 · 𝑋) + 𝑄) = 0)
39	35	addid2d 11106	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (0 + 𝑄) = 𝑄)
40	24, 38, 39	3eqtr3rd 2787	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝑄 = 0)
41	40	oveq1d 7270	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑄 / 2) = (0 / 2))
42		2cn 11978	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ∈ ℂ
43		2ne0 12007	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ≠ 0
44	42, 43	div0i 11639	. . . . . . . . . . . . . . . . . . 19 ⊢ (0 / 2) = 0
45	41, 44	eqtrdi 2795	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑄 / 2) = 0)
46	17, 45	eqtrd 2778	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝑁 = 0)
47	46	sq0id 13839	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑁↑2) = 0)
48		dcubic.m	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑀 = (𝑃 / 3))
49		3cn 11984	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 3 ∈ ℂ
50	49	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 3 ∈ ℂ)
51		3ne0 12009	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 3 ≠ 0
52	51	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 3 ≠ 0)
53	20, 50, 52	divcld 11681	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑃 / 3) ∈ ℂ)
54	48, 53	eqeltrd 2839	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑀 ∈ ℂ)
55	54	ad2antrr 722	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝑀 ∈ ℂ)
56		4cn 11988	. . . . . . . . . . . . . . . . . . . 20 ⊢ 4 ∈ ℂ
57	56	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 4 ∈ ℂ)
58		4ne0 12011	. . . . . . . . . . . . . . . . . . . 20 ⊢ 4 ≠ 0
59	58	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 4 ≠ 0)
60	18	sq0id 13839	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑋↑2) = 0)
61	60	oveq1d 7270	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑋↑2) + (4 · 𝑀)) = (0 + (4 · 𝑀)))
62		dcubic.x	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑋 ∈ ℂ)
63	62	sqcld 13790	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑋↑2) ∈ ℂ)
64		mulcl 10886	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((4 ∈ ℂ ∧ 𝑀 ∈ ℂ) → (4 · 𝑀) ∈ ℂ)
65	56, 54, 64	sylancr 586	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (4 · 𝑀) ∈ ℂ)
66	63, 65	addcld 10925	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝑋↑2) + (4 · 𝑀)) ∈ ℂ)
67	66	ad2antrr 722	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑋↑2) + (4 · 𝑀)) ∈ ℂ)
68		simprr 769	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (√‘((𝑋↑2) + (4 · 𝑀))) = 0)
69	67, 68	sqr00d 15081	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑋↑2) + (4 · 𝑀)) = 0)
70	65	ad2antrr 722	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (4 · 𝑀) ∈ ℂ)
71	70	addid2d 11106	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (0 + (4 · 𝑀)) = (4 · 𝑀))
72	61, 69, 71	3eqtr3rd 2787	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (4 · 𝑀) = 0)
73	56	mul01i 11095	. . . . . . . . . . . . . . . . . . . 20 ⊢ (4 · 0) = 0
74	72, 73	eqtr4di 2797	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (4 · 𝑀) = (4 · 0))
75	55, 32, 57, 59, 74	mulcanad 11540	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝑀 = 0)
76	75	oveq1d 7270	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑀↑3) = (0↑3))
77	76, 28	eqtrdi 2795	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑀↑3) = 0)
78	47, 77	oveq12d 7273	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑁↑2) + (𝑀↑3)) = (0 + 0))
79		00id 11080	. . . . . . . . . . . . . . 15 ⊢ (0 + 0) = 0
80	78, 79	eqtrdi 2795	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑁↑2) + (𝑀↑3)) = 0)
81	15, 80	eqtrd 2778	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝐺↑2) = 0)
82	13, 81	sqeq0d 13791	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝐺 = 0)
83	82, 46	oveq12d 7273	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝐺 − 𝑁) = (0 − 0))
84		0m0e0 12023	. . . . . . . . . . 11 ⊢ (0 − 0) = 0
85	83, 84	eqtrdi 2795	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝐺 − 𝑁) = 0)
86	11, 85	eqtrd 2778	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑇↑3) = 0)
87	86	ex 412	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) → ((𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0) → (𝑇↑3) = 0))
88	87	necon3ad 2955	. . . . . . 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 7264	. . . . . . . . . . 11 ⊢ ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0 ∧ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0) → (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) + ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = (0 + 0))
92	91, 79	eqtrdi 2795	. . . . . . . . . 10 ⊢ ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0 ∧ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0) → (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) + ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = 0)
93		oveq12 7264	. . . . . . . . . . 11 ⊢ ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0 ∧ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0) → (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) − ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = (0 − 0))
94	93, 84	eqtrdi 2795	. . . . . . . . . 10 ⊢ ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0 ∧ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0) → (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) − ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = 0)
95	92, 94	jca 511	. . . . . . . . 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 15077	. . . . . . . . . . . . 13 ⊢ (𝜑 → (√‘((𝑋↑2) + (4 · 𝑀))) ∈ ℂ)
97		halfaddsub 12136	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∈ ℂ ∧ (√‘((𝑋↑2) + (4 · 𝑀))) ∈ ℂ) → ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) + ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = 𝑋 ∧ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) − ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = (√‘((𝑋↑2) + (4 · 𝑀)))))
98	62, 96, 97	syl2anc 583	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) + ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = 𝑋 ∧ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) − ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = (√‘((𝑋↑2) + (4 · 𝑀)))))
99	98	simpld 494	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) + ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = 𝑋)
100	99	eqeq1d 2740	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) + ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = 0 ↔ 𝑋 = 0))
101	98	simprd 495	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) − ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = (√‘((𝑋↑2) + (4 · 𝑀))))
102	101	eqeq1d 2740	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) − ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = 0 ↔ (√‘((𝑋↑2) + (4 · 𝑀))) = 0))
103	100, 102	anbi12d 630	. . . . . . . . 9 ⊢ (𝜑 → (((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) + ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = 0 ∧ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) − ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = 0) ↔ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)))
104	95, 103	syl5ib 243	. . . . . . . 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 4057	. . . . . . . . . . . . . 14 ⊢ (𝑢 ∈ (ℂ ∖ {0}) → 𝑢 ∈ ℂ)
107	106	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → 𝑢 ∈ ℂ)
108	54	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → 𝑀 ∈ ℂ)
109		eldifsni 4720	. . . . . . . . . . . . . . 15 ⊢ (𝑢 ∈ (ℂ ∖ {0}) → 𝑢 ≠ 0)
110	109	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → 𝑢 ≠ 0)
111	108, 107, 110	divcld 11681	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑀 / 𝑢) ∈ ℂ)
112	62	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → 𝑋 ∈ ℂ)
113	107, 111, 112	subaddd 11280	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑢 − (𝑀 / 𝑢)) = 𝑋 ↔ ((𝑀 / 𝑢) + 𝑋) = 𝑢))
114		eqcom 2745	. . . . . . . . . . . 12 ⊢ (𝑋 = (𝑢 − (𝑀 / 𝑢)) ↔ (𝑢 − (𝑀 / 𝑢)) = 𝑋)
115		eqcom 2745	. . . . . . . . . . . 12 ⊢ (𝑢 = ((𝑀 / 𝑢) + 𝑋) ↔ ((𝑀 / 𝑢) + 𝑋) = 𝑢)
116	113, 114, 115	3bitr4g 313	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑋 = (𝑢 − (𝑀 / 𝑢)) ↔ 𝑢 = ((𝑀 / 𝑢) + 𝑋)))
117	107	sqcld 13790	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑢↑2) ∈ ℂ)
118	112, 107	mulcld 10926	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑋 · 𝑢) ∈ ℂ)
119	118, 108	addcld 10925	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑋 · 𝑢) + 𝑀) ∈ ℂ)
120	117, 119	subeq0ad 11272	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (((𝑢↑2) − ((𝑋 · 𝑢) + 𝑀)) = 0 ↔ (𝑢↑2) = ((𝑋 · 𝑢) + 𝑀)))
121	107	sqvald 13789	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑢↑2) = (𝑢 · 𝑢))
122	111, 112, 107	adddird 10931	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (((𝑀 / 𝑢) + 𝑋) · 𝑢) = (((𝑀 / 𝑢) · 𝑢) + (𝑋 · 𝑢)))
123	108, 107, 110	divcan1d 11682	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑀 / 𝑢) · 𝑢) = 𝑀)
124	123	oveq1d 7270	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (((𝑀 / 𝑢) · 𝑢) + (𝑋 · 𝑢)) = (𝑀 + (𝑋 · 𝑢)))
125	108, 118	addcomd 11107	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑀 + (𝑋 · 𝑢)) = ((𝑋 · 𝑢) + 𝑀))
126	122, 124, 125	3eqtrrd 2783	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑋 · 𝑢) + 𝑀) = (((𝑀 / 𝑢) + 𝑋) · 𝑢))
127	121, 126	eqeq12d 2754	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑢↑2) = ((𝑋 · 𝑢) + 𝑀) ↔ (𝑢 · 𝑢) = (((𝑀 / 𝑢) + 𝑋) · 𝑢)))
128	111, 112	addcld 10925	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑀 / 𝑢) + 𝑋) ∈ ℂ)
129	107, 128, 107, 110	mulcan2d 11539	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑢 · 𝑢) = (((𝑀 / 𝑢) + 𝑋) · 𝑢) ↔ 𝑢 = ((𝑀 / 𝑢) + 𝑋)))
130	120, 127, 129	3bitrd 304	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (((𝑢↑2) − ((𝑋 · 𝑢) + 𝑀)) = 0 ↔ 𝑢 = ((𝑀 / 𝑢) + 𝑋)))
131		1cnd 10901	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → 1 ∈ ℂ)
132		ax-1ne0 10871	. . . . . . . . . . . . . 14 ⊢ 1 ≠ 0
133	132	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → 1 ≠ 0)
134	62	negcld 11249	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -𝑋 ∈ ℂ)
135	134	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → -𝑋 ∈ ℂ)
136	54	negcld 11249	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -𝑀 ∈ ℂ)
137	136	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → -𝑀 ∈ ℂ)
138		sqneg 13764	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 ∈ ℂ → (-𝑋↑2) = (𝑋↑2))
139	112, 138	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (-𝑋↑2) = (𝑋↑2))
140	137	mulid2d 10924	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (1 · -𝑀) = -𝑀)
141	140	oveq2d 7271	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (4 · (1 · -𝑀)) = (4 · -𝑀))
142		mulneg2 11342	. . . . . . . . . . . . . . . . 17 ⊢ ((4 ∈ ℂ ∧ 𝑀 ∈ ℂ) → (4 · -𝑀) = -(4 · 𝑀))
143	56, 108, 142	sylancr 586	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (4 · -𝑀) = -(4 · 𝑀))
144	141, 143	eqtrd 2778	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (4 · (1 · -𝑀)) = -(4 · 𝑀))
145	139, 144	oveq12d 7273	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((-𝑋↑2) − (4 · (1 · -𝑀))) = ((𝑋↑2) − -(4 · 𝑀)))
146	63	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑋↑2) ∈ ℂ)
147	65	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (4 · 𝑀) ∈ ℂ)
148	146, 147	subnegd 11269	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑋↑2) − -(4 · 𝑀)) = ((𝑋↑2) + (4 · 𝑀)))
149	145, 148	eqtr2d 2779	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑋↑2) + (4 · 𝑀)) = ((-𝑋↑2) − (4 · (1 · -𝑀))))
150	131, 133, 135, 137, 107, 149	quad 25895	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (((1 · (𝑢↑2)) + ((-𝑋 · 𝑢) + -𝑀)) = 0 ↔ (𝑢 = ((--𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / (2 · 1)) ∨ 𝑢 = ((--𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / (2 · 1)))))
151	117	mulid2d 10924	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (1 · (𝑢↑2)) = (𝑢↑2))
152	112, 107	mulneg1d 11358	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (-𝑋 · 𝑢) = -(𝑋 · 𝑢))
153	152	oveq1d 7270	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((-𝑋 · 𝑢) + -𝑀) = (-(𝑋 · 𝑢) + -𝑀))
154	118, 108	negdid 11275	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → -((𝑋 · 𝑢) + 𝑀) = (-(𝑋 · 𝑢) + -𝑀))
155	153, 154	eqtr4d 2781	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((-𝑋 · 𝑢) + -𝑀) = -((𝑋 · 𝑢) + 𝑀))
156	151, 155	oveq12d 7273	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((1 · (𝑢↑2)) + ((-𝑋 · 𝑢) + -𝑀)) = ((𝑢↑2) + -((𝑋 · 𝑢) + 𝑀)))
157	117, 119	negsubd 11268	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑢↑2) + -((𝑋 · 𝑢) + 𝑀)) = ((𝑢↑2) − ((𝑋 · 𝑢) + 𝑀)))
158	156, 157	eqtrd 2778	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((1 · (𝑢↑2)) + ((-𝑋 · 𝑢) + -𝑀)) = ((𝑢↑2) − ((𝑋 · 𝑢) + 𝑀)))
159	158	eqeq1d 2740	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (((1 · (𝑢↑2)) + ((-𝑋 · 𝑢) + -𝑀)) = 0 ↔ ((𝑢↑2) − ((𝑋 · 𝑢) + 𝑀)) = 0))
160	112	negnegd 11253	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → --𝑋 = 𝑋)
161	160	oveq1d 7270	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (--𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) = (𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))))
162		2t1e2 12066	. . . . . . . . . . . . . . . 16 ⊢ (2 · 1) = 2
163	162	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (2 · 1) = 2)
164	161, 163	oveq12d 7273	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((--𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / (2 · 1)) = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2))
165	164	eqeq2d 2749	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑢 = ((--𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / (2 · 1)) ↔ 𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)))
166	160	oveq1d 7270	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (--𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) = (𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))))
167	166, 163	oveq12d 7273	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((--𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / (2 · 1)) = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2))
168	167	eqeq2d 2749	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑢 = ((--𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / (2 · 1)) ↔ 𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)))
169	165, 168	orbi12d 915	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑢 = ((--𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / (2 · 1)) ∨ 𝑢 = ((--𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / (2 · 1))) ↔ (𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∨ 𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2))))
170	150, 159, 169	3bitr3d 308	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (((𝑢↑2) − ((𝑋 · 𝑢) + 𝑀)) = 0 ↔ (𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∨ 𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2))))
171	116, 130, 170	3bitr2d 306	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑋 = (𝑢 − (𝑀 / 𝑢)) ↔ (𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∨ 𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2))))
172	171	rexbidva 3224	. . . . . . . . 9 ⊢ (𝜑 → (∃𝑢 ∈ (ℂ ∖ {0})𝑋 = (𝑢 − (𝑀 / 𝑢)) ↔ ∃𝑢 ∈ (ℂ ∖ {0})(𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∨ 𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2))))
173		r19.43 3277	. . . . . . . . 9 ⊢ (∃𝑢 ∈ (ℂ ∖ {0})(𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∨ 𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) ↔ (∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∨ ∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)))
174	172, 173	bitrdi 286	. . . . . . . 8 ⊢ (𝜑 → (∃𝑢 ∈ (ℂ ∖ {0})𝑋 = (𝑢 − (𝑀 / 𝑢)) ↔ (∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∨ ∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2))))
175		risset 3193	. . . . . . . . . . 11 ⊢ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ (ℂ ∖ {0}) ↔ ∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2))
176	62, 96	addcld 10925	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) ∈ ℂ)
177	176	halfcld 12148	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ ℂ)
178		eldifsn 4717	. . . . . . . . . . . . 13 ⊢ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ (ℂ ∖ {0}) ↔ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ ℂ ∧ ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0))
179	178	baib 535	. . . . . . . . . . . 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 284	. . . . . . . . . 10 ⊢ (𝜑 → (∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ↔ ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0))
182		risset 3193	. . . . . . . . . . 11 ⊢ (((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ (ℂ ∖ {0}) ↔ ∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2))
183	62, 96	subcld 11262	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) ∈ ℂ)
184	183	halfcld 12148	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ ℂ)
185		eldifsn 4717	. . . . . . . . . . . . 13 ⊢ (((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ (ℂ ∖ {0}) ↔ (((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ ℂ ∧ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0))
186	185	baib 535	. . . . . . . . . . . 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 284	. . . . . . . . . 10 ⊢ (𝜑 → (∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ↔ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0))
189	181, 188	orbi12d 915	. . . . . . . . 9 ⊢ (𝜑 → ((∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∨ ∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) ↔ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0 ∨ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0)))
190		neorian 3038	. . . . . . . . 9 ⊢ ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0 ∨ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0) ↔ ¬ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0 ∧ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0))
191	189, 190	bitrdi 286	. . . . . . . 8 ⊢ (𝜑 → ((∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∨ ∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) ↔ ¬ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0 ∧ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0)))
192	174, 191	bitrd 278	. . . . . . 7 ⊢ (𝜑 → (∃𝑢 ∈ (ℂ ∖ {0})𝑋 = (𝑢 − (𝑀 / 𝑢)) ↔ ¬ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0 ∧ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0)))
193	105, 192	sylibrd 258	. . . . . 6 ⊢ (𝜑 → (¬ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0) → ∃𝑢 ∈ (ℂ ∖ {0})𝑋 = (𝑢 − (𝑀 / 𝑢))))
194	193	imp 406	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ∃𝑢 ∈ (ℂ ∖ {0})𝑋 = (𝑢 − (𝑀 / 𝑢)))
195	90, 194	syldan 590	. . . 4 ⊢ ((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) → ∃𝑢 ∈ (ℂ ∖ {0})𝑋 = (𝑢 − (𝑀 / 𝑢)))
196	20	ad2antrr 722	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑃 ∈ ℂ)
197	34	ad2antrr 722	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑄 ∈ ℂ)
198	62	ad2antrr 722	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑋 ∈ ℂ)
199	3	ad2antrr 722	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑇 ∈ ℂ)
200	10	ad2antrr 722	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → (𝑇↑3) = (𝐺 − 𝑁))
201	12	ad2antrr 722	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝐺 ∈ ℂ)
202	14	ad2antrr 722	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → (𝐺↑2) = ((𝑁↑2) + (𝑀↑3)))
203	48	ad2antrr 722	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑀 = (𝑃 / 3))
204	16	ad2antrr 722	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑁 = (𝑄 / 2))
205	1	ad2antrr 722	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑇 ≠ 0)
206	106	ad2antrl 724	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑢 ∈ ℂ)
207	109	ad2antrl 724	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑢 ≠ 0)
208		simprr 769	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑋 = (𝑢 − (𝑀 / 𝑢)))
209		simplr 765	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0)
210	196, 197, 198, 199, 200, 201, 202, 203, 204, 205, 206, 207, 208, 209	dcubic2 25899	. . . 4 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇)))))
211	195, 210	rexlimddv 3219	. . 3 ⊢ ((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) → ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇)))))
212	211	ex 412	. 2 ⊢ (𝜑 → (((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0 → ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))))
213	20	ad2antrr 722	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑃 ∈ ℂ)
214	34	ad2antrr 722	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑄 ∈ ℂ)
215	62	ad2antrr 722	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑋 ∈ ℂ)
216		simplr 765	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑟 ∈ ℂ)
217	3	ad2antrr 722	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑇 ∈ ℂ)
218	216, 217	mulcld 10926	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → (𝑟 · 𝑇) ∈ ℂ)
219		3nn0 12181	. . . . . . 7 ⊢ 3 ∈ ℕ₀
220	219	a1i 11	. . . . . 6 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 3 ∈ ℕ₀)
221	216, 217, 220	mulexpd 13807	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → ((𝑟 · 𝑇)↑3) = ((𝑟↑3) · (𝑇↑3)))
222		simprl 767	. . . . . 6 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → (𝑟↑3) = 1)
223	222	oveq1d 7270	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → ((𝑟↑3) · (𝑇↑3)) = (1 · (𝑇↑3)))
224		expcl 13728	. . . . . . . . 9 ⊢ ((𝑇 ∈ ℂ ∧ 3 ∈ ℕ₀) → (𝑇↑3) ∈ ℂ)
225	3, 219, 224	sylancl 585	. . . . . . . 8 ⊢ (𝜑 → (𝑇↑3) ∈ ℂ)
226	225	mulid2d 10924	. . . . . . 7 ⊢ (𝜑 → (1 · (𝑇↑3)) = (𝑇↑3))
227	226, 10	eqtrd 2778	. . . . . 6 ⊢ (𝜑 → (1 · (𝑇↑3)) = (𝐺 − 𝑁))
228	227	ad2antrr 722	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → (1 · (𝑇↑3)) = (𝐺 − 𝑁))
229	221, 223, 228	3eqtrd 2782	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → ((𝑟 · 𝑇)↑3) = (𝐺 − 𝑁))
230	12	ad2antrr 722	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝐺 ∈ ℂ)
231	14	ad2antrr 722	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → (𝐺↑2) = ((𝑁↑2) + (𝑀↑3)))
232	48	ad2antrr 722	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑀 = (𝑃 / 3))
233	16	ad2antrr 722	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑁 = (𝑄 / 2))
234	132	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 1 ≠ 0)
235	222, 234	eqnetrd 3010	. . . . . 6 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → (𝑟↑3) ≠ 0)
236		oveq1 7262	. . . . . . . 8 ⊢ (𝑟 = 0 → (𝑟↑3) = (0↑3))
237	236, 28	eqtrdi 2795	. . . . . . 7 ⊢ (𝑟 = 0 → (𝑟↑3) = 0)
238	237	necon3i 2975	. . . . . 6 ⊢ ((𝑟↑3) ≠ 0 → 𝑟 ≠ 0)
239	235, 238	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑟 ≠ 0)
240	1	ad2antrr 722	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑇 ≠ 0)
241	216, 217, 239, 240	mulne0d 11557	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → (𝑟 · 𝑇) ≠ 0)
242		simprr 769	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))
243	213, 214, 215, 218, 229, 230, 231, 232, 233, 241, 242	dcubic1 25900	. . 3 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0)
244	243	rexlimdva2 3215	. 2 ⊢ (𝜑 → (∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇)))) → ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0))
245	212, 244	impbid 211	1 ⊢ (𝜑 → (((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0 ↔ ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 ∨ wo 843 = wceq 1539 ∈ wcel 2108 ≠ wne 2942 ∃wrex 3064 ∖ cdif 3880 {csn 4558 ‘cfv 6418 (class class class)co 7255 ℂcc 10800 0cc0 10802 1c1 10803 + caddc 10805 · cmul 10807 − cmin 11135 -cneg 11136 / cdiv 11562 ℕcn 11903 2c2 11958 3c3 11959 4c4 11960 ℕ₀cn0 12163 ℤcz 12249 ↑cexp 13710 √csqrt 14872

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879 ax-pre-sup 10880

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-om 7688 df-2nd 7805 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-er 8456 df-en 8692 df-dom 8693 df-sdom 8694 df-sup 9131 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-div 11563 df-nn 11904 df-2 11966 df-3 11967 df-4 11968 df-n0 12164 df-z 12250 df-uz 12512 df-rp 12660 df-seq 13650 df-exp 13711 df-cj 14738 df-re 14739 df-im 14740 df-sqrt 14874 df-abs 14875 df-dvds 15892

This theorem is referenced by: mcubic 25902

W3C validator