Theorem mcubic

Description: Solutions to a monic cubic equation, a special case of cubic . (Contributed by Mario Carneiro, 24-Apr-2015)

	Ref	Expression
Hypotheses	mcubic.b	$$⊢\phi \to B\in ℂ$$
	mcubic.c	$$⊢\phi \to C\in ℂ$$
	mcubic.d	$$⊢\phi \to D\in ℂ$$
	mcubic.x	$$⊢\phi \to X\in ℂ$$
	mcubic.t	$$⊢\phi \to T\in ℂ$$
	mcubic.3	$$⊢\phi \to T^3=\frac{N+G}{2}$$
	mcubic.g	$$⊢\phi \to G\in ℂ$$
	mcubic.2	$$⊢\phi \to G^2=N^2-4M^3$$
	mcubic.m	$$⊢\phi \to M=B^2-3C$$
	mcubic.n	$$⊢\phi \to N=2B^3-9BC+27D$$
	mcubic.0	$$⊢\phi \to T\ne 0$$
Assertion	mcubic	$$⊢\phi \to \left(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)}{3}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		mcubic.b	$$⊢\phi \to B\in ℂ$$
2		mcubic.c	$$⊢\phi \to C\in ℂ$$
3		mcubic.d	$$⊢\phi \to D\in ℂ$$
4		mcubic.x	$$⊢\phi \to X\in ℂ$$
5		mcubic.t	$$⊢\phi \to T\in ℂ$$
6		mcubic.3	$$⊢\phi \to T^3=\frac{N+G}{2}$$
7		mcubic.g	$$⊢\phi \to G\in ℂ$$
8		mcubic.2	$$⊢\phi \to G^2=N^2-4M^3$$
9		mcubic.m	$$⊢\phi \to M=B^2-3C$$
10		mcubic.n	$$⊢\phi \to N=2B^3-9BC+27D$$
11		mcubic.0	$$⊢\phi \to T\ne 0$$
12	1	sqcld	$$⊢\phi \to B^2\in ℂ$$
13		3cn	$$⊢3\in ℂ$$
14		mulcl	$$⊢\left(3\in ℂ\wedge C\in ℂ\right)\to 3C\in ℂ$$
15	13 2 14	sylancr	$$⊢\phi \to 3C\in ℂ$$
16	12 15	subcld	$$⊢\phi \to B^2-3C\in ℂ$$
17	9 16	eqeltrd	$$⊢\phi \to M\in ℂ$$
18	13	a1i	$$⊢\phi \to 3\in ℂ$$
19		3ne0	$$⊢3\ne 0$$
20	19	a1i	$$⊢\phi \to 3\ne 0$$
21	17 18 20	divcld	$$⊢\phi \to \frac{M}{3}\in ℂ$$
22	21	negcld	$$⊢\phi \to -\frac{M}{3}\in ℂ$$
23		2cn	$$⊢2\in ℂ$$
24		3nn0	$$⊢3\in {\mathbb{N}}_0$$
25		expcl	$$⊢\left(B\in ℂ\wedge 3\in {\mathbb{N}}_0\right)\to B^3\in ℂ$$
26	1 24 25	sylancl	$$⊢\phi \to B^3\in ℂ$$
27		mulcl	$$⊢\left(2\in ℂ\wedge B^3\in ℂ\right)\to 2B^3\in ℂ$$
28	23 26 27	sylancr	$$⊢\phi \to 2B^3\in ℂ$$
29		9cn	$$⊢9\in ℂ$$
30	1 2	mulcld	$$⊢\phi \to BC\in ℂ$$
31		mulcl	$$⊢\left(9\in ℂ\wedge BC\in ℂ\right)\to 9BC\in ℂ$$
32	29 30 31	sylancr	$$⊢\phi \to 9BC\in ℂ$$
33	28 32	subcld	$$⊢\phi \to 2B^3-9BC\in ℂ$$
34		2nn0	$$⊢2\in {\mathbb{N}}_0$$
35		7nn	$$⊢7\in \mathbb{N}$$
36	34 35	decnncl	$$⊢27\in \mathbb{N}$$
37	36	nncni	$$⊢27\in ℂ$$
38		mulcl	$$⊢\left(27\in ℂ\wedge D\in ℂ\right)\to 27D\in ℂ$$
39	37 3 38	sylancr	$$⊢\phi \to 27D\in ℂ$$
40	33 39	addcld	$$⊢\phi \to 2B^3-9BC+27D\in ℂ$$
41	10 40	eqeltrd	$$⊢\phi \to N\in ℂ$$
42	37	a1i	$$⊢\phi \to 27\in ℂ$$
43	36	nnne0i	$$⊢27\ne 0$$
44	43	a1i	$$⊢\phi \to 27\ne 0$$
45	41 42 44	divcld	$$⊢\phi \to \frac{N}{27}\in ℂ$$
46	1 18 20	divcld	$$⊢\phi \to \frac{B}{3}\in ℂ$$
47	4 46	addcld	$$⊢\phi \to X+\left(\frac{B}{3}\right)\in ℂ$$
48	5 18 20	divcld	$$⊢\phi \to \frac{T}{3}\in ℂ$$
49	48	negcld	$$⊢\phi \to -\frac{T}{3}\in ℂ$$
50		3nn	$$⊢3\in \mathbb{N}$$
51	50	a1i	$$⊢\phi \to 3\in \mathbb{N}$$
52		n2dvds3	$$⊢\neg 2\parallel 3$$
53	52	a1i	$$⊢\phi \to \neg 2\parallel 3$$
54		oexpneg	$$⊢\left(\frac{T}{3}\in ℂ\wedge 3\in \mathbb{N}\wedge \neg 2\parallel 3\right)\to {\left(-\left(\frac{T}{3}\right)\right)}^3=-{\left(\frac{T}{3}\right)}^3$$
55	48 51 53 54	syl3anc	$$⊢\phi \to {\left(-\left(\frac{T}{3}\right)\right)}^3=-{\left(\frac{T}{3}\right)}^3$$
56	24	a1i	$$⊢\phi \to 3\in {\mathbb{N}}_0$$
57	5 18 20 56	expdivd	$$⊢\phi \to {\left(\frac{T}{3}\right)}^3=\frac{T^3}{3^3}$$
58		3exp3	$$⊢3^3=27$$
59	58	a1i	$$⊢\phi \to 3^3=27$$
60	6 59	oveq12d	$$⊢\phi \to \frac{T^3}{3^3}=\frac{\frac{N+G}{2}}{27}$$
61	41 7	addcld	$$⊢\phi \to N+G\in ℂ$$
62		2cnd	$$⊢\phi \to 2\in ℂ$$
63		2ne0	$$⊢2\ne 0$$
64	63	a1i	$$⊢\phi \to 2\ne 0$$
65	61 62 42 64 44	divdiv32d	$$⊢\phi \to \frac{\frac{N+G}{2}}{27}=\frac{\frac{N+G}{27}}{2}$$
66	41 7	addcomd	$$⊢\phi \to N+G=G+N$$
67	66	oveq1d	$$⊢\phi \to \frac{N+G}{27}=\frac{G+N}{27}$$
68	7 41 42 44	divdird	$$⊢\phi \to \frac{G+N}{27}=\left(\frac{G}{27}\right)+\left(\frac{N}{27}\right)$$
69	67 68	eqtrd	$$⊢\phi \to \frac{N+G}{27}=\left(\frac{G}{27}\right)+\left(\frac{N}{27}\right)$$
70	69	oveq1d	$$⊢\phi \to \frac{\frac{N+G}{27}}{2}=\frac{\left(\frac{G}{27}\right)+\left(\frac{N}{27}\right)}{2}$$
71	7 42 44	divcld	$$⊢\phi \to \frac{G}{27}\in ℂ$$
72	71 45 62 64	divdird	$$⊢\phi \to \frac{\left(\frac{G}{27}\right)+\left(\frac{N}{27}\right)}{2}=\left(\frac{\frac{G}{27}}{2}\right)+\left(\frac{\frac{N}{27}}{2}\right)$$
73	65 70 72	3eqtrd	$$⊢\phi \to \frac{\frac{N+G}{2}}{27}=\left(\frac{\frac{G}{27}}{2}\right)+\left(\frac{\frac{N}{27}}{2}\right)$$
74	57 60 73	3eqtrd	$$⊢\phi \to {\left(\frac{T}{3}\right)}^3=\left(\frac{\frac{G}{27}}{2}\right)+\left(\frac{\frac{N}{27}}{2}\right)$$
75	74	negeqd	$$⊢\phi \to -{\left(\frac{T}{3}\right)}^3=-\left(\left(\frac{\frac{G}{27}}{2}\right)+\left(\frac{\frac{N}{27}}{2}\right)\right)$$
76	71	halfcld	$$⊢\phi \to \frac{\frac{G}{27}}{2}\in ℂ$$
77	45	halfcld	$$⊢\phi \to \frac{\frac{N}{27}}{2}\in ℂ$$
78	76 77	negdi2d	$$⊢\phi \to -\left(\left(\frac{\frac{G}{27}}{2}\right)+\left(\frac{\frac{N}{27}}{2}\right)\right)=-\left(\frac{\frac{G}{27}}{2}\right)-\left(\frac{\frac{N}{27}}{2}\right)$$
79	55 75 78	3eqtrd	$$⊢\phi \to {\left(-\left(\frac{T}{3}\right)\right)}^3=-\left(\frac{\frac{G}{27}}{2}\right)-\left(\frac{\frac{N}{27}}{2}\right)$$
80	76	negcld	$$⊢\phi \to -\frac{\frac{G}{27}}{2}\in ℂ$$
81		sqneg	$$⊢\frac{\frac{G}{27}}{2}\in ℂ\to {\left(-\left(\frac{\frac{G}{27}}{2}\right)\right)}^2={\left(\frac{\frac{G}{27}}{2}\right)}^2$$
82	76 81	syl	$$⊢\phi \to {\left(-\left(\frac{\frac{G}{27}}{2}\right)\right)}^2={\left(\frac{\frac{G}{27}}{2}\right)}^2$$
83	71 62 64	sqdivd	$$⊢\phi \to {\left(\frac{\frac{G}{27}}{2}\right)}^2=\frac{{\left(\frac{G}{27}\right)}^2}{2^2}$$
84	45 62 64	sqdivd	$$⊢\phi \to {\left(\frac{\frac{N}{27}}{2}\right)}^2=\frac{{\left(\frac{N}{27}\right)}^2}{2^2}$$
85	41 42 44	sqdivd	$$⊢\phi \to {\left(\frac{N}{27}\right)}^2=\frac{N^2}{{27}^2}$$
86	85	oveq1d	$$⊢\phi \to \frac{{\left(\frac{N}{27}\right)}^2}{2^2}=\frac{\frac{N^2}{{27}^2}}{2^2}$$
87	84 86	eqtr2d	$$⊢\phi \to \frac{\frac{N^2}{{27}^2}}{2^2}={\left(\frac{\frac{N}{27}}{2}\right)}^2$$
88		4cn	$$⊢4\in ℂ$$
89	88	a1i	$$⊢\phi \to 4\in ℂ$$
90		expcl	$$⊢\left(M\in ℂ\wedge 3\in {\mathbb{N}}_0\right)\to M^3\in ℂ$$
91	17 24 90	sylancl	$$⊢\phi \to M^3\in ℂ$$
92	37	sqcli	$$⊢{27}^2\in ℂ$$
93	92	a1i	$$⊢\phi \to {27}^2\in ℂ$$
94		sqne0	$$⊢27\in ℂ\to \left({27}^2\ne 0\leftrightarrow 27\ne 0\right)$$
95	42 94	syl	$$⊢\phi \to \left({27}^2\ne 0\leftrightarrow 27\ne 0\right)$$
96	44 95	mpbird	$$⊢\phi \to {27}^2\ne 0$$
97	89 91 93 96	divassd	$$⊢\phi \to \frac{4M^3}{{27}^2}=4\left(\frac{M^3}{{27}^2}\right)$$
98	29	a1i	$$⊢\phi \to 9\in ℂ$$
99		9nn	$$⊢9\in \mathbb{N}$$
100	99	nnne0i	$$⊢9\ne 0$$
101	100	a1i	$$⊢\phi \to 9\ne 0$$
102	17 98 101 56	expdivd	$$⊢\phi \to {\left(\frac{M}{9}\right)}^3=\frac{M^3}{9^3}$$
103	23 13	mulcomi	$$⊢2\cdot 3=3\cdot 2$$
104	103	oveq2i	$$⊢3^{2\cdot 3}=3^{3\cdot 2}$$
105		expmul	$$⊢\left(3\in ℂ\wedge 2\in {\mathbb{N}}_0\wedge 3\in {\mathbb{N}}_0\right)\to 3^{2\cdot 3}={\left(3^2\right)}^3$$
106	13 34 24 105	mp3an	$$⊢3^{2\cdot 3}={\left(3^2\right)}^3$$
107		expmul	$$⊢\left(3\in ℂ\wedge 3\in {\mathbb{N}}_0\wedge 2\in {\mathbb{N}}_0\right)\to 3^{3\cdot 2}={\left(3^3\right)}^2$$
108	13 24 34 107	mp3an	$$⊢3^{3\cdot 2}={\left(3^3\right)}^2$$
109	104 106 108	3eqtr3i	$$⊢{\left(3^2\right)}^3={\left(3^3\right)}^2$$
110		sq3	$$⊢3^2=9$$
111	110	oveq1i	$$⊢{\left(3^2\right)}^3=9^3$$
112	58	oveq1i	$$⊢{\left(3^3\right)}^2={27}^2$$
113	109 111 112	3eqtr3i	$$⊢9^3={27}^2$$
114	113	oveq2i	$$⊢\frac{M^3}{9^3}=\frac{M^3}{{27}^2}$$
115	102 114	eqtrdi	$$⊢\phi \to {\left(\frac{M}{9}\right)}^3=\frac{M^3}{{27}^2}$$
116	115	oveq2d	$$⊢\phi \to 4{\left(\frac{M}{9}\right)}^3=4\left(\frac{M^3}{{27}^2}\right)$$
117	97 116	eqtr4d	$$⊢\phi \to \frac{4M^3}{{27}^2}=4{\left(\frac{M}{9}\right)}^3$$
118	117	oveq1d	$$⊢\phi \to \frac{\frac{4M^3}{{27}^2}}{2^2}=\frac{4{\left(\frac{M}{9}\right)}^3}{2^2}$$
119		sq2	$$⊢2^2=4$$
120	119	oveq2i	$$⊢\frac{4{\left(\frac{M}{9}\right)}^3}{2^2}=\frac{4{\left(\frac{M}{9}\right)}^3}{4}$$
121	17 98 101	divcld	$$⊢\phi \to \frac{M}{9}\in ℂ$$
122		expcl	$$⊢\left(\frac{M}{9}\in ℂ\wedge 3\in {\mathbb{N}}_0\right)\to {\left(\frac{M}{9}\right)}^3\in ℂ$$
123	121 24 122	sylancl	$$⊢\phi \to {\left(\frac{M}{9}\right)}^3\in ℂ$$
124		4ne0	$$⊢4\ne 0$$
125	124	a1i	$$⊢\phi \to 4\ne 0$$
126	123 89 125	divcan3d	$$⊢\phi \to \frac{4{\left(\frac{M}{9}\right)}^3}{4}={\left(\frac{M}{9}\right)}^3$$
127	120 126	eqtrid	$$⊢\phi \to \frac{4{\left(\frac{M}{9}\right)}^3}{2^2}={\left(\frac{M}{9}\right)}^3$$
128	118 127	eqtrd	$$⊢\phi \to \frac{\frac{4M^3}{{27}^2}}{2^2}={\left(\frac{M}{9}\right)}^3$$
129	87 128	oveq12d	$$⊢\phi \to \left(\frac{\frac{N^2}{{27}^2}}{2^2}\right)-\left(\frac{\frac{4M^3}{{27}^2}}{2^2}\right)={\left(\frac{\frac{N}{27}}{2}\right)}^2-{\left(\frac{M}{9}\right)}^3$$
130	41	sqcld	$$⊢\phi \to N^2\in ℂ$$
131	130 93 96	divcld	$$⊢\phi \to \frac{N^2}{{27}^2}\in ℂ$$
132		mulcl	$$⊢\left(4\in ℂ\wedge M^3\in ℂ\right)\to 4M^3\in ℂ$$
133	88 91 132	sylancr	$$⊢\phi \to 4M^3\in ℂ$$
134	133 93 96	divcld	$$⊢\phi \to \frac{4M^3}{{27}^2}\in ℂ$$
135	23	sqcli	$$⊢2^2\in ℂ$$
136	135	a1i	$$⊢\phi \to 2^2\in ℂ$$
137	119 124	eqnetri	$$⊢2^2\ne 0$$
138	137	a1i	$$⊢\phi \to 2^2\ne 0$$
139	131 134 136 138	divsubdird	$$⊢\phi \to \frac{\left(\frac{N^2}{{27}^2}\right)-\left(\frac{4M^3}{{27}^2}\right)}{2^2}=\left(\frac{\frac{N^2}{{27}^2}}{2^2}\right)-\left(\frac{\frac{4M^3}{{27}^2}}{2^2}\right)$$
140	77	sqcld	$$⊢\phi \to {\left(\frac{\frac{N}{27}}{2}\right)}^2\in ℂ$$
141	140 123	negsubd	$$⊢\phi \to {\left(\frac{\frac{N}{27}}{2}\right)}^2+\left(-{\left(\frac{M}{9}\right)}^3\right)={\left(\frac{\frac{N}{27}}{2}\right)}^2-{\left(\frac{M}{9}\right)}^3$$
142	129 139 141	3eqtr4d	$$⊢\phi \to \frac{\left(\frac{N^2}{{27}^2}\right)-\left(\frac{4M^3}{{27}^2}\right)}{2^2}={\left(\frac{\frac{N}{27}}{2}\right)}^2+\left(-{\left(\frac{M}{9}\right)}^3\right)$$
143	7 42 44	sqdivd	$$⊢\phi \to {\left(\frac{G}{27}\right)}^2=\frac{G^2}{{27}^2}$$
144	8	oveq1d	$$⊢\phi \to \frac{G^2}{{27}^2}=\frac{N^2-4M^3}{{27}^2}$$
145	130 133 93 96	divsubdird	$$⊢\phi \to \frac{N^2-4M^3}{{27}^2}=\left(\frac{N^2}{{27}^2}\right)-\left(\frac{4M^3}{{27}^2}\right)$$
146	143 144 145	3eqtrd	$$⊢\phi \to {\left(\frac{G}{27}\right)}^2=\left(\frac{N^2}{{27}^2}\right)-\left(\frac{4M^3}{{27}^2}\right)$$
147	146	oveq1d	$$⊢\phi \to \frac{{\left(\frac{G}{27}\right)}^2}{2^2}=\frac{\left(\frac{N^2}{{27}^2}\right)-\left(\frac{4M^3}{{27}^2}\right)}{2^2}$$
148		oexpneg	$$⊢\left(\frac{M}{9}\in ℂ\wedge 3\in \mathbb{N}\wedge \neg 2\parallel 3\right)\to {\left(-\left(\frac{M}{9}\right)\right)}^3=-{\left(\frac{M}{9}\right)}^3$$
149	121 51 53 148	syl3anc	$$⊢\phi \to {\left(-\left(\frac{M}{9}\right)\right)}^3=-{\left(\frac{M}{9}\right)}^3$$
150	149	oveq2d	$$⊢\phi \to {\left(\frac{\frac{N}{27}}{2}\right)}^2+{\left(-\left(\frac{M}{9}\right)\right)}^3={\left(\frac{\frac{N}{27}}{2}\right)}^2+\left(-{\left(\frac{M}{9}\right)}^3\right)$$
151	142 147 150	3eqtr4d	$$⊢\phi \to \frac{{\left(\frac{G}{27}\right)}^2}{2^2}={\left(\frac{\frac{N}{27}}{2}\right)}^2+{\left(-\left(\frac{M}{9}\right)\right)}^3$$
152	82 83 151	3eqtrd	$$⊢\phi \to {\left(-\left(\frac{\frac{G}{27}}{2}\right)\right)}^2={\left(\frac{\frac{N}{27}}{2}\right)}^2+{\left(-\left(\frac{M}{9}\right)\right)}^3$$
153	17 18 18 20 20	divdiv1d	$$⊢\phi \to \frac{\frac{M}{3}}{3}=\frac{M}{3\cdot 3}$$
154		3t3e9	$$⊢3\cdot 3=9$$
155	154	oveq2i	$$⊢\frac{M}{3\cdot 3}=\frac{M}{9}$$
156	153 155	eqtrdi	$$⊢\phi \to \frac{\frac{M}{3}}{3}=\frac{M}{9}$$
157	156	negeqd	$$⊢\phi \to -\frac{\frac{M}{3}}{3}=-\frac{M}{9}$$
158	21 18 20	divnegd	$$⊢\phi \to -\frac{\frac{M}{3}}{3}=\frac{-\frac{M}{3}}{3}$$
159	157 158	eqtr3d	$$⊢\phi \to -\frac{M}{9}=\frac{-\frac{M}{3}}{3}$$
160		eqidd	$$⊢\phi \to \frac{\frac{N}{27}}{2}=\frac{\frac{N}{27}}{2}$$
161	5 18 11 20	divne0d	$$⊢\phi \to \frac{T}{3}\ne 0$$
162	48 161	negne0d	$$⊢\phi \to -\frac{T}{3}\ne 0$$
163	22 45 47 49 79 80 152 159 160 162	dcubic	$$⊢\phi \to \left({\left(X+\left(\frac{B}{3}\right)\right)}^3+\left(-\frac{M}{3}\right)\left(X+\left(\frac{B}{3}\right)\right)+\left(\frac{N}{27}\right)=0\leftrightarrow \exists r\in ℂ\left(r^3=1\wedge X+\left(\frac{B}{3}\right)=r\left(-\frac{T}{3}\right)-\left(\frac{-\frac{M}{9}}{r\left(-\frac{T}{3}\right)}\right)\right)\right)$$
164		binom3	$$⊢\left(X\in ℂ\wedge \frac{B}{3}\in ℂ\right)\to {\left(X+\left(\frac{B}{3}\right)\right)}^3=X^3+3X^2\left(\frac{B}{3}\right)+3X{\left(\frac{B}{3}\right)}^2+{\left(\frac{B}{3}\right)}^3$$
165	4 46 164	syl2anc	$$⊢\phi \to {\left(X+\left(\frac{B}{3}\right)\right)}^3=X^3+3X^2\left(\frac{B}{3}\right)+3X{\left(\frac{B}{3}\right)}^2+{\left(\frac{B}{3}\right)}^3$$
166	4	sqcld	$$⊢\phi \to X^2\in ℂ$$
167	18 166 46	mul12d	$$⊢\phi \to 3X^2\left(\frac{B}{3}\right)=X^{2}3\left(\frac{B}{3}\right)$$
168	1 18 20	divcan2d	$$⊢\phi \to 3\left(\frac{B}{3}\right)=B$$
169	168	oveq2d	$$⊢\phi \to X^{2}3\left(\frac{B}{3}\right)=X^{2}B$$
170	166 1	mulcomd	$$⊢\phi \to X^{2}B=B{X}^2$$
171	167 169 170	3eqtrd	$$⊢\phi \to 3X^2\left(\frac{B}{3}\right)=B{X}^2$$
172	171	oveq2d	$$⊢\phi \to X^3+3X^2\left(\frac{B}{3}\right)=X^3+B{X}^2$$
173	172	oveq1d	$$⊢\phi \to X^3+3X^2\left(\frac{B}{3}\right)+3X{\left(\frac{B}{3}\right)}^2+{\left(\frac{B}{3}\right)}^3=X^3+B{X}^2+3X{\left(\frac{B}{3}\right)}^2+{\left(\frac{B}{3}\right)}^3$$
174	165 173	eqtrd	$$⊢\phi \to {\left(X+\left(\frac{B}{3}\right)\right)}^3=X^3+B{X}^2+3X{\left(\frac{B}{3}\right)}^2+{\left(\frac{B}{3}\right)}^3$$
175	174	oveq1d	$$⊢\phi \to {\left(X+\left(\frac{B}{3}\right)\right)}^3+\left(-\frac{M}{3}\right)\left(X+\left(\frac{B}{3}\right)\right)+\left(\frac{N}{27}\right)=\left(X^3+B{X}^2\right)+\left(3X{\left(\frac{B}{3}\right)}^2+{\left(\frac{B}{3}\right)}^3\right)+\left(-\frac{M}{3}\right)\left(X+\left(\frac{B}{3}\right)\right)+\left(\frac{N}{27}\right)$$
176		expcl	$$⊢\left(X\in ℂ\wedge 3\in {\mathbb{N}}_0\right)\to X^3\in ℂ$$
177	4 24 176	sylancl	$$⊢\phi \to X^3\in ℂ$$
178	1 166	mulcld	$$⊢\phi \to B{X}^2\in ℂ$$
179	177 178	addcld	$$⊢\phi \to X^3+B{X}^2\in ℂ$$
180	46	sqcld	$$⊢\phi \to {\left(\frac{B}{3}\right)}^2\in ℂ$$
181	4 180	mulcld	$$⊢\phi \to X{\left(\frac{B}{3}\right)}^2\in ℂ$$
182	18 181	mulcld	$$⊢\phi \to 3X{\left(\frac{B}{3}\right)}^2\in ℂ$$
183		expcl	$$⊢\left(\frac{B}{3}\in ℂ\wedge 3\in {\mathbb{N}}_0\right)\to {\left(\frac{B}{3}\right)}^3\in ℂ$$
184	46 24 183	sylancl	$$⊢\phi \to {\left(\frac{B}{3}\right)}^3\in ℂ$$
185	182 184	addcld	$$⊢\phi \to 3X{\left(\frac{B}{3}\right)}^2+{\left(\frac{B}{3}\right)}^3\in ℂ$$
186	22 47	mulcld	$$⊢\phi \to \left(-\frac{M}{3}\right)\left(X+\left(\frac{B}{3}\right)\right)\in ℂ$$
187	186 45	addcld	$$⊢\phi \to \left(-\frac{M}{3}\right)\left(X+\left(\frac{B}{3}\right)\right)+\left(\frac{N}{27}\right)\in ℂ$$
188	179 185 187	addassd	$$⊢\phi \to \left(X^3+B{X}^2\right)+\left(3X{\left(\frac{B}{3}\right)}^2+{\left(\frac{B}{3}\right)}^3\right)+\left(-\frac{M}{3}\right)\left(X+\left(\frac{B}{3}\right)\right)+\left(\frac{N}{27}\right)=X^3+B{X}^2+\left(3X{\left(\frac{B}{3}\right)}^2+{\left(\frac{B}{3}\right)}^3\right)+\left(\left(-\frac{M}{3}\right)\left(X+\left(\frac{B}{3}\right)\right)+\left(\frac{N}{27}\right)\right)$$
189	22 4 46	adddid	$$⊢\phi \to \left(-\frac{M}{3}\right)\left(X+\left(\frac{B}{3}\right)\right)=\left(-\frac{M}{3}\right)X+\left(-\frac{M}{3}\right)\left(\frac{B}{3}\right)$$
190	189	oveq1d	$$⊢\phi \to \left(-\frac{M}{3}\right)\left(X+\left(\frac{B}{3}\right)\right)+\left(\frac{N}{27}\right)=\left(-\frac{M}{3}\right)X+\left(-\frac{M}{3}\right)\left(\frac{B}{3}\right)+\left(\frac{N}{27}\right)$$
191	22 4	mulcld	$$⊢\phi \to \left(-\frac{M}{3}\right)X\in ℂ$$
192	22 46	mulcld	$$⊢\phi \to \left(-\frac{M}{3}\right)\left(\frac{B}{3}\right)\in ℂ$$
193	191 192 45	addassd	$$⊢\phi \to \left(-\frac{M}{3}\right)X+\left(-\frac{M}{3}\right)\left(\frac{B}{3}\right)+\left(\frac{N}{27}\right)=\left(-\frac{M}{3}\right)X+\left(-\frac{M}{3}\right)\left(\frac{B}{3}\right)+\left(\frac{N}{27}\right)$$
194	9	oveq1d	$$⊢\phi \to \frac{M}{3}=\frac{B^2-3C}{3}$$
195	12 15 18 20	divsubdird	$$⊢\phi \to \frac{B^2-3C}{3}=\left(\frac{B^2}{3}\right)-\left(\frac{3C}{3}\right)$$
196	2 18 20	divcan3d	$$⊢\phi \to \frac{3C}{3}=C$$
197	196	oveq2d	$$⊢\phi \to \left(\frac{B^2}{3}\right)-\left(\frac{3C}{3}\right)=\left(\frac{B^2}{3}\right)-C$$
198	194 195 197	3eqtrd	$$⊢\phi \to \frac{M}{3}=\left(\frac{B^2}{3}\right)-C$$
199	198	negeqd	$$⊢\phi \to -\frac{M}{3}=-\left(\left(\frac{B^2}{3}\right)-C\right)$$
200	12 18 20	divcld	$$⊢\phi \to \frac{B^2}{3}\in ℂ$$
201	200 2	negsubdi2d	$$⊢\phi \to -\left(\left(\frac{B^2}{3}\right)-C\right)=C-\left(\frac{B^2}{3}\right)$$
202	199 201	eqtrd	$$⊢\phi \to -\frac{M}{3}=C-\left(\frac{B^2}{3}\right)$$
203	202	oveq1d	$$⊢\phi \to \left(-\frac{M}{3}\right)X=\left(C-\left(\frac{B^2}{3}\right)\right)X$$
204	2 200 4	subdird	$$⊢\phi \to \left(C-\left(\frac{B^2}{3}\right)\right)X=CX-\left(\frac{B^2}{3}\right)X$$
205	200 4	mulcomd	$$⊢\phi \to \left(\frac{B^2}{3}\right)X=X\left(\frac{B^2}{3}\right)$$
206	13	sqvali	$$⊢3^2=3\cdot 3$$
207	206	oveq2i	$$⊢\frac{B^2}{3^2}=\frac{B^2}{3\cdot 3}$$
208	1 18 20	sqdivd	$$⊢\phi \to {\left(\frac{B}{3}\right)}^2=\frac{B^2}{3^2}$$
209	12 18 18 20 20	divdiv1d	$$⊢\phi \to \frac{\frac{B^2}{3}}{3}=\frac{B^2}{3\cdot 3}$$
210	207 208 209	3eqtr4a	$$⊢\phi \to {\left(\frac{B}{3}\right)}^2=\frac{\frac{B^2}{3}}{3}$$
211	210	oveq2d	$$⊢\phi \to 3{\left(\frac{B}{3}\right)}^2=3\left(\frac{\frac{B^2}{3}}{3}\right)$$
212	200 18 20	divcan2d	$$⊢\phi \to 3\left(\frac{\frac{B^2}{3}}{3}\right)=\frac{B^2}{3}$$
213	211 212	eqtrd	$$⊢\phi \to 3{\left(\frac{B}{3}\right)}^2=\frac{B^2}{3}$$
214	213	oveq2d	$$⊢\phi \to X3{\left(\frac{B}{3}\right)}^2=X\left(\frac{B^2}{3}\right)$$
215	4 18 180	mul12d	$$⊢\phi \to X3{\left(\frac{B}{3}\right)}^2=3X{\left(\frac{B}{3}\right)}^2$$
216	205 214 215	3eqtr2d	$$⊢\phi \to \left(\frac{B^2}{3}\right)X=3X{\left(\frac{B}{3}\right)}^2$$
217	216	oveq2d	$$⊢\phi \to CX-\left(\frac{B^2}{3}\right)X=CX-3X{\left(\frac{B}{3}\right)}^2$$
218	203 204 217	3eqtrd	$$⊢\phi \to \left(-\frac{M}{3}\right)X=CX-3X{\left(\frac{B}{3}\right)}^2$$
219	202	oveq1d	$$⊢\phi \to \left(-\frac{M}{3}\right)\left(\frac{B}{3}\right)=\left(C-\left(\frac{B^2}{3}\right)\right)\left(\frac{B}{3}\right)$$
220	2 200 46	subdird	$$⊢\phi \to \left(C-\left(\frac{B^2}{3}\right)\right)\left(\frac{B}{3}\right)=C\left(\frac{B}{3}\right)-\left(\frac{B^2}{3}\right)\left(\frac{B}{3}\right)$$
221	2 1 18 20	divassd	$$⊢\phi \to \frac{CB}{3}=C\left(\frac{B}{3}\right)$$
222	2 1	mulcomd	$$⊢\phi \to CB=BC$$
223	222	oveq1d	$$⊢\phi \to \frac{CB}{3}=\frac{BC}{3}$$
224	221 223	eqtr3d	$$⊢\phi \to C\left(\frac{B}{3}\right)=\frac{BC}{3}$$
225	12 18 1 18 20 20	divmuldivd	$$⊢\phi \to \left(\frac{B^2}{3}\right)\left(\frac{B}{3}\right)=\frac{B^{2}B}{3\cdot 3}$$
226		df-3	$$⊢3=2+1$$
227	226	oveq2i	$$⊢B^3=B^{2+1}$$
228		expp1	$$⊢\left(B\in ℂ\wedge 2\in {\mathbb{N}}_0\right)\to B^{2+1}=B^{2}B$$
229	1 34 228	sylancl	$$⊢\phi \to B^{2+1}=B^{2}B$$
230	227 229	eqtr2id	$$⊢\phi \to B^{2}B=B^3$$
231	154	a1i	$$⊢\phi \to 3\cdot 3=9$$
232	230 231	oveq12d	$$⊢\phi \to \frac{B^{2}B}{3\cdot 3}=\frac{B^3}{9}$$
233	225 232	eqtrd	$$⊢\phi \to \left(\frac{B^2}{3}\right)\left(\frac{B}{3}\right)=\frac{B^3}{9}$$
234	224 233	oveq12d	$$⊢\phi \to C\left(\frac{B}{3}\right)-\left(\frac{B^2}{3}\right)\left(\frac{B}{3}\right)=\left(\frac{BC}{3}\right)-\left(\frac{B^3}{9}\right)$$
235	219 220 234	3eqtrd	$$⊢\phi \to \left(-\frac{M}{3}\right)\left(\frac{B}{3}\right)=\left(\frac{BC}{3}\right)-\left(\frac{B^3}{9}\right)$$
236	10	oveq1d	$$⊢\phi \to \frac{N}{27}=\frac{2B^3-9BC+27D}{27}$$
237	33 39 42 44	divdird	$$⊢\phi \to \frac{2B^3-9BC+27D}{27}=\left(\frac{2B^3-9BC}{27}\right)+\left(\frac{27D}{27}\right)$$
238	28 32 42 44	divsubdird	$$⊢\phi \to \frac{2B^3-9BC}{27}=\left(\frac{2B^3}{27}\right)-\left(\frac{9BC}{27}\right)$$
239		9t3e27	$$⊢9\cdot 3=27$$
240	239	oveq2i	$$⊢\frac{9BC}{9\cdot 3}=\frac{9BC}{27}$$
241	30 18 98 20 101	divcan5d	$$⊢\phi \to \frac{9BC}{9\cdot 3}=\frac{BC}{3}$$
242	240 241	eqtr3id	$$⊢\phi \to \frac{9BC}{27}=\frac{BC}{3}$$
243	242	oveq2d	$$⊢\phi \to \left(\frac{2B^3}{27}\right)-\left(\frac{9BC}{27}\right)=\left(\frac{2B^3}{27}\right)-\left(\frac{BC}{3}\right)$$
244	238 243	eqtrd	$$⊢\phi \to \frac{2B^3-9BC}{27}=\left(\frac{2B^3}{27}\right)-\left(\frac{BC}{3}\right)$$
245	3 42 44	divcan3d	$$⊢\phi \to \frac{27D}{27}=D$$
246	244 245	oveq12d	$$⊢\phi \to \left(\frac{2B^3-9BC}{27}\right)+\left(\frac{27D}{27}\right)=\left(\frac{2B^3}{27}\right)-\left(\frac{BC}{3}\right)+D$$
247	236 237 246	3eqtrd	$$⊢\phi \to \frac{N}{27}=\left(\frac{2B^3}{27}\right)-\left(\frac{BC}{3}\right)+D$$
248	235 247	oveq12d	$$⊢\phi \to \left(-\frac{M}{3}\right)\left(\frac{B}{3}\right)+\left(\frac{N}{27}\right)=\left(\left(\frac{BC}{3}\right)-\left(\frac{B^3}{9}\right)\right)+\left(\left(\frac{2B^3}{27}\right)-\left(\frac{BC}{3}\right)\right)+D$$
249	26 98 101	divcld	$$⊢\phi \to \frac{B^3}{9}\in ℂ$$
250	28 42 44	divcld	$$⊢\phi \to \frac{2B^3}{27}\in ℂ$$
251	249 250	negsubdi2d	$$⊢\phi \to -\left(\left(\frac{B^3}{9}\right)-\left(\frac{2B^3}{27}\right)\right)=\left(\frac{2B^3}{27}\right)-\left(\frac{B^3}{9}\right)$$
252	1 18 20 56	expdivd	$$⊢\phi \to {\left(\frac{B}{3}\right)}^3=\frac{B^3}{3^3}$$
253	58	oveq2i	$$⊢\frac{B^3}{3^3}=\frac{B^3}{27}$$
254		ax-1cn	$$⊢1\in ℂ$$
255		2p1e3	$$⊢2+1=3$$
256	13 23 254 255	subaddrii	$$⊢3-2=1$$
257	256	oveq1i	$$⊢\left(3-2\right)B^3=1B^3$$
258	26	mulid2d	$$⊢\phi \to 1B^3=B^3$$
259	257 258	eqtrid	$$⊢\phi \to \left(3-2\right)B^3=B^3$$
260	18 62 26	subdird	$$⊢\phi \to \left(3-2\right)B^3=3B^3-2B^3$$
261	259 260	eqtr3d	$$⊢\phi \to B^3=3B^3-2B^3$$
262	261	oveq1d	$$⊢\phi \to \frac{B^3}{27}=\frac{3B^3-2B^3}{27}$$
263		mulcl	$$⊢\left(3\in ℂ\wedge B^3\in ℂ\right)\to 3B^3\in ℂ$$
264	13 26 263	sylancr	$$⊢\phi \to 3B^3\in ℂ$$
265	264 28 42 44	divsubdird	$$⊢\phi \to \frac{3B^3-2B^3}{27}=\left(\frac{3B^3}{27}\right)-\left(\frac{2B^3}{27}\right)$$
266	262 265	eqtrd	$$⊢\phi \to \frac{B^3}{27}=\left(\frac{3B^3}{27}\right)-\left(\frac{2B^3}{27}\right)$$
267	253 266	eqtrid	$$⊢\phi \to \frac{B^3}{3^3}=\left(\frac{3B^3}{27}\right)-\left(\frac{2B^3}{27}\right)$$
268	29 13 239	mulcomli	$$⊢3\cdot 9=27$$
269	268	oveq2i	$$⊢\frac{3B^3}{3\cdot 9}=\frac{3B^3}{27}$$
270	26 98 18 101 20	divcan5d	$$⊢\phi \to \frac{3B^3}{3\cdot 9}=\frac{B^3}{9}$$
271	269 270	eqtr3id	$$⊢\phi \to \frac{3B^3}{27}=\frac{B^3}{9}$$
272	271	oveq1d	$$⊢\phi \to \left(\frac{3B^3}{27}\right)-\left(\frac{2B^3}{27}\right)=\left(\frac{B^3}{9}\right)-\left(\frac{2B^3}{27}\right)$$
273	252 267 272	3eqtrd	$$⊢\phi \to {\left(\frac{B}{3}\right)}^3=\left(\frac{B^3}{9}\right)-\left(\frac{2B^3}{27}\right)$$
274	273	negeqd	$$⊢\phi \to -{\left(\frac{B}{3}\right)}^3=-\left(\left(\frac{B^3}{9}\right)-\left(\frac{2B^3}{27}\right)\right)$$
275	30 18 20	divcld	$$⊢\phi \to \frac{BC}{3}\in ℂ$$
276	275 249 250	npncan3d	$$⊢\phi \to \left(\left(\frac{BC}{3}\right)-\left(\frac{B^3}{9}\right)\right)+\left(\frac{2B^3}{27}\right)-\left(\frac{BC}{3}\right)=\left(\frac{2B^3}{27}\right)-\left(\frac{B^3}{9}\right)$$
277	251 274 276	3eqtr4d	$$⊢\phi \to -{\left(\frac{B}{3}\right)}^3=\left(\left(\frac{BC}{3}\right)-\left(\frac{B^3}{9}\right)\right)+\left(\frac{2B^3}{27}\right)-\left(\frac{BC}{3}\right)$$
278	277	oveq1d	$$⊢\phi \to -{\left(\frac{B}{3}\right)}^3+D=\left(\left(\frac{BC}{3}\right)-\left(\frac{B^3}{9}\right)\right)+\left(\left(\frac{2B^3}{27}\right)-\left(\frac{BC}{3}\right)\right)+D$$
279	184	negcld	$$⊢\phi \to -{\left(\frac{B}{3}\right)}^3\in ℂ$$
280	279 3	addcomd	$$⊢\phi \to -{\left(\frac{B}{3}\right)}^3+D=D+\left(-{\left(\frac{B}{3}\right)}^3\right)$$
281	235 192	eqeltrrd	$$⊢\phi \to \left(\frac{BC}{3}\right)-\left(\frac{B^3}{9}\right)\in ℂ$$
282	250 275	subcld	$$⊢\phi \to \left(\frac{2B^3}{27}\right)-\left(\frac{BC}{3}\right)\in ℂ$$
283	281 282 3	addassd	$$⊢\phi \to \left(\left(\frac{BC}{3}\right)-\left(\frac{B^3}{9}\right)\right)+\left(\left(\frac{2B^3}{27}\right)-\left(\frac{BC}{3}\right)\right)+D=\left(\left(\frac{BC}{3}\right)-\left(\frac{B^3}{9}\right)\right)+\left(\left(\frac{2B^3}{27}\right)-\left(\frac{BC}{3}\right)\right)+D$$
284	278 280 283	3eqtr3d	$$⊢\phi \to D+\left(-{\left(\frac{B}{3}\right)}^3\right)=\left(\left(\frac{BC}{3}\right)-\left(\frac{B^3}{9}\right)\right)+\left(\left(\frac{2B^3}{27}\right)-\left(\frac{BC}{3}\right)\right)+D$$
285	3 184	negsubd	$$⊢\phi \to D+\left(-{\left(\frac{B}{3}\right)}^3\right)=D-{\left(\frac{B}{3}\right)}^3$$
286	248 284 285	3eqtr2d	$$⊢\phi \to \left(-\frac{M}{3}\right)\left(\frac{B}{3}\right)+\left(\frac{N}{27}\right)=D-{\left(\frac{B}{3}\right)}^3$$
287	218 286	oveq12d	$$⊢\phi \to \left(-\frac{M}{3}\right)X+\left(-\frac{M}{3}\right)\left(\frac{B}{3}\right)+\left(\frac{N}{27}\right)=\left(CX-3X{\left(\frac{B}{3}\right)}^2\right)+D-{\left(\frac{B}{3}\right)}^3$$
288	190 193 287	3eqtrd	$$⊢\phi \to \left(-\frac{M}{3}\right)\left(X+\left(\frac{B}{3}\right)\right)+\left(\frac{N}{27}\right)=\left(CX-3X{\left(\frac{B}{3}\right)}^2\right)+D-{\left(\frac{B}{3}\right)}^3$$
289	2 4	mulcld	$$⊢\phi \to CX\in ℂ$$
290	289 3 182 184	addsub4d	$$⊢\phi \to CX+D-\left(3X{\left(\frac{B}{3}\right)}^2+{\left(\frac{B}{3}\right)}^3\right)=\left(CX-3X{\left(\frac{B}{3}\right)}^2\right)+D-{\left(\frac{B}{3}\right)}^3$$
291	288 290	eqtr4d	$$⊢\phi \to \left(-\frac{M}{3}\right)\left(X+\left(\frac{B}{3}\right)\right)+\left(\frac{N}{27}\right)=CX+D-\left(3X{\left(\frac{B}{3}\right)}^2+{\left(\frac{B}{3}\right)}^3\right)$$
292	291	oveq2d	$$⊢\phi \to 3X{\left(\frac{B}{3}\right)}^2+{\left(\frac{B}{3}\right)}^3+\left(-\frac{M}{3}\right)\left(X+\left(\frac{B}{3}\right)\right)+\left(\frac{N}{27}\right)=3X{\left(\frac{B}{3}\right)}^2+{\left(\frac{B}{3}\right)}^3+\left(CX+D-\left(3X{\left(\frac{B}{3}\right)}^2+{\left(\frac{B}{3}\right)}^3\right)\right)$$
293	289 3	addcld	$$⊢\phi \to CX+D\in ℂ$$
294	185 293	pncan3d	$$⊢\phi \to 3X{\left(\frac{B}{3}\right)}^2+{\left(\frac{B}{3}\right)}^3+\left(CX+D-\left(3X{\left(\frac{B}{3}\right)}^2+{\left(\frac{B}{3}\right)}^3\right)\right)=CX+D$$
295	292 294	eqtrd	$$⊢\phi \to 3X{\left(\frac{B}{3}\right)}^2+{\left(\frac{B}{3}\right)}^3+\left(-\frac{M}{3}\right)\left(X+\left(\frac{B}{3}\right)\right)+\left(\frac{N}{27}\right)=CX+D$$
296	295	oveq2d	$$⊢\phi \to X^3+B{X}^2+\left(3X{\left(\frac{B}{3}\right)}^2+{\left(\frac{B}{3}\right)}^3\right)+\left(\left(-\frac{M}{3}\right)\left(X+\left(\frac{B}{3}\right)\right)+\left(\frac{N}{27}\right)\right)=X^3+B{X}^2+CX+D$$
297	175 188 296	3eqtrd	$$⊢\phi \to {\left(X+\left(\frac{B}{3}\right)\right)}^3+\left(-\frac{M}{3}\right)\left(X+\left(\frac{B}{3}\right)\right)+\left(\frac{N}{27}\right)=X^3+B{X}^2+CX+D$$
298	297	eqeq1d	$$⊢\phi \to \left({\left(X+\left(\frac{B}{3}\right)\right)}^3+\left(-\frac{M}{3}\right)\left(X+\left(\frac{B}{3}\right)\right)+\left(\frac{N}{27}\right)=0\leftrightarrow X^3+B{X}^2+CX+D=0\right)$$
299		oveq1	$$⊢r=0\to r^3=0^3$$
300		0exp	$$⊢3\in \mathbb{N}\to 0^3=0$$
301	50 300	ax-mp	$$⊢0^3=0$$
302	299 301	eqtrdi	$$⊢r=0\to r^3=0$$
303		0ne1	$$⊢0\ne 1$$
304	303	a1i	$$⊢r=0\to 0\ne 1$$
305	302 304	eqnetrd	$$⊢r=0\to r^3\ne 1$$
306	305	necon2i	$$⊢r^3=1\to r\ne 0$$
307		eqcom	$$⊢X=-\frac{B+rT+\left(\frac{M}{rT}\right)}{3}\leftrightarrow -\frac{B+rT+\left(\frac{M}{rT}\right)}{3}=X$$
308	1	adantr	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to B\in ℂ$$
309		simprl	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to r\in ℂ$$
310	5	adantr	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to T\in ℂ$$
311	309 310	mulcld	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to rT\in ℂ$$
312	17	adantr	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to M\in ℂ$$
313		simprr	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to r\ne 0$$
314	11	adantr	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to T\ne 0$$
315	309 310 313 314	mulne0d	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to rT\ne 0$$
316	312 311 315	divcld	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to \frac{M}{rT}\in ℂ$$
317	311 316	addcld	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to rT+\left(\frac{M}{rT}\right)\in ℂ$$
318	13	a1i	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to 3\in ℂ$$
319	19	a1i	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to 3\ne 0$$
320	308 317 318 319	divdird	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to \frac{B+rT+\left(\frac{M}{rT}\right)}{3}=\left(\frac{B}{3}\right)+\left(\frac{rT+\left(\frac{M}{rT}\right)}{3}\right)$$
321	308 311 316	addassd	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to B+rT+\left(\frac{M}{rT}\right)=B+rT+\left(\frac{M}{rT}\right)$$
322	321	oveq1d	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to \frac{B+rT+\left(\frac{M}{rT}\right)}{3}=\frac{B+rT+\left(\frac{M}{rT}\right)}{3}$$
323	46	adantr	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to \frac{B}{3}\in ℂ$$
324	317 318 319	divcld	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to \frac{rT+\left(\frac{M}{rT}\right)}{3}\in ℂ$$
325	323 324	subnegd	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to \left(\frac{B}{3}\right)-\left(-\frac{rT+\left(\frac{M}{rT}\right)}{3}\right)=\left(\frac{B}{3}\right)+\left(\frac{rT+\left(\frac{M}{rT}\right)}{3}\right)$$
326	320 322 325	3eqtr4d	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to \frac{B+rT+\left(\frac{M}{rT}\right)}{3}=\left(\frac{B}{3}\right)-\left(-\frac{rT+\left(\frac{M}{rT}\right)}{3}\right)$$
327	326	negeqd	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to -\frac{B+rT+\left(\frac{M}{rT}\right)}{3}=-\left(\left(\frac{B}{3}\right)-\left(-\frac{rT+\left(\frac{M}{rT}\right)}{3}\right)\right)$$
328	324	negcld	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to -\frac{rT+\left(\frac{M}{rT}\right)}{3}\in ℂ$$
329	323 328	negsubdi2d	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to -\left(\left(\frac{B}{3}\right)-\left(-\frac{rT+\left(\frac{M}{rT}\right)}{3}\right)\right)=-\left(\frac{rT+\left(\frac{M}{rT}\right)}{3}\right)-\left(\frac{B}{3}\right)$$
330	327 329	eqtrd	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to -\frac{B+rT+\left(\frac{M}{rT}\right)}{3}=-\left(\frac{rT+\left(\frac{M}{rT}\right)}{3}\right)-\left(\frac{B}{3}\right)$$
331	330	eqeq1d	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to \left(-\frac{B+rT+\left(\frac{M}{rT}\right)}{3}=X\leftrightarrow -\left(\frac{rT+\left(\frac{M}{rT}\right)}{3}\right)-\left(\frac{B}{3}\right)=X\right)$$
332	307 331	syl5bb	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to \left(X=-\frac{B+rT+\left(\frac{M}{rT}\right)}{3}\leftrightarrow -\left(\frac{rT+\left(\frac{M}{rT}\right)}{3}\right)-\left(\frac{B}{3}\right)=X\right)$$
333	4	adantr	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to X\in ℂ$$
334	328 323 333	subadd2d	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to \left(-\left(\frac{rT+\left(\frac{M}{rT}\right)}{3}\right)-\left(\frac{B}{3}\right)=X\leftrightarrow X+\left(\frac{B}{3}\right)=-\frac{rT+\left(\frac{M}{rT}\right)}{3}\right)$$
335	311 316 318 319	divdird	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to \frac{rT+\left(\frac{M}{rT}\right)}{3}=\left(\frac{rT}{3}\right)+\left(\frac{\frac{M}{rT}}{3}\right)$$
336	335	negeqd	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to -\frac{rT+\left(\frac{M}{rT}\right)}{3}=-\left(\left(\frac{rT}{3}\right)+\left(\frac{\frac{M}{rT}}{3}\right)\right)$$
337	311 318 319	divcld	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to \frac{rT}{3}\in ℂ$$
338	316 318 319	divcld	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to \frac{\frac{M}{rT}}{3}\in ℂ$$
339	337 338	negdi2d	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to -\left(\left(\frac{rT}{3}\right)+\left(\frac{\frac{M}{rT}}{3}\right)\right)=-\left(\frac{rT}{3}\right)-\left(\frac{\frac{M}{rT}}{3}\right)$$
340	309 310 318 319	divassd	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to \frac{rT}{3}=r\left(\frac{T}{3}\right)$$
341	340	negeqd	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to -\frac{rT}{3}=-r\left(\frac{T}{3}\right)$$
342	48	adantr	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to \frac{T}{3}\in ℂ$$
343	309 342	mulneg2d	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to r\left(-\frac{T}{3}\right)=-r\left(\frac{T}{3}\right)$$
344	341 343	eqtr4d	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to -\frac{rT}{3}=r\left(-\frac{T}{3}\right)$$
345	312 311 318 315 319	divdiv32d	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to \frac{\frac{M}{rT}}{3}=\frac{\frac{M}{3}}{rT}$$
346	21	adantr	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to \frac{M}{3}\in ℂ$$
347	346 311 318 315 319	divcan7d	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to \frac{\frac{\frac{M}{3}}{3}}{\frac{rT}{3}}=\frac{\frac{M}{3}}{rT}$$
348	156	oveq1d	$$⊢\phi \to \frac{\frac{\frac{M}{3}}{3}}{\frac{rT}{3}}=\frac{\frac{M}{9}}{\frac{rT}{3}}$$
349	348	adantr	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to \frac{\frac{\frac{M}{3}}{3}}{\frac{rT}{3}}=\frac{\frac{M}{9}}{\frac{rT}{3}}$$
350	345 347 349	3eqtr2d	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to \frac{\frac{M}{rT}}{3}=\frac{\frac{M}{9}}{\frac{rT}{3}}$$
351	121	adantr	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to \frac{M}{9}\in ℂ$$
352	311 318 315 319	divne0d	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to \frac{rT}{3}\ne 0$$
353	351 337 352	div2negd	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to \frac{-\frac{M}{9}}{-\frac{rT}{3}}=\frac{\frac{M}{9}}{\frac{rT}{3}}$$
354	344	oveq2d	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to \frac{-\frac{M}{9}}{-\frac{rT}{3}}=\frac{-\frac{M}{9}}{r\left(-\frac{T}{3}\right)}$$
355	350 353 354	3eqtr2d	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to \frac{\frac{M}{rT}}{3}=\frac{-\frac{M}{9}}{r\left(-\frac{T}{3}\right)}$$
356	344 355	oveq12d	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to -\left(\frac{rT}{3}\right)-\left(\frac{\frac{M}{rT}}{3}\right)=r\left(-\frac{T}{3}\right)-\left(\frac{-\frac{M}{9}}{r\left(-\frac{T}{3}\right)}\right)$$
357	336 339 356	3eqtrd	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to -\frac{rT+\left(\frac{M}{rT}\right)}{3}=r\left(-\frac{T}{3}\right)-\left(\frac{-\frac{M}{9}}{r\left(-\frac{T}{3}\right)}\right)$$
358	357	eqeq2d	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to \left(X+\left(\frac{B}{3}\right)=-\frac{rT+\left(\frac{M}{rT}\right)}{3}\leftrightarrow X+\left(\frac{B}{3}\right)=r\left(-\frac{T}{3}\right)-\left(\frac{-\frac{M}{9}}{r\left(-\frac{T}{3}\right)}\right)\right)$$
359	332 334 358	3bitrrd	$$⊢\left(\phi \wedge \left(r\in ℂ\wedge r\ne 0\right)\right)\to \left(X+\left(\frac{B}{3}\right)=r\left(-\frac{T}{3}\right)-\left(\frac{-\frac{M}{9}}{r\left(-\frac{T}{3}\right)}\right)\leftrightarrow X=-\frac{B+rT+\left(\frac{M}{rT}\right)}{3}\right)$$
360	359	anassrs	$$⊢\left(\left(\phi \wedge r\in ℂ\right)\wedge r\ne 0\right)\to \left(X+\left(\frac{B}{3}\right)=r\left(-\frac{T}{3}\right)-\left(\frac{-\frac{M}{9}}{r\left(-\frac{T}{3}\right)}\right)\leftrightarrow X=-\frac{B+rT+\left(\frac{M}{rT}\right)}{3}\right)$$
361	306 360	sylan2	$$⊢\left(\left(\phi \wedge r\in ℂ\right)\wedge r^3=1\right)\to \left(X+\left(\frac{B}{3}\right)=r\left(-\frac{T}{3}\right)-\left(\frac{-\frac{M}{9}}{r\left(-\frac{T}{3}\right)}\right)\leftrightarrow X=-\frac{B+rT+\left(\frac{M}{rT}\right)}{3}\right)$$
362	361	pm5.32da	$$⊢\left(\phi \wedge r\in ℂ\right)\to \left(\left(r^3=1\wedge X+\left(\frac{B}{3}\right)=r\left(-\frac{T}{3}\right)-\left(\frac{-\frac{M}{9}}{r\left(-\frac{T}{3}\right)}\right)\right)\leftrightarrow \left(r^3=1\wedge X=-\frac{B+rT+\left(\frac{M}{rT}\right)}{3}\right)\right)$$
363	362	rexbidva	$$⊢\phi \to \left(\exists r\in ℂ\left(r^3=1\wedge X+\left(\frac{B}{3}\right)=r\left(-\frac{T}{3}\right)-\left(\frac{-\frac{M}{9}}{r\left(-\frac{T}{3}\right)}\right)\right)\leftrightarrow \exists r\in ℂ\left(r^3=1\wedge X=-\frac{B+rT+\left(\frac{M}{rT}\right)}{3}\right)\right)$$
364	163 298 363	3bitr3d	$$⊢\phi \to \left(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)}{3}\right)\right)$$