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		4t2e8	$$⊢4\cdot 2=8$$
111	11 35 110	mulcomli	$$⊢2\cdot 4=8$$
112	111	oveq2i	$$⊢2^{2\cdot 4}=2^8$$
113	109 112	eqtr3i	$$⊢{\left(2^2\right)}^4=2^8$$
114		sq2	$$⊢2^2=4$$
115	114	oveq1i	$$⊢{\left(2^2\right)}^4=4^4$$
116	113 115	eqtr3i	$$⊢2^8=4^4$$
117		2exp8	$$⊢2^8=256$$
118	116 117	eqtr3i	$$⊢4^4=256$$
119	118	oveq2i	$$⊢\frac{A^4}{4^4}=\frac{A^4}{256}$$
120	107 119	eqtrdi	$$⊢\phi \to {\left(\frac{A}{4}\right)}^4=\frac{A^4}{256}$$
121	104 120	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)$$
122	71 121	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)$$
123	26 122	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)$$
124	10 17 123	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)$$
125	124	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$$
126		expcl	$$⊢\left(X\in ℂ\wedge 4\in {\mathbb{N}}_0\right)\to X^4\in ℂ$$
127	8 105 126	sylancl	$$⊢\phi \to X^4\in ℂ$$
128	1 20	mulcld	$$⊢\phi \to A{X}^3\in ℂ$$
129	127 128	addcld	$$⊢\phi \to X^4+A{X}^3\in ℂ$$
130		mulcl	$$⊢\left(\frac{3}{8}\in ℂ\wedge A^2\in ℂ\right)\to \left(\frac{3}{8}\right)A^2\in ℂ$$
131	57 48 130	sylancr	$$⊢\phi \to \left(\frac{3}{8}\right)A^2\in ℂ$$
132	131 31	mulcld	$$⊢\phi \to \left(\frac{3}{8}\right)A^2{X}^2\in ℂ$$
133	88 93 95	divcld	$$⊢\phi \to \frac{A^3}{8}\in ℂ$$
134	133	halfcld	$$⊢\phi \to \frac{\frac{A^3}{8}}{2}\in ℂ$$
135	134 8	mulcld	$$⊢\phi \to \left(\frac{\frac{A^3}{8}}{2}\right)X\in ℂ$$
136		expcl	$$⊢\left(A\in ℂ\wedge 4\in {\mathbb{N}}_0\right)\to A^4\in ℂ$$
137	1 105 136	sylancl	$$⊢\phi \to A^4\in ℂ$$
138		5nn0	$$⊢5\in {\mathbb{N}}_0$$
139	79 138	deccl	$$⊢25\in {\mathbb{N}}_0$$
140	139 27	decnncl	$$⊢256\in \mathbb{N}$$
141	140	nncni	$$⊢256\in ℂ$$
142	141	a1i	$$⊢\phi \to 256\in ℂ$$
143	140	nnne0i	$$⊢256\ne 0$$
144	143	a1i	$$⊢\phi \to 256\ne 0$$
145	137 142 144	divcld	$$⊢\phi \to \frac{A^4}{256}\in ℂ$$
146	135 145	addcld	$$⊢\phi \to \left(\frac{\frac{A^3}{8}}{2}\right)X+\left(\frac{A^4}{256}\right)\in ℂ$$
147	132 146	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 ℂ$$
148	1 2 3 4 5 6 7	quart1cl	$$⊢\phi \to \left(P\in ℂ\wedge Q\in ℂ\wedge R\in ℂ\right)$$
149	148	simp1d	$$⊢\phi \to P\in ℂ$$
150	8 15	addcld	$$⊢\phi \to X+\left(\frac{A}{4}\right)\in ℂ$$
151	9 150	eqeltrd	$$⊢\phi \to Y\in ℂ$$
152	151	sqcld	$$⊢\phi \to Y^2\in ℂ$$
153	149 152	mulcld	$$⊢\phi \to P{Y}^2\in ℂ$$
154	129 147 153	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$$
155	125 154	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$$
156	155	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$$
157	147 153	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 ℂ$$
158	148	simp2d	$$⊢\phi \to Q\in ℂ$$
159	158 151	mulcld	$$⊢\phi \to QY\in ℂ$$
160	148	simp3d	$$⊢\phi \to R\in ℂ$$
161	159 160	addcld	$$⊢\phi \to QY+R\in ℂ$$
162	129 157 161	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)$$
163	9	oveq1d	$$⊢\phi \to Y^2={\left(X+\left(\frac{A}{4}\right)\right)}^2$$
164		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$$
165	8 15 164	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$$
166	8 15	mulcld	$$⊢\phi \to X\left(\frac{A}{4}\right)\in ℂ$$
167		mulcl	$$⊢\left(2\in ℂ\wedge X\left(\frac{A}{4}\right)\in ℂ\right)\to 2X\left(\frac{A}{4}\right)\in ℂ$$
168	35 166 167	sylancr	$$⊢\phi \to 2X\left(\frac{A}{4}\right)\in ℂ$$
169	31 168 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$$
170	163 165 169	3eqtrd	$$⊢\phi \to Y^2=X^2+2X\left(\frac{A}{4}\right)+{\left(\frac{A}{4}\right)}^2$$
171	170	oveq2d	$$⊢\phi \to P{Y}^2=P\left(X^2+2X\left(\frac{A}{4}\right)+{\left(\frac{A}{4}\right)}^2\right)$$
172	168 30	addcld	$$⊢\phi \to 2X\left(\frac{A}{4}\right)+{\left(\frac{A}{4}\right)}^2\in ℂ$$
173	149 31 172	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)$$
174	171 173	eqtrd	$$⊢\phi \to P{Y}^2=P{X}^2+P\left(2X\left(\frac{A}{4}\right)+{\left(\frac{A}{4}\right)}^2\right)$$
175	174	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)$$
176	149 31	mulcld	$$⊢\phi \to P{X}^2\in ℂ$$
177	149 172	mulcld	$$⊢\phi \to P\left(2X\left(\frac{A}{4}\right)+{\left(\frac{A}{4}\right)}^2\right)\in ℂ$$
178	132 146 176 177	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)$$
179	131 149 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$$
180	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$$
181	131 2	pncan3d	$$⊢\phi \to \left(\frac{3}{8}\right)A^2+B-\left(\frac{3}{8}\right)A^2=B$$
182	180 181	eqtrd	$$⊢\phi \to \left(\frac{3}{8}\right)A^2+P=B$$
183	182	oveq1d	$$⊢\phi \to \left(\left(\frac{3}{8}\right)A^2+P\right)X^2=B{X}^2$$
184	179 183	eqtr3d	$$⊢\phi \to \left(\frac{3}{8}\right)A^2{X}^2+P{X}^2=B{X}^2$$
185	184	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)$$
186	175 178 185	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)$$
187	186	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$$
188	2 31	mulcld	$$⊢\phi \to B{X}^2\in ℂ$$
189	146 177	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 ℂ$$
190	188 189 161	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)$$
191	1 2	mulcld	$$⊢\phi \to AB\in ℂ$$
192	191	halfcld	$$⊢\phi \to \frac{AB}{2}\in ℂ$$
193	192 133	subcld	$$⊢\phi \to \left(\frac{AB}{2}\right)-\left(\frac{A^3}{8}\right)\in ℂ$$
194	193 8	mulcld	$$⊢\phi \to \left(\left(\frac{AB}{2}\right)-\left(\frac{A^3}{8}\right)\right)X\in ℂ$$
195	149 30	mulcld	$$⊢\phi \to P{\left(\frac{A}{4}\right)}^2\in ℂ$$
196	145 195	addcld	$$⊢\phi \to \left(\frac{A^4}{256}\right)+P{\left(\frac{A}{4}\right)}^2\in ℂ$$
197	158 8	mulcld	$$⊢\phi \to QX\in ℂ$$
198	158 15	mulcld	$$⊢\phi \to Q\left(\frac{A}{4}\right)\in ℂ$$
199	198 160	addcld	$$⊢\phi \to Q\left(\frac{A}{4}\right)+R\in ℂ$$
200	194 196 197 199	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)$$
201	149 168 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$$
202	201	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$$
203	149 168	mulcld	$$⊢\phi \to P2X\left(\frac{A}{4}\right)\in ℂ$$
204	135 145 203 195	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$$
205	1 94 94 97 97	divdiv1d	$$⊢\phi \to \frac{\frac{A}{2}}{2}=\frac{A}{2\cdot 2}$$
206		2t2e4	$$⊢2\cdot 2=4$$
207	206	oveq2i	$$⊢\frac{A}{2\cdot 2}=\frac{A}{4}$$
208	205 207	eqtrdi	$$⊢\phi \to \frac{\frac{A}{2}}{2}=\frac{A}{4}$$
209	208	oveq2d	$$⊢\phi \to 2\left(\frac{\frac{A}{2}}{2}\right)=2\left(\frac{A}{4}\right)$$
210	1	halfcld	$$⊢\phi \to \frac{A}{2}\in ℂ$$
211	210 94 97	divcan2d	$$⊢\phi \to 2\left(\frac{\frac{A}{2}}{2}\right)=\frac{A}{2}$$
212	209 211	eqtr3d	$$⊢\phi \to 2\left(\frac{A}{4}\right)=\frac{A}{2}$$
213	212	oveq2d	$$⊢\phi \to X2\left(\frac{A}{4}\right)=X\left(\frac{A}{2}\right)$$
214	8 210	mulcomd	$$⊢\phi \to X\left(\frac{A}{2}\right)=\left(\frac{A}{2}\right)X$$
215	213 214	eqtrd	$$⊢\phi \to X2\left(\frac{A}{4}\right)=\left(\frac{A}{2}\right)X$$
216	215	oveq2d	$$⊢\phi \to PX2\left(\frac{A}{4}\right)=P\left(\frac{A}{2}\right)X$$
217	94 8 15	mul12d	$$⊢\phi \to 2X\left(\frac{A}{4}\right)=X2\left(\frac{A}{4}\right)$$
218	217	oveq2d	$$⊢\phi \to P2X\left(\frac{A}{4}\right)=PX2\left(\frac{A}{4}\right)$$
219	149 210 8	mulassd	$$⊢\phi \to P\left(\frac{A}{2}\right)X=P\left(\frac{A}{2}\right)X$$
220	216 218 219	3eqtr4d	$$⊢\phi \to P2X\left(\frac{A}{4}\right)=P\left(\frac{A}{2}\right)X$$
221	220	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$$
222	149 210	mulcld	$$⊢\phi \to P\left(\frac{A}{2}\right)\in ℂ$$
223	134 222 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$$
224	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)$$
225	2 131 210	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)$$
226	2 1 94 97	divassd	$$⊢\phi \to \frac{BA}{2}=B\left(\frac{A}{2}\right)$$
227	2 1	mulcomd	$$⊢\phi \to BA=AB$$
228	227	oveq1d	$$⊢\phi \to \frac{BA}{2}=\frac{AB}{2}$$
229	226 228	eqtr3d	$$⊢\phi \to B\left(\frac{A}{2}\right)=\frac{AB}{2}$$
230	77	oveq2i	$$⊢A^3=A^{2+1}$$
231		expp1	$$⊢\left(A\in ℂ\wedge 2\in {\mathbb{N}}_0\right)\to A^{2+1}=A^{2}A$$
232	1 79 231	sylancl	$$⊢\phi \to A^{2+1}=A^{2}A$$
233	230 232	eqtrid	$$⊢\phi \to A^3=A^{2}A$$
234	233	oveq2d	$$⊢\phi \to \left(\frac{3}{8}\right)A^3=\left(\frac{3}{8}\right)A^{2}A$$
235	39	a1i	$$⊢\phi \to 3\in ℂ$$
236	235 88 93 95	div23d	$$⊢\phi \to \frac{3A^3}{8}=\left(\frac{3}{8}\right)A^3$$
237	57	a1i	$$⊢\phi \to \frac{3}{8}\in ℂ$$
238	237 48 1	mulassd	$$⊢\phi \to \left(\frac{3}{8}\right)A^{2}A=\left(\frac{3}{8}\right)A^{2}A$$
239	234 236 238	3eqtr4rd	$$⊢\phi \to \left(\frac{3}{8}\right)A^{2}A=\frac{3A^3}{8}$$
240	235 88 93 95	divassd	$$⊢\phi \to \frac{3A^3}{8}=3\left(\frac{A^3}{8}\right)$$
241	239 240	eqtrd	$$⊢\phi \to \left(\frac{3}{8}\right)A^{2}A=3\left(\frac{A^3}{8}\right)$$
242	241	oveq1d	$$⊢\phi \to \frac{\left(\frac{3}{8}\right)A^{2}A}{2}=\frac{3\left(\frac{A^3}{8}\right)}{2}$$
243	131 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)$$
244	235 133 94 97	divassd	$$⊢\phi \to \frac{3\left(\frac{A^3}{8}\right)}{2}=3\left(\frac{\frac{A^3}{8}}{2}\right)$$
245	242 243 244	3eqtr3d	$$⊢\phi \to \left(\frac{3}{8}\right)A^2\left(\frac{A}{2}\right)=3\left(\frac{\frac{A^3}{8}}{2}\right)$$
246	229 245	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)$$
247	224 225 246	3eqtrd	$$⊢\phi \to P\left(\frac{A}{2}\right)=\left(\frac{AB}{2}\right)-3\left(\frac{\frac{A^3}{8}}{2}\right)$$
248	247	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)$$
249		mulcl	$$⊢\left(3\in ℂ\wedge \frac{\frac{A^3}{8}}{2}\in ℂ\right)\to 3\left(\frac{\frac{A^3}{8}}{2}\right)\in ℂ$$
250	39 134 249	sylancr	$$⊢\phi \to 3\left(\frac{\frac{A^3}{8}}{2}\right)\in ℂ$$
251	134 192 250	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)$$
252	192 250 134	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)$$
253	134	mullidd	$$⊢\phi \to 1\left(\frac{\frac{A^3}{8}}{2}\right)=\frac{\frac{A^3}{8}}{2}$$
254	253	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)$$
255		3m1e2	$$⊢3-1=2$$
256	255	oveq1i	$$⊢\left(3-1\right)\left(\frac{\frac{A^3}{8}}{2}\right)=2\left(\frac{\frac{A^3}{8}}{2}\right)$$
257		1cnd	$$⊢\phi \to 1\in ℂ$$
258	235 257 134	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)$$
259	133 94 97	divcan2d	$$⊢\phi \to 2\left(\frac{\frac{A^3}{8}}{2}\right)=\frac{A^3}{8}$$
260	256 258 259	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}$$
261	254 260	eqtr3d	$$⊢\phi \to 3\left(\frac{\frac{A^3}{8}}{2}\right)-\left(\frac{\frac{A^3}{8}}{2}\right)=\frac{A^3}{8}$$
262	261	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)$$
263	251 252 262	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)$$
264	248 263	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)$$
265	264	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$$
266	221 223 265	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$$
267	266	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$$
268	202 204 267	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$$
269	9	oveq2d	$$⊢\phi \to QY=Q\left(X+\left(\frac{A}{4}\right)\right)$$
270	158 8 15	adddid	$$⊢\phi \to Q\left(X+\left(\frac{A}{4}\right)\right)=QX+Q\left(\frac{A}{4}\right)$$
271	269 270	eqtrd	$$⊢\phi \to QY=QX+Q\left(\frac{A}{4}\right)$$
272	271	oveq1d	$$⊢\phi \to QY+R=QX+Q\left(\frac{A}{4}\right)+R$$
273	197 198 160	addassd	$$⊢\phi \to QX+Q\left(\frac{A}{4}\right)+R=QX+Q\left(\frac{A}{4}\right)+R$$
274	272 273	eqtrd	$$⊢\phi \to QY+R=QX+Q\left(\frac{A}{4}\right)+R$$
275	268 274	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)$$
276	193 158	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)$$
277	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)$$
278	3 192	subcld	$$⊢\phi \to C-\left(\frac{AB}{2}\right)\in ℂ$$
279	278 133 192	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)$$
280	3 192	npcand	$$⊢\phi \to C-\left(\frac{AB}{2}\right)+\left(\frac{AB}{2}\right)=C$$
281	279 280	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$$
282	276 277 281	3eqtrd	$$⊢\phi \to \left(\frac{AB}{2}\right)-\left(\frac{A^3}{8}\right)+Q=C$$
283	282	oveq1d	$$⊢\phi \to \left(\left(\frac{AB}{2}\right)-\left(\frac{A^3}{8}\right)+Q\right)X=CX$$
284	193 158 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$$
285	283 284	eqtr3d	$$⊢\phi \to CX=\left(\left(\frac{AB}{2}\right)-\left(\frac{A^3}{8}\right)\right)X+QX$$
286	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$$
287	285 286	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)$$
288	200 275 287	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$$
289	288	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$$
290	187 190 289	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$$
291	290	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)$$
292	156 162 291	3eqtrrd	$$⊢\phi \to X^4+A{X}^3+B{X}^2+\left(CX+D\right)=Y^4+P{Y}^2+QY+R$$