Theorem dquart

Description: Solve a depressed quartic equation. To eliminate S , which is the square root of a solution M to the resolvent cubic equation, apply cubic or one of its variants. (Contributed by Mario Carneiro, 6-May-2015)

	Ref	Expression
Hypotheses	dquart.b	$$⊢\phi \to B\in ℂ$$
	dquart.c	$$⊢\phi \to C\in ℂ$$
	dquart.x	$$⊢\phi \to X\in ℂ$$
	dquart.s	$$⊢\phi \to S\in ℂ$$
	dquart.m	$$⊢\phi \to M={2S}^2$$
	dquart.m0	$$⊢\phi \to M\ne 0$$
	dquart.i	$$⊢\phi \to I\in ℂ$$
	dquart.i2	$$⊢\phi \to I^2=\left(-S^2\right)-\left(\frac{B}{2}\right)+\left(\frac{\frac{C}{4}}{S}\right)$$
	dquart.d	$$⊢\phi \to D\in ℂ$$
	dquart.3	$$⊢\phi \to M^3+2B{M}^2+\left(B^2-4D\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}+\left(-C^2\right)=0$$
	dquart.j	$$⊢\phi \to J\in ℂ$$
	dquart.j2	$$⊢\phi \to J^2=\left(-S^2\right)-\left(\frac{B}{2}\right)-\left(\frac{\frac{C}{4}}{S}\right)$$
