Metamath Proof Explorer

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 ∧ 𝑋 = ( ( 𝑟 · 𝑇 ) − ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) ) ) )