Theorem quart1

Description: Depress a quartic equation. (Contributed by Mario Carneiro, 6-May-2015)

	Ref	Expression
Hypotheses	quart1.a	$$⊢\phi \to A\in ℂ$$
	quart1.b	$$⊢\phi \to B\in ℂ$$
	quart1.c	$$⊢\phi \to C\in ℂ$$
	quart1.d	$$⊢\phi \to D\in ℂ$$
	quart1.p	$$⊢\phi \to P=B-\left(\frac{3}{8}\right)A^2$$
	quart1.q	$$⊢\phi \to Q=C-\left(\frac{AB}{2}\right)+\left(\frac{A^3}{8}\right)$$
	quart1.r	$$⊢\phi \to R=\left(D-\left(\frac{CA}{4}\right)\right)+\left(\frac{A^{2}B}{16}\right)-\left(\frac{3}{256}\right)A^4$$
	quart1.x	$$⊢\phi \to X\in ℂ$$
	quart1.y	$$⊢\phi \to Y=X+\left(\frac{A}{4}\right)$$
Assertion	quart1	$$⊢\phi \to X^4+A{X}^3+B{X}^2+\left(CX+D\right)=Y^4+P{Y}^2+QY+R$$

Proof

Step	Hyp	Ref	Expression
1		quart1.a	$$⊢\phi \to A\in ℂ$$
2		quart1.b	$$⊢\phi \to B\in ℂ$$
3		quart1.c	$$⊢\phi \to C\in ℂ$$
4		quart1.d	$$⊢\phi \to D\in ℂ$$
5		quart1.p	$$⊢\phi \to P=B-\left(\frac{3}{8}\right)A^2$$
6		quart1.q	$$⊢\phi \to Q=C-\left(\frac{AB}{2}\right)+\left(\frac{A^3}{8}\right)$$
7		quart1.r	$$⊢\phi \to R=\left(D-\left(\frac{CA}{4}\right)\right)+\left(\frac{A^{2}B}{16}\right)-\left(\frac{3}{256}\right)A^4$$
8		quart1.x	$$⊢\phi \to X\in ℂ$$
9		quart1.y	$$⊢\phi \to Y=X+\left(\frac{A}{4}\right)$$
10	9	oveq1d	$$⊢\phi \to Y^4={\left(X+\left(\frac{A}{4}\right)\right)}^4$$
11		4cn	$$⊢4\in ℂ$$
12	11	a1i	$$⊢\phi \to 4\in ℂ$$
13		4ne0	$$⊢4\ne 0$$
14	13	a1i	$$⊢\phi \to 4\ne 0$$
15	1 12 14	divcld	$$⊢\phi \to \frac{A}{4}\in ℂ$$
16		binom4	$$⊢\left(X\in ℂ\wedge \frac{A}{4}\in ℂ\right)\to {\left(X+\left(\frac{A}{4}\right)\right)}^4=X^4+4X^3\left(\frac{A}{4}\right)+6X^2{\left(\frac{A}{4}\right)}^2+\left(4X{\left(\frac{A}{4}\right)}^3+{\left(\frac{A}{4}\right)}^4\right)$$
17	8 15 16	syl2anc	$$⊢\phi \to {\left(X+\left(\frac{A}{4}\right)\right)}^4=X^4+4X^3\left(\frac{A}{4}\right)+6X^2{\left(\frac{A}{4}\right)}^2+\left(4X{\left(\frac{A}{4}\right)}^3+{\left(\frac{A}{4}\right)}^4\right)$$
18		3nn0	$$⊢3\in {\mathbb{N}}_0$$
19		expcl	$$⊢\left(X\in ℂ\wedge 3\in {\mathbb{N}}_0\right)\to X^3\in ℂ$$
20	8 18 19	sylancl	$$⊢\phi \to X^3\in ℂ$$
21	12 20 15	mul12d	$$⊢\phi \to 4X^3\left(\frac{A}{4}\right)=X^{3}4\left(\frac{A}{4}\right)$$
22	1 12 14	divcan2d	$$⊢\phi \to 4\left(\frac{A}{4}\right)=A$$
23	22	oveq2d	$$⊢\phi \to X^{3}4\left(\frac{A}{4}\right)=X^{3}A$$
24	20 1	mulcomd	$$⊢\phi \to X^{3}A=A{X}^3$$
25	21 23 24	3eqtrd	$$⊢\phi \to 4X^3\left(\frac{A}{4}\right)=A{X}^3$$
26	25	oveq2d	$$⊢\phi \to X^4+4X^3\left(\frac{A}{4}\right)=X^4+A{X}^3$$
27		6nn	$$⊢6\in \mathbb{N}$$
28	27	nncni	$$⊢6\in ℂ$$
29	28	a1i	$$⊢\phi \to 6\in ℂ$$
30	15	sqcld	$$⊢\phi \to {\left(\frac{A}{4}\right)}^2\in ℂ$$
31	8	sqcld	$$⊢\phi \to X^2\in ℂ$$
32	29 30 31	mulassd	$$⊢\phi \to 6{\left(\frac{A}{4}\right)}^2{X}^2=6{\left(\frac{A}{4}\right)}^2{X}^2$$
33		3cn	$$⊢3\in ℂ$$
34		2cn	$$⊢2\in ℂ$$
35		3t2e6	$$⊢3\cdot 2=6$$
36	33 34 35	mulcomli	$$⊢2\cdot 3=6$$
37		8cn	$$⊢8\in ℂ$$
38		8t2e16	$$⊢8\cdot 2=16$$
39	37 34 38	mulcomli	$$⊢2\cdot 8=16$$
40	36 39	oveq12i	$$⊢\frac{2\cdot 3}{2\cdot 8}=\frac{6}{16}$$
41		8nn	$$⊢8\in \mathbb{N}$$
42	41	nnne0i	$$⊢8\ne 0$$
43	37 42	pm3.2i	$$⊢\left(8\in ℂ\wedge 8\ne 0\right)$$
44		2cnne0	$$⊢\left(2\in ℂ\wedge 2\ne 0\right)$$
45		divcan5	$$⊢\left(3\in ℂ\wedge \left(8\in ℂ\wedge 8\ne 0\right)\wedge \left(2\in ℂ\wedge 2\ne 0\right)\right)\to \frac{2\cdot 3}{2\cdot 8}=\frac{3}{8}$$
46	33 43 44 45	mp3an	$$⊢\frac{2\cdot 3}{2\cdot 8}=\frac{3}{8}$$
47	40 46	eqtr3i	$$⊢\frac{6}{16}=\frac{3}{8}$$
48	47	oveq2i	$$⊢A^2\left(\frac{6}{16}\right)=A^2\left(\frac{3}{8}\right)$$
49	1	sqcld	$$⊢\phi \to A^2\in ℂ$$
50		1nn0	$$⊢1\in {\mathbb{N}}_0$$
51	50 27	decnncl	$$⊢16\in \mathbb{N}$$
52	51	nncni	$$⊢16\in ℂ$$
53	52	a1i	$$⊢\phi \to 16\in ℂ$$
54	51	nnne0i	$$⊢16\ne 0$$
55	54	a1i	$$⊢\phi \to 16\ne 0$$
56	49 29 53 55	div12d	$$⊢\phi \to A^2\left(\frac{6}{16}\right)=6\left(\frac{A^2}{16}\right)$$
57	48 56	eqtr3id	$$⊢\phi \to A^2\left(\frac{3}{8}\right)=6\left(\frac{A^2}{16}\right)$$
58	33 37 42	divcli	$$⊢\frac{3}{8}\in ℂ$$
59		mulcom	$$⊢\left(\frac{3}{8}\in ℂ\wedge A^2\in ℂ\right)\to \left(\frac{3}{8}\right)A^2=A^2\left(\frac{3}{8}\right)$$
60	58 49 59	sylancr	$$⊢\phi \to \left(\frac{3}{8}\right)A^2=A^2\left(\frac{3}{8}\right)$$
61	1 12 14	sqdivd	$$⊢\phi \to {\left(\frac{A}{4}\right)}^2=\frac{A^2}{4^2}$$
62	11	sqvali	$$⊢4^2=4\cdot 4$$
63		4t4e16	$$⊢4\cdot 4=16$$
64	62 63	eqtri	$$⊢4^2=16$$
65	64	oveq2i	$$⊢\frac{A^2}{4^2}=\frac{A^2}{16}$$
66	61 65	eqtrdi	$$⊢\phi \to {\left(\frac{A}{4}\right)}^2=\frac{A^2}{16}$$
67	66	oveq2d	$$⊢\phi \to 6{\left(\frac{A}{4}\right)}^2=6\left(\frac{A^2}{16}\right)$$
68	57 60 67	3eqtr4d	$$⊢\phi \to \left(\frac{3}{8}\right)A^2=6{\left(\frac{A}{4}\right)}^2$$
69	68	oveq1d	$$⊢\phi \to \left(\frac{3}{8}\right)A^2{X}^2=6{\left(\frac{A}{4}\right)}^2{X}^2$$
70	31 30	mulcomd	$$⊢\phi \to X^2{\left(\frac{A}{4}\right)}^2={\left(\frac{A}{4}\right)}^2{X}^2$$
71	70	oveq2d	$$⊢\phi \to 6X^2{\left(\frac{A}{4}\right)}^2=6{\left(\frac{A}{4}\right)}^2{X}^2$$
72	32 69 71	3eqtr4rd	$$⊢\phi \to 6X^2{\left(\frac{A}{4}\right)}^2=\left(\frac{3}{8}\right)A^2{X}^2$$
73		expcl	$$⊢\left(\frac{A}{4}\in ℂ\wedge 3\in {\mathbb{N}}_0\right)\to {\left(\frac{A}{4}\right)}^3\in ℂ$$
74	15 18 73	sylancl	$$⊢\phi \to {\left(\frac{A}{4}\right)}^3\in ℂ$$
75	12 8 74	mul12d	$$⊢\phi \to 4X{\left(\frac{A}{4}\right)}^3=X4{\left(\frac{A}{4}\right)}^3$$
76	12 74	mulcld	$$⊢\phi \to 4{\left(\frac{A}{4}\right)}^3\in ℂ$$
77	8 76	mulcomd	$$⊢\phi \to X4{\left(\frac{A}{4}\right)}^3=4{\left(\frac{A}{4}\right)}^{3}X$$
78		df-3	$$⊢3=2+1$$
79	78	oveq2i	$$⊢4^3=4^{2+1}$$
80		2nn0	$$⊢2\in {\mathbb{N}}_0$$
81		expp1	$$⊢\left(4\in ℂ\wedge 2\in {\mathbb{N}}_0\right)\to 4^{2+1}=4^2\cdot 4$$
82	11 80 81	mp2an	$$⊢4^{2+1}=4^2\cdot 4$$
83	64	oveq1i	$$⊢4^2\cdot 4=16\cdot 4$$
84	79 82 83	3eqtri	$$⊢4^3=16\cdot 4$$
85	84	oveq2i	$$⊢\frac{A^3}{4^3}=\frac{A^3}{16\cdot 4}$$
86	18	a1i	$$⊢\phi \to 3\in {\mathbb{N}}_0$$
87	1 12 14 86	expdivd	$$⊢\phi \to {\left(\frac{A}{4}\right)}^3=\frac{A^3}{4^3}$$
88		expcl	$$⊢\left(A\in ℂ\wedge 3\in {\mathbb{N}}_0\right)\to A^3\in ℂ$$
89	1 18 88	sylancl	$$⊢\phi \to A^3\in ℂ$$
90	89 53 12 55 14	divdiv1d	$$⊢\phi \to \frac{\frac{A^3}{16}}{4}=\frac{A^3}{16\cdot 4}$$
91	85 87 90	3eqtr4a	$$⊢\phi \to {\left(\frac{A}{4}\right)}^3=\frac{\frac{A^3}{16}}{4}$$
92	91	oveq2d	$$⊢\phi \to 4{\left(\frac{A}{4}\right)}^3=4\left(\frac{\frac{A^3}{16}}{4}\right)$$
93	38	oveq2i	$$⊢\frac{A^3}{8\cdot 2}=\frac{A^3}{16}$$
94	37	a1i	$$⊢\phi \to 8\in ℂ$$
95	34	a1i	$$⊢\phi \to 2\in ℂ$$
96	42	a1i	$$⊢\phi \to 8\ne 0$$
97		2ne0	$$⊢2\ne 0$$
98	97	a1i	$$⊢\phi \to 2\ne 0$$
99	89 94 95 96 98	divdiv1d	$$⊢\phi \to \frac{\frac{A^3}{8}}{2}=\frac{A^3}{8\cdot 2}$$
100	89 53 55	divcld	$$⊢\phi \to \frac{A^3}{16}\in ℂ$$
101	100 12 14	divcan2d	$$⊢\phi \to 4\left(\frac{\frac{A^3}{16}}{4}\right)=\frac{A^3}{16}$$
102	93 99 101	3eqtr4a	$$⊢\phi \to \frac{\frac{A^3}{8}}{2}=4\left(\frac{\frac{A^3}{16}}{4}\right)$$
103	92 102	eqtr4d	$$⊢\phi \to 4{\left(\frac{A}{4}\right)}^3=\frac{\frac{A^3}{8}}{2}$$
104	103	oveq1d	$$⊢\phi \to 4{\left(\frac{A}{4}\right)}^{3}X=\left(\frac{\frac{A^3}{8}}{2}\right)X$$
105	75 77 104	3eqtrd	$$⊢\phi \to 4X{\left(\frac{A}{4}\right)}^3=\left(\frac{\frac{A^3}{8}}{2}\right)X$$
106		4nn0	$$⊢4\in {\mathbb{N}}_0$$
107	106	a1i	$$⊢\phi \to 4\in {\mathbb{N}}_0$$
108	1 12 14 107	expdivd	$$⊢\phi \to {\left(\frac{A}{4}\right)}^4=\frac{A^4}{4^4}$$
109		expmul	$$⊢\left(2\in ℂ\wedge 2\in {\mathbb{N}}_0\wedge 4\in {\mathbb{N}}_0\right)\to 2^{2\cdot 4}={\left(2^2\right)}^4$$
110	34 80 106 109	mp3an	$$⊢2^{2\cdot 4}={\left(2^2\right)}^4$$
111		4t2e8	$$⊢4\cdot 2=8$$
112	11 34 111	mulcomli	$$⊢2\cdot 4=8$$
113	112	oveq2i	$$⊢2^{2\cdot 4}=2^8$$
114	110 113	eqtr3i	$$⊢{\left(2^2\right)}^4=2^8$$
115		sq2	$$⊢2^2=4$$
116	115	oveq1i	$$⊢{\left(2^2\right)}^4=4^4$$
117	114 116	eqtr3i	$$⊢2^8=4^4$$
118		2exp8	$$⊢2^8=256$$
119	117 118	eqtr3i	$$⊢4^4=256$$
120	119	oveq2i	$$⊢\frac{A^4}{4^4}=\frac{A^4}{256}$$
121	108 120	eqtrdi	$$⊢\phi \to {\left(\frac{A}{4}\right)}^4=\frac{A^4}{256}$$
122	105 121	oveq12d	$$⊢\phi \to 4X{\left(\frac{A}{4}\right)}^3+{\left(\frac{A}{4}\right)}^4=\left(\frac{\frac{A^3}{8}}{2}\right)X+\left(\frac{A^4}{256}\right)$$
123	72 122	oveq12d	$$⊢\phi \to 6X^2{\left(\frac{A}{4}\right)}^2+4X{\left(\frac{A}{4}\right)}^3+{\left(\frac{A}{4}\right)}^4=\left(\frac{3}{8}\right)A^2{X}^2+\left(\frac{\frac{A^3}{8}}{2}\right)X+\left(\frac{A^4}{256}\right)$$
124	26 123	oveq12d	$$⊢\phi \to X^4+4X^3\left(\frac{A}{4}\right)+6X^2{\left(\frac{A}{4}\right)}^2+\left(4X{\left(\frac{A}{4}\right)}^3+{\left(\frac{A}{4}\right)}^4\right)=X^4+A{X}^3+\left(\frac{3}{8}\right)A^2{X}^2+\left(\left(\frac{\frac{A^3}{8}}{2}\right)X+\left(\frac{A^4}{256}\right)\right)$$
125	10 17 124	3eqtrd	$$⊢\phi \to Y^4=X^4+A{X}^3+\left(\frac{3}{8}\right)A^2{X}^2+\left(\left(\frac{\frac{A^3}{8}}{2}\right)X+\left(\frac{A^4}{256}\right)\right)$$
126	125	oveq1d	$$⊢\phi \to Y^4+P{Y}^2=\left(X^4+A{X}^3\right)+\left(\left(\frac{3}{8}\right)A^2{X}^2+\left(\frac{\frac{A^3}{8}}{2}\right)X+\left(\frac{A^4}{256}\right)\right)+P{Y}^2$$
127		expcl	$$⊢\left(X\in ℂ\wedge 4\in {\mathbb{N}}_0\right)\to X^4\in ℂ$$
128	8 106 127	sylancl	$$⊢\phi \to X^4\in ℂ$$
129	1 20	mulcld	$$⊢\phi \to A{X}^3\in ℂ$$
130	128 129	addcld	$$⊢\phi \to X^4+A{X}^3\in ℂ$$
131		mulcl	$$⊢\left(\frac{3}{8}\in ℂ\wedge A^2\in ℂ\right)\to \left(\frac{3}{8}\right)A^2\in ℂ$$
132	58 49 131	sylancr	$$⊢\phi \to \left(\frac{3}{8}\right)A^2\in ℂ$$
133	132 31	mulcld	$$⊢\phi \to \left(\frac{3}{8}\right)A^2{X}^2\in ℂ$$
134	89 94 96	divcld	$$⊢\phi \to \frac{A^3}{8}\in ℂ$$
135	134	halfcld	$$⊢\phi \to \frac{\frac{A^3}{8}}{2}\in ℂ$$
136	135 8	mulcld	$$⊢\phi \to \left(\frac{\frac{A^3}{8}}{2}\right)X\in ℂ$$
137		expcl	$$⊢\left(A\in ℂ\wedge 4\in {\mathbb{N}}_0\right)\to A^4\in ℂ$$
138	1 106 137	sylancl	$$⊢\phi \to A^4\in ℂ$$
139		5nn0	$$⊢5\in {\mathbb{N}}_0$$
140	80 139	deccl	$$⊢25\in {\mathbb{N}}_0$$
141	140 27	decnncl	$$⊢256\in \mathbb{N}$$
142	141	nncni	$$⊢256\in ℂ$$
143	142	a1i	$$⊢\phi \to 256\in ℂ$$
144	141	nnne0i	$$⊢256\ne 0$$
145	144	a1i	$$⊢\phi \to 256\ne 0$$
146	138 143 145	divcld	$$⊢\phi \to \frac{A^4}{256}\in ℂ$$
147	136 146	addcld	$$⊢\phi \to \left(\frac{\frac{A^3}{8}}{2}\right)X+\left(\frac{A^4}{256}\right)\in ℂ$$
148	133 147	addcld	$$⊢\phi \to \left(\frac{3}{8}\right)A^2{X}^2+\left(\frac{\frac{A^3}{8}}{2}\right)X+\left(\frac{A^4}{256}\right)\in ℂ$$
149	1 2 3 4 5 6 7	quart1cl	$$⊢\phi \to \left(P\in ℂ\wedge Q\in ℂ\wedge R\in ℂ\right)$$
150	149	simp1d	$$⊢\phi \to P\in ℂ$$
151	8 15	addcld	$$⊢\phi \to X+\left(\frac{A}{4}\right)\in ℂ$$
152	9 151	eqeltrd	$$⊢\phi \to Y\in ℂ$$
153	152	sqcld	$$⊢\phi \to Y^2\in ℂ$$
154	150 153	mulcld	$$⊢\phi \to P{Y}^2\in ℂ$$
155	130 148 154	addassd	$$⊢\phi \to \left(X^4+A{X}^3\right)+\left(\left(\frac{3}{8}\right)A^2{X}^2+\left(\frac{\frac{A^3}{8}}{2}\right)X+\left(\frac{A^4}{256}\right)\right)+P{Y}^2=X^4+A{X}^3+\left(\left(\frac{3}{8}\right)A^2{X}^2+\left(\frac{\frac{A^3}{8}}{2}\right)X+\left(\frac{A^4}{256}\right)\right)+P{Y}^2$$
156	126 155	eqtrd	$$⊢\phi \to Y^4+P{Y}^2=X^4+A{X}^3+\left(\left(\frac{3}{8}\right)A^2{X}^2+\left(\frac{\frac{A^3}{8}}{2}\right)X+\left(\frac{A^4}{256}\right)\right)+P{Y}^2$$
157	156	oveq1d	$$⊢\phi \to Y^4+P{Y}^2+QY+R=\left(X^4+A{X}^3\right)+\left(\left(\frac{3}{8}\right)A^2{X}^2+\left(\left(\frac{\frac{A^3}{8}}{2}\right)X+\left(\frac{A^4}{256}\right)\right)+P{Y}^2\right)+QY+R$$
158	148 154	addcld	$$⊢\phi \to \left(\frac{3}{8}\right)A^2{X}^2+\left(\left(\frac{\frac{A^3}{8}}{2}\right)X+\left(\frac{A^4}{256}\right)\right)+P{Y}^2\in ℂ$$
159	149	simp2d	$$⊢\phi \to Q\in ℂ$$
160	159 152	mulcld	$$⊢\phi \to QY\in ℂ$$
161	149	simp3d	$$⊢\phi \to R\in ℂ$$
162	160 161	addcld	$$⊢\phi \to QY+R\in ℂ$$
163	130 158 162	addassd	$$⊢\phi \to \left(X^4+A{X}^3\right)+\left(\left(\frac{3}{8}\right)A^2{X}^2+\left(\left(\frac{\frac{A^3}{8}}{2}\right)X+\left(\frac{A^4}{256}\right)\right)+P{Y}^2\right)+QY+R=X^4+A{X}^3+\left(\left(\frac{3}{8}\right)A^2{X}^2+\left(\left(\frac{\frac{A^3}{8}}{2}\right)X+\left(\frac{A^4}{256}\right)\right)+P{Y}^2\right)+\left(QY+R\right)$$
164	9	oveq1d	$$⊢\phi \to Y^2={\left(X+\left(\frac{A}{4}\right)\right)}^2$$
165		binom2	$$⊢\left(X\in ℂ\wedge \frac{A}{4}\in ℂ\right)\to {\left(X+\left(\frac{A}{4}\right)\right)}^2=X^2+2X\left(\frac{A}{4}\right)+{\left(\frac{A}{4}\right)}^2$$
166	8 15 165	syl2anc	$$⊢\phi \to {\left(X+\left(\frac{A}{4}\right)\right)}^2=X^2+2X\left(\frac{A}{4}\right)+{\left(\frac{A}{4}\right)}^2$$
167	8 15	mulcld	$$⊢\phi \to X\left(\frac{A}{4}\right)\in ℂ$$
168		mulcl	$$⊢\left(2\in ℂ\wedge X\left(\frac{A}{4}\right)\in ℂ\right)\to 2X\left(\frac{A}{4}\right)\in ℂ$$
169	34 167 168	sylancr	$$⊢\phi \to 2X\left(\frac{A}{4}\right)\in ℂ$$
170	31 169 30	addassd	$$⊢\phi \to X^2+2X\left(\frac{A}{4}\right)+{\left(\frac{A}{4}\right)}^2=X^2+2X\left(\frac{A}{4}\right)+{\left(\frac{A}{4}\right)}^2$$
171	164 166 170	3eqtrd	$$⊢\phi \to Y^2=X^2+2X\left(\frac{A}{4}\right)+{\left(\frac{A}{4}\right)}^2$$
172	171	oveq2d	$$⊢\phi \to P{Y}^2=P\left(X^2+2X\left(\frac{A}{4}\right)+{\left(\frac{A}{4}\right)}^2\right)$$
173	169 30	addcld	$$⊢\phi \to 2X\left(\frac{A}{4}\right)+{\left(\frac{A}{4}\right)}^2\in ℂ$$
174	150 31 173	adddid	$$⊢\phi \to P\left(X^2+2X\left(\frac{A}{4}\right)+{\left(\frac{A}{4}\right)}^2\right)=P{X}^2+P\left(2X\left(\frac{A}{4}\right)+{\left(\frac{A}{4}\right)}^2\right)$$
175	172 174	eqtrd	$$⊢\phi \to P{Y}^2=P{X}^2+P\left(2X\left(\frac{A}{4}\right)+{\left(\frac{A}{4}\right)}^2\right)$$
176	175	oveq2d	$$⊢\phi \to \left(\frac{3}{8}\right)A^2{X}^2+\left(\left(\frac{\frac{A^3}{8}}{2}\right)X+\left(\frac{A^4}{256}\right)\right)+P{Y}^2=\left(\frac{3}{8}\right)A^2{X}^2+\left(\left(\frac{\frac{A^3}{8}}{2}\right)X+\left(\frac{A^4}{256}\right)\right)+P{X}^2+P\left(2X\left(\frac{A}{4}\right)+{\left(\frac{A}{4}\right)}^2\right)$$
177	150 31	mulcld	$$⊢\phi \to P{X}^2\in ℂ$$
178	150 173	mulcld	$$⊢\phi \to P\left(2X\left(\frac{A}{4}\right)+{\left(\frac{A}{4}\right)}^2\right)\in ℂ$$
179	133 147 177 178	add4d	$$⊢\phi \to \left(\frac{3}{8}\right)A^2{X}^2+\left(\left(\frac{\frac{A^3}{8}}{2}\right)X+\left(\frac{A^4}{256}\right)\right)+P{X}^2+P\left(2X\left(\frac{A}{4}\right)+{\left(\frac{A}{4}\right)}^2\right)=\left(\frac{3}{8}\right)A^2{X}^2+P{X}^2+\left(\left(\frac{\frac{A^3}{8}}{2}\right)X+\left(\frac{A^4}{256}\right)\right)+P\left(2X\left(\frac{A}{4}\right)+{\left(\frac{A}{4}\right)}^2\right)$$
180	132 150 31	adddird	$$⊢\phi \to \left(\left(\frac{3}{8}\right)A^2+P\right)X^2=\left(\frac{3}{8}\right)A^2{X}^2+P{X}^2$$
181	5	oveq2d	$$⊢\phi \to \left(\frac{3}{8}\right)A^2+P=\left(\frac{3}{8}\right)A^2+B-\left(\frac{3}{8}\right)A^2$$
182	132 2	pncan3d	$$⊢\phi \to \left(\frac{3}{8}\right)A^2+B-\left(\frac{3}{8}\right)A^2=B$$
183	181 182	eqtrd	$$⊢\phi \to \left(\frac{3}{8}\right)A^2+P=B$$
184	183	oveq1d	$$⊢\phi \to \left(\left(\frac{3}{8}\right)A^2+P\right)X^2=B{X}^2$$
185	180 184	eqtr3d	$$⊢\phi \to \left(\frac{3}{8}\right)A^2{X}^2+P{X}^2=B{X}^2$$
186	185	oveq1d	$$⊢\phi \to \left(\frac{3}{8}\right)A^2{X}^2+P{X}^2+\left(\left(\frac{\frac{A^3}{8}}{2}\right)X+\left(\frac{A^4}{256}\right)\right)+P\left(2X\left(\frac{A}{4}\right)+{\left(\frac{A}{4}\right)}^2\right)=B{X}^2+\left(\left(\frac{\frac{A^3}{8}}{2}\right)X+\left(\frac{A^4}{256}\right)\right)+P\left(2X\left(\frac{A}{4}\right)+{\left(\frac{A}{4}\right)}^2\right)$$
187	176 179 186	3eqtrd	$$⊢\phi \to \left(\frac{3}{8}\right)A^2{X}^2+\left(\left(\frac{\frac{A^3}{8}}{2}\right)X+\left(\frac{A^4}{256}\right)\right)+P{Y}^2=B{X}^2+\left(\left(\frac{\frac{A^3}{8}}{2}\right)X+\left(\frac{A^4}{256}\right)\right)+P\left(2X\left(\frac{A}{4}\right)+{\left(\frac{A}{4}\right)}^2\right)$$
188	187	oveq1d	$$⊢\phi \to \left(\left(\frac{3}{8}\right)A^2{X}^2+\left(\frac{\frac{A^3}{8}}{2}\right)X+\left(\frac{A^4}{256}\right)\right)+P{Y}^2+QY+R=B{X}^2+\left(\left(\frac{\frac{A^3}{8}}{2}\right)X+\left(\frac{A^4}{256}\right)+P\left(2X\left(\frac{A}{4}\right)+{\left(\frac{A}{4}\right)}^2\right)\right)+QY+R$$
189	2 31	mulcld	$$⊢\phi \to B{X}^2\in ℂ$$
190	147 178	addcld	$$⊢\phi \to \left(\frac{\frac{A^3}{8}}{2}\right)X+\left(\frac{A^4}{256}\right)+P\left(2X\left(\frac{A}{4}\right)+{\left(\frac{A}{4}\right)}^2\right)\in ℂ$$
191	189 190 162	addassd	$$⊢\phi \to B{X}^2+\left(\left(\frac{\frac{A^3}{8}}{2}\right)X+\left(\frac{A^4}{256}\right)+P\left(2X\left(\frac{A}{4}\right)+{\left(\frac{A}{4}\right)}^2\right)\right)+QY+R=B{X}^2+\left(\left(\frac{\frac{A^3}{8}}{2}\right)X+\left(\frac{A^4}{256}\right)+P\left(2X\left(\frac{A}{4}\right)+{\left(\frac{A}{4}\right)}^2\right)\right)+\left(QY+R\right)$$
192	1 2	mulcld	$$⊢\phi \to AB\in ℂ$$
193	192	halfcld	$$⊢\phi \to \frac{AB}{2}\in ℂ$$
194	193 134	subcld	$$⊢\phi \to \left(\frac{AB}{2}\right)-\left(\frac{A^3}{8}\right)\in ℂ$$
195	194 8	mulcld	$$⊢\phi \to \left(\left(\frac{AB}{2}\right)-\left(\frac{A^3}{8}\right)\right)X\in ℂ$$
196	150 30	mulcld	$$⊢\phi \to P{\left(\frac{A}{4}\right)}^2\in ℂ$$
197	146 196	addcld	$$⊢\phi \to \left(\frac{A^4}{256}\right)+P{\left(\frac{A}{4}\right)}^2\in ℂ$$
198	159 8	mulcld	$$⊢\phi \to QX\in ℂ$$
199	159 15	mulcld	$$⊢\phi \to Q\left(\frac{A}{4}\right)\in ℂ$$
200	199 161	addcld	$$⊢\phi \to Q\left(\frac{A}{4}\right)+R\in ℂ$$
201	195 197 198 200	add4d	$$⊢\phi \to \left(\left(\frac{AB}{2}\right)-\left(\frac{A^3}{8}\right)\right)X+\left(\left(\frac{A^4}{256}\right)+P{\left(\frac{A}{4}\right)}^2\right)+QX+\left(Q\left(\frac{A}{4}\right)+R\right)=\left(\left(\frac{AB}{2}\right)-\left(\frac{A^3}{8}\right)\right)X+QX+\left(\left(\frac{A^4}{256}\right)+P{\left(\frac{A}{4}\right)}^2\right)+\left(Q\left(\frac{A}{4}\right)+R\right)$$
202	150 169 30	adddid	$$⊢\phi \to P\left(2X\left(\frac{A}{4}\right)+{\left(\frac{A}{4}\right)}^2\right)=P2X\left(\frac{A}{4}\right)+P{\left(\frac{A}{4}\right)}^2$$
203	202	oveq2d	$$⊢\phi \to \left(\frac{\frac{A^3}{8}}{2}\right)X+\left(\frac{A^4}{256}\right)+P\left(2X\left(\frac{A}{4}\right)+{\left(\frac{A}{4}\right)}^2\right)=\left(\frac{\frac{A^3}{8}}{2}\right)X+\left(\frac{A^4}{256}\right)+P2X\left(\frac{A}{4}\right)+P{\left(\frac{A}{4}\right)}^2$$
204	150 169	mulcld	$$⊢\phi \to P2X\left(\frac{A}{4}\right)\in ℂ$$
205	136 146 204 196	add4d	$$⊢\phi \to \left(\frac{\frac{A^3}{8}}{2}\right)X+\left(\frac{A^4}{256}\right)+P2X\left(\frac{A}{4}\right)+P{\left(\frac{A}{4}\right)}^2=\left(\frac{\frac{A^3}{8}}{2}\right)X+P2X\left(\frac{A}{4}\right)+\left(\frac{A^4}{256}\right)+P{\left(\frac{A}{4}\right)}^2$$
206	1 95 95 98 98	divdiv1d	$$⊢\phi \to \frac{\frac{A}{2}}{2}=\frac{A}{2\cdot 2}$$
207		2t2e4	$$⊢2\cdot 2=4$$
208	207	oveq2i	$$⊢\frac{A}{2\cdot 2}=\frac{A}{4}$$
209	206 208	eqtrdi	$$⊢\phi \to \frac{\frac{A}{2}}{2}=\frac{A}{4}$$
210	209	oveq2d	$$⊢\phi \to 2\left(\frac{\frac{A}{2}}{2}\right)=2\left(\frac{A}{4}\right)$$
211	1	halfcld	$$⊢\phi \to \frac{A}{2}\in ℂ$$
212	211 95 98	divcan2d	$$⊢\phi \to 2\left(\frac{\frac{A}{2}}{2}\right)=\frac{A}{2}$$
213	210 212	eqtr3d	$$⊢\phi \to 2\left(\frac{A}{4}\right)=\frac{A}{2}$$
214	213	oveq2d	$$⊢\phi \to X2\left(\frac{A}{4}\right)=X\left(\frac{A}{2}\right)$$
215	8 211	mulcomd	$$⊢\phi \to X\left(\frac{A}{2}\right)=\left(\frac{A}{2}\right)X$$
216	214 215	eqtrd	$$⊢\phi \to X2\left(\frac{A}{4}\right)=\left(\frac{A}{2}\right)X$$
217	216	oveq2d	$$⊢\phi \to PX2\left(\frac{A}{4}\right)=P\left(\frac{A}{2}\right)X$$
218	95 8 15	mul12d	$$⊢\phi \to 2X\left(\frac{A}{4}\right)=X2\left(\frac{A}{4}\right)$$
219	218	oveq2d	$$⊢\phi \to P2X\left(\frac{A}{4}\right)=PX2\left(\frac{A}{4}\right)$$
220	150 211 8	mulassd	$$⊢\phi \to P\left(\frac{A}{2}\right)X=P\left(\frac{A}{2}\right)X$$
221	217 219 220	3eqtr4d	$$⊢\phi \to P2X\left(\frac{A}{4}\right)=P\left(\frac{A}{2}\right)X$$
222	221	oveq2d	$$⊢\phi \to \left(\frac{\frac{A^3}{8}}{2}\right)X+P2X\left(\frac{A}{4}\right)=\left(\frac{\frac{A^3}{8}}{2}\right)X+P\left(\frac{A}{2}\right)X$$
223	150 211	mulcld	$$⊢\phi \to P\left(\frac{A}{2}\right)\in ℂ$$
224	135 223 8	adddird	$$⊢\phi \to \left(\left(\frac{\frac{A^3}{8}}{2}\right)+P\left(\frac{A}{2}\right)\right)X=\left(\frac{\frac{A^3}{8}}{2}\right)X+P\left(\frac{A}{2}\right)X$$
225	5	oveq1d	$$⊢\phi \to P\left(\frac{A}{2}\right)=\left(B-\left(\frac{3}{8}\right)A^2\right)\left(\frac{A}{2}\right)$$
226	2 132 211	subdird	$$⊢\phi \to \left(B-\left(\frac{3}{8}\right)A^2\right)\left(\frac{A}{2}\right)=B\left(\frac{A}{2}\right)-\left(\frac{3}{8}\right)A^2\left(\frac{A}{2}\right)$$
227	2 1 95 98	divassd	$$⊢\phi \to \frac{BA}{2}=B\left(\frac{A}{2}\right)$$
228	2 1	mulcomd	$$⊢\phi \to BA=AB$$
229	228	oveq1d	$$⊢\phi \to \frac{BA}{2}=\frac{AB}{2}$$
230	227 229	eqtr3d	$$⊢\phi \to B\left(\frac{A}{2}\right)=\frac{AB}{2}$$
231	78	oveq2i	$$⊢A^3=A^{2+1}$$
232		expp1	$$⊢\left(A\in ℂ\wedge 2\in {\mathbb{N}}_0\right)\to A^{2+1}=A^{2}A$$
233	1 80 232	sylancl	$$⊢\phi \to A^{2+1}=A^{2}A$$
234	231 233	eqtrid	$$⊢\phi \to A^3=A^{2}A$$
235	234	oveq2d	$$⊢\phi \to \left(\frac{3}{8}\right)A^3=\left(\frac{3}{8}\right)A^{2}A$$
236	33	a1i	$$⊢\phi \to 3\in ℂ$$
237	236 89 94 96	div23d	$$⊢\phi \to \frac{3A^3}{8}=\left(\frac{3}{8}\right)A^3$$
238	58	a1i	$$⊢\phi \to \frac{3}{8}\in ℂ$$
239	238 49 1	mulassd	$$⊢\phi \to \left(\frac{3}{8}\right)A^{2}A=\left(\frac{3}{8}\right)A^{2}A$$
240	235 237 239	3eqtr4rd	$$⊢\phi \to \left(\frac{3}{8}\right)A^{2}A=\frac{3A^3}{8}$$
241	236 89 94 96	divassd	$$⊢\phi \to \frac{3A^3}{8}=3\left(\frac{A^3}{8}\right)$$
242	240 241	eqtrd	$$⊢\phi \to \left(\frac{3}{8}\right)A^{2}A=3\left(\frac{A^3}{8}\right)$$
243	242	oveq1d	$$⊢\phi \to \frac{\left(\frac{3}{8}\right)A^{2}A}{2}=\frac{3\left(\frac{A^3}{8}\right)}{2}$$
244	132 1 95 98	divassd	$$⊢\phi \to \frac{\left(\frac{3}{8}\right)A^{2}A}{2}=\left(\frac{3}{8}\right)A^2\left(\frac{A}{2}\right)$$
245	236 134 95 98	divassd	$$⊢\phi \to \frac{3\left(\frac{A^3}{8}\right)}{2}=3\left(\frac{\frac{A^3}{8}}{2}\right)$$
246	243 244 245	3eqtr3d	$$⊢\phi \to \left(\frac{3}{8}\right)A^2\left(\frac{A}{2}\right)=3\left(\frac{\frac{A^3}{8}}{2}\right)$$
247	230 246	oveq12d	$$⊢\phi \to B\left(\frac{A}{2}\right)-\left(\frac{3}{8}\right)A^2\left(\frac{A}{2}\right)=\left(\frac{AB}{2}\right)-3\left(\frac{\frac{A^3}{8}}{2}\right)$$
248	225 226 247	3eqtrd	$$⊢\phi \to P\left(\frac{A}{2}\right)=\left(\frac{AB}{2}\right)-3\left(\frac{\frac{A^3}{8}}{2}\right)$$
249	248	oveq2d	$$⊢\phi \to \left(\frac{\frac{A^3}{8}}{2}\right)+P\left(\frac{A}{2}\right)=\left(\frac{\frac{A^3}{8}}{2}\right)+\left(\frac{AB}{2}\right)-3\left(\frac{\frac{A^3}{8}}{2}\right)$$
250		mulcl	$$⊢\left(3\in ℂ\wedge \frac{\frac{A^3}{8}}{2}\in ℂ\right)\to 3\left(\frac{\frac{A^3}{8}}{2}\right)\in ℂ$$
251	33 135 250	sylancr	$$⊢\phi \to 3\left(\frac{\frac{A^3}{8}}{2}\right)\in ℂ$$
252	135 193 251	addsub12d	$$⊢\phi \to \left(\frac{\frac{A^3}{8}}{2}\right)+\left(\frac{AB}{2}\right)-3\left(\frac{\frac{A^3}{8}}{2}\right)=\left(\frac{AB}{2}\right)+\left(\frac{\frac{A^3}{8}}{2}\right)-3\left(\frac{\frac{A^3}{8}}{2}\right)$$
253	193 251 135	subsub2d	$$⊢\phi \to \left(\frac{AB}{2}\right)-\left(3\left(\frac{\frac{A^3}{8}}{2}\right)-\left(\frac{\frac{A^3}{8}}{2}\right)\right)=\left(\frac{AB}{2}\right)+\left(\frac{\frac{A^3}{8}}{2}\right)-3\left(\frac{\frac{A^3}{8}}{2}\right)$$
254	135	mulid2d	$$⊢\phi \to 1\left(\frac{\frac{A^3}{8}}{2}\right)=\frac{\frac{A^3}{8}}{2}$$
255	254	oveq2d	$$⊢\phi \to 3\left(\frac{\frac{A^3}{8}}{2}\right)-1\left(\frac{\frac{A^3}{8}}{2}\right)=3\left(\frac{\frac{A^3}{8}}{2}\right)-\left(\frac{\frac{A^3}{8}}{2}\right)$$
256		3m1e2	$$⊢3-1=2$$
257	256	oveq1i	$$⊢\left(3-1\right)\left(\frac{\frac{A^3}{8}}{2}\right)=2\left(\frac{\frac{A^3}{8}}{2}\right)$$
258		1cnd	$$⊢\phi \to 1\in ℂ$$
259	236 258 135	subdird	$$⊢\phi \to \left(3-1\right)\left(\frac{\frac{A^3}{8}}{2}\right)=3\left(\frac{\frac{A^3}{8}}{2}\right)-1\left(\frac{\frac{A^3}{8}}{2}\right)$$
260	134 95 98	divcan2d	$$⊢\phi \to 2\left(\frac{\frac{A^3}{8}}{2}\right)=\frac{A^3}{8}$$
261	257 259 260	3eqtr3a	$$⊢\phi \to 3\left(\frac{\frac{A^3}{8}}{2}\right)-1\left(\frac{\frac{A^3}{8}}{2}\right)=\frac{A^3}{8}$$
262	255 261	eqtr3d	$$⊢\phi \to 3\left(\frac{\frac{A^3}{8}}{2}\right)-\left(\frac{\frac{A^3}{8}}{2}\right)=\frac{A^3}{8}$$
263	262	oveq2d	$$⊢\phi \to \left(\frac{AB}{2}\right)-\left(3\left(\frac{\frac{A^3}{8}}{2}\right)-\left(\frac{\frac{A^3}{8}}{2}\right)\right)=\left(\frac{AB}{2}\right)-\left(\frac{A^3}{8}\right)$$
264	252 253 263	3eqtr2d	$$⊢\phi \to \left(\frac{\frac{A^3}{8}}{2}\right)+\left(\frac{AB}{2}\right)-3\left(\frac{\frac{A^3}{8}}{2}\right)=\left(\frac{AB}{2}\right)-\left(\frac{A^3}{8}\right)$$
265	249 264	eqtrd	$$⊢\phi \to \left(\frac{\frac{A^3}{8}}{2}\right)+P\left(\frac{A}{2}\right)=\left(\frac{AB}{2}\right)-\left(\frac{A^3}{8}\right)$$
266	265	oveq1d	$$⊢\phi \to \left(\left(\frac{\frac{A^3}{8}}{2}\right)+P\left(\frac{A}{2}\right)\right)X=\left(\left(\frac{AB}{2}\right)-\left(\frac{A^3}{8}\right)\right)X$$
267	222 224 266	3eqtr2d	$$⊢\phi \to \left(\frac{\frac{A^3}{8}}{2}\right)X+P2X\left(\frac{A}{4}\right)=\left(\left(\frac{AB}{2}\right)-\left(\frac{A^3}{8}\right)\right)X$$
268	267	oveq1d	$$⊢\phi \to \left(\frac{\frac{A^3}{8}}{2}\right)X+P2X\left(\frac{A}{4}\right)+\left(\frac{A^4}{256}\right)+P{\left(\frac{A}{4}\right)}^2=\left(\left(\frac{AB}{2}\right)-\left(\frac{A^3}{8}\right)\right)X+\left(\frac{A^4}{256}\right)+P{\left(\frac{A}{4}\right)}^2$$
269	203 205 268	3eqtrd	$$⊢\phi \to \left(\frac{\frac{A^3}{8}}{2}\right)X+\left(\frac{A^4}{256}\right)+P\left(2X\left(\frac{A}{4}\right)+{\left(\frac{A}{4}\right)}^2\right)=\left(\left(\frac{AB}{2}\right)-\left(\frac{A^3}{8}\right)\right)X+\left(\frac{A^4}{256}\right)+P{\left(\frac{A}{4}\right)}^2$$
270	9	oveq2d	$$⊢\phi \to QY=Q\left(X+\left(\frac{A}{4}\right)\right)$$
271	159 8 15	adddid	$$⊢\phi \to Q\left(X+\left(\frac{A}{4}\right)\right)=QX+Q\left(\frac{A}{4}\right)$$
272	270 271	eqtrd	$$⊢\phi \to QY=QX+Q\left(\frac{A}{4}\right)$$
273	272	oveq1d	$$⊢\phi \to QY+R=QX+Q\left(\frac{A}{4}\right)+R$$
274	198 199 161	addassd	$$⊢\phi \to QX+Q\left(\frac{A}{4}\right)+R=QX+Q\left(\frac{A}{4}\right)+R$$
275	273 274	eqtrd	$$⊢\phi \to QY+R=QX+Q\left(\frac{A}{4}\right)+R$$
276	269 275	oveq12d	$$⊢\phi \to \left(\left(\frac{\frac{A^3}{8}}{2}\right)X+\left(\frac{A^4}{256}\right)\right)+P\left(2X\left(\frac{A}{4}\right)+{\left(\frac{A}{4}\right)}^2\right)+QY+R=\left(\left(\frac{AB}{2}\right)-\left(\frac{A^3}{8}\right)\right)X+\left(\left(\frac{A^4}{256}\right)+P{\left(\frac{A}{4}\right)}^2\right)+QX+\left(Q\left(\frac{A}{4}\right)+R\right)$$
277	194 159	addcomd	$$⊢\phi \to \left(\frac{AB}{2}\right)-\left(\frac{A^3}{8}\right)+Q=Q+\left(\frac{AB}{2}\right)-\left(\frac{A^3}{8}\right)$$
278	6	oveq1d	$$⊢\phi \to Q+\left(\frac{AB}{2}\right)-\left(\frac{A^3}{8}\right)=\left(C-\left(\frac{AB}{2}\right)\right)+\left(\frac{A^3}{8}\right)+\left(\left(\frac{AB}{2}\right)-\left(\frac{A^3}{8}\right)\right)$$
279	3 193	subcld	$$⊢\phi \to C-\left(\frac{AB}{2}\right)\in ℂ$$
280	279 134 193	ppncand	$$⊢\phi \to \left(C-\left(\frac{AB}{2}\right)\right)+\left(\frac{A^3}{8}\right)+\left(\left(\frac{AB}{2}\right)-\left(\frac{A^3}{8}\right)\right)=C-\left(\frac{AB}{2}\right)+\left(\frac{AB}{2}\right)$$
281	3 193	npcand	$$⊢\phi \to C-\left(\frac{AB}{2}\right)+\left(\frac{AB}{2}\right)=C$$
282	280 281	eqtrd	$$⊢\phi \to \left(C-\left(\frac{AB}{2}\right)\right)+\left(\frac{A^3}{8}\right)+\left(\left(\frac{AB}{2}\right)-\left(\frac{A^3}{8}\right)\right)=C$$
283	277 278 282	3eqtrd	$$⊢\phi \to \left(\frac{AB}{2}\right)-\left(\frac{A^3}{8}\right)+Q=C$$
284	283	oveq1d	$$⊢\phi \to \left(\left(\frac{AB}{2}\right)-\left(\frac{A^3}{8}\right)+Q\right)X=CX$$
285	194 159 8	adddird	$$⊢\phi \to \left(\left(\frac{AB}{2}\right)-\left(\frac{A^3}{8}\right)+Q\right)X=\left(\left(\frac{AB}{2}\right)-\left(\frac{A^3}{8}\right)\right)X+QX$$
286	284 285	eqtr3d	$$⊢\phi \to CX=\left(\left(\frac{AB}{2}\right)-\left(\frac{A^3}{8}\right)\right)X+QX$$
287	1 2 3 4 5 6 7 8 9	quart1lem	$$⊢\phi \to D=\left(\frac{A^4}{256}\right)+P{\left(\frac{A}{4}\right)}^2+Q\left(\frac{A}{4}\right)+R$$
288	286 287	oveq12d	$$⊢\phi \to CX+D=\left(\left(\frac{AB}{2}\right)-\left(\frac{A^3}{8}\right)\right)X+QX+\left(\left(\frac{A^4}{256}\right)+P{\left(\frac{A}{4}\right)}^2\right)+\left(Q\left(\frac{A}{4}\right)+R\right)$$
289	201 276 288	3eqtr4d	$$⊢\phi \to \left(\left(\frac{\frac{A^3}{8}}{2}\right)X+\left(\frac{A^4}{256}\right)\right)+P\left(2X\left(\frac{A}{4}\right)+{\left(\frac{A}{4}\right)}^2\right)+QY+R=CX+D$$
290	289	oveq2d	$$⊢\phi \to B{X}^2+\left(\left(\frac{\frac{A^3}{8}}{2}\right)X+\left(\frac{A^4}{256}\right)+P\left(2X\left(\frac{A}{4}\right)+{\left(\frac{A}{4}\right)}^2\right)\right)+\left(QY+R\right)=B{X}^2+CX+D$$
291	188 191 290	3eqtrd	$$⊢\phi \to \left(\left(\frac{3}{8}\right)A^2{X}^2+\left(\frac{\frac{A^3}{8}}{2}\right)X+\left(\frac{A^4}{256}\right)\right)+P{Y}^2+QY+R=B{X}^2+CX+D$$
292	291	oveq2d	$$⊢\phi \to X^4+A{X}^3+\left(\left(\frac{3}{8}\right)A^2{X}^2+\left(\left(\frac{\frac{A^3}{8}}{2}\right)X+\left(\frac{A^4}{256}\right)\right)+P{Y}^2\right)+\left(QY+R\right)=X^4+A{X}^3+B{X}^2+\left(CX+D\right)$$
293	157 163 292	3eqtrrd	$$⊢\phi \to X^4+A{X}^3+B{X}^2+\left(CX+D\right)=Y^4+P{Y}^2+QY+R$$