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 26777

Description: Solutions to the depressed cubic, a special case of cubic 26780. (The definitions of 𝑀, 𝑁, 𝐺, 𝑇 here differ from mcubic 26778 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 12625	. . . . . . . . . 10 ⊢ 3 ∈ ℤ
6		expne0i 14091	. . . . . . . . . 10 ⊢ ((𝑇 ∈ ℂ ∧ 𝑇 ≠ 0 ∧ 3 ∈ ℤ) → (𝑇↑3) ≠ 0)
7	5, 6	mp3an3 1447	. . . . . . . . 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 725	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑇↑3) = (𝐺 − 𝑁))
12		dcubic.g	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐺 ∈ ℂ)
13	12	ad2antrr 725	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝐺 ∈ ℂ)
14		dcubic.2	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐺↑2) = ((𝑁↑2) + (𝑀↑3)))
15	14	ad2antrr 725	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝐺↑2) = ((𝑁↑2) + (𝑀↑3)))
16		dcubic.n	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑁 = (𝑄 / 2))
17	16	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝑁 = (𝑄 / 2))
18		simprl 770	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝑋 = 0)
19	18	oveq2d 7436	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑃 · 𝑋) = (𝑃 · 0))
20		dcubic.c	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑃 ∈ ℂ)
21	20	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝑃 ∈ ℂ)
22	21	mul01d 11443	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑃 · 0) = 0)
23	19, 22	eqtrd 2768	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑃 · 𝑋) = 0)
24	23	oveq1d 7435	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑃 · 𝑋) + 𝑄) = (0 + 𝑄))
25	18	oveq1d 7435	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑋↑3) = (0↑3))
26		3nn 12321	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 3 ∈ ℕ
27		0exp 14094	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (3 ∈ ℕ → (0↑3) = 0)
28	26, 27	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (0↑3) = 0
29	25, 28	eqtrdi 2784	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑋↑3) = 0)
30	29	oveq1d 7435	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = (0 + ((𝑃 · 𝑋) + 𝑄)))
31		simplr 768	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0)
32		0cnd 11237	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 0 ∈ ℂ)
33	23, 32	eqeltrd 2829	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑃 · 𝑋) ∈ ℂ)
34		dcubic.d	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑄 ∈ ℂ)
35	34	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝑄 ∈ ℂ)
36	33, 35	addcld 11263	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑃 · 𝑋) + 𝑄) ∈ ℂ)
37	36	addlidd 11445	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (0 + ((𝑃 · 𝑋) + 𝑄)) = ((𝑃 · 𝑋) + 𝑄))
38	30, 31, 37	3eqtr3rd 2777	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑃 · 𝑋) + 𝑄) = 0)
39	35	addlidd 11445	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (0 + 𝑄) = 𝑄)
40	24, 38, 39	3eqtr3rd 2777	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝑄 = 0)
41	40	oveq1d 7435	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑄 / 2) = (0 / 2))
42		2cn 12317	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ∈ ℂ
43		2ne0 12346	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ≠ 0
44	42, 43	div0i 11978	. . . . . . . . . . . . . . . . . . 19 ⊢ (0 / 2) = 0
45	41, 44	eqtrdi 2784	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑄 / 2) = 0)
46	17, 45	eqtrd 2768	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝑁 = 0)
47	46	sq0id 14189	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑁↑2) = 0)
48		dcubic.m	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑀 = (𝑃 / 3))
49		3cn 12323	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 3 ∈ ℂ
50	49	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 3 ∈ ℂ)
51		3ne0 12348	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 3 ≠ 0
52	51	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 3 ≠ 0)
53	20, 50, 52	divcld 12020	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑃 / 3) ∈ ℂ)
54	48, 53	eqeltrd 2829	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑀 ∈ ℂ)
55	54	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝑀 ∈ ℂ)
56		4cn 12327	. . . . . . . . . . . . . . . . . . . 20 ⊢ 4 ∈ ℂ
57	56	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 4 ∈ ℂ)
58		4ne0 12350	. . . . . . . . . . . . . . . . . . . 20 ⊢ 4 ≠ 0
59	58	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 4 ≠ 0)
60	18	sq0id 14189	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑋↑2) = 0)
61	60	oveq1d 7435	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑋↑2) + (4 · 𝑀)) = (0 + (4 · 𝑀)))
62		dcubic.x	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑋 ∈ ℂ)
63	62	sqcld 14140	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑋↑2) ∈ ℂ)
64		mulcl 11222	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((4 ∈ ℂ ∧ 𝑀 ∈ ℂ) → (4 · 𝑀) ∈ ℂ)
65	56, 54, 64	sylancr 586	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (4 · 𝑀) ∈ ℂ)
66	63, 65	addcld 11263	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝑋↑2) + (4 · 𝑀)) ∈ ℂ)
67	66	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑋↑2) + (4 · 𝑀)) ∈ ℂ)
68		simprr 772	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (√‘((𝑋↑2) + (4 · 𝑀))) = 0)
69	67, 68	sqr00d 15420	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑋↑2) + (4 · 𝑀)) = 0)
70	65	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (4 · 𝑀) ∈ ℂ)
71	70	addlidd 11445	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (0 + (4 · 𝑀)) = (4 · 𝑀))
72	61, 69, 71	3eqtr3rd 2777	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (4 · 𝑀) = 0)
73	56	mul01i 11434	. . . . . . . . . . . . . . . . . . . 20 ⊢ (4 · 0) = 0
74	72, 73	eqtr4di 2786	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (4 · 𝑀) = (4 · 0))
75	55, 32, 57, 59, 74	mulcanad 11879	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝑀 = 0)
76	75	oveq1d 7435	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑀↑3) = (0↑3))
77	76, 28	eqtrdi 2784	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑀↑3) = 0)
78	47, 77	oveq12d 7438	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑁↑2) + (𝑀↑3)) = (0 + 0))
79		00id 11419	. . . . . . . . . . . . . . 15 ⊢ (0 + 0) = 0
80	78, 79	eqtrdi 2784	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑁↑2) + (𝑀↑3)) = 0)
81	15, 80	eqtrd 2768	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝐺↑2) = 0)
82	13, 81	sqeq0d 14141	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝐺 = 0)
83	82, 46	oveq12d 7438	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝐺 − 𝑁) = (0 − 0))
84		0m0e0 12362	. . . . . . . . . . 11 ⊢ (0 − 0) = 0
85	83, 84	eqtrdi 2784	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝐺 − 𝑁) = 0)
86	11, 85	eqtrd 2768	. . . . . . . . 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 2950	. . . . . . 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 7429	. . . . . . . . . . 11 ⊢ ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0 ∧ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0) → (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) + ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = (0 + 0))
92	91, 79	eqtrdi 2784	. . . . . . . . . 10 ⊢ ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0 ∧ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0) → (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) + ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = 0)
93		oveq12 7429	. . . . . . . . . . 11 ⊢ ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0 ∧ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0) → (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) − ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = (0 − 0))
94	93, 84	eqtrdi 2784	. . . . . . . . . 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 15416	. . . . . . . . . . . . 13 ⊢ (𝜑 → (√‘((𝑋↑2) + (4 · 𝑀))) ∈ ℂ)
97		halfaddsub 12475	. . . . . . . . . . . . 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 2730	. . . . . . . . . 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 2730	. . . . . . . . . 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	imbitrid 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 4125	. . . . . . . . . . . . . 14 ⊢ (𝑢 ∈ (ℂ ∖ {0}) → 𝑢 ∈ ℂ)
107	106	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → 𝑢 ∈ ℂ)
108	54	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → 𝑀 ∈ ℂ)
109		eldifsni 4794	. . . . . . . . . . . . . . 15 ⊢ (𝑢 ∈ (ℂ ∖ {0}) → 𝑢 ≠ 0)
110	109	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → 𝑢 ≠ 0)
111	108, 107, 110	divcld 12020	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑀 / 𝑢) ∈ ℂ)
112	62	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → 𝑋 ∈ ℂ)
113	107, 111, 112	subaddd 11619	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑢 − (𝑀 / 𝑢)) = 𝑋 ↔ ((𝑀 / 𝑢) + 𝑋) = 𝑢))
114		eqcom 2735	. . . . . . . . . . . 12 ⊢ (𝑋 = (𝑢 − (𝑀 / 𝑢)) ↔ (𝑢 − (𝑀 / 𝑢)) = 𝑋)
115		eqcom 2735	. . . . . . . . . . . 12 ⊢ (𝑢 = ((𝑀 / 𝑢) + 𝑋) ↔ ((𝑀 / 𝑢) + 𝑋) = 𝑢)
116	113, 114, 115	3bitr4g 314	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑋 = (𝑢 − (𝑀 / 𝑢)) ↔ 𝑢 = ((𝑀 / 𝑢) + 𝑋)))
117	107	sqcld 14140	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑢↑2) ∈ ℂ)
118	112, 107	mulcld 11264	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑋 · 𝑢) ∈ ℂ)
119	118, 108	addcld 11263	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑋 · 𝑢) + 𝑀) ∈ ℂ)
120	117, 119	subeq0ad 11611	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (((𝑢↑2) − ((𝑋 · 𝑢) + 𝑀)) = 0 ↔ (𝑢↑2) = ((𝑋 · 𝑢) + 𝑀)))
121	107	sqvald 14139	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑢↑2) = (𝑢 · 𝑢))
122	111, 112, 107	adddird 11269	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (((𝑀 / 𝑢) + 𝑋) · 𝑢) = (((𝑀 / 𝑢) · 𝑢) + (𝑋 · 𝑢)))
123	108, 107, 110	divcan1d 12021	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑀 / 𝑢) · 𝑢) = 𝑀)
124	123	oveq1d 7435	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (((𝑀 / 𝑢) · 𝑢) + (𝑋 · 𝑢)) = (𝑀 + (𝑋 · 𝑢)))
125	108, 118	addcomd 11446	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑀 + (𝑋 · 𝑢)) = ((𝑋 · 𝑢) + 𝑀))
126	122, 124, 125	3eqtrrd 2773	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑋 · 𝑢) + 𝑀) = (((𝑀 / 𝑢) + 𝑋) · 𝑢))
127	121, 126	eqeq12d 2744	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑢↑2) = ((𝑋 · 𝑢) + 𝑀) ↔ (𝑢 · 𝑢) = (((𝑀 / 𝑢) + 𝑋) · 𝑢)))
128	111, 112	addcld 11263	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑀 / 𝑢) + 𝑋) ∈ ℂ)
129	107, 128, 107, 110	mulcan2d 11878	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑢 · 𝑢) = (((𝑀 / 𝑢) + 𝑋) · 𝑢) ↔ 𝑢 = ((𝑀 / 𝑢) + 𝑋)))
130	120, 127, 129	3bitrd 305	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (((𝑢↑2) − ((𝑋 · 𝑢) + 𝑀)) = 0 ↔ 𝑢 = ((𝑀 / 𝑢) + 𝑋)))
131		1cnd 11239	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → 1 ∈ ℂ)
132		ax-1ne0 11207	. . . . . . . . . . . . . 14 ⊢ 1 ≠ 0
133	132	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → 1 ≠ 0)
134	62	negcld 11588	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -𝑋 ∈ ℂ)
135	134	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → -𝑋 ∈ ℂ)
136	54	negcld 11588	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -𝑀 ∈ ℂ)
137	136	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → -𝑀 ∈ ℂ)
138		sqneg 14112	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 ∈ ℂ → (-𝑋↑2) = (𝑋↑2))
139	112, 138	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (-𝑋↑2) = (𝑋↑2))
140	137	mullidd 11262	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (1 · -𝑀) = -𝑀)
141	140	oveq2d 7436	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (4 · (1 · -𝑀)) = (4 · -𝑀))
142		mulneg2 11681	. . . . . . . . . . . . . . . . 17 ⊢ ((4 ∈ ℂ ∧ 𝑀 ∈ ℂ) → (4 · -𝑀) = -(4 · 𝑀))
143	56, 108, 142	sylancr 586	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (4 · -𝑀) = -(4 · 𝑀))
144	141, 143	eqtrd 2768	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (4 · (1 · -𝑀)) = -(4 · 𝑀))
145	139, 144	oveq12d 7438	. . . . . . . . . . . . . 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 11608	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑋↑2) − -(4 · 𝑀)) = ((𝑋↑2) + (4 · 𝑀)))
149	145, 148	eqtr2d 2769	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑋↑2) + (4 · 𝑀)) = ((-𝑋↑2) − (4 · (1 · -𝑀))))
150	131, 133, 135, 137, 107, 149	quad 26771	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (((1 · (𝑢↑2)) + ((-𝑋 · 𝑢) + -𝑀)) = 0 ↔ (𝑢 = ((--𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / (2 · 1)) ∨ 𝑢 = ((--𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / (2 · 1)))))
151	117	mullidd 11262	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (1 · (𝑢↑2)) = (𝑢↑2))
152	112, 107	mulneg1d 11697	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (-𝑋 · 𝑢) = -(𝑋 · 𝑢))
153	152	oveq1d 7435	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((-𝑋 · 𝑢) + -𝑀) = (-(𝑋 · 𝑢) + -𝑀))
154	118, 108	negdid 11614	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → -((𝑋 · 𝑢) + 𝑀) = (-(𝑋 · 𝑢) + -𝑀))
155	153, 154	eqtr4d 2771	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((-𝑋 · 𝑢) + -𝑀) = -((𝑋 · 𝑢) + 𝑀))
156	151, 155	oveq12d 7438	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((1 · (𝑢↑2)) + ((-𝑋 · 𝑢) + -𝑀)) = ((𝑢↑2) + -((𝑋 · 𝑢) + 𝑀)))
157	117, 119	negsubd 11607	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑢↑2) + -((𝑋 · 𝑢) + 𝑀)) = ((𝑢↑2) − ((𝑋 · 𝑢) + 𝑀)))
158	156, 157	eqtrd 2768	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((1 · (𝑢↑2)) + ((-𝑋 · 𝑢) + -𝑀)) = ((𝑢↑2) − ((𝑋 · 𝑢) + 𝑀)))
159	158	eqeq1d 2730	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (((1 · (𝑢↑2)) + ((-𝑋 · 𝑢) + -𝑀)) = 0 ↔ ((𝑢↑2) − ((𝑋 · 𝑢) + 𝑀)) = 0))
160	112	negnegd 11592	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → --𝑋 = 𝑋)
161	160	oveq1d 7435	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (--𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) = (𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))))
162		2t1e2 12405	. . . . . . . . . . . . . . . 16 ⊢ (2 · 1) = 2
163	162	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (2 · 1) = 2)
164	161, 163	oveq12d 7438	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((--𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / (2 · 1)) = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2))
165	164	eqeq2d 2739	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑢 = ((--𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / (2 · 1)) ↔ 𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)))
166	160	oveq1d 7435	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (--𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) = (𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))))
167	166, 163	oveq12d 7438	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((--𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / (2 · 1)) = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2))
168	167	eqeq2d 2739	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑢 = ((--𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / (2 · 1)) ↔ 𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)))
169	165, 168	orbi12d 917	. . . . . . . . . . . 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 3173	. . . . . . . . 9 ⊢ (𝜑 → (∃𝑢 ∈ (ℂ ∖ {0})𝑋 = (𝑢 − (𝑀 / 𝑢)) ↔ ∃𝑢 ∈ (ℂ ∖ {0})(𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∨ 𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2))))
173		r19.43 3119	. . . . . . . . 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 3227	. . . . . . . . . . 11 ⊢ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ (ℂ ∖ {0}) ↔ ∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2))
176	62, 96	addcld 11263	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) ∈ ℂ)
177	176	halfcld 12487	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ ℂ)
178		eldifsn 4791	. . . . . . . . . . . . 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 285	. . . . . . . . . 10 ⊢ (𝜑 → (∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ↔ ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0))
182		risset 3227	. . . . . . . . . . 11 ⊢ (((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ (ℂ ∖ {0}) ↔ ∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2))
183	62, 96	subcld 11601	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) ∈ ℂ)
184	183	halfcld 12487	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ ℂ)
185		eldifsn 4791	. . . . . . . . . . . . 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 285	. . . . . . . . . 10 ⊢ (𝜑 → (∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ↔ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0))
189	181, 188	orbi12d 917	. . . . . . . . 9 ⊢ (𝜑 → ((∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∨ ∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) ↔ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0 ∨ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0)))
190		neorian 3034	. . . . . . . . 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 279	. . . . . . 7 ⊢ (𝜑 → (∃𝑢 ∈ (ℂ ∖ {0})𝑋 = (𝑢 − (𝑀 / 𝑢)) ↔ ¬ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0 ∧ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0)))
193	105, 192	sylibrd 259	. . . . . 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 725	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑃 ∈ ℂ)
197	34	ad2antrr 725	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑄 ∈ ℂ)
198	62	ad2antrr 725	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑋 ∈ ℂ)
199	3	ad2antrr 725	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑇 ∈ ℂ)
200	10	ad2antrr 725	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → (𝑇↑3) = (𝐺 − 𝑁))
201	12	ad2antrr 725	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝐺 ∈ ℂ)
202	14	ad2antrr 725	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → (𝐺↑2) = ((𝑁↑2) + (𝑀↑3)))
203	48	ad2antrr 725	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑀 = (𝑃 / 3))
204	16	ad2antrr 725	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑁 = (𝑄 / 2))
205	1	ad2antrr 725	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑇 ≠ 0)
206	106	ad2antrl 727	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑢 ∈ ℂ)
207	109	ad2antrl 727	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑢 ≠ 0)
208		simprr 772	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑋 = (𝑢 − (𝑀 / 𝑢)))
209		simplr 768	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0)
210	196, 197, 198, 199, 200, 201, 202, 203, 204, 205, 206, 207, 208, 209	dcubic2 26775	. . . 4 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇)))))
211	195, 210	rexlimddv 3158	. . 3 ⊢ ((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) → ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇)))))
212	211	ex 412	. 2 ⊢ (𝜑 → (((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0 → ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))))
213	20	ad2antrr 725	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑃 ∈ ℂ)
214	34	ad2antrr 725	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑄 ∈ ℂ)
215	62	ad2antrr 725	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑋 ∈ ℂ)
216		simplr 768	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑟 ∈ ℂ)
217	3	ad2antrr 725	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑇 ∈ ℂ)
218	216, 217	mulcld 11264	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → (𝑟 · 𝑇) ∈ ℂ)
219		3nn0 12520	. . . . . . 7 ⊢ 3 ∈ ℕ₀
220	219	a1i 11	. . . . . 6 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 3 ∈ ℕ₀)
221	216, 217, 220	mulexpd 14157	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → ((𝑟 · 𝑇)↑3) = ((𝑟↑3) · (𝑇↑3)))
222		simprl 770	. . . . . 6 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → (𝑟↑3) = 1)
223	222	oveq1d 7435	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → ((𝑟↑3) · (𝑇↑3)) = (1 · (𝑇↑3)))
224		expcl 14076	. . . . . . . . 9 ⊢ ((𝑇 ∈ ℂ ∧ 3 ∈ ℕ₀) → (𝑇↑3) ∈ ℂ)
225	3, 219, 224	sylancl 585	. . . . . . . 8 ⊢ (𝜑 → (𝑇↑3) ∈ ℂ)
226	225	mullidd 11262	. . . . . . 7 ⊢ (𝜑 → (1 · (𝑇↑3)) = (𝑇↑3))
227	226, 10	eqtrd 2768	. . . . . 6 ⊢ (𝜑 → (1 · (𝑇↑3)) = (𝐺 − 𝑁))
228	227	ad2antrr 725	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → (1 · (𝑇↑3)) = (𝐺 − 𝑁))
229	221, 223, 228	3eqtrd 2772	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → ((𝑟 · 𝑇)↑3) = (𝐺 − 𝑁))
230	12	ad2antrr 725	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝐺 ∈ ℂ)
231	14	ad2antrr 725	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → (𝐺↑2) = ((𝑁↑2) + (𝑀↑3)))
232	48	ad2antrr 725	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑀 = (𝑃 / 3))
233	16	ad2antrr 725	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑁 = (𝑄 / 2))
234	132	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 1 ≠ 0)
235	222, 234	eqnetrd 3005	. . . . . 6 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → (𝑟↑3) ≠ 0)
236		oveq1 7427	. . . . . . . 8 ⊢ (𝑟 = 0 → (𝑟↑3) = (0↑3))
237	236, 28	eqtrdi 2784	. . . . . . 7 ⊢ (𝑟 = 0 → (𝑟↑3) = 0)
238	237	necon3i 2970	. . . . . 6 ⊢ ((𝑟↑3) ≠ 0 → 𝑟 ≠ 0)
239	235, 238	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑟 ≠ 0)
240	1	ad2antrr 725	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑇 ≠ 0)
241	216, 217, 239, 240	mulne0d 11896	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → (𝑟 · 𝑇) ≠ 0)
242		simprr 772	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))
243	213, 214, 215, 218, 229, 230, 231, 232, 233, 241, 242	dcubic1 26776	. . 3 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0)
244	243	rexlimdva2 3154	. 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 846 = wceq 1534 ∈ wcel 2099 ≠ wne 2937 ∃wrex 3067 ∖ cdif 3944 {csn 4629 ‘cfv 6548 (class class class)co 7420 ℂcc 11136 0cc0 11138 1c1 11139 + caddc 11141 · cmul 11143 − cmin 11474 -cneg 11475 / cdiv 11901 ℕcn 12242 2c2 12297 3c3 12298 4c4 12299 ℕ₀cn0 12502 ℤcz 12588 ↑cexp 14058 √csqrt 15212

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2699 ax-sep 5299 ax-nul 5306 ax-pow 5365 ax-pr 5429 ax-un 7740 ax-cnex 11194 ax-resscn 11195 ax-1cn 11196 ax-icn 11197 ax-addcl 11198 ax-addrcl 11199 ax-mulcl 11200 ax-mulrcl 11201 ax-mulcom 11202 ax-addass 11203 ax-mulass 11204 ax-distr 11205 ax-i2m1 11206 ax-1ne0 11207 ax-1rid 11208 ax-rnegex 11209 ax-rrecex 11210 ax-cnre 11211 ax-pre-lttri 11212 ax-pre-lttrn 11213 ax-pre-ltadd 11214 ax-pre-mulgt0 11215 ax-pre-sup 11216

This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3or 1086 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2530 df-eu 2559 df-clab 2706 df-cleq 2720 df-clel 2806 df-nfc 2881 df-ne 2938 df-nel 3044 df-ral 3059 df-rex 3068 df-rmo 3373 df-reu 3374 df-rab 3430 df-v 3473 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4909 df-iun 4998 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5576 df-eprel 5582 df-po 5590 df-so 5591 df-fr 5633 df-we 5635 df-xp 5684 df-rel 5685 df-cnv 5686 df-co 5687 df-dm 5688 df-rn 5689 df-res 5690 df-ima 5691 df-pred 6305 df-ord 6372 df-on 6373 df-lim 6374 df-suc 6375 df-iota 6500 df-fun 6550 df-fn 6551 df-f 6552 df-f1 6553 df-fo 6554 df-f1o 6555 df-fv 6556 df-riota 7376 df-ov 7423 df-oprab 7424 df-mpo 7425 df-om 7871 df-2nd 7994 df-frecs 8286 df-wrecs 8317 df-recs 8391 df-rdg 8430 df-er 8724 df-en 8964 df-dom 8965 df-sdom 8966 df-sup 9465 df-pnf 11280 df-mnf 11281 df-xr 11282 df-ltxr 11283 df-le 11284 df-sub 11476 df-neg 11477 df-div 11902 df-nn 12243 df-2 12305 df-3 12306 df-4 12307 df-n0 12503 df-z 12589 df-uz 12853 df-rp 13007 df-seq 13999 df-exp 14059 df-cj 15078 df-re 15079 df-im 15080 df-sqrt 15214 df-abs 15215 df-dvds 16231

This theorem is referenced by: mcubic 26778

W3C validator