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	$$⊢\phi \to P\in ℂ$$
	dcubic.d	$$⊢\phi \to Q\in ℂ$$
	dcubic.x	$$⊢\phi \to X\in ℂ$$
	dcubic.t	$$⊢\phi \to T\in ℂ$$
	dcubic.3	$$⊢\phi \to T^3=G-N$$
	dcubic.g	$$⊢\phi \to G\in ℂ$$
	dcubic.2	$$⊢\phi \to G^2=N^2+M^3$$
	dcubic.m	$$⊢\phi \to M=\frac{P}{3}$$
	dcubic.n	$$⊢\phi \to N=\frac{Q}{2}$$
	dcubic.0	$$⊢\phi \to T\ne 0$$
	dcubic2.u	$$⊢\phi \to U\in ℂ$$
	dcubic2.z	$$⊢\phi \to U\ne 0$$
	dcubic2.2	$$⊢\phi \to X=U-\left(\frac{M}{U}\right)$$
	dcubic2.x	$$⊢\phi \to X^3+PX+Q=0$$
Assertion	dcubic2	$$⊢\phi \to \exists r\in ℂ\left(r^3=1\wedge X=rT-\left(\frac{M}{rT}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		dcubic.c	$$⊢\phi \to P\in ℂ$$
2		dcubic.d	$$⊢\phi \to Q\in ℂ$$
3		dcubic.x	$$⊢\phi \to X\in ℂ$$
4		dcubic.t	$$⊢\phi \to T\in ℂ$$
5		dcubic.3	$$⊢\phi \to T^3=G-N$$
6		dcubic.g	$$⊢\phi \to G\in ℂ$$
7		dcubic.2	$$⊢\phi \to G^2=N^2+M^3$$
8		dcubic.m	$$⊢\phi \to M=\frac{P}{3}$$
9		dcubic.n	$$⊢\phi \to N=\frac{Q}{2}$$
10		dcubic.0	$$⊢\phi \to T\ne 0$$
11		dcubic2.u	$$⊢\phi \to U\in ℂ$$
12		dcubic2.z	$$⊢\phi \to U\ne 0$$
13		dcubic2.2	$$⊢\phi \to X=U-\left(\frac{M}{U}\right)$$
14		dcubic2.x	$$⊢\phi \to X^3+PX+Q=0$$
15	11 4 10	divcld	$$⊢\phi \to \frac{U}{T}\in ℂ$$
16	15	adantr	$$⊢\left(\phi \wedge U^3=G-N\right)\to \frac{U}{T}\in ℂ$$
17		3nn0	$$⊢3\in {\mathbb{N}}_0$$
18	17	a1i	$$⊢\phi \to 3\in {\mathbb{N}}_0$$
19	11 4 10 18	expdivd	$$⊢\phi \to {\left(\frac{U}{T}\right)}^3=\frac{U^3}{T^3}$$
20	19	adantr	$$⊢\left(\phi \wedge U^3=G-N\right)\to {\left(\frac{U}{T}\right)}^3=\frac{U^3}{T^3}$$
21		oveq1	$$⊢U^3=G-N\to \frac{U^3}{T^3}=\frac{G-N}{T^3}$$
22	5	oveq1d	$$⊢\phi \to \frac{T^3}{T^3}=\frac{G-N}{T^3}$$
23		expcl	$$⊢\left(T\in ℂ\wedge 3\in {\mathbb{N}}_0\right)\to T^3\in ℂ$$
24	4 17 23	sylancl	$$⊢\phi \to T^3\in ℂ$$
25		3z	$$⊢3\in \mathbb{Z}$$
26	25	a1i	$$⊢\phi \to 3\in \mathbb{Z}$$
27	4 10 26	expne0d	$$⊢\phi \to T^3\ne 0$$
28	24 27	dividd	$$⊢\phi \to \frac{T^3}{T^3}=1$$
29	22 28	eqtr3d	$$⊢\phi \to \frac{G-N}{T^3}=1$$
30	21 29	sylan9eqr	$$⊢\left(\phi \wedge U^3=G-N\right)\to \frac{U^3}{T^3}=1$$
31	20 30	eqtrd	$$⊢\left(\phi \wedge U^3=G-N\right)\to {\left(\frac{U}{T}\right)}^3=1$$
32	11 4 10	divcan1d	$$⊢\phi \to \left(\frac{U}{T}\right)T=U$$
33	32	oveq2d	$$⊢\phi \to \frac{M}{\left(\frac{U}{T}\right)T}=\frac{M}{U}$$
34	32 33	oveq12d	$$⊢\phi \to \left(\frac{U}{T}\right)T-\left(\frac{M}{\left(\frac{U}{T}\right)T}\right)=U-\left(\frac{M}{U}\right)$$
35	13 34	eqtr4d	$$⊢\phi \to X=\left(\frac{U}{T}\right)T-\left(\frac{M}{\left(\frac{U}{T}\right)T}\right)$$
36	35	adantr	$$⊢\left(\phi \wedge U^3=G-N\right)\to X=\left(\frac{U}{T}\right)T-\left(\frac{M}{\left(\frac{U}{T}\right)T}\right)$$
37		oveq1	$$⊢r=\frac{U}{T}\to r^3={\left(\frac{U}{T}\right)}^3$$
38	37	eqeq1d	$$⊢r=\frac{U}{T}\to \left(r^3=1\leftrightarrow {\left(\frac{U}{T}\right)}^3=1\right)$$
39		oveq1	$$⊢r=\frac{U}{T}\to rT=\left(\frac{U}{T}\right)T$$
40	39	oveq2d	$$⊢r=\frac{U}{T}\to \frac{M}{rT}=\frac{M}{\left(\frac{U}{T}\right)T}$$
41	39 40	oveq12d	$$⊢r=\frac{U}{T}\to rT-\left(\frac{M}{rT}\right)=\left(\frac{U}{T}\right)T-\left(\frac{M}{\left(\frac{U}{T}\right)T}\right)$$
42	41	eqeq2d	$$⊢r=\frac{U}{T}\to \left(X=rT-\left(\frac{M}{rT}\right)\leftrightarrow X=\left(\frac{U}{T}\right)T-\left(\frac{M}{\left(\frac{U}{T}\right)T}\right)\right)$$
43	38 42	anbi12d	$$⊢r=\frac{U}{T}\to \left(\left(r^3=1\wedge X=rT-\left(\frac{M}{rT}\right)\right)\leftrightarrow \left({\left(\frac{U}{T}\right)}^3=1\wedge X=\left(\frac{U}{T}\right)T-\left(\frac{M}{\left(\frac{U}{T}\right)T}\right)\right)\right)$$
44	43	rspcev	$$⊢\left(\frac{U}{T}\in ℂ\wedge \left({\left(\frac{U}{T}\right)}^3=1\wedge X=\left(\frac{U}{T}\right)T-\left(\frac{M}{\left(\frac{U}{T}\right)T}\right)\right)\right)\to \exists r\in ℂ\left(r^3=1\wedge X=rT-\left(\frac{M}{rT}\right)\right)$$
45	16 31 36 44	syl12anc	$$⊢\left(\phi \wedge U^3=G-N\right)\to \exists r\in ℂ\left(r^3=1\wedge X=rT-\left(\frac{M}{rT}\right)\right)$$
46		3cn	$$⊢3\in ℂ$$
47	46	a1i	$$⊢\phi \to 3\in ℂ$$
48		3ne0	$$⊢3\ne 0$$
49	48	a1i	$$⊢\phi \to 3\ne 0$$
50	1 47 49	divcld	$$⊢\phi \to \frac{P}{3}\in ℂ$$
51	8 50	eqeltrd	$$⊢\phi \to M\in ℂ$$
52	51 11 12	divcld	$$⊢\phi \to \frac{M}{U}\in ℂ$$
53	52	negcld	$$⊢\phi \to -\frac{M}{U}\in ℂ$$
54	53 4 10	divcld	$$⊢\phi \to \frac{-\frac{M}{U}}{T}\in ℂ$$
55	54	adantr	$$⊢\left(\phi \wedge U^3=-\left(G+N\right)\right)\to \frac{-\frac{M}{U}}{T}\in ℂ$$
56	53 4 10 18	expdivd	$$⊢\phi \to {\left(\frac{-\frac{M}{U}}{T}\right)}^3=\frac{{\left(-\left(\frac{M}{U}\right)\right)}^3}{T^3}$$
57	51 11 12	divnegd	$$⊢\phi \to -\frac{M}{U}=\frac{-M}{U}$$
58	57	oveq1d	$$⊢\phi \to {\left(-\left(\frac{M}{U}\right)\right)}^3={\left(\frac{-M}{U}\right)}^3$$
59	51	negcld	$$⊢\phi \to -M\in ℂ$$
60	59 11 12 18	expdivd	$$⊢\phi \to {\left(\frac{-M}{U}\right)}^3=\frac{{\left(-M\right)}^3}{U^3}$$
61	5	oveq2d	$$⊢\phi \to \left(G+N\right)T^3=\left(G+N\right)\left(G-N\right)$$
62	2	halfcld	$$⊢\phi \to \frac{Q}{2}\in ℂ$$
63	9 62	eqeltrd	$$⊢\phi \to N\in ℂ$$
64		subsq	$$⊢\left(G\in ℂ\wedge N\in ℂ\right)\to G^2-N^2=\left(G+N\right)\left(G-N\right)$$
65	6 63 64	syl2anc	$$⊢\phi \to G^2-N^2=\left(G+N\right)\left(G-N\right)$$
66	61 65	eqtr4d	$$⊢\phi \to \left(G+N\right)T^3=G^2-N^2$$
67	7	oveq1d	$$⊢\phi \to G^2-N^2=N^2+M^3-N^2$$
68	63	sqcld	$$⊢\phi \to N^2\in ℂ$$
69		expcl	$$⊢\left(M\in ℂ\wedge 3\in {\mathbb{N}}_0\right)\to M^3\in ℂ$$
70	51 17 69	sylancl	$$⊢\phi \to M^3\in ℂ$$
71	68 70	pncan2d	$$⊢\phi \to N^2+M^3-N^2=M^3$$
72	66 67 71	3eqtrd	$$⊢\phi \to \left(G+N\right)T^3=M^3$$
73	72	negeqd	$$⊢\phi \to -\left(G+N\right)T^3=-M^3$$
74	6 63	addcld	$$⊢\phi \to G+N\in ℂ$$
75	74 24	mulneg1d	$$⊢\phi \to \left(-\left(G+N\right)\right)T^3=-\left(G+N\right)T^3$$
76		3nn	$$⊢3\in \mathbb{N}$$
77	76	a1i	$$⊢\phi \to 3\in \mathbb{N}$$
78		n2dvds3	$$⊢\neg 2\parallel 3$$
79	78	a1i	$$⊢\phi \to \neg 2\parallel 3$$
80		oexpneg	$$⊢\left(M\in ℂ\wedge 3\in \mathbb{N}\wedge \neg 2\parallel 3\right)\to {\left(-M\right)}^3=-M^3$$
81	51 77 79 80	syl3anc	$$⊢\phi \to {\left(-M\right)}^3=-M^3$$
82	73 75 81	3eqtr4d	$$⊢\phi \to \left(-\left(G+N\right)\right)T^3={\left(-M\right)}^3$$
83	82	oveq1d	$$⊢\phi \to \frac{\left(-\left(G+N\right)\right)T^3}{U^3}=\frac{{\left(-M\right)}^3}{U^3}$$
84	74	negcld	$$⊢\phi \to -\left(G+N\right)\in ℂ$$
85		expcl	$$⊢\left(U\in ℂ\wedge 3\in {\mathbb{N}}_0\right)\to U^3\in ℂ$$
86	11 17 85	sylancl	$$⊢\phi \to U^3\in ℂ$$
87	11 12 26	expne0d	$$⊢\phi \to U^3\ne 0$$
88	84 24 86 87	div23d	$$⊢\phi \to \frac{\left(-\left(G+N\right)\right)T^3}{U^3}=\left(\frac{-\left(G+N\right)}{U^3}\right)T^3$$
89	83 88	eqtr3d	$$⊢\phi \to \frac{{\left(-M\right)}^3}{U^3}=\left(\frac{-\left(G+N\right)}{U^3}\right)T^3$$
90	58 60 89	3eqtrd	$$⊢\phi \to {\left(-\left(\frac{M}{U}\right)\right)}^3=\left(\frac{-\left(G+N\right)}{U^3}\right)T^3$$
91	90	oveq1d	$$⊢\phi \to \frac{{\left(-\left(\frac{M}{U}\right)\right)}^3}{T^3}=\frac{\left(\frac{-\left(G+N\right)}{U^3}\right)T^3}{T^3}$$
92	84 86 87	divcld	$$⊢\phi \to \frac{-\left(G+N\right)}{U^3}\in ℂ$$
93	92 24 27	divcan4d	$$⊢\phi \to \frac{\left(\frac{-\left(G+N\right)}{U^3}\right)T^3}{T^3}=\frac{-\left(G+N\right)}{U^3}$$
94	56 91 93	3eqtrd	$$⊢\phi \to {\left(\frac{-\frac{M}{U}}{T}\right)}^3=\frac{-\left(G+N\right)}{U^3}$$
95	94	adantr	$$⊢\left(\phi \wedge U^3=-\left(G+N\right)\right)\to {\left(\frac{-\frac{M}{U}}{T}\right)}^3=\frac{-\left(G+N\right)}{U^3}$$
96		oveq1	$$⊢U^3=-\left(G+N\right)\to \frac{U^3}{U^3}=\frac{-\left(G+N\right)}{U^3}$$
97	96	eqcomd	$$⊢U^3=-\left(G+N\right)\to \frac{-\left(G+N\right)}{U^3}=\frac{U^3}{U^3}$$
98	86 87	dividd	$$⊢\phi \to \frac{U^3}{U^3}=1$$
99	97 98	sylan9eqr	$$⊢\left(\phi \wedge U^3=-\left(G+N\right)\right)\to \frac{-\left(G+N\right)}{U^3}=1$$
100	95 99	eqtrd	$$⊢\left(\phi \wedge U^3=-\left(G+N\right)\right)\to {\left(\frac{-\frac{M}{U}}{T}\right)}^3=1$$
101	52 11	neg2subd	$$⊢\phi \to -\left(\frac{M}{U}\right)-\left(-U\right)=U-\left(\frac{M}{U}\right)$$
102	13 101	eqtr4d	$$⊢\phi \to X=-\left(\frac{M}{U}\right)-\left(-U\right)$$
103	102	adantr	$$⊢\left(\phi \wedge U^3=-\left(G+N\right)\right)\to X=-\left(\frac{M}{U}\right)-\left(-U\right)$$
104	53 4 10	divcan1d	$$⊢\phi \to \left(\frac{-\frac{M}{U}}{T}\right)T=-\frac{M}{U}$$
105	104	adantr	$$⊢\left(\phi \wedge U^3=-\left(G+N\right)\right)\to \left(\frac{-\frac{M}{U}}{T}\right)T=-\frac{M}{U}$$
106	51 11 12	divneg2d	$$⊢\phi \to -\frac{M}{U}=\frac{M}{-U}$$
107	104 106	eqtrd	$$⊢\phi \to \left(\frac{-\frac{M}{U}}{T}\right)T=\frac{M}{-U}$$
108	107	adantr	$$⊢\left(\phi \wedge U^3=-\left(G+N\right)\right)\to \left(\frac{-\frac{M}{U}}{T}\right)T=\frac{M}{-U}$$
109	108	oveq2d	$$⊢\left(\phi \wedge U^3=-\left(G+N\right)\right)\to \frac{M}{\left(\frac{-\frac{M}{U}}{T}\right)T}=\frac{M}{\frac{M}{-U}}$$
110	51	adantr	$$⊢\left(\phi \wedge U^3=-\left(G+N\right)\right)\to M\in ℂ$$
111	11	negcld	$$⊢\phi \to -U\in ℂ$$
112	111	adantr	$$⊢\left(\phi \wedge U^3=-\left(G+N\right)\right)\to -U\in ℂ$$
113	75 73	eqtrd	$$⊢\phi \to \left(-\left(G+N\right)\right)T^3=-M^3$$
114	113	adantr	$$⊢\left(\phi \wedge U^3=-\left(G+N\right)\right)\to \left(-\left(G+N\right)\right)T^3=-M^3$$
115	84	adantr	$$⊢\left(\phi \wedge U^3=-\left(G+N\right)\right)\to -\left(G+N\right)\in ℂ$$
116	24	adantr	$$⊢\left(\phi \wedge U^3=-\left(G+N\right)\right)\to T^3\in ℂ$$
117		simpr	$$⊢\left(\phi \wedge U^3=-\left(G+N\right)\right)\to U^3=-\left(G+N\right)$$
118	87	adantr	$$⊢\left(\phi \wedge U^3=-\left(G+N\right)\right)\to U^3\ne 0$$
119	117 118	eqnetrrd	$$⊢\left(\phi \wedge U^3=-\left(G+N\right)\right)\to -\left(G+N\right)\ne 0$$
120	27	adantr	$$⊢\left(\phi \wedge U^3=-\left(G+N\right)\right)\to T^3\ne 0$$
121	115 116 119 120	mulne0d	$$⊢\left(\phi \wedge U^3=-\left(G+N\right)\right)\to \left(-\left(G+N\right)\right)T^3\ne 0$$
122	114 121	eqnetrrd	$$⊢\left(\phi \wedge U^3=-\left(G+N\right)\right)\to -M^3\ne 0$$
123		oveq1	$$⊢M=0\to M^3=0^3$$
124		0exp	$$⊢3\in \mathbb{N}\to 0^3=0$$
125	76 124	ax-mp	$$⊢0^3=0$$
126	123 125	eqtrdi	$$⊢M=0\to M^3=0$$
127	126	negeqd	$$⊢M=0\to -M^3=-0$$
128		neg0	$$⊢-0=0$$
129	127 128	eqtrdi	$$⊢M=0\to -M^3=0$$
130	129	necon3i	$$⊢-M^3\ne 0\to M\ne 0$$
131	122 130	syl	$$⊢\left(\phi \wedge U^3=-\left(G+N\right)\right)\to M\ne 0$$
132	11 12	negne0d	$$⊢\phi \to -U\ne 0$$
133	132	adantr	$$⊢\left(\phi \wedge U^3=-\left(G+N\right)\right)\to -U\ne 0$$
134	110 112 131 133	ddcand	$$⊢\left(\phi \wedge U^3=-\left(G+N\right)\right)\to \frac{M}{\frac{M}{-U}}=-U$$
135	109 134	eqtrd	$$⊢\left(\phi \wedge U^3=-\left(G+N\right)\right)\to \frac{M}{\left(\frac{-\frac{M}{U}}{T}\right)T}=-U$$
136	105 135	oveq12d	$$⊢\left(\phi \wedge U^3=-\left(G+N\right)\right)\to \left(\frac{-\frac{M}{U}}{T}\right)T-\left(\frac{M}{\left(\frac{-\frac{M}{U}}{T}\right)T}\right)=-\left(\frac{M}{U}\right)-\left(-U\right)$$
137	103 136	eqtr4d	$$⊢\left(\phi \wedge U^3=-\left(G+N\right)\right)\to X=\left(\frac{-\frac{M}{U}}{T}\right)T-\left(\frac{M}{\left(\frac{-\frac{M}{U}}{T}\right)T}\right)$$
138		oveq1	$$⊢r=\frac{-\frac{M}{U}}{T}\to r^3={\left(\frac{-\frac{M}{U}}{T}\right)}^3$$
139	138	eqeq1d	$$⊢r=\frac{-\frac{M}{U}}{T}\to \left(r^3=1\leftrightarrow {\left(\frac{-\frac{M}{U}}{T}\right)}^3=1\right)$$
140		oveq1	$$⊢r=\frac{-\frac{M}{U}}{T}\to rT=\left(\frac{-\frac{M}{U}}{T}\right)T$$
141	140	oveq2d	$$⊢r=\frac{-\frac{M}{U}}{T}\to \frac{M}{rT}=\frac{M}{\left(\frac{-\frac{M}{U}}{T}\right)T}$$
142	140 141	oveq12d	$$⊢r=\frac{-\frac{M}{U}}{T}\to rT-\left(\frac{M}{rT}\right)=\left(\frac{-\frac{M}{U}}{T}\right)T-\left(\frac{M}{\left(\frac{-\frac{M}{U}}{T}\right)T}\right)$$
143	142	eqeq2d	$$⊢r=\frac{-\frac{M}{U}}{T}\to \left(X=rT-\left(\frac{M}{rT}\right)\leftrightarrow X=\left(\frac{-\frac{M}{U}}{T}\right)T-\left(\frac{M}{\left(\frac{-\frac{M}{U}}{T}\right)T}\right)\right)$$
144	139 143	anbi12d	$$⊢r=\frac{-\frac{M}{U}}{T}\to \left(\left(r^3=1\wedge X=rT-\left(\frac{M}{rT}\right)\right)\leftrightarrow \left({\left(\frac{-\frac{M}{U}}{T}\right)}^3=1\wedge X=\left(\frac{-\frac{M}{U}}{T}\right)T-\left(\frac{M}{\left(\frac{-\frac{M}{U}}{T}\right)T}\right)\right)\right)$$
145	144	rspcev	$$⊢\left(\frac{-\frac{M}{U}}{T}\in ℂ\wedge \left({\left(\frac{-\frac{M}{U}}{T}\right)}^3=1\wedge X=\left(\frac{-\frac{M}{U}}{T}\right)T-\left(\frac{M}{\left(\frac{-\frac{M}{U}}{T}\right)T}\right)\right)\right)\to \exists r\in ℂ\left(r^3=1\wedge X=rT-\left(\frac{M}{rT}\right)\right)$$
146	55 100 137 145	syl12anc	$$⊢\left(\phi \wedge U^3=-\left(G+N\right)\right)\to \exists r\in ℂ\left(r^3=1\wedge X=rT-\left(\frac{M}{rT}\right)\right)$$
147	86	sqcld	$$⊢\phi \to {\left(U^3\right)}^2\in ℂ$$
148	147	mulid2d	$$⊢\phi \to 1{\left(U^3\right)}^2={\left(U^3\right)}^2$$
149	2 86	mulcld	$$⊢\phi \to Q{U}^3\in ℂ$$
150	149 70	negsubd	$$⊢\phi \to Q{U}^3+\left(-M^3\right)=Q{U}^3-M^3$$
151	148 150	oveq12d	$$⊢\phi \to 1{\left(U^3\right)}^2+Q{U}^3+\left(-M^3\right)={\left(U^3\right)}^2+Q{U}^3-M^3$$
152	1 2 3 4 5 6 7 8 9 10 11 12 13	dcubic1lem	$$⊢\phi \to \left(X^3+PX+Q=0\leftrightarrow {\left(U^3\right)}^2+Q{U}^3-M^3=0\right)$$
153	14 152	mpbid	$$⊢\phi \to {\left(U^3\right)}^2+Q{U}^3-M^3=0$$
154	151 153	eqtrd	$$⊢\phi \to 1{\left(U^3\right)}^2+Q{U}^3+\left(-M^3\right)=0$$
155		1cnd	$$⊢\phi \to 1\in ℂ$$
156		ax-1ne0	$$⊢1\ne 0$$
157	156	a1i	$$⊢\phi \to 1\ne 0$$
158	70	negcld	$$⊢\phi \to -M^3\in ℂ$$
159		2cn	$$⊢2\in ℂ$$
160		mulcl	$$⊢\left(2\in ℂ\wedge G\in ℂ\right)\to 2G\in ℂ$$
161	159 6 160	sylancr	$$⊢\phi \to 2G\in ℂ$$
162		sqmul	$$⊢\left(2\in ℂ\wedge G\in ℂ\right)\to {2G}^2=2^2{G}^2$$
163	159 6 162	sylancr	$$⊢\phi \to {2G}^2=2^2{G}^2$$
164	7	oveq2d	$$⊢\phi \to 2^2{G}^2=2^2\left(N^2+M^3\right)$$
165	159	sqcli	$$⊢2^2\in ℂ$$
166		mulcl	$$⊢\left(2^2\in ℂ\wedge N^2\in ℂ\right)\to 2^2{N}^2\in ℂ$$
167	165 68 166	sylancr	$$⊢\phi \to 2^2{N}^2\in ℂ$$
168		mulcl	$$⊢\left(2^2\in ℂ\wedge M^3\in ℂ\right)\to 2^2{M}^3\in ℂ$$
169	165 70 168	sylancr	$$⊢\phi \to 2^2{M}^3\in ℂ$$
170	167 169	subnegd	$$⊢\phi \to 2^2{N}^2-\left(-2^2{M}^3\right)=2^2{N}^2+2^2{M}^3$$
171	9	oveq2d	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=2\left(\frac{Q}{2}\right)$$
172	159	a1i	$$⊢\phi \to 2\in ℂ$$
173		2ne0	$$⊢2\ne 0$$
174	173	a1i	$$⊢\phi \to 2\ne 0$$
175	2 172 174	divcan2d	$$⊢\phi \to 2\left(\frac{Q}{2}\right)=Q$$
176	171 175	eqtrd	$$⊢\phi \to 2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=Q$$
177	176	oveq1d	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^2=Q^2$$
178		sqmul	$$⊢\left(2\in ℂ\wedge N\in ℂ\right)\to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^2=2^2{N}^2$$
179	159 63 178	sylancr	$$⊢\phi \to {2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^2=2^2{N}^2$$
180	177 179	eqtr3d	$$⊢\phi \to Q^2=2^2{N}^2$$
181	158	mulid2d	$$⊢\phi \to 1\left(-M^3\right)=-M^3$$
182	181	oveq2d	$$⊢\phi \to 41\left(-M^3\right)=4\left(-M^3\right)$$
183		4cn	$$⊢4\in ℂ$$
184		mulneg2	$$⊢\left(4\in ℂ\wedge M^3\in ℂ\right)\to 4\left(-M^3\right)=-4M^3$$
185	183 70 184	sylancr	$$⊢\phi \to 4\left(-M^3\right)=-4M^3$$
186	182 185	eqtrd	$$⊢\phi \to 41\left(-M^3\right)=-4M^3$$
187		sq2	$$⊢2^2=4$$
188	187	oveq1i	$$⊢2^2{M}^3=4M^3$$
189	188	negeqi	$$⊢-2^2{M}^3=-4M^3$$
190	186 189	eqtr4di	$$⊢\phi \to 41\left(-M^3\right)=-2^2{M}^3$$
191	180 190	oveq12d	$$⊢\phi \to Q^2-41\left(-M^3\right)=2^2{N}^2-\left(-2^2{M}^3\right)$$
192	165	a1i	$$⊢\phi \to 2^2\in ℂ$$
193	192 68 70	adddid	$$⊢\phi \to 2^2\left(N^2+M^3\right)=2^2{N}^2+2^2{M}^3$$
194	170 191 193	3eqtr4rd	$$⊢\phi \to 2^2\left(N^2+M^3\right)=Q^2-41\left(-M^3\right)$$
195	163 164 194	3eqtrd	$$⊢\phi \to {2G}^2=Q^2-41\left(-M^3\right)$$
196	155 157 2 158 86 161 195	quad2	$$⊢\phi \to \left(1{\left(U^3\right)}^2+Q{U}^3+\left(-M^3\right)=0\leftrightarrow \left(U^3=\frac{-Q+2G}{2\cdot 1}\vee U^3=\frac{-Q-2G}{2\cdot 1}\right)\right)$$
197	154 196	mpbid	$$⊢\phi \to \left(U^3=\frac{-Q+2G}{2\cdot 1}\vee U^3=\frac{-Q-2G}{2\cdot 1}\right)$$
198		2t1e2	$$⊢2\cdot 1=2$$
199	198	oveq2i	$$⊢\frac{-Q+2G}{2\cdot 1}=\frac{-Q+2G}{2}$$
200	2	negcld	$$⊢\phi \to -Q\in ℂ$$
201	200 161 172 174	divdird	$$⊢\phi \to \frac{-Q+2G}{2}=\left(\frac{-Q}{2}\right)+\left(\frac{2G}{2}\right)$$
202	9	negeqd	$$⊢\phi \to -N=-\frac{Q}{2}$$
203	2 172 174	divnegd	$$⊢\phi \to -\frac{Q}{2}=\frac{-Q}{2}$$
204	202 203	eqtr2d	$$⊢\phi \to \frac{-Q}{2}=-N$$
205	6 172 174	divcan3d	$$⊢\phi \to \frac{2G}{2}=G$$
206	204 205	oveq12d	$$⊢\phi \to \left(\frac{-Q}{2}\right)+\left(\frac{2G}{2}\right)=-N+G$$
207	63	negcld	$$⊢\phi \to -N\in ℂ$$
208	207 6	addcomd	$$⊢\phi \to -N+G=G+\mathrm{-<mi\; mathcolor="\#808">N</mi>}$$
209	6 63	negsubd	$$⊢\phi \to G+\mathrm{-<mi\; mathcolor="\#808">N</mi>}=G-N$$
210	208 209	eqtrd	$$⊢\phi \to -N+G=G-N$$
211	201 206 210	3eqtrd	$$⊢\phi \to \frac{-Q+2G}{2}=G-N$$
212	199 211	syl5eq	$$⊢\phi \to \frac{-Q+2G}{2\cdot 1}=G-N$$
213	212	eqeq2d	$$⊢\phi \to \left(U^3=\frac{-Q+2G}{2\cdot 1}\leftrightarrow U^3=G-N\right)$$
214	198	oveq2i	$$⊢\frac{-Q-2G}{2\cdot 1}=\frac{-Q-2G}{2}$$
215	204 205	oveq12d	$$⊢\phi \to \left(\frac{-Q}{2}\right)-\left(\frac{2G}{2}\right)=-N-G$$
216	200 161 172 174	divsubdird	$$⊢\phi \to \frac{-Q-2G}{2}=\left(\frac{-Q}{2}\right)-\left(\frac{2G}{2}\right)$$
217	6 63	addcomd	$$⊢\phi \to G+N=N+G$$
218	217	negeqd	$$⊢\phi \to -\left(G+N\right)=-\left(N+G\right)$$
219	63 6	negdi2d	$$⊢\phi \to -\left(N+G\right)=-N-G$$
220	218 219	eqtrd	$$⊢\phi \to -\left(G+N\right)=-N-G$$
221	215 216 220	3eqtr4d	$$⊢\phi \to \frac{-Q-2G}{2}=-\left(G+N\right)$$
222	214 221	syl5eq	$$⊢\phi \to \frac{-Q-2G}{2\cdot 1}=-\left(G+N\right)$$
223	222	eqeq2d	$$⊢\phi \to \left(U^3=\frac{-Q-2G}{2\cdot 1}\leftrightarrow U^3=-\left(G+N\right)\right)$$
224	213 223	orbi12d	$$⊢\phi \to \left(\left(U^3=\frac{-Q+2G}{2\cdot 1}\vee U^3=\frac{-Q-2G}{2\cdot 1}\right)\leftrightarrow \left(U^3=G-N\vee U^3=-\left(G+N\right)\right)\right)$$
225	197 224	mpbid	$$⊢\phi \to \left(U^3=G-N\vee U^3=-\left(G+N\right)\right)$$
226	45 146 225	mpjaodan	$$⊢\phi \to \exists r\in ℂ\left(r^3=1\wedge X=rT-\left(\frac{M}{rT}\right)\right)$$