Theorem cubic2

Description: The solution to the general cubic equation, for arbitrary choices G and T of the square and cube roots. (Contributed by Mario Carneiro, 23-Apr-2015)

	Ref	Expression
Hypotheses	cubic2.a	$$⊢\phi \to A\in ℂ$$
	cubic2.z	$$⊢\phi \to A\ne 0$$
	cubic2.b	$$⊢\phi \to B\in ℂ$$
	cubic2.c	$$⊢\phi \to C\in ℂ$$
	cubic2.d	$$⊢\phi \to D\in ℂ$$
	cubic2.x	$$⊢\phi \to X\in ℂ$$
	cubic2.t	$$⊢\phi \to T\in ℂ$$
	cubic2.3	$$⊢\phi \to T^3=\frac{N+G}{2}$$
	cubic2.g	$$⊢\phi \to G\in ℂ$$
	cubic2.2	$$⊢\phi \to G^2=N^2-4M^3$$
	cubic2.m	$$⊢\phi \to M=B^2-3AC$$
	cubic2.n	$$⊢\phi \to N=2B^3-9ABC+27A^{2}D$$
	cubic2.0	$$⊢\phi \to T\ne 0$$
Assertion	cubic2	$$⊢\phi \to \left(A{X}^3+B{X}^2+CX+D=0\leftrightarrow \exists r\in ℂ\left(r^3=1\wedge X=-\frac{B+rT+\left(\frac{M}{rT}\right)}{3A}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		cubic2.a	$$⊢\phi \to A\in ℂ$$
2		cubic2.z	$$⊢\phi \to A\ne 0$$
3		cubic2.b	$$⊢\phi \to B\in ℂ$$
4		cubic2.c	$$⊢\phi \to C\in ℂ$$
5		cubic2.d	$$⊢\phi \to D\in ℂ$$
6		cubic2.x	$$⊢\phi \to X\in ℂ$$
7		cubic2.t	$$⊢\phi \to T\in ℂ$$
8		cubic2.3	$$⊢\phi \to T^3=\frac{N+G}{2}$$
9		cubic2.g	$$⊢\phi \to G\in ℂ$$
10		cubic2.2	$$⊢\phi \to G^2=N^2-4M^3$$
11		cubic2.m	$$⊢\phi \to M=B^2-3AC$$
12		cubic2.n	$$⊢\phi \to N=2B^3-9ABC+27A^{2}D$$
13		cubic2.0	$$⊢\phi \to T\ne 0$$
14		3nn0	$$⊢3\in {\mathbb{N}}_0$$
15		expcl	$$⊢\left(X\in ℂ\wedge 3\in {\mathbb{N}}_0\right)\to X^3\in ℂ$$
16	6 14 15	sylancl	$$⊢\phi \to X^3\in ℂ$$
17	1 16	mulcld	$$⊢\phi \to A{X}^3\in ℂ$$
18	6	sqcld	$$⊢\phi \to X^2\in ℂ$$
19	3 18	mulcld	$$⊢\phi \to B{X}^2\in ℂ$$
20	17 19	addcld	$$⊢\phi \to A{X}^3+B{X}^2\in ℂ$$
21	4 6	mulcld	$$⊢\phi \to CX\in ℂ$$
22	21 5	addcld	$$⊢\phi \to CX+D\in ℂ$$
23	20 22	addcld	$$⊢\phi \to A{X}^3+B{X}^2+CX+D\in ℂ$$
24	23 1 2	diveq0ad	$$⊢\phi \to \left(\frac{A{X}^3+B{X}^2+CX+D}{A}=0\leftrightarrow A{X}^3+B{X}^2+CX+D=0\right)$$
25	20 22 1 2	divdird	$$⊢\phi \to \frac{A{X}^3+B{X}^2+CX+D}{A}=\left(\frac{A{X}^3+B{X}^2}{A}\right)+\left(\frac{CX+D}{A}\right)$$
26	17 19 1 2	divdird	$$⊢\phi \to \frac{A{X}^3+B{X}^2}{A}=\left(\frac{A{X}^3}{A}\right)+\left(\frac{B{X}^2}{A}\right)$$
27	16 1 2	divcan3d	$$⊢\phi \to \frac{A{X}^3}{A}=X^3$$
28	3 18 1 2	div23d	$$⊢\phi \to \frac{B{X}^2}{A}=\left(\frac{B}{A}\right)X^2$$
29	27 28	oveq12d	$$⊢\phi \to \left(\frac{A{X}^3}{A}\right)+\left(\frac{B{X}^2}{A}\right)=X^3+\left(\frac{B}{A}\right)X^2$$
30	26 29	eqtrd	$$⊢\phi \to \frac{A{X}^3+B{X}^2}{A}=X^3+\left(\frac{B}{A}\right)X^2$$
31	21 5 1 2	divdird	$$⊢\phi \to \frac{CX+D}{A}=\left(\frac{CX}{A}\right)+\left(\frac{D}{A}\right)$$
32	4 6 1 2	div23d	$$⊢\phi \to \frac{CX}{A}=\left(\frac{C}{A}\right)X$$
33	32	oveq1d	$$⊢\phi \to \left(\frac{CX}{A}\right)+\left(\frac{D}{A}\right)=\left(\frac{C}{A}\right)X+\left(\frac{D}{A}\right)$$
34	31 33	eqtrd	$$⊢\phi \to \frac{CX+D}{A}=\left(\frac{C}{A}\right)X+\left(\frac{D}{A}\right)$$
35	30 34	oveq12d	$$⊢\phi \to \left(\frac{A{X}^3+B{X}^2}{A}\right)+\left(\frac{CX+D}{A}\right)=X^3+\left(\frac{B}{A}\right)X^2+\left(\frac{C}{A}\right)X+\left(\frac{D}{A}\right)$$
36	25 35	eqtrd	$$⊢\phi \to \frac{A{X}^3+B{X}^2+CX+D}{A}=X^3+\left(\frac{B}{A}\right)X^2+\left(\frac{C}{A}\right)X+\left(\frac{D}{A}\right)$$
37	36	eqeq1d	$$⊢\phi \to \left(\frac{A{X}^3+B{X}^2+CX+D}{A}=0\leftrightarrow X^3+\left(\frac{B}{A}\right)X^2+\left(\frac{C}{A}\right)X+\left(\frac{D}{A}\right)=0\right)$$
38	24 37	bitr3d	$$⊢\phi \to \left(A{X}^3+B{X}^2+CX+D=0\leftrightarrow X^3+\left(\frac{B}{A}\right)X^2+\left(\frac{C}{A}\right)X+\left(\frac{D}{A}\right)=0\right)$$
39	3 1 2	divcld	$$⊢\phi \to \frac{B}{A}\in ℂ$$
40	4 1 2	divcld	$$⊢\phi \to \frac{C}{A}\in ℂ$$
41	5 1 2	divcld	$$⊢\phi \to \frac{D}{A}\in ℂ$$
42	7 1 2	divcld	$$⊢\phi \to \frac{T}{A}\in ℂ$$
43	14	a1i	$$⊢\phi \to 3\in {\mathbb{N}}_0$$
44	7 1 2 43	expdivd	$$⊢\phi \to {\left(\frac{T}{A}\right)}^3=\frac{T^3}{A^3}$$
45	8	oveq1d	$$⊢\phi \to \frac{T^3}{A^3}=\frac{\frac{N+G}{2}}{A^3}$$
46		2cn	$$⊢2\in ℂ$$
47		expcl	$$⊢\left(B\in ℂ\wedge 3\in {\mathbb{N}}_0\right)\to B^3\in ℂ$$
48	3 14 47	sylancl	$$⊢\phi \to B^3\in ℂ$$
49		mulcl	$$⊢\left(2\in ℂ\wedge B^3\in ℂ\right)\to 2B^3\in ℂ$$
50	46 48 49	sylancr	$$⊢\phi \to 2B^3\in ℂ$$
51		9cn	$$⊢9\in ℂ$$
52		mulcl	$$⊢\left(9\in ℂ\wedge A\in ℂ\right)\to 9A\in ℂ$$
53	51 1 52	sylancr	$$⊢\phi \to 9A\in ℂ$$
54	3 4	mulcld	$$⊢\phi \to BC\in ℂ$$
55	53 54	mulcld	$$⊢\phi \to 9ABC\in ℂ$$
56	50 55	subcld	$$⊢\phi \to 2B^3-9ABC\in ℂ$$
57		2nn0	$$⊢2\in {\mathbb{N}}_0$$
58		7nn	$$⊢7\in \mathbb{N}$$
59	57 58	decnncl	$$⊢27\in \mathbb{N}$$
60	59	nncni	$$⊢27\in ℂ$$
61	1	sqcld	$$⊢\phi \to A^2\in ℂ$$
62	61 5	mulcld	$$⊢\phi \to A^{2}D\in ℂ$$
63		mulcl	$$⊢\left(27\in ℂ\wedge A^{2}D\in ℂ\right)\to 27A^{2}D\in ℂ$$
64	60 62 63	sylancr	$$⊢\phi \to 27A^{2}D\in ℂ$$
65	56 64	addcld	$$⊢\phi \to 2B^3-9ABC+27A^{2}D\in ℂ$$
66	12 65	eqeltrd	$$⊢\phi \to N\in ℂ$$
67	66 9	addcld	$$⊢\phi \to N+G\in ℂ$$
68		2cnd	$$⊢\phi \to 2\in ℂ$$
69		expcl	$$⊢\left(A\in ℂ\wedge 3\in {\mathbb{N}}_0\right)\to A^3\in ℂ$$
70	1 14 69	sylancl	$$⊢\phi \to A^3\in ℂ$$
71		2ne0	$$⊢2\ne 0$$
72	71	a1i	$$⊢\phi \to 2\ne 0$$
73		3z	$$⊢3\in \mathbb{Z}$$
74	73	a1i	$$⊢\phi \to 3\in \mathbb{Z}$$
75	1 2 74	expne0d	$$⊢\phi \to A^3\ne 0$$
76	67 68 70 72 75	divdiv32d	$$⊢\phi \to \frac{\frac{N+G}{2}}{A^3}=\frac{\frac{N+G}{A^3}}{2}$$
77	66 9 70 75	divdird	$$⊢\phi \to \frac{N+G}{A^3}=\left(\frac{N}{A^3}\right)+\left(\frac{G}{A^3}\right)$$
78	77	oveq1d	$$⊢\phi \to \frac{\frac{N+G}{A^3}}{2}=\frac{\left(\frac{N}{A^3}\right)+\left(\frac{G}{A^3}\right)}{2}$$
79	76 78	eqtrd	$$⊢\phi \to \frac{\frac{N+G}{2}}{A^3}=\frac{\left(\frac{N}{A^3}\right)+\left(\frac{G}{A^3}\right)}{2}$$
80	44 45 79	3eqtrd	$$⊢\phi \to {\left(\frac{T}{A}\right)}^3=\frac{\left(\frac{N}{A^3}\right)+\left(\frac{G}{A^3}\right)}{2}$$
81	9 70 75	divcld	$$⊢\phi \to \frac{G}{A^3}\in ℂ$$
82	9 70 75	sqdivd	$$⊢\phi \to {\left(\frac{G}{A^3}\right)}^2=\frac{G^2}{{\left(A^3\right)}^2}$$
83	10	oveq1d	$$⊢\phi \to \frac{G^2}{{\left(A^3\right)}^2}=\frac{N^2-4M^3}{{\left(A^3\right)}^2}$$
84	66	sqcld	$$⊢\phi \to N^2\in ℂ$$
85		4cn	$$⊢4\in ℂ$$
86	3	sqcld	$$⊢\phi \to B^2\in ℂ$$
87		3cn	$$⊢3\in ℂ$$
88	1 4	mulcld	$$⊢\phi \to AC\in ℂ$$
89		mulcl	$$⊢\left(3\in ℂ\wedge AC\in ℂ\right)\to 3AC\in ℂ$$
90	87 88 89	sylancr	$$⊢\phi \to 3AC\in ℂ$$
91	86 90	subcld	$$⊢\phi \to B^2-3AC\in ℂ$$
92	11 91	eqeltrd	$$⊢\phi \to M\in ℂ$$
93		expcl	$$⊢\left(M\in ℂ\wedge 3\in {\mathbb{N}}_0\right)\to M^3\in ℂ$$
94	92 14 93	sylancl	$$⊢\phi \to M^3\in ℂ$$
95		mulcl	$$⊢\left(4\in ℂ\wedge M^3\in ℂ\right)\to 4M^3\in ℂ$$
96	85 94 95	sylancr	$$⊢\phi \to 4M^3\in ℂ$$
97	70	sqcld	$$⊢\phi \to {\left(A^3\right)}^2\in ℂ$$
98		sqne0	$$⊢A^3\in ℂ\to \left({\left(A^3\right)}^2\ne 0\leftrightarrow A^3\ne 0\right)$$
99	70 98	syl	$$⊢\phi \to \left({\left(A^3\right)}^2\ne 0\leftrightarrow A^3\ne 0\right)$$
100	75 99	mpbird	$$⊢\phi \to {\left(A^3\right)}^2\ne 0$$
101	84 96 97 100	divsubdird	$$⊢\phi \to \frac{N^2-4M^3}{{\left(A^3\right)}^2}=\left(\frac{N^2}{{\left(A^3\right)}^2}\right)-\left(\frac{4M^3}{{\left(A^3\right)}^2}\right)$$
102	66 70 75	sqdivd	$$⊢\phi \to {\left(\frac{N}{A^3}\right)}^2=\frac{N^2}{{\left(A^3\right)}^2}$$
103		2z	$$⊢2\in \mathbb{Z}$$
104	103	a1i	$$⊢\phi \to 2\in \mathbb{Z}$$
105	1 2 104	expne0d	$$⊢\phi \to A^2\ne 0$$
106	92 61 105 43	expdivd	$$⊢\phi \to {\left(\frac{M}{A^2}\right)}^3=\frac{M^3}{{\left(A^2\right)}^3}$$
107	46 87	mulcomi	$$⊢2\cdot 3=3\cdot 2$$
108	107	oveq2i	$$⊢A^{2\cdot 3}=A^{3\cdot 2}$$
109	57	a1i	$$⊢\phi \to 2\in {\mathbb{N}}_0$$
110	1 43 109	expmuld	$$⊢\phi \to A^{2\cdot 3}={\left(A^2\right)}^3$$
111	1 109 43	expmuld	$$⊢\phi \to A^{3\cdot 2}={\left(A^3\right)}^2$$
112	108 110 111	3eqtr3a	$$⊢\phi \to {\left(A^2\right)}^3={\left(A^3\right)}^2$$
113	112	oveq2d	$$⊢\phi \to \frac{M^3}{{\left(A^2\right)}^3}=\frac{M^3}{{\left(A^3\right)}^2}$$
114	106 113	eqtrd	$$⊢\phi \to {\left(\frac{M}{A^2}\right)}^3=\frac{M^3}{{\left(A^3\right)}^2}$$
115	114	oveq2d	$$⊢\phi \to 4{\left(\frac{M}{A^2}\right)}^3=4\left(\frac{M^3}{{\left(A^3\right)}^2}\right)$$
116	85	a1i	$$⊢\phi \to 4\in ℂ$$
117	116 94 97 100	divassd	$$⊢\phi \to \frac{4M^3}{{\left(A^3\right)}^2}=4\left(\frac{M^3}{{\left(A^3\right)}^2}\right)$$
118	115 117	eqtr4d	$$⊢\phi \to 4{\left(\frac{M}{A^2}\right)}^3=\frac{4M^3}{{\left(A^3\right)}^2}$$
119	102 118	oveq12d	$$⊢\phi \to {\left(\frac{N}{A^3}\right)}^2-4{\left(\frac{M}{A^2}\right)}^3=\left(\frac{N^2}{{\left(A^3\right)}^2}\right)-\left(\frac{4M^3}{{\left(A^3\right)}^2}\right)$$
120	101 119	eqtr4d	$$⊢\phi \to \frac{N^2-4M^3}{{\left(A^3\right)}^2}={\left(\frac{N}{A^3}\right)}^2-4{\left(\frac{M}{A^2}\right)}^3$$
121	82 83 120	3eqtrd	$$⊢\phi \to {\left(\frac{G}{A^3}\right)}^2={\left(\frac{N}{A^3}\right)}^2-4{\left(\frac{M}{A^2}\right)}^3$$
122	86 90 61 105	divsubdird	$$⊢\phi \to \frac{B^2-3AC}{A^2}=\left(\frac{B^2}{A^2}\right)-\left(\frac{3AC}{A^2}\right)$$
123	11	oveq1d	$$⊢\phi \to \frac{M}{A^2}=\frac{B^2-3AC}{A^2}$$
124	3 1 2	sqdivd	$$⊢\phi \to {\left(\frac{B}{A}\right)}^2=\frac{B^2}{A^2}$$
125	1	sqvald	$$⊢\phi \to A^2=AA$$
126	125	oveq2d	$$⊢\phi \to \frac{AC}{A^2}=\frac{AC}{AA}$$
127	4 1 1 2 2	divcan5d	$$⊢\phi \to \frac{AC}{AA}=\frac{C}{A}$$
128	126 127	eqtr2d	$$⊢\phi \to \frac{C}{A}=\frac{AC}{A^2}$$
129	128	oveq2d	$$⊢\phi \to 3\left(\frac{C}{A}\right)=3\left(\frac{AC}{A^2}\right)$$
130	87	a1i	$$⊢\phi \to 3\in ℂ$$
131	130 88 61 105	divassd	$$⊢\phi \to \frac{3AC}{A^2}=3\left(\frac{AC}{A^2}\right)$$
132	129 131	eqtr4d	$$⊢\phi \to 3\left(\frac{C}{A}\right)=\frac{3AC}{A^2}$$
133	124 132	oveq12d	$$⊢\phi \to {\left(\frac{B}{A}\right)}^2-3\left(\frac{C}{A}\right)=\left(\frac{B^2}{A^2}\right)-\left(\frac{3AC}{A^2}\right)$$
134	122 123 133	3eqtr4d	$$⊢\phi \to \frac{M}{A^2}={\left(\frac{B}{A}\right)}^2-3\left(\frac{C}{A}\right)$$
135	56 64 70 75	divdird	$$⊢\phi \to \frac{2B^3-9ABC+27A^{2}D}{A^3}=\left(\frac{2B^3-9ABC}{A^3}\right)+\left(\frac{27A^{2}D}{A^3}\right)$$
136	12	oveq1d	$$⊢\phi \to \frac{N}{A^3}=\frac{2B^3-9ABC+27A^{2}D}{A^3}$$
137	3 1 2 43	expdivd	$$⊢\phi \to {\left(\frac{B}{A}\right)}^3=\frac{B^3}{A^3}$$
138	137	oveq2d	$$⊢\phi \to 2{\left(\frac{B}{A}\right)}^3=2\left(\frac{B^3}{A^3}\right)$$
139	68 48 70 75	divassd	$$⊢\phi \to \frac{2B^3}{A^3}=2\left(\frac{B^3}{A^3}\right)$$
140	138 139	eqtr4d	$$⊢\phi \to 2{\left(\frac{B}{A}\right)}^3=\frac{2B^3}{A^3}$$
141	51	a1i	$$⊢\phi \to 9\in ℂ$$
142	1 54	mulcld	$$⊢\phi \to ABC\in ℂ$$
143	141 142 70 75	divassd	$$⊢\phi \to \frac{9ABC}{A^3}=9\left(\frac{ABC}{A^3}\right)$$
144	141 1 54	mulassd	$$⊢\phi \to 9ABC=9ABC$$
145	144	oveq1d	$$⊢\phi \to \frac{9ABC}{A^3}=\frac{9ABC}{A^3}$$
146	54 61 1 105 2	divcan5d	$$⊢\phi \to \frac{ABC}{A{A}^2}=\frac{BC}{A^2}$$
147		df-3	$$⊢3=2+1$$
148	147	oveq2i	$$⊢A^3=A^{2+1}$$
149		expp1	$$⊢\left(A\in ℂ\wedge 2\in {\mathbb{N}}_0\right)\to A^{2+1}=A^{2}A$$
150	1 57 149	sylancl	$$⊢\phi \to A^{2+1}=A^{2}A$$
151	148 150	syl5eq	$$⊢\phi \to A^3=A^{2}A$$
152	61 1	mulcomd	$$⊢\phi \to A^{2}A=A{A}^2$$
153	151 152	eqtrd	$$⊢\phi \to A^3=A{A}^2$$
154	153	oveq2d	$$⊢\phi \to \frac{ABC}{A^3}=\frac{ABC}{A{A}^2}$$
155	3 1 4 1 2 2	divmuldivd	$$⊢\phi \to \left(\frac{B}{A}\right)\left(\frac{C}{A}\right)=\frac{BC}{AA}$$
156	125	oveq2d	$$⊢\phi \to \frac{BC}{A^2}=\frac{BC}{AA}$$
157	155 156	eqtr4d	$$⊢\phi \to \left(\frac{B}{A}\right)\left(\frac{C}{A}\right)=\frac{BC}{A^2}$$
158	146 154 157	3eqtr4rd	$$⊢\phi \to \left(\frac{B}{A}\right)\left(\frac{C}{A}\right)=\frac{ABC}{A^3}$$
159	158	oveq2d	$$⊢\phi \to 9\left(\frac{B}{A}\right)\left(\frac{C}{A}\right)=9\left(\frac{ABC}{A^3}\right)$$
160	143 145 159	3eqtr4rd	$$⊢\phi \to 9\left(\frac{B}{A}\right)\left(\frac{C}{A}\right)=\frac{9ABC}{A^3}$$
161	140 160	oveq12d	$$⊢\phi \to 2{\left(\frac{B}{A}\right)}^3-9\left(\frac{B}{A}\right)\left(\frac{C}{A}\right)=\left(\frac{2B^3}{A^3}\right)-\left(\frac{9ABC}{A^3}\right)$$
162	50 55 70 75	divsubdird	$$⊢\phi \to \frac{2B^3-9ABC}{A^3}=\left(\frac{2B^3}{A^3}\right)-\left(\frac{9ABC}{A^3}\right)$$
163	161 162	eqtr4d	$$⊢\phi \to 2{\left(\frac{B}{A}\right)}^3-9\left(\frac{B}{A}\right)\left(\frac{C}{A}\right)=\frac{2B^3-9ABC}{A^3}$$
164	151	oveq2d	$$⊢\phi \to \frac{A^{2}D}{A^3}=\frac{A^{2}D}{A^{2}A}$$
165	5 1 61 2 105	divcan5d	$$⊢\phi \to \frac{A^{2}D}{A^{2}A}=\frac{D}{A}$$
166	164 165	eqtr2d	$$⊢\phi \to \frac{D}{A}=\frac{A^{2}D}{A^3}$$
167	166	oveq2d	$$⊢\phi \to 27\left(\frac{D}{A}\right)=27\left(\frac{A^{2}D}{A^3}\right)$$
168	60	a1i	$$⊢\phi \to 27\in ℂ$$
169	168 62 70 75	divassd	$$⊢\phi \to \frac{27A^{2}D}{A^3}=27\left(\frac{A^{2}D}{A^3}\right)$$
170	167 169	eqtr4d	$$⊢\phi \to 27\left(\frac{D}{A}\right)=\frac{27A^{2}D}{A^3}$$
171	163 170	oveq12d	$$⊢\phi \to 2{\left(\frac{B}{A}\right)}^3-9\left(\frac{B}{A}\right)\left(\frac{C}{A}\right)+27\left(\frac{D}{A}\right)=\left(\frac{2B^3-9ABC}{A^3}\right)+\left(\frac{27A^{2}D}{A^3}\right)$$
172	135 136 171	3eqtr4d	$$⊢\phi \to \frac{N}{A^3}=2{\left(\frac{B}{A}\right)}^3-9\left(\frac{B}{A}\right)\left(\frac{C}{A}\right)+27\left(\frac{D}{A}\right)$$
173	7 1 13 2	divne0d	$$⊢\phi \to \frac{T}{A}\ne 0$$
174	39 40 41 6 42 80 81 121 134 172 173	mcubic	$$⊢\phi \to \left(X^3+\left(\frac{B}{A}\right)X^2+\left(\frac{C}{A}\right)X+\left(\frac{D}{A}\right)=0\leftrightarrow \exists r\in ℂ\left(r^3=1\wedge X=-\frac{\left(\frac{B}{A}\right)+r\left(\frac{T}{A}\right)+\left(\frac{\frac{M}{A^2}}{r\left(\frac{T}{A}\right)}\right)}{3}\right)\right)$$
175		oveq1	$$⊢r=0\to r^3=0^3$$
176		3nn	$$⊢3\in \mathbb{N}$$
177		0exp	$$⊢3\in \mathbb{N}\to 0^3=0$$
178	176 177	ax-mp	$$⊢0^3=0$$
179	175 178	eqtrdi	$$⊢r=0\to r^3=0$$
180		0ne1	$$⊢0\ne 1$$
181	180	a1i	$$⊢r=0\to 0\ne 1$$
182	179 181	eqnetrd	$$⊢r=0\to r^3\ne 1$$
183	182	necon2i	$$⊢r^3=1\to r\ne 0$$
184		simprl	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to r\in ℂ$$
185	7	adantr	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to T\in ℂ$$
186	1	adantr	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to A\in ℂ$$
187	2	adantr	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to A\ne 0$$
188	184 185 186 187	divassd	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to \frac{rT}{A}=r\left(\frac{T}{A}\right)$$
189	188	eqcomd	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to r\left(\frac{T}{A}\right)=\frac{rT}{A}$$
190	189	oveq2d	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to \left(\frac{B}{A}\right)+r\left(\frac{T}{A}\right)=\left(\frac{B}{A}\right)+\left(\frac{rT}{A}\right)$$
191	3	adantr	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to B\in ℂ$$
192	184 185	mulcld	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to rT\in ℂ$$
193	191 192 186 187	divdird	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to \frac{B+rT}{A}=\left(\frac{B}{A}\right)+\left(\frac{rT}{A}\right)$$
194	190 193	eqtr4d	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to \left(\frac{B}{A}\right)+r\left(\frac{T}{A}\right)=\frac{B+rT}{A}$$
195	92	adantr	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to M\in ℂ$$
196	195 186 187	divcld	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to \frac{M}{A}\in ℂ$$
197		simprr	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to r\ne 0$$
198	13	adantr	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to T\ne 0$$
199	184 185 197 198	mulne0d	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to rT\ne 0$$
200	196 192 186 199 187	divcan7d	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to \frac{\frac{\frac{M}{A}}{A}}{\frac{rT}{A}}=\frac{\frac{M}{A}}{rT}$$
201	195 186 186 187 187	divdiv1d	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to \frac{\frac{M}{A}}{A}=\frac{M}{AA}$$
202	186	sqvald	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to A^2=AA$$
203	202	oveq2d	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to \frac{M}{A^2}=\frac{M}{AA}$$
204	201 203	eqtr4d	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to \frac{\frac{M}{A}}{A}=\frac{M}{A^2}$$
205	204 188	oveq12d	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to \frac{\frac{\frac{M}{A}}{A}}{\frac{rT}{A}}=\frac{\frac{M}{A^2}}{r\left(\frac{T}{A}\right)}$$
206	195 186 192 187 199	divdiv32d	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to \frac{\frac{M}{A}}{rT}=\frac{\frac{M}{rT}}{A}$$
207	200 205 206	3eqtr3d	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to \frac{\frac{M}{A^2}}{r\left(\frac{T}{A}\right)}=\frac{\frac{M}{rT}}{A}$$
208	194 207	oveq12d	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to \left(\frac{B}{A}\right)+r\left(\frac{T}{A}\right)+\left(\frac{\frac{M}{A^2}}{r\left(\frac{T}{A}\right)}\right)=\left(\frac{B+rT}{A}\right)+\left(\frac{\frac{M}{rT}}{A}\right)$$
209	191 192	addcld	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to B+rT\in ℂ$$
210	195 192 199	divcld	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to \frac{M}{rT}\in ℂ$$
211	209 210 186 187	divdird	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to \frac{B+rT+\left(\frac{M}{rT}\right)}{A}=\left(\frac{B+rT}{A}\right)+\left(\frac{\frac{M}{rT}}{A}\right)$$
212	208 211	eqtr4d	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to \left(\frac{B}{A}\right)+r\left(\frac{T}{A}\right)+\left(\frac{\frac{M}{A^2}}{r\left(\frac{T}{A}\right)}\right)=\frac{B+rT+\left(\frac{M}{rT}\right)}{A}$$
213	212	oveq1d	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to \frac{\left(\frac{B}{A}\right)+r\left(\frac{T}{A}\right)+\left(\frac{\frac{M}{A^2}}{r\left(\frac{T}{A}\right)}\right)}{3}=\frac{\frac{B+rT+\left(\frac{M}{rT}\right)}{A}}{3}$$
214	209 210	addcld	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to B+rT+\left(\frac{M}{rT}\right)\in ℂ$$
215	87	a1i	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to 3\in ℂ$$
216		3ne0	$$⊢3\ne 0$$
217	216	a1i	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to 3\ne 0$$
218	214 186 215 187 217	divdiv1d	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to \frac{\frac{B+rT+\left(\frac{M}{rT}\right)}{A}}{3}=\frac{B+rT+\left(\frac{M}{rT}\right)}{A\cdot 3}$$
219		mulcom	$$⊢\left(A\in ℂ\wedge 3\in ℂ\right)\to A\cdot 3=3A$$
220	186 87 219	sylancl	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to A\cdot 3=3A$$
221	220	oveq2d	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to \frac{B+rT+\left(\frac{M}{rT}\right)}{A\cdot 3}=\frac{B+rT+\left(\frac{M}{rT}\right)}{3A}$$
222	213 218 221	3eqtrd	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to \frac{\left(\frac{B}{A}\right)+r\left(\frac{T}{A}\right)+\left(\frac{\frac{M}{A^2}}{r\left(\frac{T}{A}\right)}\right)}{3}=\frac{B+rT+\left(\frac{M}{rT}\right)}{3A}$$
223	222	negeqd	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to -\frac{\left(\frac{B}{A}\right)+r\left(\frac{T}{A}\right)+\left(\frac{\frac{M}{A^2}}{r\left(\frac{T}{A}\right)}\right)}{3}=-\frac{B+rT+\left(\frac{M}{rT}\right)}{3A}$$
224	223	eqeq2d	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to \left(X=-\frac{\left(\frac{B}{A}\right)+r\left(\frac{T}{A}\right)+\left(\frac{\frac{M}{A^2}}{r\left(\frac{T}{A}\right)}\right)}{3}\leftrightarrow X=-\frac{B+rT+\left(\frac{M}{rT}\right)}{3A}\right)$$
225	224	anassrs	$$⊢\left(\left(\phi \wedge r\in ℂ\right)\wedge r\ne 0\right)\to \left(X=-\frac{\left(\frac{B}{A}\right)+r\left(\frac{T}{A}\right)+\left(\frac{\frac{M}{A^2}}{r\left(\frac{T}{A}\right)}\right)}{3}\leftrightarrow X=-\frac{B+rT+\left(\frac{M}{rT}\right)}{3A}\right)$$
226	183 225	sylan2	$$⊢\left(\left(\phi \wedge r\in ℂ\right)\wedge r^3=1\right)\to \left(X=-\frac{\left(\frac{B}{A}\right)+r\left(\frac{T}{A}\right)+\left(\frac{\frac{M}{A^2}}{r\left(\frac{T}{A}\right)}\right)}{3}\leftrightarrow X=-\frac{B+rT+\left(\frac{M}{rT}\right)}{3A}\right)$$
227	226	pm5.32da	$$⊢\left(\phi \wedge r\in ℂ\right)\to \left(\left(r^3=1\wedge X=-\frac{\left(\frac{B}{A}\right)+r\left(\frac{T}{A}\right)+\left(\frac{\frac{M}{A^2}}{r\left(\frac{T}{A}\right)}\right)}{3}\right)\leftrightarrow \left(r^3=1\wedge X=-\frac{B+rT+\left(\frac{M}{rT}\right)}{3A}\right)\right)$$
228	227	rexbidva	$$⊢\phi \to \left(\exists r\in ℂ\left(r^3=1\wedge X=-\frac{\left(\frac{B}{A}\right)+r\left(\frac{T}{A}\right)+\left(\frac{\frac{M}{A^2}}{r\left(\frac{T}{A}\right)}\right)}{3}\right)\leftrightarrow \exists r\in ℂ\left(r^3=1\wedge X=-\frac{B+rT+\left(\frac{M}{rT}\right)}{3A}\right)\right)$$
229	38 174 228	3bitrd	$$⊢\phi \to \left(A{X}^3+B{X}^2+CX+D=0\leftrightarrow \exists r\in ℂ\left(r^3=1\wedge X=-\frac{B+rT+\left(\frac{M}{rT}\right)}{3A}\right)\right)$$