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 26989

Description: Solutions to the depressed cubic, a special case of cubic 26992. (The definitions of 𝑀, 𝑁, 𝐺, 𝑇 here differ from mcubic 26990 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 485	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) → 𝑇 ≠ 0)
3		dcubic.t	. . . . . . . . 9 ⊢ (𝜑 → 𝑇 ∈ ℂ)
4	3	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) → 𝑇 ∈ ℂ)
5		3z 12628	. . . . . . . . . 10 ⊢ 3 ∈ ℤ
6		expne0i 14132	. . . . . . . . . 10 ⊢ ((𝑇 ∈ ℂ ∧ 𝑇 ≠ 0 ∧ 3 ∈ ℤ) → (𝑇↑3) ≠ 0)
7	5, 6	mp3an3 1479	. . . . . . . . 9 ⊢ ((𝑇 ∈ ℂ ∧ 𝑇 ≠ 0) → (𝑇↑3) ≠ 0)
8	7	ex 417	. . . . . . . 8 ⊢ (𝑇 ∈ ℂ → (𝑇 ≠ 0 → (𝑇↑3) ≠ 0))
9	4, 8	syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) → (𝑇 ≠ 0 → (𝑇↑3) ≠ 0))
10		dcubic.3	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑇↑3) = (𝐺 − 𝑁))
11	10	ad2antrr 738	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑇↑3) = (𝐺 − 𝑁))
12		dcubic.g	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐺 ∈ ℂ)
13	12	ad2antrr 738	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝐺 ∈ ℂ)
14		dcubic.2	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐺↑2) = ((𝑁↑2) + (𝑀↑3)))
15	14	ad2antrr 738	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝐺↑2) = ((𝑁↑2) + (𝑀↑3)))
16		dcubic.n	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑁 = (𝑄 / 2))
17	16	ad2antrr 738	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝑁 = (𝑄 / 2))
18		simprl 782	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝑋 = 0)
19	18	oveq2d 7428	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑃 · 𝑋) = (𝑃 · 0))
20		dcubic.c	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑃 ∈ ℂ)
21	20	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝑃 ∈ ℂ)
22	21	mul01d 11410	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑃 · 0) = 0)
23	19, 22	eqtrd 2798	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑃 · 𝑋) = 0)
24	23	oveq1d 7427	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑃 · 𝑋) + 𝑄) = (0 + 𝑄))
25	18	oveq1d 7427	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑋↑3) = (0↑3))
26		3nn 12321	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 3 ∈ ℕ
27		0exp 14135	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (3 ∈ ℕ → (0↑3) = 0)
28	26, 27	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (0↑3) = 0
29	25, 28	eqtrdi 2814	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑋↑3) = 0)
30	29	oveq1d 7427	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = (0 + ((𝑃 · 𝑋) + 𝑄)))
31		simplr 780	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0)
32		0cnd 11200	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 0 ∈ ℂ)
33	23, 32	eqeltrd 2863	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑃 · 𝑋) ∈ ℂ)
34		dcubic.d	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑄 ∈ ℂ)
35	34	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝑄 ∈ ℂ)
36	33, 35	addcld 11229	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑃 · 𝑋) + 𝑄) ∈ ℂ)
37	36	addlidd 11412	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (0 + ((𝑃 · 𝑋) + 𝑄)) = ((𝑃 · 𝑋) + 𝑄))
38	30, 31, 37	3eqtr3rd 2807	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑃 · 𝑋) + 𝑄) = 0)
39	35	addlidd 11412	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (0 + 𝑄) = 𝑄)
40	24, 38, 39	3eqtr3rd 2807	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝑄 = 0)
41	40	oveq1d 7427	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑄 / 2) = (0 / 2))
42		2cn 12317	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ∈ ℂ
43		2ne0 12348	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ≠ 0
44	42, 43	div0i 11950	. . . . . . . . . . . . . . . . . . 19 ⊢ (0 / 2) = 0
45	41, 44	eqtrdi 2814	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑄 / 2) = 0)
46	17, 45	eqtrd 2798	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝑁 = 0)
47	46	sq0id 14232	. . . . . . . . . . . . . . . 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 12351	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 3 ≠ 0
52	51	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 3 ≠ 0)
53	20, 50, 52	divcld 11992	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑃 / 3) ∈ ℂ)
54	48, 53	eqeltrd 2863	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑀 ∈ ℂ)
55	54	ad2antrr 738	. . . . . . . . . . . . . . . . . . 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 12353	. . . . . . . . . . . . . . . . . . . 20 ⊢ 4 ≠ 0
59	58	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 4 ≠ 0)
60	18	sq0id 14232	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑋↑2) = 0)
61	60	oveq1d 7427	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑋↑2) + (4 · 𝑀)) = (0 + (4 · 𝑀)))
62		dcubic.x	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑋 ∈ ℂ)
63	62	sqcld 14182	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑋↑2) ∈ ℂ)
64		mulcl 11185	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((4 ∈ ℂ ∧ 𝑀 ∈ ℂ) → (4 · 𝑀) ∈ ℂ)
65	56, 54, 64	sylancr 598	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (4 · 𝑀) ∈ ℂ)
66	63, 65	addcld 11229	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝑋↑2) + (4 · 𝑀)) ∈ ℂ)
67	66	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑋↑2) + (4 · 𝑀)) ∈ ℂ)
68		simprr 784	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (√‘((𝑋↑2) + (4 · 𝑀))) = 0)
69	67, 68	sqr00d 15497	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑋↑2) + (4 · 𝑀)) = 0)
70	65	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (4 · 𝑀) ∈ ℂ)
71	70	addlidd 11412	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (0 + (4 · 𝑀)) = (4 · 𝑀))
72	61, 69, 71	3eqtr3rd 2807	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (4 · 𝑀) = 0)
73	56	mul01i 11401	. . . . . . . . . . . . . . . . . . . 20 ⊢ (4 · 0) = 0
74	72, 73	eqtr4di 2816	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (4 · 𝑀) = (4 · 0))
75	55, 32, 57, 59, 74	mulcanad 11850	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝑀 = 0)
76	75	oveq1d 7427	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑀↑3) = (0↑3))
77	76, 28	eqtrdi 2814	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑀↑3) = 0)
78	47, 77	oveq12d 7430	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑁↑2) + (𝑀↑3)) = (0 + 0))
79		00id 11386	. . . . . . . . . . . . . . 15 ⊢ (0 + 0) = 0
80	78, 79	eqtrdi 2814	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ((𝑁↑2) + (𝑀↑3)) = 0)
81	15, 80	eqtrd 2798	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝐺↑2) = 0)
82	13, 81	sqeq0d 14183	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → 𝐺 = 0)
83	82, 46	oveq12d 7430	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝐺 − 𝑁) = (0 − 0))
84		0m0e0 12360	. . . . . . . . . . 11 ⊢ (0 − 0) = 0
85	83, 84	eqtrdi 2814	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝐺 − 𝑁) = 0)
86	11, 85	eqtrd 2798	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → (𝑇↑3) = 0)
87	86	ex 417	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) → ((𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0) → (𝑇↑3) = 0))
88	87	necon3ad 2971	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) → ((𝑇↑3) ≠ 0 → ¬ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)))
89	9, 88	syld 48	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) → (𝑇 ≠ 0 → ¬ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)))
90	2, 89	mpd 16	. . . . 5 ⊢ ((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) → ¬ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0))
91		oveq12 7421	. . . . . . . . . . 11 ⊢ ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0 ∧ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0) → (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) + ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = (0 + 0))
92	91, 79	eqtrdi 2814	. . . . . . . . . 10 ⊢ ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0 ∧ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0) → (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) + ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = 0)
93		oveq12 7421	. . . . . . . . . . 11 ⊢ ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0 ∧ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0) → (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) − ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = (0 − 0))
94	93, 84	eqtrdi 2814	. . . . . . . . . 10 ⊢ ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0 ∧ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0) → (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) − ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = 0)
95	92, 94	jca 520	. . . . . . . . 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 15493	. . . . . . . . . . . . 13 ⊢ (𝜑 → (√‘((𝑋↑2) + (4 · 𝑀))) ∈ ℂ)
97		halfaddsub 12478	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∈ ℂ ∧ (√‘((𝑋↑2) + (4 · 𝑀))) ∈ ℂ) → ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) + ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = 𝑋 ∧ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) − ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = (√‘((𝑋↑2) + (4 · 𝑀)))))
98	62, 96, 97	syl2anc 595	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) + ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = 𝑋 ∧ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) − ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = (√‘((𝑋↑2) + (4 · 𝑀)))))
99	98	simpld 499	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) + ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = 𝑋)
100	99	eqeq1d 2765	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) + ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = 0 ↔ 𝑋 = 0))
101	98	simprd 500	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) − ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = (√‘((𝑋↑2) + (4 · 𝑀))))
102	101	eqeq1d 2765	. . . . . . . . . 10 ⊢ (𝜑 → ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) − ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = 0 ↔ (√‘((𝑋↑2) + (4 · 𝑀))) = 0))
103	100, 102	anbi12d 643	. . . . . . . . 9 ⊢ (𝜑 → (((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) + ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = 0 ∧ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) − ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) = 0) ↔ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)))
104	95, 103	imbitrid 247	. . . . . . . 8 ⊢ (𝜑 → ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0 ∧ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0) → (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)))
105	104	con3d 153	. . . . . . 7 ⊢ (𝜑 → (¬ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0) → ¬ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0 ∧ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0)))
106		eldifi 4086	. . . . . . . . . . . . . 14 ⊢ (𝑢 ∈ (ℂ ∖ {0}) → 𝑢 ∈ ℂ)
107	106	adantl 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → 𝑢 ∈ ℂ)
108	54	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → 𝑀 ∈ ℂ)
109		eldifsni 4759	. . . . . . . . . . . . . . 15 ⊢ (𝑢 ∈ (ℂ ∖ {0}) → 𝑢 ≠ 0)
110	109	adantl 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → 𝑢 ≠ 0)
111	108, 107, 110	divcld 11992	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑀 / 𝑢) ∈ ℂ)
112	62	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → 𝑋 ∈ ℂ)
113	107, 111, 112	subaddd 11588	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑢 − (𝑀 / 𝑢)) = 𝑋 ↔ ((𝑀 / 𝑢) + 𝑋) = 𝑢))
114		eqcom 2770	. . . . . . . . . . . 12 ⊢ (𝑋 = (𝑢 − (𝑀 / 𝑢)) ↔ (𝑢 − (𝑀 / 𝑢)) = 𝑋)
115		eqcom 2770	. . . . . . . . . . . 12 ⊢ (𝑢 = ((𝑀 / 𝑢) + 𝑋) ↔ ((𝑀 / 𝑢) + 𝑋) = 𝑢)
116	113, 114, 115	3bitr4g 317	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑋 = (𝑢 − (𝑀 / 𝑢)) ↔ 𝑢 = ((𝑀 / 𝑢) + 𝑋)))
117	107	sqcld 14182	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑢↑2) ∈ ℂ)
118	112, 107	mulcld 11230	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑋 · 𝑢) ∈ ℂ)
119	118, 108	addcld 11229	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑋 · 𝑢) + 𝑀) ∈ ℂ)
120	117, 119	subeq0ad 11580	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (((𝑢↑2) − ((𝑋 · 𝑢) + 𝑀)) = 0 ↔ (𝑢↑2) = ((𝑋 · 𝑢) + 𝑀)))
121	107	sqvald 14181	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑢↑2) = (𝑢 · 𝑢))
122	111, 112, 107	adddird 11235	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (((𝑀 / 𝑢) + 𝑋) · 𝑢) = (((𝑀 / 𝑢) · 𝑢) + (𝑋 · 𝑢)))
123	108, 107, 110	divcan1d 11993	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑀 / 𝑢) · 𝑢) = 𝑀)
124	123	oveq1d 7427	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (((𝑀 / 𝑢) · 𝑢) + (𝑋 · 𝑢)) = (𝑀 + (𝑋 · 𝑢)))
125	108, 118	addcomd 11413	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑀 + (𝑋 · 𝑢)) = ((𝑋 · 𝑢) + 𝑀))
126	122, 124, 125	3eqtrrd 2803	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑋 · 𝑢) + 𝑀) = (((𝑀 / 𝑢) + 𝑋) · 𝑢))
127	121, 126	eqeq12d 2779	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑢↑2) = ((𝑋 · 𝑢) + 𝑀) ↔ (𝑢 · 𝑢) = (((𝑀 / 𝑢) + 𝑋) · 𝑢)))
128	111, 112	addcld 11229	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑀 / 𝑢) + 𝑋) ∈ ℂ)
129	107, 128, 107, 110	mulcan2d 11849	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑢 · 𝑢) = (((𝑀 / 𝑢) + 𝑋) · 𝑢) ↔ 𝑢 = ((𝑀 / 𝑢) + 𝑋)))
130	120, 127, 129	3bitrd 308	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (((𝑢↑2) − ((𝑋 · 𝑢) + 𝑀)) = 0 ↔ 𝑢 = ((𝑀 / 𝑢) + 𝑋)))
131		1cnd 11203	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → 1 ∈ ℂ)
132		ax-1ne0 11170	. . . . . . . . . . . . . 14 ⊢ 1 ≠ 0
133	132	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → 1 ≠ 0)
134	62	negcld 11557	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -𝑋 ∈ ℂ)
135	134	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → -𝑋 ∈ ℂ)
136	54	negcld 11557	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -𝑀 ∈ ℂ)
137	136	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → -𝑀 ∈ ℂ)
138		sqneg 14153	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 ∈ ℂ → (-𝑋↑2) = (𝑋↑2))
139	112, 138	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (-𝑋↑2) = (𝑋↑2))
140	137	mullidd 11228	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (1 · -𝑀) = -𝑀)
141	140	oveq2d 7428	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (4 · (1 · -𝑀)) = (4 · -𝑀))
142		mulneg2 11652	. . . . . . . . . . . . . . . . 17 ⊢ ((4 ∈ ℂ ∧ 𝑀 ∈ ℂ) → (4 · -𝑀) = -(4 · 𝑀))
143	56, 108, 142	sylancr 598	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (4 · -𝑀) = -(4 · 𝑀))
144	141, 143	eqtrd 2798	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (4 · (1 · -𝑀)) = -(4 · 𝑀))
145	139, 144	oveq12d 7430	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((-𝑋↑2) − (4 · (1 · -𝑀))) = ((𝑋↑2) − -(4 · 𝑀)))
146	63	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑋↑2) ∈ ℂ)
147	65	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (4 · 𝑀) ∈ ℂ)
148	146, 147	subnegd 11577	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑋↑2) − -(4 · 𝑀)) = ((𝑋↑2) + (4 · 𝑀)))
149	145, 148	eqtr2d 2799	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑋↑2) + (4 · 𝑀)) = ((-𝑋↑2) − (4 · (1 · -𝑀))))
150	131, 133, 135, 137, 107, 149	quad 26983	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (((1 · (𝑢↑2)) + ((-𝑋 · 𝑢) + -𝑀)) = 0 ↔ (𝑢 = ((--𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / (2 · 1)) ∨ 𝑢 = ((--𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / (2 · 1)))))
151	117	mullidd 11228	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (1 · (𝑢↑2)) = (𝑢↑2))
152	112, 107	mulneg1d 11668	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (-𝑋 · 𝑢) = -(𝑋 · 𝑢))
153	152	oveq1d 7427	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((-𝑋 · 𝑢) + -𝑀) = (-(𝑋 · 𝑢) + -𝑀))
154	118, 108	negdid 11583	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → -((𝑋 · 𝑢) + 𝑀) = (-(𝑋 · 𝑢) + -𝑀))
155	153, 154	eqtr4d 2801	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((-𝑋 · 𝑢) + -𝑀) = -((𝑋 · 𝑢) + 𝑀))
156	151, 155	oveq12d 7430	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((1 · (𝑢↑2)) + ((-𝑋 · 𝑢) + -𝑀)) = ((𝑢↑2) + -((𝑋 · 𝑢) + 𝑀)))
157	117, 119	negsubd 11576	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑢↑2) + -((𝑋 · 𝑢) + 𝑀)) = ((𝑢↑2) − ((𝑋 · 𝑢) + 𝑀)))
158	156, 157	eqtrd 2798	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((1 · (𝑢↑2)) + ((-𝑋 · 𝑢) + -𝑀)) = ((𝑢↑2) − ((𝑋 · 𝑢) + 𝑀)))
159	158	eqeq1d 2765	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (((1 · (𝑢↑2)) + ((-𝑋 · 𝑢) + -𝑀)) = 0 ↔ ((𝑢↑2) − ((𝑋 · 𝑢) + 𝑀)) = 0))
160	112	negnegd 11561	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → --𝑋 = 𝑋)
161	160	oveq1d 7427	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (--𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) = (𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))))
162		2t1e2 12404	. . . . . . . . . . . . . . . 16 ⊢ (2 · 1) = 2
163	162	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (2 · 1) = 2)
164	161, 163	oveq12d 7430	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((--𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / (2 · 1)) = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2))
165	164	eqeq2d 2774	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑢 = ((--𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / (2 · 1)) ↔ 𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)))
166	160	oveq1d 7427	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (--𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) = (𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))))
167	166, 163	oveq12d 7430	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((--𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / (2 · 1)) = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2))
168	167	eqeq2d 2774	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑢 = ((--𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / (2 · 1)) ↔ 𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)))
169	165, 168	orbi12d 931	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → ((𝑢 = ((--𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / (2 · 1)) ∨ 𝑢 = ((--𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / (2 · 1))) ↔ (𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∨ 𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2))))
170	150, 159, 169	3bitr3d 312	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (((𝑢↑2) − ((𝑋 · 𝑢) + 𝑀)) = 0 ↔ (𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∨ 𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2))))
171	116, 130, 170	3bitr2d 310	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑢 ∈ (ℂ ∖ {0})) → (𝑋 = (𝑢 − (𝑀 / 𝑢)) ↔ (𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∨ 𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2))))
172	171	rexbidva 3187	. . . . . . . . 9 ⊢ (𝜑 → (∃𝑢 ∈ (ℂ ∖ {0})𝑋 = (𝑢 − (𝑀 / 𝑢)) ↔ ∃𝑢 ∈ (ℂ ∖ {0})(𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∨ 𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2))))
173		r19.43 3133	. . . . . . . . 9 ⊢ (∃𝑢 ∈ (ℂ ∖ {0})(𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∨ 𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) ↔ (∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∨ ∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)))
174	172, 173	bitrdi 290	. . . . . . . 8 ⊢ (𝜑 → (∃𝑢 ∈ (ℂ ∖ {0})𝑋 = (𝑢 − (𝑀 / 𝑢)) ↔ (∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∨ ∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2))))
175		risset 3240	. . . . . . . . . . 11 ⊢ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ (ℂ ∖ {0}) ↔ ∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2))
176	62, 96	addcld 11229	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) ∈ ℂ)
177	176	halfcld 12490	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ ℂ)
178		eldifsn 4754	. . . . . . . . . . . . 13 ⊢ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ (ℂ ∖ {0}) ↔ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ ℂ ∧ ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0))
179	178	baib 544	. . . . . . . . . . . 12 ⊢ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ ℂ → (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ (ℂ ∖ {0}) ↔ ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0))
180	177, 179	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ (ℂ ∖ {0}) ↔ ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0))
181	175, 180	bitr3id 288	. . . . . . . . . 10 ⊢ (𝜑 → (∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ↔ ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0))
182		risset 3240	. . . . . . . . . . 11 ⊢ (((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ (ℂ ∖ {0}) ↔ ∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2))
183	62, 96	subcld 11570	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) ∈ ℂ)
184	183	halfcld 12490	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ ℂ)
185		eldifsn 4754	. . . . . . . . . . . . 13 ⊢ (((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ (ℂ ∖ {0}) ↔ (((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ ℂ ∧ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0))
186	185	baib 544	. . . . . . . . . . . 12 ⊢ (((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ ℂ → (((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ (ℂ ∖ {0}) ↔ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0))
187	184, 186	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∈ (ℂ ∖ {0}) ↔ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0))
188	182, 187	bitr3id 288	. . . . . . . . . 10 ⊢ (𝜑 → (∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ↔ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0))
189	181, 188	orbi12d 931	. . . . . . . . 9 ⊢ (𝜑 → ((∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∨ ∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) ↔ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0 ∨ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0)))
190		neorian 3053	. . . . . . . . 9 ⊢ ((((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0 ∨ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ≠ 0) ↔ ¬ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0 ∧ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0))
191	189, 190	bitrdi 290	. . . . . . . 8 ⊢ (𝜑 → ((∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) ∨ ∃𝑢 ∈ (ℂ ∖ {0})𝑢 = ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2)) ↔ ¬ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0 ∧ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0)))
192	174, 191	bitrd 282	. . . . . . 7 ⊢ (𝜑 → (∃𝑢 ∈ (ℂ ∖ {0})𝑋 = (𝑢 − (𝑀 / 𝑢)) ↔ ¬ (((𝑋 + (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0 ∧ ((𝑋 − (√‘((𝑋↑2) + (4 · 𝑀)))) / 2) = 0)))
193	105, 192	sylibrd 262	. . . . . 6 ⊢ (𝜑 → (¬ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0) → ∃𝑢 ∈ (ℂ ∖ {0})𝑋 = (𝑢 − (𝑀 / 𝑢))))
194	193	imp 411	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝑋 = 0 ∧ (√‘((𝑋↑2) + (4 · 𝑀))) = 0)) → ∃𝑢 ∈ (ℂ ∖ {0})𝑋 = (𝑢 − (𝑀 / 𝑢)))
195	90, 194	syldan 602	. . . 4 ⊢ ((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) → ∃𝑢 ∈ (ℂ ∖ {0})𝑋 = (𝑢 − (𝑀 / 𝑢)))
196	20	ad2antrr 738	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑃 ∈ ℂ)
197	34	ad2antrr 738	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑄 ∈ ℂ)
198	62	ad2antrr 738	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑋 ∈ ℂ)
199	3	ad2antrr 738	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑇 ∈ ℂ)
200	10	ad2antrr 738	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → (𝑇↑3) = (𝐺 − 𝑁))
201	12	ad2antrr 738	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝐺 ∈ ℂ)
202	14	ad2antrr 738	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → (𝐺↑2) = ((𝑁↑2) + (𝑀↑3)))
203	48	ad2antrr 738	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑀 = (𝑃 / 3))
204	16	ad2antrr 738	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑁 = (𝑄 / 2))
205	1	ad2antrr 738	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑇 ≠ 0)
206	106	ad2antrl 740	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑢 ∈ ℂ)
207	109	ad2antrl 740	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑢 ≠ 0)
208		simprr 784	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → 𝑋 = (𝑢 − (𝑀 / 𝑢)))
209		simplr 780	. . . . 5 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0)
210	196, 197, 198, 199, 200, 201, 202, 203, 204, 205, 206, 207, 208, 209	dcubic2 26987	. . . 4 ⊢ (((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) ∧ (𝑢 ∈ (ℂ ∖ {0}) ∧ 𝑋 = (𝑢 − (𝑀 / 𝑢)))) → ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇)))))
211	195, 210	rexlimddv 3172	. . 3 ⊢ ((𝜑 ∧ ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0) → ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇)))))
212	211	ex 417	. 2 ⊢ (𝜑 → (((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0 → ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))))
213	20	ad2antrr 738	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑃 ∈ ℂ)
214	34	ad2antrr 738	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑄 ∈ ℂ)
215	62	ad2antrr 738	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑋 ∈ ℂ)
216		simplr 780	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑟 ∈ ℂ)
217	3	ad2antrr 738	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑇 ∈ ℂ)
218	216, 217	mulcld 11230	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → (𝑟 · 𝑇) ∈ ℂ)
219		3nn0 12523	. . . . . . 7 ⊢ 3 ∈ ℕ₀
220	219	a1i 11	. . . . . 6 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 3 ∈ ℕ₀)
221	216, 217, 220	mulexpd 14199	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → ((𝑟 · 𝑇)↑3) = ((𝑟↑3) · (𝑇↑3)))
222		simprl 782	. . . . . 6 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → (𝑟↑3) = 1)
223	222	oveq1d 7427	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → ((𝑟↑3) · (𝑇↑3)) = (1 · (𝑇↑3)))
224		expcl 14117	. . . . . . . . 9 ⊢ ((𝑇 ∈ ℂ ∧ 3 ∈ ℕ₀) → (𝑇↑3) ∈ ℂ)
225	3, 219, 224	sylancl 597	. . . . . . . 8 ⊢ (𝜑 → (𝑇↑3) ∈ ℂ)
226	225	mullidd 11228	. . . . . . 7 ⊢ (𝜑 → (1 · (𝑇↑3)) = (𝑇↑3))
227	226, 10	eqtrd 2798	. . . . . 6 ⊢ (𝜑 → (1 · (𝑇↑3)) = (𝐺 − 𝑁))
228	227	ad2antrr 738	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → (1 · (𝑇↑3)) = (𝐺 − 𝑁))
229	221, 223, 228	3eqtrd 2802	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → ((𝑟 · 𝑇)↑3) = (𝐺 − 𝑁))
230	12	ad2antrr 738	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝐺 ∈ ℂ)
231	14	ad2antrr 738	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → (𝐺↑2) = ((𝑁↑2) + (𝑀↑3)))
232	48	ad2antrr 738	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑀 = (𝑃 / 3))
233	16	ad2antrr 738	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑁 = (𝑄 / 2))
234	132	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 1 ≠ 0)
235	222, 234	eqnetrd 3025	. . . . . 6 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → (𝑟↑3) ≠ 0)
236		oveq1 7419	. . . . . . . 8 ⊢ (𝑟 = 0 → (𝑟↑3) = (0↑3))
237	236, 28	eqtrdi 2814	. . . . . . 7 ⊢ (𝑟 = 0 → (𝑟↑3) = 0)
238	237	necon3i 2990	. . . . . 6 ⊢ ((𝑟↑3) ≠ 0 → 𝑟 ≠ 0)
239	235, 238	syl 18	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑟 ≠ 0)
240	1	ad2antrr 738	. . . . 5 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑇 ≠ 0)
241	216, 217, 239, 240	mulne0d 11867	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → (𝑟 · 𝑇) ≠ 0)
242		simprr 784	. . . 4 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))
243	213, 214, 215, 218, 229, 230, 231, 232, 233, 241, 242	dcubic1 26988	. . 3 ⊢ (((𝜑 ∧ 𝑟 ∈ ℂ) ∧ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))) → ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0)
244	243	rexlimdva2 3168	. 2 ⊢ (𝜑 → (∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇)))) → ((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0))
245	212, 244	impbid 215	1 ⊢ (𝜑 → (((𝑋↑3) + ((𝑃 · 𝑋) + 𝑄)) = 0 ↔ ∃𝑟 ∈ ℂ ((𝑟↑3) = 1 ∧ 𝑋 = ((𝑟 · 𝑇) − (𝑀 / (𝑟 · 𝑇))))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∨ wo 860 = wceq 1570 ∈ wcel 2143 ≠ wne 2958 ∃wrex 3089 ∖ cdif 3903 {csn 4590 ‘cfv 6538 (class class class)co 7412 ℂcc 11099 0cc0 11101 1c1 11102 + caddc 11104 · cmul 11106 − cmin 11442 -cneg 11443 / cdiv 11872 ℕcn 12234 2c2 12296 3c3 12297 4c4 12298 ℕ₀cn0 12505 ℤcz 12592 ↑cexp 14099 √csqrt 15286

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-sep 5258 ax-nul 5270 ax-pow 5338 ax-pr 5406 ax-un 7734 ax-cnex 11157 ax-resscn 11158 ax-1cn 11159 ax-icn 11160 ax-addcl 11161 ax-addrcl 11162 ax-mulcl 11163 ax-mulrcl 11164 ax-mulcom 11165 ax-addass 11166 ax-mulass 11167 ax-distr 11168 ax-i2m1 11169 ax-1ne0 11170 ax-1rid 11171 ax-rnegex 11172 ax-rrecex 11173 ax-cnre 11174 ax-pre-lttri 11175 ax-pre-lttrn 11176 ax-pre-ltadd 11177 ax-pre-mulgt0 11178 ax-pre-sup 11179

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3746 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4288 df-if 4489 df-pw 4565 df-sn 4591 df-pr 4593 df-op 4597 df-uni 4874 df-iun 4959 df-br 5111 df-opab 5175 df-mpt 5194 df-tr 5220 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7864 df-2nd 7988 df-frecs 8279 df-wrecs 8310 df-recs 8359 df-rdg 8398 df-er 8695 df-en 8945 df-dom 8946 df-sdom 8947 df-sup 9403 df-pnf 11246 df-mnf 11247 df-xr 11248 df-ltxr 11249 df-le 11250 df-sub 11444 df-neg 11445 df-div 11873 df-nn 12235 df-2 12304 df-3 12305 df-4 12306 df-n0 12506 df-z 12593 df-uz 12864 df-rp 13018 df-seq 14040 df-exp 14100 df-cj 15152 df-re 15153 df-im 15154 df-sqrt 15288 df-abs 15289 df-dvds 16312

This theorem is referenced by: mcubic 26990

W3C validator