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