Metamath Proof Explorer

Theorem dcubic2

Description: Reverse direction of dcubic . Given a solution U to the "substitution" quadratic equation X = U - M / U , show that X is in the desired form. (Contributed by Mario Carneiro, 25-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 )
dcubic2.u ⊢ ( 𝜑 → 𝑈 ∈ ℂ )
dcubic2.z ⊢ ( 𝜑 → 𝑈 ≠ 0 )
dcubic2.2 ⊢ ( 𝜑 → 𝑋 = ( 𝑈 − ( 𝑀 / 𝑈 ) ) )
dcubic2.x ⊢ ( 𝜑 → ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 )
Assertion dcubic2 ( 𝜑 → ∃ 𝑟 ∈ ℂ ( ( 𝑟 ↑ 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 dcubic2.u ⊢ ( 𝜑 → 𝑈 ∈ ℂ )
12 dcubic2.z ⊢ ( 𝜑 → 𝑈 ≠ 0 )
13 dcubic2.2 ⊢ ( 𝜑 → 𝑋 = ( 𝑈 − ( 𝑀 / 𝑈 ) ) )
14 dcubic2.x ⊢ ( 𝜑 → ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 )
15 11 4 10 divcld ⊢ ( 𝜑 → ( 𝑈 / 𝑇 ) ∈ ℂ )
16 15 adantr ⊢ ( ( 𝜑 ∧ ( 𝑈 ↑ 3 ) = ( 𝐺 − 𝑁 ) ) → ( 𝑈 / 𝑇 ) ∈ ℂ )
17 3nn0 ⊢ 3 ∈ ℕ0
18 17 a1i ⊢ ( 𝜑 → 3 ∈ ℕ0 )
19 11 4 10 18 expdivd ⊢ ( 𝜑 → ( ( 𝑈 / 𝑇 ) ↑ 3 ) = ( ( 𝑈 ↑ 3 ) / ( 𝑇 ↑ 3 ) ) )
20 19 adantr ⊢ ( ( 𝜑 ∧ ( 𝑈 ↑ 3 ) = ( 𝐺 − 𝑁 ) ) → ( ( 𝑈 / 𝑇 ) ↑ 3 ) = ( ( 𝑈 ↑ 3 ) / ( 𝑇 ↑ 3 ) ) )
21 oveq1 ⊢ ( ( 𝑈 ↑ 3 ) = ( 𝐺 − 𝑁 ) → ( ( 𝑈 ↑ 3 ) / ( 𝑇 ↑ 3 ) ) = ( ( 𝐺 − 𝑁 ) / ( 𝑇 ↑ 3 ) ) )
22 5 oveq1d ⊢ ( 𝜑 → ( ( 𝑇 ↑ 3 ) / ( 𝑇 ↑ 3 ) ) = ( ( 𝐺 − 𝑁 ) / ( 𝑇 ↑ 3 ) ) )
23 expcl ⊢ ( ( 𝑇 ∈ ℂ ∧ 3 ∈ ℕ0 ) → ( 𝑇 ↑ 3 ) ∈ ℂ )
24 4 17 23 sylancl ⊢ ( 𝜑 → ( 𝑇 ↑ 3 ) ∈ ℂ )
25 3z ⊢ 3 ∈ ℤ
26 25 a1i ⊢ ( 𝜑 → 3 ∈ ℤ )
27 4 10 26 expne0d ⊢ ( 𝜑 → ( 𝑇 ↑ 3 ) ≠ 0 )
28 24 27 dividd ⊢ ( 𝜑 → ( ( 𝑇 ↑ 3 ) / ( 𝑇 ↑ 3 ) ) = 1 )
29 22 28 eqtr3d ⊢ ( 𝜑 → ( ( 𝐺 − 𝑁 ) / ( 𝑇 ↑ 3 ) ) = 1 )
30 21 29 sylan9eqr ⊢ ( ( 𝜑 ∧ ( 𝑈 ↑ 3 ) = ( 𝐺 − 𝑁 ) ) → ( ( 𝑈 ↑ 3 ) / ( 𝑇 ↑ 3 ) ) = 1 )
31 20 30 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑈 ↑ 3 ) = ( 𝐺 − 𝑁 ) ) → ( ( 𝑈 / 𝑇 ) ↑ 3 ) = 1 )
32 11 4 10 divcan1d ⊢ ( 𝜑 → ( ( 𝑈 / 𝑇 ) · 𝑇 ) = 𝑈 )
33 32 oveq2d ⊢ ( 𝜑 → ( 𝑀 / ( ( 𝑈 / 𝑇 ) · 𝑇 ) ) = ( 𝑀 / 𝑈 ) )
34 32 33 oveq12d ⊢ ( 𝜑 → ( ( ( 𝑈 / 𝑇 ) · 𝑇 ) − ( 𝑀 / ( ( 𝑈 / 𝑇 ) · 𝑇 ) ) ) = ( 𝑈 − ( 𝑀 / 𝑈 ) ) )
35 13 34 eqtr4d ⊢ ( 𝜑 → 𝑋 = ( ( ( 𝑈 / 𝑇 ) · 𝑇 ) − ( 𝑀 / ( ( 𝑈 / 𝑇 ) · 𝑇 ) ) ) )
36 35 adantr ⊢ ( ( 𝜑 ∧ ( 𝑈 ↑ 3 ) = ( 𝐺 − 𝑁 ) ) → 𝑋 = ( ( ( 𝑈 / 𝑇 ) · 𝑇 ) − ( 𝑀 / ( ( 𝑈 / 𝑇 ) · 𝑇 ) ) ) )
37 oveq1 ⊢ ( 𝑟 = ( 𝑈 / 𝑇 ) → ( 𝑟 ↑ 3 ) = ( ( 𝑈 / 𝑇 ) ↑ 3 ) )
38 37 eqeq1d ⊢ ( 𝑟 = ( 𝑈 / 𝑇 ) → ( ( 𝑟 ↑ 3 ) = 1 ↔ ( ( 𝑈 / 𝑇 ) ↑ 3 ) = 1 ) )
39 oveq1 ⊢ ( 𝑟 = ( 𝑈 / 𝑇 ) → ( 𝑟 · 𝑇 ) = ( ( 𝑈 / 𝑇 ) · 𝑇 ) )
40 39 oveq2d ⊢ ( 𝑟 = ( 𝑈 / 𝑇 ) → ( 𝑀 / ( 𝑟 · 𝑇 ) ) = ( 𝑀 / ( ( 𝑈 / 𝑇 ) · 𝑇 ) ) )
41 39 40 oveq12d ⊢ ( 𝑟 = ( 𝑈 / 𝑇 ) → ( ( 𝑟 · 𝑇 ) − ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) = ( ( ( 𝑈 / 𝑇 ) · 𝑇 ) − ( 𝑀 / ( ( 𝑈 / 𝑇 ) · 𝑇 ) ) ) )
42 41 eqeq2d ⊢ ( 𝑟 = ( 𝑈 / 𝑇 ) → ( 𝑋 = ( ( 𝑟 · 𝑇 ) − ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) ↔ 𝑋 = ( ( ( 𝑈 / 𝑇 ) · 𝑇 ) − ( 𝑀 / ( ( 𝑈 / 𝑇 ) · 𝑇 ) ) ) ) )
43 38 42 anbi12d ⊢ ( 𝑟 = ( 𝑈 / 𝑇 ) → ( ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = ( ( 𝑟 · 𝑇 ) − ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) ) ↔ ( ( ( 𝑈 / 𝑇 ) ↑ 3 ) = 1 ∧ 𝑋 = ( ( ( 𝑈 / 𝑇 ) · 𝑇 ) − ( 𝑀 / ( ( 𝑈 / 𝑇 ) · 𝑇 ) ) ) ) ) )
44 43 rspcev ⊢ ( ( ( 𝑈 / 𝑇 ) ∈ ℂ ∧ ( ( ( 𝑈 / 𝑇 ) ↑ 3 ) = 1 ∧ 𝑋 = ( ( ( 𝑈 / 𝑇 ) · 𝑇 ) − ( 𝑀 / ( ( 𝑈 / 𝑇 ) · 𝑇 ) ) ) ) ) → ∃ 𝑟 ∈ ℂ ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = ( ( 𝑟 · 𝑇 ) − ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) ) )
45 16 31 36 44 syl12anc ⊢ ( ( 𝜑 ∧ ( 𝑈 ↑ 3 ) = ( 𝐺 − 𝑁 ) ) → ∃ 𝑟 ∈ ℂ ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = ( ( 𝑟 · 𝑇 ) − ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) ) )
46 3cn ⊢ 3 ∈ ℂ
47 46 a1i ⊢ ( 𝜑 → 3 ∈ ℂ )
48 3ne0 ⊢ 3 ≠ 0
49 48 a1i ⊢ ( 𝜑 → 3 ≠ 0 )
50 1 47 49 divcld ⊢ ( 𝜑 → ( 𝑃 / 3 ) ∈ ℂ )
51 8 50 eqeltrd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
52 51 11 12 divcld ⊢ ( 𝜑 → ( 𝑀 / 𝑈 ) ∈ ℂ )
53 52 negcld ⊢ ( 𝜑 → - ( 𝑀 / 𝑈 ) ∈ ℂ )
54 53 4 10 divcld ⊢ ( 𝜑 → ( - ( 𝑀 / 𝑈 ) / 𝑇 ) ∈ ℂ )
55 54 adantr ⊢ ( ( 𝜑 ∧ ( 𝑈 ↑ 3 ) = - ( 𝐺 + 𝑁 ) ) → ( - ( 𝑀 / 𝑈 ) / 𝑇 ) ∈ ℂ )
56 53 4 10 18 expdivd ⊢ ( 𝜑 → ( ( - ( 𝑀 / 𝑈 ) / 𝑇 ) ↑ 3 ) = ( ( - ( 𝑀 / 𝑈 ) ↑ 3 ) / ( 𝑇 ↑ 3 ) ) )
57 51 11 12 divnegd ⊢ ( 𝜑 → - ( 𝑀 / 𝑈 ) = ( - 𝑀 / 𝑈 ) )
58 57 oveq1d ⊢ ( 𝜑 → ( - ( 𝑀 / 𝑈 ) ↑ 3 ) = ( ( - 𝑀 / 𝑈 ) ↑ 3 ) )
59 51 negcld ⊢ ( 𝜑 → - 𝑀 ∈ ℂ )
60 59 11 12 18 expdivd ⊢ ( 𝜑 → ( ( - 𝑀 / 𝑈 ) ↑ 3 ) = ( ( - 𝑀 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) )
61 5 oveq2d ⊢ ( 𝜑 → ( ( 𝐺 + 𝑁 ) · ( 𝑇 ↑ 3 ) ) = ( ( 𝐺 + 𝑁 ) · ( 𝐺 − 𝑁 ) ) )
62 2 halfcld ⊢ ( 𝜑 → ( 𝑄 / 2 ) ∈ ℂ )
63 9 62 eqeltrd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
64 subsq ⊢ ( ( 𝐺 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( 𝐺 ↑ 2 ) − ( 𝑁 ↑ 2 ) ) = ( ( 𝐺 + 𝑁 ) · ( 𝐺 − 𝑁 ) ) )
65 6 63 64 syl2anc ⊢ ( 𝜑 → ( ( 𝐺 ↑ 2 ) − ( 𝑁 ↑ 2 ) ) = ( ( 𝐺 + 𝑁 ) · ( 𝐺 − 𝑁 ) ) )
66 61 65 eqtr4d ⊢ ( 𝜑 → ( ( 𝐺 + 𝑁 ) · ( 𝑇 ↑ 3 ) ) = ( ( 𝐺 ↑ 2 ) − ( 𝑁 ↑ 2 ) ) )
67 7 oveq1d ⊢ ( 𝜑 → ( ( 𝐺 ↑ 2 ) − ( 𝑁 ↑ 2 ) ) = ( ( ( 𝑁 ↑ 2 ) + ( 𝑀 ↑ 3 ) ) − ( 𝑁 ↑ 2 ) ) )
68 63 sqcld ⊢ ( 𝜑 → ( 𝑁 ↑ 2 ) ∈ ℂ )
69 expcl ⊢ ( ( 𝑀 ∈ ℂ ∧ 3 ∈ ℕ0 ) → ( 𝑀 ↑ 3 ) ∈ ℂ )
70 51 17 69 sylancl ⊢ ( 𝜑 → ( 𝑀 ↑ 3 ) ∈ ℂ )
71 68 70 pncan2d ⊢ ( 𝜑 → ( ( ( 𝑁 ↑ 2 ) + ( 𝑀 ↑ 3 ) ) − ( 𝑁 ↑ 2 ) ) = ( 𝑀 ↑ 3 ) )
72 66 67 71 3eqtrd ⊢ ( 𝜑 → ( ( 𝐺 + 𝑁 ) · ( 𝑇 ↑ 3 ) ) = ( 𝑀 ↑ 3 ) )
73 72 negeqd ⊢ ( 𝜑 → - ( ( 𝐺 + 𝑁 ) · ( 𝑇 ↑ 3 ) ) = - ( 𝑀 ↑ 3 ) )
74 6 63 addcld ⊢ ( 𝜑 → ( 𝐺 + 𝑁 ) ∈ ℂ )
75 74 24 mulneg1d ⊢ ( 𝜑 → ( - ( 𝐺 + 𝑁 ) · ( 𝑇 ↑ 3 ) ) = - ( ( 𝐺 + 𝑁 ) · ( 𝑇 ↑ 3 ) ) )
76 3nn ⊢ 3 ∈ ℕ
77 76 a1i ⊢ ( 𝜑 → 3 ∈ ℕ )
78 n2dvds3 ⊢ ¬ 2 ∥ 3
79 78 a1i ⊢ ( 𝜑 → ¬ 2 ∥ 3 )
80 oexpneg ⊢ ( ( 𝑀 ∈ ℂ ∧ 3 ∈ ℕ ∧ ¬ 2 ∥ 3 ) → ( - 𝑀 ↑ 3 ) = - ( 𝑀 ↑ 3 ) )
81 51 77 79 80 syl3anc ⊢ ( 𝜑 → ( - 𝑀 ↑ 3 ) = - ( 𝑀 ↑ 3 ) )
82 73 75 81 3eqtr4d ⊢ ( 𝜑 → ( - ( 𝐺 + 𝑁 ) · ( 𝑇 ↑ 3 ) ) = ( - 𝑀 ↑ 3 ) )
83 82 oveq1d ⊢ ( 𝜑 → ( ( - ( 𝐺 + 𝑁 ) · ( 𝑇 ↑ 3 ) ) / ( 𝑈 ↑ 3 ) ) = ( ( - 𝑀 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) )
84 74 negcld ⊢ ( 𝜑 → - ( 𝐺 + 𝑁 ) ∈ ℂ )
85 expcl ⊢ ( ( 𝑈 ∈ ℂ ∧ 3 ∈ ℕ0 ) → ( 𝑈 ↑ 3 ) ∈ ℂ )
86 11 17 85 sylancl ⊢ ( 𝜑 → ( 𝑈 ↑ 3 ) ∈ ℂ )
87 11 12 26 expne0d ⊢ ( 𝜑 → ( 𝑈 ↑ 3 ) ≠ 0 )
88 84 24 86 87 div23d ⊢ ( 𝜑 → ( ( - ( 𝐺 + 𝑁 ) · ( 𝑇 ↑ 3 ) ) / ( 𝑈 ↑ 3 ) ) = ( ( - ( 𝐺 + 𝑁 ) / ( 𝑈 ↑ 3 ) ) · ( 𝑇 ↑ 3 ) ) )
89 83 88 eqtr3d ⊢ ( 𝜑 → ( ( - 𝑀 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) = ( ( - ( 𝐺 + 𝑁 ) / ( 𝑈 ↑ 3 ) ) · ( 𝑇 ↑ 3 ) ) )
90 58 60 89 3eqtrd ⊢ ( 𝜑 → ( - ( 𝑀 / 𝑈 ) ↑ 3 ) = ( ( - ( 𝐺 + 𝑁 ) / ( 𝑈 ↑ 3 ) ) · ( 𝑇 ↑ 3 ) ) )
91 90 oveq1d ⊢ ( 𝜑 → ( ( - ( 𝑀 / 𝑈 ) ↑ 3 ) / ( 𝑇 ↑ 3 ) ) = ( ( ( - ( 𝐺 + 𝑁 ) / ( 𝑈 ↑ 3 ) ) · ( 𝑇 ↑ 3 ) ) / ( 𝑇 ↑ 3 ) ) )
92 84 86 87 divcld ⊢ ( 𝜑 → ( - ( 𝐺 + 𝑁 ) / ( 𝑈 ↑ 3 ) ) ∈ ℂ )
93 92 24 27 divcan4d ⊢ ( 𝜑 → ( ( ( - ( 𝐺 + 𝑁 ) / ( 𝑈 ↑ 3 ) ) · ( 𝑇 ↑ 3 ) ) / ( 𝑇 ↑ 3 ) ) = ( - ( 𝐺 + 𝑁 ) / ( 𝑈 ↑ 3 ) ) )
94 56 91 93 3eqtrd ⊢ ( 𝜑 → ( ( - ( 𝑀 / 𝑈 ) / 𝑇 ) ↑ 3 ) = ( - ( 𝐺 + 𝑁 ) / ( 𝑈 ↑ 3 ) ) )
95 94 adantr ⊢ ( ( 𝜑 ∧ ( 𝑈 ↑ 3 ) = - ( 𝐺 + 𝑁 ) ) → ( ( - ( 𝑀 / 𝑈 ) / 𝑇 ) ↑ 3 ) = ( - ( 𝐺 + 𝑁 ) / ( 𝑈 ↑ 3 ) ) )
96 oveq1 ⊢ ( ( 𝑈 ↑ 3 ) = - ( 𝐺 + 𝑁 ) → ( ( 𝑈 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) = ( - ( 𝐺 + 𝑁 ) / ( 𝑈 ↑ 3 ) ) )
97 96 eqcomd ⊢ ( ( 𝑈 ↑ 3 ) = - ( 𝐺 + 𝑁 ) → ( - ( 𝐺 + 𝑁 ) / ( 𝑈 ↑ 3 ) ) = ( ( 𝑈 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) )
98 86 87 dividd ⊢ ( 𝜑 → ( ( 𝑈 ↑ 3 ) / ( 𝑈 ↑ 3 ) ) = 1 )
99 97 98 sylan9eqr ⊢ ( ( 𝜑 ∧ ( 𝑈 ↑ 3 ) = - ( 𝐺 + 𝑁 ) ) → ( - ( 𝐺 + 𝑁 ) / ( 𝑈 ↑ 3 ) ) = 1 )
100 95 99 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑈 ↑ 3 ) = - ( 𝐺 + 𝑁 ) ) → ( ( - ( 𝑀 / 𝑈 ) / 𝑇 ) ↑ 3 ) = 1 )
101 52 11 neg2subd ⊢ ( 𝜑 → ( - ( 𝑀 / 𝑈 ) − - 𝑈 ) = ( 𝑈 − ( 𝑀 / 𝑈 ) ) )
102 13 101 eqtr4d ⊢ ( 𝜑 → 𝑋 = ( - ( 𝑀 / 𝑈 ) − - 𝑈 ) )
103 102 adantr ⊢ ( ( 𝜑 ∧ ( 𝑈 ↑ 3 ) = - ( 𝐺 + 𝑁 ) ) → 𝑋 = ( - ( 𝑀 / 𝑈 ) − - 𝑈 ) )
104 53 4 10 divcan1d ⊢ ( 𝜑 → ( ( - ( 𝑀 / 𝑈 ) / 𝑇 ) · 𝑇 ) = - ( 𝑀 / 𝑈 ) )
105 104 adantr ⊢ ( ( 𝜑 ∧ ( 𝑈 ↑ 3 ) = - ( 𝐺 + 𝑁 ) ) → ( ( - ( 𝑀 / 𝑈 ) / 𝑇 ) · 𝑇 ) = - ( 𝑀 / 𝑈 ) )
106 51 11 12 divneg2d ⊢ ( 𝜑 → - ( 𝑀 / 𝑈 ) = ( 𝑀 / - 𝑈 ) )
107 104 106 eqtrd ⊢ ( 𝜑 → ( ( - ( 𝑀 / 𝑈 ) / 𝑇 ) · 𝑇 ) = ( 𝑀 / - 𝑈 ) )
108 107 adantr ⊢ ( ( 𝜑 ∧ ( 𝑈 ↑ 3 ) = - ( 𝐺 + 𝑁 ) ) → ( ( - ( 𝑀 / 𝑈 ) / 𝑇 ) · 𝑇 ) = ( 𝑀 / - 𝑈 ) )
109 108 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑈 ↑ 3 ) = - ( 𝐺 + 𝑁 ) ) → ( 𝑀 / ( ( - ( 𝑀 / 𝑈 ) / 𝑇 ) · 𝑇 ) ) = ( 𝑀 / ( 𝑀 / - 𝑈 ) ) )
110 51 adantr ⊢ ( ( 𝜑 ∧ ( 𝑈 ↑ 3 ) = - ( 𝐺 + 𝑁 ) ) → 𝑀 ∈ ℂ )
111 11 negcld ⊢ ( 𝜑 → - 𝑈 ∈ ℂ )
112 111 adantr ⊢ ( ( 𝜑 ∧ ( 𝑈 ↑ 3 ) = - ( 𝐺 + 𝑁 ) ) → - 𝑈 ∈ ℂ )
113 75 73 eqtrd ⊢ ( 𝜑 → ( - ( 𝐺 + 𝑁 ) · ( 𝑇 ↑ 3 ) ) = - ( 𝑀 ↑ 3 ) )
114 113 adantr ⊢ ( ( 𝜑 ∧ ( 𝑈 ↑ 3 ) = - ( 𝐺 + 𝑁 ) ) → ( - ( 𝐺 + 𝑁 ) · ( 𝑇 ↑ 3 ) ) = - ( 𝑀 ↑ 3 ) )
115 84 adantr ⊢ ( ( 𝜑 ∧ ( 𝑈 ↑ 3 ) = - ( 𝐺 + 𝑁 ) ) → - ( 𝐺 + 𝑁 ) ∈ ℂ )
116 24 adantr ⊢ ( ( 𝜑 ∧ ( 𝑈 ↑ 3 ) = - ( 𝐺 + 𝑁 ) ) → ( 𝑇 ↑ 3 ) ∈ ℂ )
117 simpr ⊢ ( ( 𝜑 ∧ ( 𝑈 ↑ 3 ) = - ( 𝐺 + 𝑁 ) ) → ( 𝑈 ↑ 3 ) = - ( 𝐺 + 𝑁 ) )
118 87 adantr ⊢ ( ( 𝜑 ∧ ( 𝑈 ↑ 3 ) = - ( 𝐺 + 𝑁 ) ) → ( 𝑈 ↑ 3 ) ≠ 0 )
119 117 118 eqnetrrd ⊢ ( ( 𝜑 ∧ ( 𝑈 ↑ 3 ) = - ( 𝐺 + 𝑁 ) ) → - ( 𝐺 + 𝑁 ) ≠ 0 )
120 27 adantr ⊢ ( ( 𝜑 ∧ ( 𝑈 ↑ 3 ) = - ( 𝐺 + 𝑁 ) ) → ( 𝑇 ↑ 3 ) ≠ 0 )
121 115 116 119 120 mulne0d ⊢ ( ( 𝜑 ∧ ( 𝑈 ↑ 3 ) = - ( 𝐺 + 𝑁 ) ) → ( - ( 𝐺 + 𝑁 ) · ( 𝑇 ↑ 3 ) ) ≠ 0 )
122 114 121 eqnetrrd ⊢ ( ( 𝜑 ∧ ( 𝑈 ↑ 3 ) = - ( 𝐺 + 𝑁 ) ) → - ( 𝑀 ↑ 3 ) ≠ 0 )
123 oveq1 ⊢ ( 𝑀 = 0 → ( 𝑀 ↑ 3 ) = ( 0 ↑ 3 ) )
124 0exp ⊢ ( 3 ∈ ℕ → ( 0 ↑ 3 ) = 0 )
125 76 124 ax-mp ⊢ ( 0 ↑ 3 ) = 0
126 123 125 eqtrdi ⊢ ( 𝑀 = 0 → ( 𝑀 ↑ 3 ) = 0 )
127 126 negeqd ⊢ ( 𝑀 = 0 → - ( 𝑀 ↑ 3 ) = - 0 )
128 neg0 ⊢ - 0 = 0
129 127 128 eqtrdi ⊢ ( 𝑀 = 0 → - ( 𝑀 ↑ 3 ) = 0 )
130 129 necon3i ⊢ ( - ( 𝑀 ↑ 3 ) ≠ 0 → 𝑀 ≠ 0 )
131 122 130 syl ⊢ ( ( 𝜑 ∧ ( 𝑈 ↑ 3 ) = - ( 𝐺 + 𝑁 ) ) → 𝑀 ≠ 0 )
132 11 12 negne0d ⊢ ( 𝜑 → - 𝑈 ≠ 0 )
133 132 adantr ⊢ ( ( 𝜑 ∧ ( 𝑈 ↑ 3 ) = - ( 𝐺 + 𝑁 ) ) → - 𝑈 ≠ 0 )
134 110 112 131 133 ddcand ⊢ ( ( 𝜑 ∧ ( 𝑈 ↑ 3 ) = - ( 𝐺 + 𝑁 ) ) → ( 𝑀 / ( 𝑀 / - 𝑈 ) ) = - 𝑈 )
135 109 134 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑈 ↑ 3 ) = - ( 𝐺 + 𝑁 ) ) → ( 𝑀 / ( ( - ( 𝑀 / 𝑈 ) / 𝑇 ) · 𝑇 ) ) = - 𝑈 )
136 105 135 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑈 ↑ 3 ) = - ( 𝐺 + 𝑁 ) ) → ( ( ( - ( 𝑀 / 𝑈 ) / 𝑇 ) · 𝑇 ) − ( 𝑀 / ( ( - ( 𝑀 / 𝑈 ) / 𝑇 ) · 𝑇 ) ) ) = ( - ( 𝑀 / 𝑈 ) − - 𝑈 ) )
137 103 136 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑈 ↑ 3 ) = - ( 𝐺 + 𝑁 ) ) → 𝑋 = ( ( ( - ( 𝑀 / 𝑈 ) / 𝑇 ) · 𝑇 ) − ( 𝑀 / ( ( - ( 𝑀 / 𝑈 ) / 𝑇 ) · 𝑇 ) ) ) )
138 oveq1 ⊢ ( 𝑟 = ( - ( 𝑀 / 𝑈 ) / 𝑇 ) → ( 𝑟 ↑ 3 ) = ( ( - ( 𝑀 / 𝑈 ) / 𝑇 ) ↑ 3 ) )
139 138 eqeq1d ⊢ ( 𝑟 = ( - ( 𝑀 / 𝑈 ) / 𝑇 ) → ( ( 𝑟 ↑ 3 ) = 1 ↔ ( ( - ( 𝑀 / 𝑈 ) / 𝑇 ) ↑ 3 ) = 1 ) )
140 oveq1 ⊢ ( 𝑟 = ( - ( 𝑀 / 𝑈 ) / 𝑇 ) → ( 𝑟 · 𝑇 ) = ( ( - ( 𝑀 / 𝑈 ) / 𝑇 ) · 𝑇 ) )
141 140 oveq2d ⊢ ( 𝑟 = ( - ( 𝑀 / 𝑈 ) / 𝑇 ) → ( 𝑀 / ( 𝑟 · 𝑇 ) ) = ( 𝑀 / ( ( - ( 𝑀 / 𝑈 ) / 𝑇 ) · 𝑇 ) ) )
142 140 141 oveq12d ⊢ ( 𝑟 = ( - ( 𝑀 / 𝑈 ) / 𝑇 ) → ( ( 𝑟 · 𝑇 ) − ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) = ( ( ( - ( 𝑀 / 𝑈 ) / 𝑇 ) · 𝑇 ) − ( 𝑀 / ( ( - ( 𝑀 / 𝑈 ) / 𝑇 ) · 𝑇 ) ) ) )
143 142 eqeq2d ⊢ ( 𝑟 = ( - ( 𝑀 / 𝑈 ) / 𝑇 ) → ( 𝑋 = ( ( 𝑟 · 𝑇 ) − ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) ↔ 𝑋 = ( ( ( - ( 𝑀 / 𝑈 ) / 𝑇 ) · 𝑇 ) − ( 𝑀 / ( ( - ( 𝑀 / 𝑈 ) / 𝑇 ) · 𝑇 ) ) ) ) )
144 139 143 anbi12d ⊢ ( 𝑟 = ( - ( 𝑀 / 𝑈 ) / 𝑇 ) → ( ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = ( ( 𝑟 · 𝑇 ) − ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) ) ↔ ( ( ( - ( 𝑀 / 𝑈 ) / 𝑇 ) ↑ 3 ) = 1 ∧ 𝑋 = ( ( ( - ( 𝑀 / 𝑈 ) / 𝑇 ) · 𝑇 ) − ( 𝑀 / ( ( - ( 𝑀 / 𝑈 ) / 𝑇 ) · 𝑇 ) ) ) ) ) )
145 144 rspcev ⊢ ( ( ( - ( 𝑀 / 𝑈 ) / 𝑇 ) ∈ ℂ ∧ ( ( ( - ( 𝑀 / 𝑈 ) / 𝑇 ) ↑ 3 ) = 1 ∧ 𝑋 = ( ( ( - ( 𝑀 / 𝑈 ) / 𝑇 ) · 𝑇 ) − ( 𝑀 / ( ( - ( 𝑀 / 𝑈 ) / 𝑇 ) · 𝑇 ) ) ) ) ) → ∃ 𝑟 ∈ ℂ ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = ( ( 𝑟 · 𝑇 ) − ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) ) )
146 55 100 137 145 syl12anc ⊢ ( ( 𝜑 ∧ ( 𝑈 ↑ 3 ) = - ( 𝐺 + 𝑁 ) ) → ∃ 𝑟 ∈ ℂ ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = ( ( 𝑟 · 𝑇 ) − ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) ) )
147 86 sqcld ⊢ ( 𝜑 → ( ( 𝑈 ↑ 3 ) ↑ 2 ) ∈ ℂ )
148 147 mulid2d ⊢ ( 𝜑 → ( 1 · ( ( 𝑈 ↑ 3 ) ↑ 2 ) ) = ( ( 𝑈 ↑ 3 ) ↑ 2 ) )
149 2 86 mulcld ⊢ ( 𝜑 → ( 𝑄 · ( 𝑈 ↑ 3 ) ) ∈ ℂ )
150 149 70 negsubd ⊢ ( 𝜑 → ( ( 𝑄 · ( 𝑈 ↑ 3 ) ) + - ( 𝑀 ↑ 3 ) ) = ( ( 𝑄 · ( 𝑈 ↑ 3 ) ) − ( 𝑀 ↑ 3 ) ) )
151 148 150 oveq12d ⊢ ( 𝜑 → ( ( 1 · ( ( 𝑈 ↑ 3 ) ↑ 2 ) ) + ( ( 𝑄 · ( 𝑈 ↑ 3 ) ) + - ( 𝑀 ↑ 3 ) ) ) = ( ( ( 𝑈 ↑ 3 ) ↑ 2 ) + ( ( 𝑄 · ( 𝑈 ↑ 3 ) ) − ( 𝑀 ↑ 3 ) ) ) )
152 1 2 3 4 5 6 7 8 9 10 11 12 13 dcubic1lem ⊢ ( 𝜑 → ( ( ( 𝑋 ↑ 3 ) + ( ( 𝑃 · 𝑋 ) + 𝑄 ) ) = 0 ↔ ( ( ( 𝑈 ↑ 3 ) ↑ 2 ) + ( ( 𝑄 · ( 𝑈 ↑ 3 ) ) − ( 𝑀 ↑ 3 ) ) ) = 0 ) )
153 14 152 mpbid ⊢ ( 𝜑 → ( ( ( 𝑈 ↑ 3 ) ↑ 2 ) + ( ( 𝑄 · ( 𝑈 ↑ 3 ) ) − ( 𝑀 ↑ 3 ) ) ) = 0 )
154 151 153 eqtrd ⊢ ( 𝜑 → ( ( 1 · ( ( 𝑈 ↑ 3 ) ↑ 2 ) ) + ( ( 𝑄 · ( 𝑈 ↑ 3 ) ) + - ( 𝑀 ↑ 3 ) ) ) = 0 )
155 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
156 ax-1ne0 ⊢ 1 ≠ 0
157 156 a1i ⊢ ( 𝜑 → 1 ≠ 0 )
158 70 negcld ⊢ ( 𝜑 → - ( 𝑀 ↑ 3 ) ∈ ℂ )
159 2cn ⊢ 2 ∈ ℂ
160 mulcl ⊢ ( ( 2 ∈ ℂ ∧ 𝐺 ∈ ℂ ) → ( 2 · 𝐺 ) ∈ ℂ )
161 159 6 160 sylancr ⊢ ( 𝜑 → ( 2 · 𝐺 ) ∈ ℂ )
162 sqmul ⊢ ( ( 2 ∈ ℂ ∧ 𝐺 ∈ ℂ ) → ( ( 2 · 𝐺 ) ↑ 2 ) = ( ( 2 ↑ 2 ) · ( 𝐺 ↑ 2 ) ) )
163 159 6 162 sylancr ⊢ ( 𝜑 → ( ( 2 · 𝐺 ) ↑ 2 ) = ( ( 2 ↑ 2 ) · ( 𝐺 ↑ 2 ) ) )
164 7 oveq2d ⊢ ( 𝜑 → ( ( 2 ↑ 2 ) · ( 𝐺 ↑ 2 ) ) = ( ( 2 ↑ 2 ) · ( ( 𝑁 ↑ 2 ) + ( 𝑀 ↑ 3 ) ) ) )
165 159 sqcli ⊢ ( 2 ↑ 2 ) ∈ ℂ
166 mulcl ⊢ ( ( ( 2 ↑ 2 ) ∈ ℂ ∧ ( 𝑁 ↑ 2 ) ∈ ℂ ) → ( ( 2 ↑ 2 ) · ( 𝑁 ↑ 2 ) ) ∈ ℂ )
167 165 68 166 sylancr ⊢ ( 𝜑 → ( ( 2 ↑ 2 ) · ( 𝑁 ↑ 2 ) ) ∈ ℂ )
168 mulcl ⊢ ( ( ( 2 ↑ 2 ) ∈ ℂ ∧ ( 𝑀 ↑ 3 ) ∈ ℂ ) → ( ( 2 ↑ 2 ) · ( 𝑀 ↑ 3 ) ) ∈ ℂ )
169 165 70 168 sylancr ⊢ ( 𝜑 → ( ( 2 ↑ 2 ) · ( 𝑀 ↑ 3 ) ) ∈ ℂ )
170 167 169 subnegd ⊢ ( 𝜑 → ( ( ( 2 ↑ 2 ) · ( 𝑁 ↑ 2 ) ) − - ( ( 2 ↑ 2 ) · ( 𝑀 ↑ 3 ) ) ) = ( ( ( 2 ↑ 2 ) · ( 𝑁 ↑ 2 ) ) + ( ( 2 ↑ 2 ) · ( 𝑀 ↑ 3 ) ) ) )
171 9 oveq2d ⊢ ( 𝜑 → ( 2 · 𝑁 ) = ( 2 · ( 𝑄 / 2 ) ) )
172 159 a1i ⊢ ( 𝜑 → 2 ∈ ℂ )
173 2ne0 ⊢ 2 ≠ 0
174 173 a1i ⊢ ( 𝜑 → 2 ≠ 0 )
175 2 172 174 divcan2d ⊢ ( 𝜑 → ( 2 · ( 𝑄 / 2 ) ) = 𝑄 )
176 171 175 eqtrd ⊢ ( 𝜑 → ( 2 · 𝑁 ) = 𝑄 )
177 176 oveq1d ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑ 2 ) = ( 𝑄 ↑ 2 ) )
178 sqmul ⊢ ( ( 2 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( 2 · 𝑁 ) ↑ 2 ) = ( ( 2 ↑ 2 ) · ( 𝑁 ↑ 2 ) ) )
179 159 63 178 sylancr ⊢ ( 𝜑 → ( ( 2 · 𝑁 ) ↑ 2 ) = ( ( 2 ↑ 2 ) · ( 𝑁 ↑ 2 ) ) )
180 177 179 eqtr3d ⊢ ( 𝜑 → ( 𝑄 ↑ 2 ) = ( ( 2 ↑ 2 ) · ( 𝑁 ↑ 2 ) ) )
181 158 mulid2d ⊢ ( 𝜑 → ( 1 · - ( 𝑀 ↑ 3 ) ) = - ( 𝑀 ↑ 3 ) )
182 181 oveq2d ⊢ ( 𝜑 → ( 4 · ( 1 · - ( 𝑀 ↑ 3 ) ) ) = ( 4 · - ( 𝑀 ↑ 3 ) ) )
183 4cn ⊢ 4 ∈ ℂ
184 mulneg2 ⊢ ( ( 4 ∈ ℂ ∧ ( 𝑀 ↑ 3 ) ∈ ℂ ) → ( 4 · - ( 𝑀 ↑ 3 ) ) = - ( 4 · ( 𝑀 ↑ 3 ) ) )
185 183 70 184 sylancr ⊢ ( 𝜑 → ( 4 · - ( 𝑀 ↑ 3 ) ) = - ( 4 · ( 𝑀 ↑ 3 ) ) )
186 182 185 eqtrd ⊢ ( 𝜑 → ( 4 · ( 1 · - ( 𝑀 ↑ 3 ) ) ) = - ( 4 · ( 𝑀 ↑ 3 ) ) )
187 sq2 ⊢ ( 2 ↑ 2 ) = 4
188 187 oveq1i ⊢ ( ( 2 ↑ 2 ) · ( 𝑀 ↑ 3 ) ) = ( 4 · ( 𝑀 ↑ 3 ) )
189 188 negeqi ⊢ - ( ( 2 ↑ 2 ) · ( 𝑀 ↑ 3 ) ) = - ( 4 · ( 𝑀 ↑ 3 ) )
190 186 189 eqtr4di ⊢ ( 𝜑 → ( 4 · ( 1 · - ( 𝑀 ↑ 3 ) ) ) = - ( ( 2 ↑ 2 ) · ( 𝑀 ↑ 3 ) ) )
191 180 190 oveq12d ⊢ ( 𝜑 → ( ( 𝑄 ↑ 2 ) − ( 4 · ( 1 · - ( 𝑀 ↑ 3 ) ) ) ) = ( ( ( 2 ↑ 2 ) · ( 𝑁 ↑ 2 ) ) − - ( ( 2 ↑ 2 ) · ( 𝑀 ↑ 3 ) ) ) )
192 165 a1i ⊢ ( 𝜑 → ( 2 ↑ 2 ) ∈ ℂ )
193 192 68 70 adddid ⊢ ( 𝜑 → ( ( 2 ↑ 2 ) · ( ( 𝑁 ↑ 2 ) + ( 𝑀 ↑ 3 ) ) ) = ( ( ( 2 ↑ 2 ) · ( 𝑁 ↑ 2 ) ) + ( ( 2 ↑ 2 ) · ( 𝑀 ↑ 3 ) ) ) )
194 170 191 193 3eqtr4rd ⊢ ( 𝜑 → ( ( 2 ↑ 2 ) · ( ( 𝑁 ↑ 2 ) + ( 𝑀 ↑ 3 ) ) ) = ( ( 𝑄 ↑ 2 ) − ( 4 · ( 1 · - ( 𝑀 ↑ 3 ) ) ) ) )
195 163 164 194 3eqtrd ⊢ ( 𝜑 → ( ( 2 · 𝐺 ) ↑ 2 ) = ( ( 𝑄 ↑ 2 ) − ( 4 · ( 1 · - ( 𝑀 ↑ 3 ) ) ) ) )
196 155 157 2 158 86 161 195 quad2 ⊢ ( 𝜑 → ( ( ( 1 · ( ( 𝑈 ↑ 3 ) ↑ 2 ) ) + ( ( 𝑄 · ( 𝑈 ↑ 3 ) ) + - ( 𝑀 ↑ 3 ) ) ) = 0 ↔ ( ( 𝑈 ↑ 3 ) = ( ( - 𝑄 + ( 2 · 𝐺 ) ) / ( 2 · 1 ) ) ∨ ( 𝑈 ↑ 3 ) = ( ( - 𝑄 − ( 2 · 𝐺 ) ) / ( 2 · 1 ) ) ) ) )
197 154 196 mpbid ⊢ ( 𝜑 → ( ( 𝑈 ↑ 3 ) = ( ( - 𝑄 + ( 2 · 𝐺 ) ) / ( 2 · 1 ) ) ∨ ( 𝑈 ↑ 3 ) = ( ( - 𝑄 − ( 2 · 𝐺 ) ) / ( 2 · 1 ) ) ) )
198 2t1e2 ⊢ ( 2 · 1 ) = 2
199 198 oveq2i ⊢ ( ( - 𝑄 + ( 2 · 𝐺 ) ) / ( 2 · 1 ) ) = ( ( - 𝑄 + ( 2 · 𝐺 ) ) / 2 )
200 2 negcld ⊢ ( 𝜑 → - 𝑄 ∈ ℂ )
201 200 161 172 174 divdird ⊢ ( 𝜑 → ( ( - 𝑄 + ( 2 · 𝐺 ) ) / 2 ) = ( ( - 𝑄 / 2 ) + ( ( 2 · 𝐺 ) / 2 ) ) )
202 9 negeqd ⊢ ( 𝜑 → - 𝑁 = - ( 𝑄 / 2 ) )
203 2 172 174 divnegd ⊢ ( 𝜑 → - ( 𝑄 / 2 ) = ( - 𝑄 / 2 ) )
204 202 203 eqtr2d ⊢ ( 𝜑 → ( - 𝑄 / 2 ) = - 𝑁 )
205 6 172 174 divcan3d ⊢ ( 𝜑 → ( ( 2 · 𝐺 ) / 2 ) = 𝐺 )
206 204 205 oveq12d ⊢ ( 𝜑 → ( ( - 𝑄 / 2 ) + ( ( 2 · 𝐺 ) / 2 ) ) = ( - 𝑁 + 𝐺 ) )
207 63 negcld ⊢ ( 𝜑 → - 𝑁 ∈ ℂ )
208 207 6 addcomd ⊢ ( 𝜑 → ( - 𝑁 + 𝐺 ) = ( 𝐺 + - 𝑁 ) )
209 6 63 negsubd ⊢ ( 𝜑 → ( 𝐺 + - 𝑁 ) = ( 𝐺 − 𝑁 ) )
210 208 209 eqtrd ⊢ ( 𝜑 → ( - 𝑁 + 𝐺 ) = ( 𝐺 − 𝑁 ) )
211 201 206 210 3eqtrd ⊢ ( 𝜑 → ( ( - 𝑄 + ( 2 · 𝐺 ) ) / 2 ) = ( 𝐺 − 𝑁 ) )
212 199 211 syl5eq ⊢ ( 𝜑 → ( ( - 𝑄 + ( 2 · 𝐺 ) ) / ( 2 · 1 ) ) = ( 𝐺 − 𝑁 ) )
213 212 eqeq2d ⊢ ( 𝜑 → ( ( 𝑈 ↑ 3 ) = ( ( - 𝑄 + ( 2 · 𝐺 ) ) / ( 2 · 1 ) ) ↔ ( 𝑈 ↑ 3 ) = ( 𝐺 − 𝑁 ) ) )
214 198 oveq2i ⊢ ( ( - 𝑄 − ( 2 · 𝐺 ) ) / ( 2 · 1 ) ) = ( ( - 𝑄 − ( 2 · 𝐺 ) ) / 2 )
215 204 205 oveq12d ⊢ ( 𝜑 → ( ( - 𝑄 / 2 ) − ( ( 2 · 𝐺 ) / 2 ) ) = ( - 𝑁 − 𝐺 ) )
216 200 161 172 174 divsubdird ⊢ ( 𝜑 → ( ( - 𝑄 − ( 2 · 𝐺 ) ) / 2 ) = ( ( - 𝑄 / 2 ) − ( ( 2 · 𝐺 ) / 2 ) ) )
217 6 63 addcomd ⊢ ( 𝜑 → ( 𝐺 + 𝑁 ) = ( 𝑁 + 𝐺 ) )
218 217 negeqd ⊢ ( 𝜑 → - ( 𝐺 + 𝑁 ) = - ( 𝑁 + 𝐺 ) )
219 63 6 negdi2d ⊢ ( 𝜑 → - ( 𝑁 + 𝐺 ) = ( - 𝑁 − 𝐺 ) )
220 218 219 eqtrd ⊢ ( 𝜑 → - ( 𝐺 + 𝑁 ) = ( - 𝑁 − 𝐺 ) )
221 215 216 220 3eqtr4d ⊢ ( 𝜑 → ( ( - 𝑄 − ( 2 · 𝐺 ) ) / 2 ) = - ( 𝐺 + 𝑁 ) )
222 214 221 syl5eq ⊢ ( 𝜑 → ( ( - 𝑄 − ( 2 · 𝐺 ) ) / ( 2 · 1 ) ) = - ( 𝐺 + 𝑁 ) )
223 222 eqeq2d ⊢ ( 𝜑 → ( ( 𝑈 ↑ 3 ) = ( ( - 𝑄 − ( 2 · 𝐺 ) ) / ( 2 · 1 ) ) ↔ ( 𝑈 ↑ 3 ) = - ( 𝐺 + 𝑁 ) ) )
224 213 223 orbi12d ⊢ ( 𝜑 → ( ( ( 𝑈 ↑ 3 ) = ( ( - 𝑄 + ( 2 · 𝐺 ) ) / ( 2 · 1 ) ) ∨ ( 𝑈 ↑ 3 ) = ( ( - 𝑄 − ( 2 · 𝐺 ) ) / ( 2 · 1 ) ) ) ↔ ( ( 𝑈 ↑ 3 ) = ( 𝐺 − 𝑁 ) ∨ ( 𝑈 ↑ 3 ) = - ( 𝐺 + 𝑁 ) ) ) )
225 197 224 mpbid ⊢ ( 𝜑 → ( ( 𝑈 ↑ 3 ) = ( 𝐺 − 𝑁 ) ∨ ( 𝑈 ↑ 3 ) = - ( 𝐺 + 𝑁 ) ) )
226 45 146 225 mpjaodan ⊢ ( 𝜑 → ∃ 𝑟 ∈ ℂ ( ( 𝑟 ↑ 3 ) = 1 ∧ 𝑋 = ( ( 𝑟 · 𝑇 ) − ( 𝑀 / ( 𝑟 · 𝑇 ) ) ) ) )