Assertion	dquart	$$⊢\phi \to \left(X^4+B{X}^2+CX+D=0\leftrightarrow \left(\left(X=-S+I\vee X=-S-I\right)\vee \left(X=S+J\vee X=S-J\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		dquart.b	$$⊢\phi \to B\in ℂ$$
2		dquart.c	$$⊢\phi \to C\in ℂ$$
3		dquart.x	$$⊢\phi \to X\in ℂ$$
4		dquart.s	$$⊢\phi \to S\in ℂ$$
5		dquart.m	$$⊢\phi \to M={2S}^2$$
6		dquart.m0	$$⊢\phi \to M\ne 0$$
7		dquart.i	$$⊢\phi \to I\in ℂ$$
8		dquart.i2	$$⊢\phi \to I^2=\left(-S^2\right)-\left(\frac{B}{2}\right)+\left(\frac{\frac{C}{4}}{S}\right)$$
9		dquart.d	$$⊢\phi \to D\in ℂ$$
10		dquart.3	$$⊢\phi \to M^3+2B{M}^2+\left(B^2-4D\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}+\left(-C^2\right)=0$$
11		dquart.j	$$⊢\phi \to J\in ℂ$$
12		dquart.j2	$$⊢\phi \to J^2=\left(-S^2\right)-\left(\frac{B}{2}\right)-\left(\frac{\frac{C}{4}}{S}\right)$$
13	3	sqcld	$$⊢\phi \to X^2\in ℂ$$
14		2cn	$$⊢2\in ℂ$$
15		mulcl	$$⊢\left(2\in ℂ\wedge S\in ℂ\right)\to 2S\in ℂ$$
16	14 4 15	sylancr	$$⊢\phi \to 2S\in ℂ$$
17	16	sqcld	$$⊢\phi \to {2S}^2\in ℂ$$
18	5 17	eqeltrd	$$⊢\phi \to M\in ℂ$$
19	18 1	addcld	$$⊢\phi \to M+B\in ℂ$$
20	19	halfcld	$$⊢\phi \to \frac{M+B}{2}\in ℂ$$
21		binom2	$$⊢\left(X^2\in ℂ\wedge \frac{M+B}{2}\in ℂ\right)\to {\left(X^2+\left(\frac{M+B}{2}\right)\right)}^2={\left(X^2\right)}^2+2X^2\left(\frac{M+B}{2}\right)+{\left(\frac{M+B}{2}\right)}^2$$
22	13 20 21	syl2anc	$$⊢\phi \to {\left(X^2+\left(\frac{M+B}{2}\right)\right)}^2={\left(X^2\right)}^2+2X^2\left(\frac{M+B}{2}\right)+{\left(\frac{M+B}{2}\right)}^2$$
23		2nn0	$$⊢2\in {\mathbb{N}}_0$$
24	23	a1i	$$⊢\phi \to 2\in {\mathbb{N}}_0$$
25	3 24 24	expmuld	$$⊢\phi \to X^{2\cdot 2}={\left(X^2\right)}^2$$
26		2t2e4	$$⊢2\cdot 2=4$$
27	26	oveq2i	$$⊢X^{2\cdot 2}=X^4$$
28	25 27	eqtr3di	$$⊢\phi \to {\left(X^2\right)}^2=X^4$$
29	14	a1i	$$⊢\phi \to 2\in ℂ$$
30	29 13 20	mul12d	$$⊢\phi \to 2X^2\left(\frac{M+B}{2}\right)=X^{2}2\left(\frac{M+B}{2}\right)$$
31		2ne0	$$⊢2\ne 0$$
32	31	a1i	$$⊢\phi \to 2\ne 0$$
33	19 29 32	divcan2d	$$⊢\phi \to 2\left(\frac{M+B}{2}\right)=M+B$$
34	33	oveq2d	$$⊢\phi \to X^{2}2\left(\frac{M+B}{2}\right)=X^2\left(M+B\right)$$
35	13 19	mulcomd	$$⊢\phi \to X^2\left(M+B\right)=\left(M+B\right)X^2$$
36	34 35	eqtrd	$$⊢\phi \to X^{2}2\left(\frac{M+B}{2}\right)=\left(M+B\right)X^2$$
37	18 1 13	adddird	$$⊢\phi \to \left(M+B\right)X^2=M{X}^2+B{X}^2$$
38	30 36 37	3eqtrd	$$⊢\phi \to 2X^2\left(\frac{M+B}{2}\right)=M{X}^2+B{X}^2$$
39	28 38	oveq12d	$$⊢\phi \to {\left(X^2\right)}^2+2X^2\left(\frac{M+B}{2}\right)=X^4+M{X}^2+B{X}^2$$
40		4nn0	$$⊢4\in {\mathbb{N}}_0$$
41		expcl	$$⊢\left(X\in ℂ\wedge 4\in {\mathbb{N}}_0\right)\to X^4\in ℂ$$
42	3 40 41	sylancl	$$⊢\phi \to X^4\in ℂ$$
43	18 13	mulcld	$$⊢\phi \to M{X}^2\in ℂ$$
44	1 13	mulcld	$$⊢\phi \to B{X}^2\in ℂ$$
45	42 43 44	add12d	$$⊢\phi \to X^4+M{X}^2+B{X}^2=M{X}^2+X^4+B{X}^2$$
46	39 45	eqtrd	$$⊢\phi \to {\left(X^2\right)}^2+2X^2\left(\frac{M+B}{2}\right)=M{X}^2+X^4+B{X}^2$$
47	46	oveq1d	$$⊢\phi \to {\left(X^2\right)}^2+2X^2\left(\frac{M+B}{2}\right)+{\left(\frac{M+B}{2}\right)}^2=M{X}^2+\left(X^4+B{X}^2\right)+{\left(\frac{M+B}{2}\right)}^2$$
48	42 44	addcld	$$⊢\phi \to X^4+B{X}^2\in ℂ$$
49	20	sqcld	$$⊢\phi \to {\left(\frac{M+B}{2}\right)}^2\in ℂ$$
50	43 48 49	addassd	$$⊢\phi \to M{X}^2+\left(X^4+B{X}^2\right)+{\left(\frac{M+B}{2}\right)}^2=M{X}^2+\left(X^4+B{X}^2\right)+{\left(\frac{M+B}{2}\right)}^2$$
51	22 47 50	3eqtrd	$$⊢\phi \to {\left(X^2+\left(\frac{M+B}{2}\right)\right)}^2=M{X}^2+\left(X^4+B{X}^2\right)+{\left(\frac{M+B}{2}\right)}^2$$
52	18	halfcld	$$⊢\phi \to \frac{M}{2}\in ℂ$$
53	52 3	mulcld	$$⊢\phi \to \left(\frac{M}{2}\right)X\in ℂ$$
54		4cn	$$⊢4\in ℂ$$
55	54	a1i	$$⊢\phi \to 4\in ℂ$$
56		4ne0	$$⊢4\ne 0$$
57	56	a1i	$$⊢\phi \to 4\ne 0$$
58	2 55 57	divcld	$$⊢\phi \to \frac{C}{4}\in ℂ$$
59	53 58	subcld	$$⊢\phi \to \left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)\in ℂ$$
60	5 6	eqnetrrd	$$⊢\phi \to {2S}^2\ne 0$$
61		sqne0	$$⊢2S\in ℂ\to \left({2S}^2\ne 0\leftrightarrow 2S\ne 0\right)$$
62	16 61	syl	$$⊢\phi \to \left({2S}^2\ne 0\leftrightarrow 2S\ne 0\right)$$
63	60 62	mpbid	$$⊢\phi \to 2S\ne 0$$
64		mulne0b	$$⊢\left(2\in ℂ\wedge S\in ℂ\right)\to \left(\left(2\ne 0\wedge S\ne 0\right)\leftrightarrow 2S\ne 0\right)$$
65	14 4 64	sylancr	$$⊢\phi \to \left(\left(2\ne 0\wedge S\ne 0\right)\leftrightarrow 2S\ne 0\right)$$
66	63 65	mpbird	$$⊢\phi \to \left(2\ne 0\wedge S\ne 0\right)$$
67	66	simprd	$$⊢\phi \to S\ne 0$$
68	59 4 29 67 32	divcan5d	$$⊢\phi \to \frac{2\left(\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)\right)}{2S}=\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}$$
69	29 53 58	subdid	$$⊢\phi \to 2\left(\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)\right)=2\left(\frac{M}{2}\right)X-2\left(\frac{C}{4}\right)$$
70	29 52 3	mulassd	$$⊢\phi \to 2\left(\frac{M}{2}\right)X=2\left(\frac{M}{2}\right)X$$
71	18 29 32	divcan2d	$$⊢\phi \to 2\left(\frac{M}{2}\right)=M$$
72	71	oveq1d	$$⊢\phi \to 2\left(\frac{M}{2}\right)X=MX$$
73	70 72	eqtr3d	$$⊢\phi \to 2\left(\frac{M}{2}\right)X=MX$$
74	29 2 55 57	divassd	$$⊢\phi \to \frac{2C}{4}=2\left(\frac{C}{4}\right)$$
75	26	oveq2i	$$⊢\frac{2C}{2\cdot 2}=\frac{2C}{4}$$
76	2 29 29 32 32	divcan5d	$$⊢\phi \to \frac{2C}{2\cdot 2}=\frac{C}{2}$$
77	75 76	eqtr3id	$$⊢\phi \to \frac{2C}{4}=\frac{C}{2}$$
78	74 77	eqtr3d	$$⊢\phi \to 2\left(\frac{C}{4}\right)=\frac{C}{2}$$
79	73 78	oveq12d	$$⊢\phi \to 2\left(\frac{M}{2}\right)X-2\left(\frac{C}{4}\right)=MX-\left(\frac{C}{2}\right)$$
80	69 79	eqtrd	$$⊢\phi \to 2\left(\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)\right)=MX-\left(\frac{C}{2}\right)$$
81	80	oveq1d	$$⊢\phi \to \frac{2\left(\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)\right)}{2S}=\frac{MX-\left(\frac{C}{2}\right)}{2S}$$
82	68 81	eqtr3d	$$⊢\phi \to \frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}=\frac{MX-\left(\frac{C}{2}\right)}{2S}$$
83	82	oveq1d	$$⊢\phi \to {\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\right)}^2={\left(\frac{MX-\left(\frac{C}{2}\right)}{2S}\right)}^2$$
84	18 3	mulcld	$$⊢\phi \to MX\in ℂ$$
85	2	halfcld	$$⊢\phi \to \frac{C}{2}\in ℂ$$
86	84 85	subcld	$$⊢\phi \to MX-\left(\frac{C}{2}\right)\in ℂ$$
87	86 16 63	sqdivd	$$⊢\phi \to {\left(\frac{MX-\left(\frac{C}{2}\right)}{2S}\right)}^2=\frac{{\left(MX-\left(\frac{C}{2}\right)\right)}^2}{{2S}^2}$$
88	18	sqcld	$$⊢\phi \to M^2\in ℂ$$
89	88 13	mulcld	$$⊢\phi \to M^2{X}^2\in ℂ$$
90	84 2	mulcld	$$⊢\phi \to MXC\in ℂ$$
91	89 90	subcld	$$⊢\phi \to M^2{X}^2-MXC\in ℂ$$
92	2	sqcld	$$⊢\phi \to C^2\in ℂ$$
93	92 55 57	divcld	$$⊢\phi \to \frac{C^2}{4}\in ℂ$$
94	91 93 18 6	divdird	$$⊢\phi \to \frac{M^2{X}^2-MXC+\left(\frac{C^2}{4}\right)}{M}=\left(\frac{M^2{X}^2-MXC}{M}\right)+\left(\frac{\frac{C^2}{4}}{M}\right)$$
95		binom2sub	$$⊢\left(MX\in ℂ\wedge \frac{C}{2}\in ℂ\right)\to {\left(MX-\left(\frac{C}{2}\right)\right)}^2={MX}^2-2MX\left(\frac{C}{2}\right)+{\left(\frac{C}{2}\right)}^2$$
96	84 85 95	syl2anc	$$⊢\phi \to {\left(MX-\left(\frac{C}{2}\right)\right)}^2={MX}^2-2MX\left(\frac{C}{2}\right)+{\left(\frac{C}{2}\right)}^2$$
97	18 3	sqmuld	$$⊢\phi \to {MX}^2=M^2{X}^2$$
98	29 84 85	mul12d	$$⊢\phi \to 2MX\left(\frac{C}{2}\right)=MX2\left(\frac{C}{2}\right)$$
99	2 29 32	divcan2d	$$⊢\phi \to 2\left(\frac{C}{2}\right)=C$$
100	99	oveq2d	$$⊢\phi \to MX2\left(\frac{C}{2}\right)=MXC$$
101	98 100	eqtrd	$$⊢\phi \to 2MX\left(\frac{C}{2}\right)=MXC$$
102	97 101	oveq12d	$$⊢\phi \to {MX}^2-2MX\left(\frac{C}{2}\right)=M^2{X}^2-MXC$$
103	2 29 32	sqdivd	$$⊢\phi \to {\left(\frac{C}{2}\right)}^2=\frac{C^2}{2^2}$$
104		sq2	$$⊢2^2=4$$
105	104	oveq2i	$$⊢\frac{C^2}{2^2}=\frac{C^2}{4}$$
106	103 105	eqtrdi	$$⊢\phi \to {\left(\frac{C}{2}\right)}^2=\frac{C^2}{4}$$
107	102 106	oveq12d	$$⊢\phi \to {MX}^2-2MX\left(\frac{C}{2}\right)+{\left(\frac{C}{2}\right)}^2=M^2{X}^2-MXC+\left(\frac{C^2}{4}\right)$$
108	96 107	eqtr2d	$$⊢\phi \to M^2{X}^2-MXC+\left(\frac{C^2}{4}\right)={\left(MX-\left(\frac{C}{2}\right)\right)}^2$$
109	108 5	oveq12d	$$⊢\phi \to \frac{M^2{X}^2-MXC+\left(\frac{C^2}{4}\right)}{M}=\frac{{\left(MX-\left(\frac{C}{2}\right)\right)}^2}{{2S}^2}$$
110	89 90 18 6	divsubdird	$$⊢\phi \to \frac{M^2{X}^2-MXC}{M}=\left(\frac{M^2{X}^2}{M}\right)-\left(\frac{MXC}{M}\right)$$
111	88 13 18 6	div23d	$$⊢\phi \to \frac{M^2{X}^2}{M}=\left(\frac{M^2}{M}\right)X^2$$
112	18	sqvald	$$⊢\phi \to M^2=\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
113	112	oveq1d	$$⊢\phi \to \frac{M^2}{M}=\frac{\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}}{M}$$
114	18 18 6	divcan3d	$$⊢\phi \to \frac{\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}}{M}=M$$
115	113 114	eqtrd	$$⊢\phi \to \frac{M^2}{M}=M$$
116	115	oveq1d	$$⊢\phi \to \left(\frac{M^2}{M}\right)X^2=M{X}^2$$
117	111 116	eqtrd	$$⊢\phi \to \frac{M^2{X}^2}{M}=M{X}^2$$
118	18 3 2	mul32d	$$⊢\phi \to MXC=MCX$$
119	18 2 3	mulassd	$$⊢\phi \to MCX=MCX$$
120	118 119	eqtrd	$$⊢\phi \to MXC=MCX$$
121	120	oveq1d	$$⊢\phi \to \frac{MXC}{M}=\frac{MCX}{M}$$
122	2 3	mulcld	$$⊢\phi \to CX\in ℂ$$
123	122 18 6	divcan3d	$$⊢\phi \to \frac{MCX}{M}=CX$$
124	121 123	eqtrd	$$⊢\phi \to \frac{MXC}{M}=CX$$
125	117 124	oveq12d	$$⊢\phi \to \left(\frac{M^2{X}^2}{M}\right)-\left(\frac{MXC}{M}\right)=M{X}^2-CX$$
126	110 125	eqtrd	$$⊢\phi \to \frac{M^2{X}^2-MXC}{M}=M{X}^2-CX$$
127	126	oveq1d	$$⊢\phi \to \left(\frac{M^2{X}^2-MXC}{M}\right)+\left(\frac{\frac{C^2}{4}}{M}\right)=M{X}^2-CX+\left(\frac{\frac{C^2}{4}}{M}\right)$$
128	93 18 6	divcld	$$⊢\phi \to \frac{\frac{C^2}{4}}{M}\in ℂ$$
129	43 122 128	subsubd	$$⊢\phi \to M{X}^2-\left(CX-\left(\frac{\frac{C^2}{4}}{M}\right)\right)=M{X}^2-CX+\left(\frac{\frac{C^2}{4}}{M}\right)$$
130	127 129	eqtr4d	$$⊢\phi \to \left(\frac{M^2{X}^2-MXC}{M}\right)+\left(\frac{\frac{C^2}{4}}{M}\right)=M{X}^2-\left(CX-\left(\frac{\frac{C^2}{4}}{M}\right)\right)$$
131	94 109 130	3eqtr3d	$$⊢\phi \to \frac{{\left(MX-\left(\frac{C}{2}\right)\right)}^2}{{2S}^2}=M{X}^2-\left(CX-\left(\frac{\frac{C^2}{4}}{M}\right)\right)$$
132	83 87 131	3eqtrd	$$⊢\phi \to {\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\right)}^2=M{X}^2-\left(CX-\left(\frac{\frac{C^2}{4}}{M}\right)\right)$$
133	51 132	oveq12d	$$⊢\phi \to {\left(X^2+\left(\frac{M+B}{2}\right)\right)}^2-{\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\right)}^2=M{X}^2+\left(X^4+B{X}^2+{\left(\frac{M+B}{2}\right)}^2\right)-\left(M{X}^2-\left(CX-\left(\frac{\frac{C^2}{4}}{M}\right)\right)\right)$$
134	48 49	addcld	$$⊢\phi \to X^4+B{X}^2+{\left(\frac{M+B}{2}\right)}^2\in ℂ$$
135	122 128	subcld	$$⊢\phi \to CX-\left(\frac{\frac{C^2}{4}}{M}\right)\in ℂ$$
136	43 134 135	pnncand	$$⊢\phi \to M{X}^2+\left(X^4+B{X}^2+{\left(\frac{M+B}{2}\right)}^2\right)-\left(M{X}^2-\left(CX-\left(\frac{\frac{C^2}{4}}{M}\right)\right)\right)=\left(X^4+B{X}^2\right)+{\left(\frac{M+B}{2}\right)}^2+\left(CX-\left(\frac{\frac{C^2}{4}}{M}\right)\right)$$
137	128	negcld	$$⊢\phi \to -\frac{\frac{C^2}{4}}{M}\in ℂ$$
138	48 49 122 137	add4d	$$⊢\phi \to \left(X^4+B{X}^2\right)+{\left(\frac{M+B}{2}\right)}^2+CX+\left(-\frac{\frac{C^2}{4}}{M}\right)=\left(X^4+B{X}^2\right)+CX+{\left(\frac{M+B}{2}\right)}^2+\left(-\frac{\frac{C^2}{4}}{M}\right)$$
139	122 128	negsubd	$$⊢\phi \to CX+\left(-\frac{\frac{C^2}{4}}{M}\right)=CX-\left(\frac{\frac{C^2}{4}}{M}\right)$$
140	139	oveq2d	$$⊢\phi \to \left(X^4+B{X}^2\right)+{\left(\frac{M+B}{2}\right)}^2+CX+\left(-\frac{\frac{C^2}{4}}{M}\right)=\left(X^4+B{X}^2\right)+{\left(\frac{M+B}{2}\right)}^2+\left(CX-\left(\frac{\frac{C^2}{4}}{M}\right)\right)$$
141	49 128	negsubd	$$⊢\phi \to {\left(\frac{M+B}{2}\right)}^2+\left(-\frac{\frac{C^2}{4}}{M}\right)={\left(\frac{M+B}{2}\right)}^2-\left(\frac{\frac{C^2}{4}}{M}\right)$$
142	1 2 3 4 5 6 7 8 9 10	dquartlem2	$$⊢\phi \to {\left(\frac{M+B}{2}\right)}^2-\left(\frac{\frac{C^2}{4}}{M}\right)=D$$
143	141 142	eqtrd	$$⊢\phi \to {\left(\frac{M+B}{2}\right)}^2+\left(-\frac{\frac{C^2}{4}}{M}\right)=D$$
144	143	oveq2d	$$⊢\phi \to \left(X^4+B{X}^2\right)+CX+{\left(\frac{M+B}{2}\right)}^2+\left(-\frac{\frac{C^2}{4}}{M}\right)=\left(X^4+B{X}^2\right)+CX+D$$
145	48 122 9	addassd	$$⊢\phi \to \left(X^4+B{X}^2\right)+CX+D=X^4+B{X}^2+CX+D$$
146	144 145	eqtrd	$$⊢\phi \to \left(X^4+B{X}^2\right)+CX+{\left(\frac{M+B}{2}\right)}^2+\left(-\frac{\frac{C^2}{4}}{M}\right)=X^4+B{X}^2+CX+D$$
147	138 140 146	3eqtr3d	$$⊢\phi \to \left(X^4+B{X}^2\right)+{\left(\frac{M+B}{2}\right)}^2+\left(CX-\left(\frac{\frac{C^2}{4}}{M}\right)\right)=X^4+B{X}^2+CX+D$$
148	133 136 147	3eqtrd	$$⊢\phi \to {\left(X^2+\left(\frac{M+B}{2}\right)\right)}^2-{\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\right)}^2=X^4+B{X}^2+CX+D$$
149	13 20	addcld	$$⊢\phi \to X^2+\left(\frac{M+B}{2}\right)\in ℂ$$
150	59 4 67	divcld	$$⊢\phi \to \frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\in ℂ$$
151		subsq	$$⊢\left(X^2+\left(\frac{M+B}{2}\right)\in ℂ\wedge \frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\in ℂ\right)\to {\left(X^2+\left(\frac{M+B}{2}\right)\right)}^2-{\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\right)}^2=\left(X^2+\left(\frac{M+B}{2}\right)+\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\right)\right)\left(X^2+\left(\frac{M+B}{2}\right)-\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\right)\right)$$
152	149 150 151	syl2anc	$$⊢\phi \to {\left(X^2+\left(\frac{M+B}{2}\right)\right)}^2-{\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\right)}^2=\left(X^2+\left(\frac{M+B}{2}\right)+\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\right)\right)\left(X^2+\left(\frac{M+B}{2}\right)-\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\right)\right)$$
153	148 152	eqtr3d	$$⊢\phi \to X^4+B{X}^2+CX+D=\left(X^2+\left(\frac{M+B}{2}\right)+\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\right)\right)\left(X^2+\left(\frac{M+B}{2}\right)-\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\right)\right)$$
154	153	eqeq1d	$$⊢\phi \to \left(X^4+B{X}^2+CX+D=0\leftrightarrow \left(X^2+\left(\frac{M+B}{2}\right)+\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\right)\right)\left(X^2+\left(\frac{M+B}{2}\right)-\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\right)\right)=0\right)$$
155	149 150	addcld	$$⊢\phi \to X^2+\left(\frac{M+B}{2}\right)+\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\right)\in ℂ$$
156	149 150	subcld	$$⊢\phi \to X^2+\left(\frac{M+B}{2}\right)-\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\right)\in ℂ$$
157	155 156	mul0ord	$$⊢\phi \to \left(\left(X^2+\left(\frac{M+B}{2}\right)+\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\right)\right)\left(X^2+\left(\frac{M+B}{2}\right)-\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\right)\right)=0\leftrightarrow \left(X^2+\left(\frac{M+B}{2}\right)+\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\right)=0\vee X^2+\left(\frac{M+B}{2}\right)-\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\right)=0\right)\right)$$
158	1 2 3 4 5 6 7 8	dquartlem1	$$⊢\phi \to \left(X^2+\left(\frac{M+B}{2}\right)+\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\right)=0\leftrightarrow \left(X=-S+I\vee X=-S-I\right)\right)$$
159	4	negcld	$$⊢\phi \to -S\in ℂ$$
160		sqneg	$$⊢2S\in ℂ\to {\left(-2S\right)}^2={2S}^2$$
161	16 160	syl	$$⊢\phi \to {\left(-2S\right)}^2={2S}^2$$
162	5 161	eqtr4d	$$⊢\phi \to M={\left(-2S\right)}^2$$
163		mulneg2	$$⊢\left(2\in ℂ\wedge S\in ℂ\right)\to 2\left(-S\right)=-2S$$
164	14 4 163	sylancr	$$⊢\phi \to 2\left(-S\right)=-2S$$
165	164	oveq1d	$$⊢\phi \to {2\left(-S\right)}^2={\left(-2S\right)}^2$$
166	162 165	eqtr4d	$$⊢\phi \to M={2\left(-S\right)}^2$$
167	4	sqcld	$$⊢\phi \to S^2\in ℂ$$
168	167	negcld	$$⊢\phi \to -S^2\in ℂ$$
169	1	halfcld	$$⊢\phi \to \frac{B}{2}\in ℂ$$
170	168 169	subcld	$$⊢\phi \to -S^2-\left(\frac{B}{2}\right)\in ℂ$$
171	58 4 67	divcld	$$⊢\phi \to \frac{\frac{C}{4}}{S}\in ℂ$$
172	170 171	negsubd	$$⊢\phi \to \left(-S^2\right)-\left(\frac{B}{2}\right)+\left(-\frac{\frac{C}{4}}{S}\right)=\left(-S^2\right)-\left(\frac{B}{2}\right)-\left(\frac{\frac{C}{4}}{S}\right)$$
173		sqneg	$$⊢S\in ℂ\to {\left(-S\right)}^2=S^2$$
174	4 173	syl	$$⊢\phi \to {\left(-S\right)}^2=S^2$$
175	174	eqcomd	$$⊢\phi \to S^2={\left(-S\right)}^2$$
176	175	negeqd	$$⊢\phi \to -S^2=-{\left(-S\right)}^2$$
177	176	oveq1d	$$⊢\phi \to -S^2-\left(\frac{B}{2}\right)=-{\left(-S\right)}^2-\left(\frac{B}{2}\right)$$
178	58 4 67	divneg2d	$$⊢\phi \to -\frac{\frac{C}{4}}{S}=\frac{\frac{C}{4}}{-S}$$
179	177 178	oveq12d	$$⊢\phi \to \left(-S^2\right)-\left(\frac{B}{2}\right)+\left(-\frac{\frac{C}{4}}{S}\right)=\left(-{\left(-S\right)}^2\right)-\left(\frac{B}{2}\right)+\left(\frac{\frac{C}{4}}{-S}\right)$$
180	12 172 179	3eqtr2d	$$⊢\phi \to J^2=\left(-{\left(-S\right)}^2\right)-\left(\frac{B}{2}\right)+\left(\frac{\frac{C}{4}}{-S}\right)$$
181	1 2 3 159 166 6 11 180	dquartlem1	$$⊢\phi \to \left(X^2+\left(\frac{M+B}{2}\right)+\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{-S}\right)=0\leftrightarrow \left(X=-\left(-S\right)+J\vee X=-\left(-S\right)-J\right)\right)$$
182	59 4 67	divneg2d	$$⊢\phi \to -\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}=\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{-S}$$
183	182	oveq2d	$$⊢\phi \to X^2+\left(\frac{M+B}{2}\right)+\left(-\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\right)=X^2+\left(\frac{M+B}{2}\right)+\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{-S}\right)$$
184	149 150	negsubd	$$⊢\phi \to X^2+\left(\frac{M+B}{2}\right)+\left(-\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\right)=X^2+\left(\frac{M+B}{2}\right)-\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\right)$$
185	183 184	eqtr3d	$$⊢\phi \to X^2+\left(\frac{M+B}{2}\right)+\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{-S}\right)=X^2+\left(\frac{M+B}{2}\right)-\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\right)$$
186	185	eqeq1d	$$⊢\phi \to \left(X^2+\left(\frac{M+B}{2}\right)+\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{-S}\right)=0\leftrightarrow X^2+\left(\frac{M+B}{2}\right)-\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\right)=0\right)$$
187	4	negnegd	$$⊢\phi \to -\left(-S\right)=S$$
188	187	oveq1d	$$⊢\phi \to -\left(-S\right)+J=S+J$$
189	188	eqeq2d	$$⊢\phi \to \left(X=-\left(-S\right)+J\leftrightarrow X=S+J\right)$$
190	187	oveq1d	$$⊢\phi \to -\left(-S\right)-J=S-J$$
191	190	eqeq2d	$$⊢\phi \to \left(X=-\left(-S\right)-J\leftrightarrow X=S-J\right)$$
192	189 191	orbi12d	$$⊢\phi \to \left(\left(X=-\left(-S\right)+J\vee X=-\left(-S\right)-J\right)\leftrightarrow \left(X=S+J\vee X=S-J\right)\right)$$
193	181 186 192	3bitr3d	$$⊢\phi \to \left(X^2+\left(\frac{M+B}{2}\right)-\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\right)=0\leftrightarrow \left(X=S+J\vee X=S-J\right)\right)$$
194	158 193	orbi12d	$$⊢\phi \to \left(\left(X^2+\left(\frac{M+B}{2}\right)+\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\right)=0\vee X^2+\left(\frac{M+B}{2}\right)-\left(\frac{\left(\frac{M}{2}\right)X-\left(\frac{C}{4}\right)}{S}\right)=0\right)\leftrightarrow \left(\left(X=-S+I\vee X=-S-I\right)\vee \left(X=S+J\vee X=S-J\right)\right)\right)$$
195	154 157 194	3bitrd	$$⊢\phi \to \left(X^4+B{X}^2+CX+D=0\leftrightarrow \left(\left(X=-S+I\vee X=-S-I\right)\vee \left(X=S+J\vee X=S-J\right)\right)\right)$$