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 25996

Description: Solutions to the depressed cubic, a special case of cubic 25999. (The definitions of 𝑀, 𝑁, 𝐺, 𝑇 here differ from mcubic 25997 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 12353	. . . . . . . . . 10 ⊢ 3 ∈ ℤ
6		expne0i 13815	. . . . . . . . . 10 ⊢ ((𝑇 ∈ ℂ ∧ 𝑇 ≠ 0 ∧ 3 ∈ ℤ) → (𝑇↑3) ≠ 0)
7	5, 6	mp3an3 1449	. . . . . . . . 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 723	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑇↑3) = (𝐺 − 𝑁))
12		dcubic.g	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐺 ∈ ℂ)
13	12	ad2antrr 723	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝐺 ∈ ℂ)
14		dcubic.2	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐺↑2) = ((𝑁↑2) + (𝑀↑3)))
15	14	ad2antrr 723	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝐺↑2) = ((𝑁↑2) + (𝑀↑3)))
16		dcubic.n	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑁 = (𝑄 / 2))
17	16	ad2antrr 723	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝑁 = (𝑄 / 2))
18		simprl 768	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝑋 = 0)
19	18	oveq2d 7291	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑃 · 𝑋) = (𝑃 · 0))
20		dcubic.c	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑃 ∈ ℂ)
21	20	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝑃 ∈ ℂ)
22	21	mul01d 11174	. . . . . . . . . . . . . . . . . . . . . . 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 7290	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑃 · 𝑋) + 𝑄) = (0 + 𝑄))
25	18	oveq1d 7290	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑋↑3) = (0↑3))
26		3nn 12052	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 3 ∈ ℕ
27		0exp 13818	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (3 ∈ ℕ → (0↑3) = 0)
28	26, 27	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (0↑3) = 0
29	25, 28	eqtrdi 2794	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑋↑3) = 0)
30	29	oveq1d 7290	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = (0 + ((𝑃 · 𝑋) + 𝑄)))
31		simplr 766	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0)
32		0cnd 10968	. . . . . . . . . . . . . . . . . . . . . . . . 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 723	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝑄 ∈ ℂ)
36	33, 35	addcld 10994	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑃 · 𝑋) + 𝑄) ∈ ℂ)
37	36	addid2d 11176	. . . . . . . . . . . . . . . . . . . . . 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 11176	. . . . . . . . . . . . . . . . . . . . 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 7290	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑄 / 2) = (0 / 2))
42		2cn 12048	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ∈ ℂ
43		2ne0 12077	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ≠ 0
44	42, 43	div0i 11709	. . . . . . . . . . . . . . . . . . 19 ⊢ (0 / 2) = 0
45	41, 44	eqtrdi 2794	. . . . . . . . . . . . . . . . . 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 13911	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑁↑2) = 0)
48		dcubic.m	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑀 = (𝑃 / 3))
49		3cn 12054	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 3 ∈ ℂ
50	49	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 3 ∈ ℂ)
51		3ne0 12079	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 3 ≠ 0
52	51	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 3 ≠ 0)
53	20, 50, 52	divcld 11751	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑃 / 3) ∈ ℂ)
54	48, 53	eqeltrd 2839	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑀 ∈ ℂ)
55	54	ad2antrr 723	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝑀 ∈ ℂ)
56		4cn 12058	. . . . . . . . . . . . . . . . . . . 20 ⊢ 4 ∈ ℂ
57	56	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 4 ∈ ℂ)
58		4ne0 12081	. . . . . . . . . . . . . . . . . . . 20 ⊢ 4 ≠ 0
59	58	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 4 ≠ 0)
60	18	sq0id 13911	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑋↑2) = 0)
61	60	oveq1d 7290	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑋↑2) + (4 · 𝑀)) = (0 + (4 · 𝑀)))
62		dcubic.x	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑋 ∈ ℂ)
63	62	sqcld 13862	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑋↑2) ∈ ℂ)
64		mulcl 10955	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((4 ∈ ℂ ∧ 𝑀 ∈ ℂ) → (4 · 𝑀) ∈ ℂ)
65	56, 54, 64	sylancr 587	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (4 · 𝑀) ∈ ℂ)
66	63, 65	addcld 10994	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝑋↑2) + (4 · 𝑀)) ∈ ℂ)
67	66	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑋↑2) + (4 · 𝑀)) ∈ ℂ)
68		simprr 770	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (√‘((𝑋↑2) + (4 · 𝑀))) = 0)
69	67, 68	sqr00d 15153	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑋↑2) + (4 · 𝑀)) = 0)
70	65	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (4 · 𝑀) ∈ ℂ)
71	70	addid2d 11176	. . . . . . . . . . . . . . . . . . . . 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 11165	. . . . . . . . . . . . . . . . . . . 20 ⊢ (4 · 0) = 0
74	72, 73	eqtr4di 2796	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (4 · 𝑀) = (4 · 0))
75	55, 32, 57, 59, 74	mulcanad 11610	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝑀 = 0)
76	75	oveq1d 7290	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑀↑3) = (0↑3))
77	76, 28	eqtrdi 2794	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑀↑3) = 0)
78	47, 77	oveq12d 7293	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑁↑2) + (𝑀↑3)) = (0 + 0))
79		00id 11150	. . . . . . . . . . . . . . 15 ⊢ (0 + 0) = 0
80	78, 79	eqtrdi 2794	. . . . . . . . . . . . . 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 13863	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝐺 = 0)
83	82, 46	oveq12d 7293	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝐺 − 𝑁) = (0 − 0))
84		0m0e0 12093	. . . . . . . . . . 11 ⊢ (0 − 0) = 0
85	83, 84	eqtrdi 2794	. . . . . . . . . 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 413	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) → ((𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0) → (𝑇↑3) = 0))
88	87	necon3ad 2956	. . . . . . 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 7284	. . . . . . . . . . 11 ⊢ ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0 ∧ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0) → (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) + ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = (0 + 0))
92	91, 79	eqtrdi 2794	. . . . . . . . . 10 ⊢ ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0 ∧ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0) → (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) + ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = 0)
93		oveq12 7284	. . . . . . . . . . 11 ⊢ ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0 ∧ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0) → (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) − ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = (0 − 0))
94	93, 84	eqtrdi 2794	. . . . . . . . . 10 ⊢ ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0 ∧ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0) → (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) − ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = 0)
95	92, 94	jca 512	. . . . . . . . 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 15149	. . . . . . . . . . . . 13 ⊢ (𝜑 → (√‘((𝑋↑2) + (4 · 𝑀))) ∈ ℂ)
97		halfaddsub 12206	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∈ ℂ ∧ (√‘((𝑋↑2) + (4 · 𝑀))) ∈ ℂ) → ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) + ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = 𝑋 ∧ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) − ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = (√‘((𝑋↑2) + (4 · 𝑀)))))
98	62, 96, 97	syl2anc 584	. . . . . . . . . . . 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 2740	. . . . . . . . . 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 2740	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) − ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = 0 ↔ (√‘((𝑋↑2) + (4 · 𝑀))) = 0))
103	100, 102	anbi12d 631	. . . . . . . . 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 4061	. . . . . . . . . . . . . 14 ⊢ (𝑢 ∈ (ℂ ∖ {0}) → 𝑢 ∈ ℂ)
107	106	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → 𝑢 ∈ ℂ)
108	54	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → 𝑀 ∈ ℂ)
109		eldifsni 4723	. . . . . . . . . . . . . . 15 ⊢ (𝑢 ∈ (ℂ ∖ {0}) → 𝑢 ≠ 0)
110	109	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → 𝑢 ≠ 0)
111	108, 107, 110	divcld 11751	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑀 / 𝑢) ∈ ℂ)
112	62	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → 𝑋 ∈ ℂ)
113	107, 111, 112	subaddd 11350	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑢 − (𝑀 / 𝑢)) = 𝑋 ↔ ((𝑀 / 𝑢) + 𝑋) = 𝑢))
114		eqcom 2745	. . . . . . . . . . . 12 ⊢ (𝑋 = (𝑢 − (𝑀 / 𝑢)) ↔ (𝑢 − (𝑀 / 𝑢)) = 𝑋)
115		eqcom 2745	. . . . . . . . . . . 12 ⊢ (𝑢 = ((𝑀 / 𝑢) + 𝑋) ↔ ((𝑀 / 𝑢) + 𝑋) = 𝑢)
116	113, 114, 115	3bitr4g 314	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑋 = (𝑢 − (𝑀 / 𝑢)) ↔ 𝑢 = ((𝑀 / 𝑢) + 𝑋)))
117	107	sqcld 13862	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑢↑2) ∈ ℂ)
118	112, 107	mulcld 10995	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑋 · 𝑢) ∈ ℂ)
119	118, 108	addcld 10994	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑋 · 𝑢) + 𝑀) ∈ ℂ)
120	117, 119	subeq0ad 11342	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (((𝑢↑2) − ((𝑋 · 𝑢) + 𝑀)) = 0 ↔ (𝑢↑2) = ((𝑋 · 𝑢) + 𝑀)))
121	107	sqvald 13861	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑢↑2) = (𝑢 · 𝑢))
122	111, 112, 107	adddird 11000	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (((𝑀 / 𝑢) + 𝑋) · 𝑢) = (((𝑀 / 𝑢) · 𝑢) + (𝑋 · 𝑢)))
123	108, 107, 110	divcan1d 11752	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑀 / 𝑢) · 𝑢) = 𝑀)
124	123	oveq1d 7290	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (((𝑀 / 𝑢) · 𝑢) + (𝑋 · 𝑢)) = (𝑀 + (𝑋 · 𝑢)))
125	108, 118	addcomd 11177	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑀 + (𝑋 · 𝑢)) = ((𝑋 · 𝑢) + 𝑀))
126	122, 124, 125	3eqtrrd 2783	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑋 · 𝑢) + 𝑀) = (((𝑀 / 𝑢) + 𝑋) · 𝑢))
127	121, 126	eqeq12d 2754	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑢↑2) = ((𝑋 · 𝑢) + 𝑀) ↔ (𝑢 · 𝑢) = (((𝑀 / 𝑢) + 𝑋) · 𝑢)))
128	111, 112	addcld 10994	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑀 / 𝑢) + 𝑋) ∈ ℂ)
129	107, 128, 107, 110	mulcan2d 11609	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑢 · 𝑢) = (((𝑀 / 𝑢) + 𝑋) · 𝑢) ↔ 𝑢 = ((𝑀 / 𝑢) + 𝑋)))
130	120, 127, 129	3bitrd 305	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (((𝑢↑2) − ((𝑋 · 𝑢) + 𝑀)) = 0 ↔ 𝑢 = ((𝑀 / 𝑢) + 𝑋)))
131		1cnd 10970	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → 1 ∈ ℂ)
132		ax-1ne0 10940	. . . . . . . . . . . . . 14 ⊢ 1 ≠ 0
133	132	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → 1 ≠ 0)
134	62	negcld 11319	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -𝑋 ∈ ℂ)
135	134	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → -𝑋 ∈ ℂ)
136	54	negcld 11319	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -𝑀 ∈ ℂ)
137	136	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → -𝑀 ∈ ℂ)
138		sqneg 13836	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 ∈ ℂ → (-𝑋↑2) = (𝑋↑2))
139	112, 138	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (-𝑋↑2) = (𝑋↑2))
140	137	mulid2d 10993	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (1 · -𝑀) = -𝑀)
141	140	oveq2d 7291	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (4 · (1 · -𝑀)) = (4 · -𝑀))
142		mulneg2 11412	. . . . . . . . . . . . . . . . 17 ⊢ ((4 ∈ ℂ ∧ 𝑀 ∈ ℂ) → (4 · -𝑀) = -(4 · 𝑀))
143	56, 108, 142	sylancr 587	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (4 · -𝑀) = -(4 · 𝑀))
144	141, 143	eqtrd 2778	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (4 · (1 · -𝑀)) = -(4 · 𝑀))
145	139, 144	oveq12d 7293	. . . . . . . . . . . . . 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 11339	. . . . . . . . . . . . . 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 25990	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (((1 · (𝑢↑2)) + ((-𝑋 · 𝑢) + -𝑀)) = 0 ↔ (𝑢 = ((--𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / (2 · 1)) ∨ 𝑢 = ((--𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / (2 · 1)))))
151	117	mulid2d 10993	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (1 · (𝑢↑2)) = (𝑢↑2))
152	112, 107	mulneg1d 11428	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (-𝑋 · 𝑢) = -(𝑋 · 𝑢))
153	152	oveq1d 7290	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((-𝑋 · 𝑢) + -𝑀) = (-(𝑋 · 𝑢) + -𝑀))
154	118, 108	negdid 11345	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → -((𝑋 · 𝑢) + 𝑀) = (-(𝑋 · 𝑢) + -𝑀))
155	153, 154	eqtr4d 2781	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((-𝑋 · 𝑢) + -𝑀) = -((𝑋 · 𝑢) + 𝑀))
156	151, 155	oveq12d 7293	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((1 · (𝑢↑2)) + ((-𝑋 · 𝑢) + -𝑀)) = ((𝑢↑2) + -((𝑋 · 𝑢) + 𝑀)))
157	117, 119	negsubd 11338	. . . . . . . . . . . . . 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 11323	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → --𝑋 = 𝑋)
161	160	oveq1d 7290	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (--𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) = (𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))))
162		2t1e2 12136	. . . . . . . . . . . . . . . 16 ⊢ (2 · 1) = 2
163	162	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (2 · 1) = 2)
164	161, 163	oveq12d 7293	. . . . . . . . . . . . . 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 7290	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (--𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) = (𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))))
167	166, 163	oveq12d 7293	. . . . . . . . . . . . . 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 916	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑢 = ((--𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / (2 · 1)) ∨ 𝑢 = ((--𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / (2 · 1))) ↔ (𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∨ 𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2))))
170	150, 159, 169	3bitr3d 309	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (((𝑢↑2) − ((𝑋 · 𝑢) + 𝑀)) = 0 ↔ (𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∨ 𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2))))
171	116, 130, 170	3bitr2d 307	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑋 = (𝑢 − (𝑀 / 𝑢)) ↔ (𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∨ 𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2))))
172	171	rexbidva 3225	. . . . . . . . 9 ⊢ (𝜑 → (∃𝑢 ∈ (ℂ ∖ {0})𝑋 = (𝑢 − (𝑀 / 𝑢)) ↔ ∃𝑢 ∈ (ℂ ∖ {0})(𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∨ 𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2))))
173		r19.43 3280	. . . . . . . . 9 ⊢ (∃𝑢 ∈ (ℂ ∖ {0})(𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∨ 𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) ↔ (∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∨ ∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)))
174	172, 173	bitrdi 287	. . . . . . . 8 ⊢ (𝜑 → (∃𝑢 ∈ (ℂ ∖ {0})𝑋 = (𝑢 − (𝑀 / 𝑢)) ↔ (∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∨ ∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2))))
175		risset 3194	. . . . . . . . . . 11 ⊢ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ (ℂ ∖ {0}) ↔ ∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2))
176	62, 96	addcld 10994	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) ∈ ℂ)
177	176	halfcld 12218	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ ℂ)
178		eldifsn 4720	. . . . . . . . . . . . 13 ⊢ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ (ℂ ∖ {0}) ↔ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ ℂ ∧ ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0))
179	178	baib 536	. . . . . . . . . . . 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 285	. . . . . . . . . 10 ⊢ (𝜑 → (∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ↔ ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0))
182		risset 3194	. . . . . . . . . . 11 ⊢ (((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ (ℂ ∖ {0}) ↔ ∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2))
183	62, 96	subcld 11332	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) ∈ ℂ)
184	183	halfcld 12218	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ ℂ)
185		eldifsn 4720	. . . . . . . . . . . . 13 ⊢ (((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ (ℂ ∖ {0}) ↔ (((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ ℂ ∧ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0))
186	185	baib 536	. . . . . . . . . . . 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 285	. . . . . . . . . 10 ⊢ (𝜑 → (∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ↔ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0))
189	181, 188	orbi12d 916	. . . . . . . . 9 ⊢ (𝜑 → ((∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∨ ∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) ↔ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0 ∨ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0)))
190		neorian 3039	. . . . . . . . 9 ⊢ ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0 ∨ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0) ↔ ¬ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0 ∧ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0))
191	189, 190	bitrdi 287	. . . . . . . 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 407	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ∃𝑢 ∈ (ℂ ∖ {0})𝑋 = (𝑢 − (𝑀 / 𝑢)))
195	90, 194	syldan 591	. . . 4 ⊢ ((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) → ∃𝑢 ∈ (ℂ ∖ {0})𝑋 = (𝑢 − (𝑀 / 𝑢)))
196	20	ad2antrr 723	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑃 ∈ ℂ)
197	34	ad2antrr 723	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑄 ∈ ℂ)
198	62	ad2antrr 723	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑋 ∈ ℂ)
199	3	ad2antrr 723	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑇 ∈ ℂ)
200	10	ad2antrr 723	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → (𝑇↑3) = (𝐺 − 𝑁))
201	12	ad2antrr 723	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝐺 ∈ ℂ)
202	14	ad2antrr 723	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → (𝐺↑2) = ((𝑁↑2) + (𝑀↑3)))
203	48	ad2antrr 723	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑀 = (𝑃 / 3))
204	16	ad2antrr 723	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑁 = (𝑄 / 2))
205	1	ad2antrr 723	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑇 ≠ 0)
206	106	ad2antrl 725	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑢 ∈ ℂ)
207	109	ad2antrl 725	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑢 ≠ 0)
208		simprr 770	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑋 = (𝑢 − (𝑀 / 𝑢)))
209		simplr 766	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0)
210	196, 197, 198, 199, 200, 201, 202, 203, 204, 205, 206, 207, 208, 209	dcubic2 25994	. . . 4 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇)))))
211	195, 210	rexlimddv 3220	. . 3 ⊢ ((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) → ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇)))))
212	211	ex 413	. 2 ⊢ (𝜑 → (((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0 → ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))))
213	20	ad2antrr 723	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑃 ∈ ℂ)
214	34	ad2antrr 723	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑄 ∈ ℂ)
215	62	ad2antrr 723	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑋 ∈ ℂ)
216		simplr 766	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑟 ∈ ℂ)
217	3	ad2antrr 723	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑇 ∈ ℂ)
218	216, 217	mulcld 10995	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → (𝑟 · 𝑇) ∈ ℂ)
219		3nn0 12251	. . . . . . 7 ⊢ 3 ∈ ℕ₀
220	219	a1i 11	. . . . . 6 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 3 ∈ ℕ₀)
221	216, 217, 220	mulexpd 13879	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → ((𝑟 · 𝑇)↑3) = ((𝑟↑3) · (𝑇↑3)))
222		simprl 768	. . . . . 6 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → (𝑟↑3) = 1)
223	222	oveq1d 7290	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → ((𝑟↑3) · (𝑇↑3)) = (1 · (𝑇↑3)))
224		expcl 13800	. . . . . . . . 9 ⊢ ((𝑇 ∈ ℂ ∧ 3 ∈ ℕ₀) → (𝑇↑3) ∈ ℂ)
225	3, 219, 224	sylancl 586	. . . . . . . 8 ⊢ (𝜑 → (𝑇↑3) ∈ ℂ)
226	225	mulid2d 10993	. . . . . . 7 ⊢ (𝜑 → (1 · (𝑇↑3)) = (𝑇↑3))
227	226, 10	eqtrd 2778	. . . . . 6 ⊢ (𝜑 → (1 · (𝑇↑3)) = (𝐺 − 𝑁))
228	227	ad2antrr 723	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → (1 · (𝑇↑3)) = (𝐺 − 𝑁))
229	221, 223, 228	3eqtrd 2782	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → ((𝑟 · 𝑇)↑3) = (𝐺 − 𝑁))
230	12	ad2antrr 723	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝐺 ∈ ℂ)
231	14	ad2antrr 723	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → (𝐺↑2) = ((𝑁↑2) + (𝑀↑3)))
232	48	ad2antrr 723	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑀 = (𝑃 / 3))
233	16	ad2antrr 723	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑁 = (𝑄 / 2))
234	132	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 1 ≠ 0)
235	222, 234	eqnetrd 3011	. . . . . 6 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → (𝑟↑3) ≠ 0)
236		oveq1 7282	. . . . . . . 8 ⊢ (𝑟 = 0 → (𝑟↑3) = (0↑3))
237	236, 28	eqtrdi 2794	. . . . . . 7 ⊢ (𝑟 = 0 → (𝑟↑3) = 0)
238	237	necon3i 2976	. . . . . 6 ⊢ ((𝑟↑3) ≠ 0 → 𝑟 ≠ 0)
239	235, 238	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑟 ≠ 0)
240	1	ad2antrr 723	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑇 ≠ 0)
241	216, 217, 239, 240	mulne0d 11627	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → (𝑟 · 𝑇) ≠ 0)
242		simprr 770	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))
243	213, 214, 215, 218, 229, 230, 231, 232, 233, 241, 242	dcubic1 25995	. . 3 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0)
244	243	rexlimdva2 3216	. 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 396 ∨ wo 844 = wceq 1539 ∈ wcel 2106 ≠ wne 2943 ∃wrex 3065 ∖ cdif 3884 {csn 4561 ‘cfv 6433 (class class class)co 7275 ℂcc 10869 0cc0 10871 1c1 10872 + caddc 10874 · cmul 10876 − cmin 11205 -cneg 11206 / cdiv 11632 ℕcn 11973 2c2 12028 3c3 12029 4c4 12030 ℕ₀cn0 12233 ℤcz 12319 ↑cexp 13782 √csqrt 14944

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588 ax-cnex 10927 ax-resscn 10928 ax-1cn 10929 ax-icn 10930 ax-addcl 10931 ax-addrcl 10932 ax-mulcl 10933 ax-mulrcl 10934 ax-mulcom 10935 ax-addass 10936 ax-mulass 10937 ax-distr 10938 ax-i2m1 10939 ax-1ne0 10940 ax-1rid 10941 ax-rnegex 10942 ax-rrecex 10943 ax-cnre 10944 ax-pre-lttri 10945 ax-pre-lttrn 10946 ax-pre-ltadd 10947 ax-pre-mulgt0 10948 ax-pre-sup 10949

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-rmo 3071 df-reu 3072 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-iun 4926 df-br 5075 df-opab 5137 df-mpt 5158 df-tr 5192 df-id 5489 df-eprel 5495 df-po 5503 df-so 5504 df-fr 5544 df-we 5546 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-pred 6202 df-ord 6269 df-on 6270 df-lim 6271 df-suc 6272 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440 df-fv 6441 df-riota 7232 df-ov 7278 df-oprab 7279 df-mpo 7280 df-om 7713 df-2nd 7832 df-frecs 8097 df-wrecs 8128 df-recs 8202 df-rdg 8241 df-er 8498 df-en 8734 df-dom 8735 df-sdom 8736 df-sup 9201 df-pnf 11011 df-mnf 11012 df-xr 11013 df-ltxr 11014 df-le 11015 df-sub 11207 df-neg 11208 df-div 11633 df-nn 11974 df-2 12036 df-3 12037 df-4 12038 df-n0 12234 df-z 12320 df-uz 12583 df-rp 12731 df-seq 13722 df-exp 13783 df-cj 14810 df-re 14811 df-im 14812 df-sqrt 14946 df-abs 14947 df-dvds 15964

This theorem is referenced by: mcubic 25997

W3C validator