Theorem dcubic

Description: Solutions to the depressed cubic, a special case of cubic . (The definitions of M , N , G , T here differ from mcubic by scale factors of -u 9 , 5 4 , 5 4 and -u 2 7 respectively, to simplify the algebra and presentation.) (Contributed by Mario Carneiro, 26-Apr-2015)

	Ref	Expression
Hypotheses	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	dcubic	⊢ ( 𝜑 → ( ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ↔ ∃ 𝑟 ∈ ℂ ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = ( ( 𝑟 · 𝑇 ) − ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		dcubic.c	⊢ ( 𝜑 → 𝑃 ∈ ℂ )
2		dcubic.d	⊢ ( 𝜑 → 𝑄 ∈ ℂ )
3		dcubic.x	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
4		dcubic.t	⊢ ( 𝜑 → 𝑇 ∈ ℂ )
5		dcubic.3	⊢ ( 𝜑 → ( 𝑇 ↑ 3 ) = ( 𝐺 − 𝑁 ) )
6		dcubic.g	⊢ ( 𝜑 → 𝐺 ∈ ℂ )
7		dcubic.2	⊢ ( 𝜑 → ( 𝐺 ↑ 2 ) = ( ( 𝑁 ↑ 2 ) + ( 𝑀 ↑ 3 ) ) )
8		dcubic.m	⊢ ( 𝜑 → 𝑀 = ( 𝑃 / 3 ) )
9		dcubic.n	⊢ ( 𝜑 → 𝑁 = ( 𝑄 / 2 ) )
10		dcubic.0	⊢ ( 𝜑 → 𝑇 ≠ 0 )
11	10	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) → 𝑇 ≠ 0 )
12	4	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) → 𝑇 ∈ ℂ )
13		3z	⊢ 3 ∈ ℤ
14		expne0i	⊢ ( ( 𝑇 ∈ ℂ ∧ 𝑇 ≠ 0 ∧ 3 ∈ ℤ ) → ( 𝑇 ↑ 3 ) ≠ 0 )
15	13 14	mp3an3	⊢ ( ( 𝑇 ∈ ℂ ∧ 𝑇 ≠ 0 ) → ( 𝑇 ↑ 3 ) ≠ 0 )
16	15	ex	⊢ ( 𝑇 ∈ ℂ → ( 𝑇 ≠ 0 → ( 𝑇 ↑ 3 ) ≠ 0 ) )
17	12 16	syl	⊢ ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) → ( 𝑇 ≠ 0 → ( 𝑇 ↑ 3 ) ≠ 0 ) )
18	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) → ( 𝑇 ↑ 3 ) = ( 𝐺 − 𝑁 ) )
19	6	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) → 𝐺 ∈ ℂ )
20	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) → ( 𝐺 ↑ 2 ) = ( ( 𝑁 ↑ 2 ) + ( 𝑀 ↑ 3 ) ) )
21	9	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) → 𝑁 = ( 𝑄 / 2 ) )
22		simprl	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) → 𝑋 = 0 )
23	22	oveq2d	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) → ( 𝑃 · 𝑋 ) = ( 𝑃 · 0 ) )
24	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) → 𝑃 ∈ ℂ )
25	24	mul01d	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) → ( 𝑃 · 0 ) = 0 )
26	23 25	eqtrd	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) → ( 𝑃 · 𝑋 ) = 0 )
27	26	oveq1d	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) → ( ( 𝑃 · 𝑋 ) + 𝑄 ) = ( 0 + 𝑄 ) )
28	22	oveq1d	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) → ( 𝑋 ↑ 3 ) = ( 0 ↑ 3 ) )
29		3nn	⊢ 3 ∈ ℕ
30		0exp	⊢ ( 3 ∈ ℕ → ( 0 ↑ 3 ) = 0 )
31	29 30	ax-mp	⊢ ( 0 ↑ 3 ) = 0
32	28 31	eqtrdi	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) → ( 𝑋 ↑ 3 ) = 0 )
33	32	oveq1d	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) → ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = ( 0 + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) )
34		simplr	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) → ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 )
35		0cnd	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) → 0 ∈ ℂ )
36	26 35	eqeltrd	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) → ( 𝑃 · 𝑋 ) ∈ ℂ )
37	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) → 𝑄 ∈ ℂ )
38	36 37	addcld	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) → ( ( 𝑃 · 𝑋 ) + 𝑄 ) ∈ ℂ )
39	38	addlidd	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) → ( 0 + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = ( ( 𝑃 · 𝑋 ) + 𝑄 ) )
40	33 34 39	3eqtr3rd	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) → ( ( 𝑃 · 𝑋 ) + 𝑄 ) = 0 )
41	37	addlidd	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) → ( 0 + 𝑄 ) = 𝑄 )
42	27 40 41	3eqtr3rd	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) → 𝑄 = 0 )
43	42	oveq1d	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) → ( 𝑄 / 2 ) = ( 0 / 2 ) )
44		2cn	⊢ 2 ∈ ℂ
45		2ne0	⊢ 2 ≠ 0
46	44 45	div0i	⊢ ( 0 / 2 ) = 0
47	43 46	eqtrdi	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) → ( 𝑄 / 2 ) = 0 )
48	21 47	eqtrd	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) → 𝑁 = 0 )
49	48	sq0id	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) → ( 𝑁 ↑ 2 ) = 0 )
50		3cn	⊢ 3 ∈ ℂ
51	50	a1i	⊢ ( 𝜑 → 3 ∈ ℂ )
52		3ne0	⊢ 3 ≠ 0
53	52	a1i	⊢ ( 𝜑 → 3 ≠ 0 )
54	1 51 53	divcld	⊢ ( 𝜑 → ( 𝑃 / 3 ) ∈ ℂ )
55	8 54	eqeltrd	⊢ ( 𝜑 → 𝑀 ∈ ℂ )
56	55	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) → 𝑀 ∈ ℂ )
57		4cn	⊢ 4 ∈ ℂ
58	57	a1i	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) → 4 ∈ ℂ )
59		4ne0	⊢ 4 ≠ 0
60	59	a1i	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) → 4 ≠ 0 )
61	22	sq0id	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) → ( 𝑋 ↑ 2 ) = 0 )
62	61	oveq1d	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) → ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) = ( 0 + ( 4 · 𝑀 ) ) )
63	3	sqcld	⊢ ( 𝜑 → ( 𝑋 ↑ 2 ) ∈ ℂ )
64		mulcl	⊢ ( ( 4 ∈ ℂ ∧ 𝑀 ∈ ℂ ) → ( 4 · 𝑀 ) ∈ ℂ )
65	57 55 64	sylancr	⊢ ( 𝜑 → ( 4 · 𝑀 ) ∈ ℂ )
66	63 65	addcld	⊢ ( 𝜑 → ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ∈ ℂ )
67	66	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) → ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ∈ ℂ )
68		simprr	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) → ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 )
69	67 68	sqr00d	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) → ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) = 0 )
70	65	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) → ( 4 · 𝑀 ) ∈ ℂ )
71	70	addlidd	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) → ( 0 + ( 4 · 𝑀 ) ) = ( 4 · 𝑀 ) )
72	62 69 71	3eqtr3rd	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) → ( 4 · 𝑀 ) = 0 )
73	57	mul01i	⊢ ( 4 · 0 ) = 0
74	72 73	eqtr4di	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) → ( 4 · 𝑀 ) = ( 4 · 0 ) )
75	56 35 58 60 74	mulcanad	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) → 𝑀 = 0 )
76	75	oveq1d	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) → ( 𝑀 ↑ 3 ) = ( 0 ↑ 3 ) )
77	76 31	eqtrdi	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) → ( 𝑀 ↑ 3 ) = 0 )
78	49 77	oveq12d	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) → ( ( 𝑁 ↑ 2 ) + ( 𝑀 ↑ 3 ) ) = ( 0 + 0 ) )
79		00id	⊢ ( 0 + 0 ) = 0
80	78 79	eqtrdi	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) → ( ( 𝑁 ↑ 2 ) + ( 𝑀 ↑ 3 ) ) = 0 )
81	20 80	eqtrd	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) → ( 𝐺 ↑ 2 ) = 0 )
82	19 81	sqeq0d	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) → 𝐺 = 0 )
83	82 48	oveq12d	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) → ( 𝐺 − 𝑁 ) = ( 0 − 0 ) )
84		0m0e0	⊢ ( 0 − 0 ) = 0
85	83 84	eqtrdi	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) → ( 𝐺 − 𝑁 ) = 0 )
86	18 85	eqtrd	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) → ( 𝑇 ↑ 3 ) = 0 )
87	86	ex	⊢ ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) → ( ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) → ( 𝑇 ↑ 3 ) = 0 ) )
88	87	necon3ad	⊢ ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) → ( ( 𝑇 ↑ 3 ) ≠ 0 → ¬ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) )
89	17 88	syld	⊢ ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) → ( 𝑇 ≠ 0 → ¬ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) )
90	11 89	mpd	⊢ ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) → ¬ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) )
91		oveq12	⊢ ( ( ( ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) = 0 ∧ ( ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) = 0 ) → ( ( ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) + ( ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ) = ( 0 + 0 ) )
92	91 79	eqtrdi	⊢ ( ( ( ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) = 0 ∧ ( ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) = 0 ) → ( ( ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) + ( ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ) = 0 )
93		oveq12	⊢ ( ( ( ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) = 0 ∧ ( ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) = 0 ) → ( ( ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) − ( ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ) = ( 0 − 0 ) )
94	93 84	eqtrdi	⊢ ( ( ( ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) = 0 ∧ ( ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) = 0 ) → ( ( ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) − ( ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ) = 0 )
95	92 94	jca	⊢ ( ( ( ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 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	⊢ ( 𝜑 → ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ∈ ℂ )
97		halfaddsub	⊢ ( ( 𝑋 ∈ ℂ ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ∈ ℂ ) → ( ( ( ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) + ( ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ) = 𝑋 ∧ ( ( ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) − ( ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ) = ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) )
98	3 96 97	syl2anc	⊢ ( 𝜑 → ( ( ( ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) + ( ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ) = 𝑋 ∧ ( ( ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) − ( ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ) = ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) )
99	98	simpld	⊢ ( 𝜑 → ( ( ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) + ( ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ) = 𝑋 )
100	99	eqeq1d	⊢ ( 𝜑 → ( ( ( ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) + ( ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ) = 0 ↔ 𝑋 = 0 ) )
101	98	simprd	⊢ ( 𝜑 → ( ( ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) − ( ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ) = ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) )
102	101	eqeq1d	⊢ ( 𝜑 → ( ( ( ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) − ( ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ) = 0 ↔ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) )
103	100 102	anbi12d	⊢ ( 𝜑 → ( ( ( ( ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) + ( ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ) = 0 ∧ ( ( ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) − ( ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ) = 0 ) ↔ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) )
104	95 103	imbitrid	⊢ ( 𝜑 → ( ( ( ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) = 0 ∧ ( ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) = 0 ) → ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) )
105	104	con3d	⊢ ( 𝜑 → ( ¬ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) → ¬ ( ( ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) = 0 ∧ ( ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) = 0 ) ) )
106		eldifi	⊢ ( 𝑢 ∈ ( ℂ ∖ { 0 } ) → 𝑢 ∈ ℂ )
107	106	adantl	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → 𝑢 ∈ ℂ )
108	55	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → 𝑀 ∈ ℂ )
109		eldifsni	⊢ ( 𝑢 ∈ ( ℂ ∖ { 0 } ) → 𝑢 ≠ 0 )
110	109	adantl	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → 𝑢 ≠ 0 )
111	108 107 110	divcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑀 / 𝑢 ) ∈ ℂ )
112	3	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → 𝑋 ∈ ℂ )
113	107 111 112	subaddd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → ( ( 𝑢 − ( 𝑀 / 𝑢 ) ) = 𝑋 ↔ ( ( 𝑀 / 𝑢 ) + 𝑋 ) = 𝑢 ) )
114		eqcom	⊢ ( 𝑋 = ( 𝑢 − ( 𝑀 / 𝑢 ) ) ↔ ( 𝑢 − ( 𝑀 / 𝑢 ) ) = 𝑋 )
115		eqcom	⊢ ( 𝑢 = ( ( 𝑀 / 𝑢 ) + 𝑋 ) ↔ ( ( 𝑀 / 𝑢 ) + 𝑋 ) = 𝑢 )
116	113 114 115	3bitr4g	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑋 = ( 𝑢 − ( 𝑀 / 𝑢 ) ) ↔ 𝑢 = ( ( 𝑀 / 𝑢 ) + 𝑋 ) ) )
117	107	sqcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑢 ↑ 2 ) ∈ ℂ )
118	112 107	mulcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑋 · 𝑢 ) ∈ ℂ )
119	118 108	addcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → ( ( 𝑋 · 𝑢 ) + 𝑀 ) ∈ ℂ )
120	117 119	subeq0ad	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → ( ( ( 𝑢 ↑ 2 ) − ( ( 𝑋 · 𝑢 ) + 𝑀 ) ) = 0 ↔ ( 𝑢 ↑ 2 ) = ( ( 𝑋 · 𝑢 ) + 𝑀 ) ) )
121	107	sqvald	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑢 ↑ 2 ) = ( 𝑢 · 𝑢 ) )
122	111 112 107	adddird	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → ( ( ( 𝑀 / 𝑢 ) + 𝑋 ) · 𝑢 ) = ( ( ( 𝑀 / 𝑢 ) · 𝑢 ) + ( 𝑋 · 𝑢 ) ) )
123	108 107 110	divcan1d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → ( ( 𝑀 / 𝑢 ) · 𝑢 ) = 𝑀 )
124	123	oveq1d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → ( ( ( 𝑀 / 𝑢 ) · 𝑢 ) + ( 𝑋 · 𝑢 ) ) = ( 𝑀 + ( 𝑋 · 𝑢 ) ) )
125	108 118	addcomd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑀 + ( 𝑋 · 𝑢 ) ) = ( ( 𝑋 · 𝑢 ) + 𝑀 ) )
126	122 124 125	3eqtrrd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → ( ( 𝑋 · 𝑢 ) + 𝑀 ) = ( ( ( 𝑀 / 𝑢 ) + 𝑋 ) · 𝑢 ) )
127	121 126	eqeq12d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → ( ( 𝑢 ↑ 2 ) = ( ( 𝑋 · 𝑢 ) + 𝑀 ) ↔ ( 𝑢 · 𝑢 ) = ( ( ( 𝑀 / 𝑢 ) + 𝑋 ) · 𝑢 ) ) )
128	111 112	addcld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → ( ( 𝑀 / 𝑢 ) + 𝑋 ) ∈ ℂ )
129	107 128 107 110	mulcan2d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → ( ( 𝑢 · 𝑢 ) = ( ( ( 𝑀 / 𝑢 ) + 𝑋 ) · 𝑢 ) ↔ 𝑢 = ( ( 𝑀 / 𝑢 ) + 𝑋 ) ) )
130	120 127 129	3bitrd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → ( ( ( 𝑢 ↑ 2 ) − ( ( 𝑋 · 𝑢 ) + 𝑀 ) ) = 0 ↔ 𝑢 = ( ( 𝑀 / 𝑢 ) + 𝑋 ) ) )
131		1cnd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → 1 ∈ ℂ )
132		ax-1ne0	⊢ 1 ≠ 0
133	132	a1i	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → 1 ≠ 0 )
134	3	negcld	⊢ ( 𝜑 → - 𝑋 ∈ ℂ )
135	134	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → - 𝑋 ∈ ℂ )
136	55	negcld	⊢ ( 𝜑 → - 𝑀 ∈ ℂ )
137	136	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → - 𝑀 ∈ ℂ )
138		sqneg	⊢ ( 𝑋 ∈ ℂ → ( - 𝑋 ↑ 2 ) = ( 𝑋 ↑ 2 ) )
139	112 138	syl	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → ( - 𝑋 ↑ 2 ) = ( 𝑋 ↑ 2 ) )
140	137	mullidd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → ( 1 · - 𝑀 ) = - 𝑀 )
141	140	oveq2d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → ( 4 · ( 1 · - 𝑀 ) ) = ( 4 · - 𝑀 ) )
142		mulneg2	⊢ ( ( 4 ∈ ℂ ∧ 𝑀 ∈ ℂ ) → ( 4 · - 𝑀 ) = - ( 4 · 𝑀 ) )
143	57 108 142	sylancr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → ( 4 · - 𝑀 ) = - ( 4 · 𝑀 ) )
144	141 143	eqtrd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → ( 4 · ( 1 · - 𝑀 ) ) = - ( 4 · 𝑀 ) )
145	139 144	oveq12d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → ( ( - 𝑋 ↑ 2 ) − ( 4 · ( 1 · - 𝑀 ) ) ) = ( ( 𝑋 ↑ 2 ) − - ( 4 · 𝑀 ) ) )
146	63	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑋 ↑ 2 ) ∈ ℂ )
147	65	adantr	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → ( 4 · 𝑀 ) ∈ ℂ )
148	146 147	subnegd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → ( ( 𝑋 ↑ 2 ) − - ( 4 · 𝑀 ) ) = ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) )
149	145 148	eqtr2d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) = ( ( - 𝑋 ↑ 2 ) − ( 4 · ( 1 · - 𝑀 ) ) ) )
150	131 133 135 137 107 149	quad	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → ( ( ( 1 · ( 𝑢 ↑ 2 ) ) + ( ( - 𝑋 · 𝑢 ) + - 𝑀 ) ) = 0 ↔ ( 𝑢 = ( ( - - 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / ( 2 · 1 ) ) ∨ 𝑢 = ( ( - - 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / ( 2 · 1 ) ) ) ) )
151	117	mullidd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → ( 1 · ( 𝑢 ↑ 2 ) ) = ( 𝑢 ↑ 2 ) )
152	112 107	mulneg1d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → ( - 𝑋 · 𝑢 ) = - ( 𝑋 · 𝑢 ) )
153	152	oveq1d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → ( ( - 𝑋 · 𝑢 ) + - 𝑀 ) = ( - ( 𝑋 · 𝑢 ) + - 𝑀 ) )
154	118 108	negdid	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → - ( ( 𝑋 · 𝑢 ) + 𝑀 ) = ( - ( 𝑋 · 𝑢 ) + - 𝑀 ) )
155	153 154	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → ( ( - 𝑋 · 𝑢 ) + - 𝑀 ) = - ( ( 𝑋 · 𝑢 ) + 𝑀 ) )
156	151 155	oveq12d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → ( ( 1 · ( 𝑢 ↑ 2 ) ) + ( ( - 𝑋 · 𝑢 ) + - 𝑀 ) ) = ( ( 𝑢 ↑ 2 ) + - ( ( 𝑋 · 𝑢 ) + 𝑀 ) ) )
157	117 119	negsubd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → ( ( 𝑢 ↑ 2 ) + - ( ( 𝑋 · 𝑢 ) + 𝑀 ) ) = ( ( 𝑢 ↑ 2 ) − ( ( 𝑋 · 𝑢 ) + 𝑀 ) ) )
158	156 157	eqtrd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → ( ( 1 · ( 𝑢 ↑ 2 ) ) + ( ( - 𝑋 · 𝑢 ) + - 𝑀 ) ) = ( ( 𝑢 ↑ 2 ) − ( ( 𝑋 · 𝑢 ) + 𝑀 ) ) )
159	158	eqeq1d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → ( ( ( 1 · ( 𝑢 ↑ 2 ) ) + ( ( - 𝑋 · 𝑢 ) + - 𝑀 ) ) = 0 ↔ ( ( 𝑢 ↑ 2 ) − ( ( 𝑋 · 𝑢 ) + 𝑀 ) ) = 0 ) )
160	112	negnegd	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → - - 𝑋 = 𝑋 )
161	160	oveq1d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → ( - - 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) = ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) )
162		2t1e2	⊢ ( 2 · 1 ) = 2
163	162	a1i	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → ( 2 · 1 ) = 2 )
164	161 163	oveq12d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → ( ( - - 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / ( 2 · 1 ) ) = ( ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) )
165	164	eqeq2d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑢 = ( ( - - 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / ( 2 · 1 ) ) ↔ 𝑢 = ( ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ) )
166	160	oveq1d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → ( - - 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) = ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) )
167	166 163	oveq12d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → ( ( - - 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / ( 2 · 1 ) ) = ( ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) )
168	167	eqeq2d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑢 = ( ( - - 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / ( 2 · 1 ) ) ↔ 𝑢 = ( ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ) )
169	165 168	orbi12d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → ( ( 𝑢 = ( ( - - 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / ( 2 · 1 ) ) ∨ 𝑢 = ( ( - - 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / ( 2 · 1 ) ) ) ↔ ( 𝑢 = ( ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ∨ 𝑢 = ( ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ) ) )
170	150 159 169	3bitr3d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → ( ( ( 𝑢 ↑ 2 ) − ( ( 𝑋 · 𝑢 ) + 𝑀 ) ) = 0 ↔ ( 𝑢 = ( ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ∨ 𝑢 = ( ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ) ) )
171	116 130 170	3bitr2d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑋 = ( 𝑢 − ( 𝑀 / 𝑢 ) ) ↔ ( 𝑢 = ( ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ∨ 𝑢 = ( ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ) ) )
172	171	rexbidva	⊢ ( 𝜑 → ( ∃ 𝑢 ∈ ( ℂ ∖ { 0 } ) 𝑋 = ( 𝑢 − ( 𝑀 / 𝑢 ) ) ↔ ∃ 𝑢 ∈ ( ℂ ∖ { 0 } ) ( 𝑢 = ( ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ∨ 𝑢 = ( ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ) ) )
173		r19.43	⊢ ( ∃ 𝑢 ∈ ( ℂ ∖ { 0 } ) ( 𝑢 = ( ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ∨ 𝑢 = ( ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ) ↔ ( ∃ 𝑢 ∈ ( ℂ ∖ { 0 } ) 𝑢 = ( ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ∨ ∃ 𝑢 ∈ ( ℂ ∖ { 0 } ) 𝑢 = ( ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ) )
174	172 173	bitrdi	⊢ ( 𝜑 → ( ∃ 𝑢 ∈ ( ℂ ∖ { 0 } ) 𝑋 = ( 𝑢 − ( 𝑀 / 𝑢 ) ) ↔ ( ∃ 𝑢 ∈ ( ℂ ∖ { 0 } ) 𝑢 = ( ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ∨ ∃ 𝑢 ∈ ( ℂ ∖ { 0 } ) 𝑢 = ( ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ) ) )
175		risset	⊢ ( ( ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ∈ ( ℂ ∖ { 0 } ) ↔ ∃ 𝑢 ∈ ( ℂ ∖ { 0 } ) 𝑢 = ( ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) )
176	3 96	addcld	⊢ ( 𝜑 → ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) ∈ ℂ )
177	176	halfcld	⊢ ( 𝜑 → ( ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ∈ ℂ )
178		eldifsn	⊢ ( ( ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ∈ ( ℂ ∖ { 0 } ) ↔ ( ( ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ∈ ℂ ∧ ( ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ≠ 0 ) )
179	178	baib	⊢ ( ( ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ∈ ℂ → ( ( ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ∈ ( ℂ ∖ { 0 } ) ↔ ( ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ≠ 0 ) )
180	177 179	syl	⊢ ( 𝜑 → ( ( ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ∈ ( ℂ ∖ { 0 } ) ↔ ( ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ≠ 0 ) )
181	175 180	bitr3id	⊢ ( 𝜑 → ( ∃ 𝑢 ∈ ( ℂ ∖ { 0 } ) 𝑢 = ( ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ↔ ( ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ≠ 0 ) )
182		risset	⊢ ( ( ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ∈ ( ℂ ∖ { 0 } ) ↔ ∃ 𝑢 ∈ ( ℂ ∖ { 0 } ) 𝑢 = ( ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) )
183	3 96	subcld	⊢ ( 𝜑 → ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) ∈ ℂ )
184	183	halfcld	⊢ ( 𝜑 → ( ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ∈ ℂ )
185		eldifsn	⊢ ( ( ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ∈ ( ℂ ∖ { 0 } ) ↔ ( ( ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ∈ ℂ ∧ ( ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ≠ 0 ) )
186	185	baib	⊢ ( ( ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ∈ ℂ → ( ( ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ∈ ( ℂ ∖ { 0 } ) ↔ ( ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ≠ 0 ) )
187	184 186	syl	⊢ ( 𝜑 → ( ( ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ∈ ( ℂ ∖ { 0 } ) ↔ ( ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ≠ 0 ) )
188	182 187	bitr3id	⊢ ( 𝜑 → ( ∃ 𝑢 ∈ ( ℂ ∖ { 0 } ) 𝑢 = ( ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ↔ ( ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ≠ 0 ) )
189	181 188	orbi12d	⊢ ( 𝜑 → ( ( ∃ 𝑢 ∈ ( ℂ ∖ { 0 } ) 𝑢 = ( ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ∨ ∃ 𝑢 ∈ ( ℂ ∖ { 0 } ) 𝑢 = ( ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ) ↔ ( ( ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ≠ 0 ∨ ( ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ≠ 0 ) ) )
190		neorian	⊢ ( ( ( ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ≠ 0 ∨ ( ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ≠ 0 ) ↔ ¬ ( ( ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) = 0 ∧ ( ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) = 0 ) )
191	189 190	bitrdi	⊢ ( 𝜑 → ( ( ∃ 𝑢 ∈ ( ℂ ∖ { 0 } ) 𝑢 = ( ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ∨ ∃ 𝑢 ∈ ( ℂ ∖ { 0 } ) 𝑢 = ( ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) ) ↔ ¬ ( ( ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) = 0 ∧ ( ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) = 0 ) ) )
192	174 191	bitrd	⊢ ( 𝜑 → ( ∃ 𝑢 ∈ ( ℂ ∖ { 0 } ) 𝑋 = ( 𝑢 − ( 𝑀 / 𝑢 ) ) ↔ ¬ ( ( ( 𝑋 + ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) = 0 ∧ ( ( 𝑋 − ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) ) / 2 ) = 0 ) ) )
193	105 192	sylibrd	⊢ ( 𝜑 → ( ¬ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) → ∃ 𝑢 ∈ ( ℂ ∖ { 0 } ) 𝑋 = ( 𝑢 − ( 𝑀 / 𝑢 ) ) ) )
194	193	imp	⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 = 0 ∧ ( √ ‘ ( ( 𝑋 ↑ 2 ) + ( 4 · 𝑀 ) ) ) = 0 ) ) → ∃ 𝑢 ∈ ( ℂ ∖ { 0 } ) 𝑋 = ( 𝑢 − ( 𝑀 / 𝑢 ) ) )
195	90 194	syldan	⊢ ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) → ∃ 𝑢 ∈ ( ℂ ∖ { 0 } ) 𝑋 = ( 𝑢 − ( 𝑀 / 𝑢 ) ) )
196	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑢 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑋 = ( 𝑢 − ( 𝑀 / 𝑢 ) ) ) ) → 𝑃 ∈ ℂ )
197	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑢 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑋 = ( 𝑢 − ( 𝑀 / 𝑢 ) ) ) ) → 𝑄 ∈ ℂ )
198	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑢 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑋 = ( 𝑢 − ( 𝑀 / 𝑢 ) ) ) ) → 𝑋 ∈ ℂ )
199	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑢 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑋 = ( 𝑢 − ( 𝑀 / 𝑢 ) ) ) ) → 𝑇 ∈ ℂ )
200	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑢 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑋 = ( 𝑢 − ( 𝑀 / 𝑢 ) ) ) ) → ( 𝑇 ↑ 3 ) = ( 𝐺 − 𝑁 ) )
201	6	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑢 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑋 = ( 𝑢 − ( 𝑀 / 𝑢 ) ) ) ) → 𝐺 ∈ ℂ )
202	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑢 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑋 = ( 𝑢 − ( 𝑀 / 𝑢 ) ) ) ) → ( 𝐺 ↑ 2 ) = ( ( 𝑁 ↑ 2 ) + ( 𝑀 ↑ 3 ) ) )
203	8	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑢 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑋 = ( 𝑢 − ( 𝑀 / 𝑢 ) ) ) ) → 𝑀 = ( 𝑃 / 3 ) )
204	9	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑢 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑋 = ( 𝑢 − ( 𝑀 / 𝑢 ) ) ) ) → 𝑁 = ( 𝑄 / 2 ) )
205	10	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑢 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑋 = ( 𝑢 − ( 𝑀 / 𝑢 ) ) ) ) → 𝑇 ≠ 0 )
206	106	ad2antrl	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑢 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑋 = ( 𝑢 − ( 𝑀 / 𝑢 ) ) ) ) → 𝑢 ∈ ℂ )
207	109	ad2antrl	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑢 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑋 = ( 𝑢 − ( 𝑀 / 𝑢 ) ) ) ) → 𝑢 ≠ 0 )
208		simprr	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑢 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑋 = ( 𝑢 − ( 𝑀 / 𝑢 ) ) ) ) → 𝑋 = ( 𝑢 − ( 𝑀 / 𝑢 ) ) )
209		simplr	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑢 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑋 = ( 𝑢 − ( 𝑀 / 𝑢 ) ) ) ) → ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 )
210	196 197 198 199 200 201 202 203 204 205 206 207 208 209	dcubic2	⊢ ( ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) ∧ ( 𝑢 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑋 = ( 𝑢 − ( 𝑀 / 𝑢 ) ) ) ) → ∃ 𝑟 ∈ ℂ ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = ( ( 𝑟 · 𝑇 ) − ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) ) )
211	195 210	rexlimddv	⊢ ( ( 𝜑 ∧ ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) → ∃ 𝑟 ∈ ℂ ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = ( ( 𝑟 · 𝑇 ) − ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) ) )
212	211	ex	⊢ ( 𝜑 → ( ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 → ∃ 𝑟 ∈ ℂ ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = ( ( 𝑟 · 𝑇 ) − ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) ) ) )
213	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℂ ) ∧ ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = ( ( 𝑟 · 𝑇 ) − ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) ) ) → 𝑃 ∈ ℂ )
214	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℂ ) ∧ ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = ( ( 𝑟 · 𝑇 ) − ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) ) ) → 𝑄 ∈ ℂ )
215	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℂ ) ∧ ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = ( ( 𝑟 · 𝑇 ) − ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) ) ) → 𝑋 ∈ ℂ )
216		simplr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℂ ) ∧ ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = ( ( 𝑟 · 𝑇 ) − ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) ) ) → 𝑟 ∈ ℂ )
217	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℂ ) ∧ ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = ( ( 𝑟 · 𝑇 ) − ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) ) ) → 𝑇 ∈ ℂ )
218	216 217	mulcld	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℂ ) ∧ ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = ( ( 𝑟 · 𝑇 ) − ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) ) ) → ( 𝑟 · 𝑇 ) ∈ ℂ )
219		3nn0	⊢ 3 ∈ ℕ0
220	219	a1i	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℂ ) ∧ ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = ( ( 𝑟 · 𝑇 ) − ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) ) ) → 3 ∈ ℕ0 )
221	216 217 220	mulexpd	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℂ ) ∧ ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = ( ( 𝑟 · 𝑇 ) − ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) ) ) → ( ( 𝑟 · 𝑇 ) ↑ 3 ) = ( ( 𝑟 ↑ 3 ) · ( 𝑇 ↑ 3 ) ) )
222		simprl	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℂ ) ∧ ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = ( ( 𝑟 · 𝑇 ) − ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) ) ) → ( 𝑟 ↑ 3 ) = 1 )
223	222	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℂ ) ∧ ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = ( ( 𝑟 · 𝑇 ) − ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) ) ) → ( ( 𝑟 ↑ 3 ) · ( 𝑇 ↑ 3 ) ) = ( 1 · ( 𝑇 ↑ 3 ) ) )
224		expcl	⊢ ( ( 𝑇 ∈ ℂ ∧ 3 ∈ ℕ0 ) → ( 𝑇 ↑ 3 ) ∈ ℂ )
225	4 219 224	sylancl	⊢ ( 𝜑 → ( 𝑇 ↑ 3 ) ∈ ℂ )
226	225	mullidd	⊢ ( 𝜑 → ( 1 · ( 𝑇 ↑ 3 ) ) = ( 𝑇 ↑ 3 ) )
227	226 5	eqtrd	⊢ ( 𝜑 → ( 1 · ( 𝑇 ↑ 3 ) ) = ( 𝐺 − 𝑁 ) )
228	227	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℂ ) ∧ ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = ( ( 𝑟 · 𝑇 ) − ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) ) ) → ( 1 · ( 𝑇 ↑ 3 ) ) = ( 𝐺 − 𝑁 ) )
229	221 223 228	3eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℂ ) ∧ ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = ( ( 𝑟 · 𝑇 ) − ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) ) ) → ( ( 𝑟 · 𝑇 ) ↑ 3 ) = ( 𝐺 − 𝑁 ) )
230	6	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℂ ) ∧ ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = ( ( 𝑟 · 𝑇 ) − ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) ) ) → 𝐺 ∈ ℂ )
231	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℂ ) ∧ ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = ( ( 𝑟 · 𝑇 ) − ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) ) ) → ( 𝐺 ↑ 2 ) = ( ( 𝑁 ↑ 2 ) + ( 𝑀 ↑ 3 ) ) )
232	8	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℂ ) ∧ ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = ( ( 𝑟 · 𝑇 ) − ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) ) ) → 𝑀 = ( 𝑃 / 3 ) )
233	9	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℂ ) ∧ ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = ( ( 𝑟 · 𝑇 ) − ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) ) ) → 𝑁 = ( 𝑄 / 2 ) )
234	132	a1i	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℂ ) ∧ ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = ( ( 𝑟 · 𝑇 ) − ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) ) ) → 1 ≠ 0 )
235	222 234	eqnetrd	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℂ ) ∧ ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = ( ( 𝑟 · 𝑇 ) − ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) ) ) → ( 𝑟 ↑ 3 ) ≠ 0 )
236		oveq1	⊢ ( 𝑟 = 0 → ( 𝑟 ↑ 3 ) = ( 0 ↑ 3 ) )
237	236 31	eqtrdi	⊢ ( 𝑟 = 0 → ( 𝑟 ↑ 3 ) = 0 )
238	237	necon3i	⊢ ( ( 𝑟 ↑ 3 ) ≠ 0 → 𝑟 ≠ 0 )
239	235 238	syl	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℂ ) ∧ ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = ( ( 𝑟 · 𝑇 ) − ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) ) ) → 𝑟 ≠ 0 )
240	10	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℂ ) ∧ ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = ( ( 𝑟 · 𝑇 ) − ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) ) ) → 𝑇 ≠ 0 )
241	216 217 239 240	mulne0d	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℂ ) ∧ ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = ( ( 𝑟 · 𝑇 ) − ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) ) ) → ( 𝑟 · 𝑇 ) ≠ 0 )
242		simprr	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℂ ) ∧ ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = ( ( 𝑟 · 𝑇 ) − ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) ) ) → 𝑋 = ( ( 𝑟 · 𝑇 ) − ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) )
243	213 214 215 218 229 230 231 232 233 241 242	dcubic1	⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℂ ) ∧ ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = ( ( 𝑟 · 𝑇 ) − ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) ) ) → ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 )
244	243	rexlimdva2	⊢ ( 𝜑 → ( ∃ 𝑟 ∈ ℂ ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = ( ( 𝑟 · 𝑇 ) − ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) ) → ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ) )
245	212 244	impbid	⊢ ( 𝜑 → ( ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ↔ ∃ 𝑟 ∈ ℂ ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = ( ( 𝑟 · 𝑇 ) − ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) ) ) )