Theorem quart1lem

Description: Lemma for quart1 . (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	quart1lem	$$⊢\phi \to D=\left(\frac{A^4}{256}\right)+P{\left(\frac{A}{4}\right)}^2+Q\left(\frac{A}{4}\right)+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	1 2	mulcld	$$⊢\phi \to AB\in ℂ$$
11	10	halfcld	$$⊢\phi \to \frac{AB}{2}\in ℂ$$
12	3 11	subcld	$$⊢\phi \to C-\left(\frac{AB}{2}\right)\in ℂ$$
13		3nn0	$$⊢3\in {\mathbb{N}}_0$$
14		expcl	$$⊢\left(A\in ℂ\wedge 3\in {\mathbb{N}}_0\right)\to A^3\in ℂ$$
15	1 13 14	sylancl	$$⊢\phi \to A^3\in ℂ$$
16		8cn	$$⊢8\in ℂ$$
17	16	a1i	$$⊢\phi \to 8\in ℂ$$
18		8nn	$$⊢8\in \mathbb{N}$$
19	18	nnne0i	$$⊢8\ne 0$$
20	19	a1i	$$⊢\phi \to 8\ne 0$$
21	15 17 20	divcld	$$⊢\phi \to \frac{A^3}{8}\in ℂ$$
22		4cn	$$⊢4\in ℂ$$
23	22	a1i	$$⊢\phi \to 4\in ℂ$$
24		4ne0	$$⊢4\ne 0$$
25	24	a1i	$$⊢\phi \to 4\ne 0$$
26	1 23 25	divcld	$$⊢\phi \to \frac{A}{4}\in ℂ$$
27	12 21 26	adddird	$$⊢\phi \to \left(C-\left(\frac{AB}{2}\right)+\left(\frac{A^3}{8}\right)\right)\left(\frac{A}{4}\right)=\left(C-\left(\frac{AB}{2}\right)\right)\left(\frac{A}{4}\right)+\left(\frac{A^3}{8}\right)\left(\frac{A}{4}\right)$$
28	6	oveq1d	$$⊢\phi \to Q\left(\frac{A}{4}\right)=\left(C-\left(\frac{AB}{2}\right)+\left(\frac{A^3}{8}\right)\right)\left(\frac{A}{4}\right)$$
29	3 1 23 25	divassd	$$⊢\phi \to \frac{CA}{4}=C\left(\frac{A}{4}\right)$$
30	1	sqvald	$$⊢\phi \to A^2=AA$$
31	30	oveq1d	$$⊢\phi \to A^{2}B=AAB$$
32	1 1 2	mul32d	$$⊢\phi \to AAB=ABA$$
33	31 32	eqtrd	$$⊢\phi \to A^{2}B=ABA$$
34	33	oveq1d	$$⊢\phi \to \frac{A^{2}B}{8}=\frac{ABA}{8}$$
35		2cn	$$⊢2\in ℂ$$
36		4t2e8	$$⊢4\cdot 2=8$$
37	22 35 36	mulcomli	$$⊢2\cdot 4=8$$
38	37	oveq2i	$$⊢\frac{ABA}{2\cdot 4}=\frac{ABA}{8}$$
39	34 38	eqtr4di	$$⊢\phi \to \frac{A^{2}B}{8}=\frac{ABA}{2\cdot 4}$$
40	35	a1i	$$⊢\phi \to 2\in ℂ$$
41		2ne0	$$⊢2\ne 0$$
42	41	a1i	$$⊢\phi \to 2\ne 0$$
43	10 40 1 23 42 25	divmuldivd	$$⊢\phi \to \left(\frac{AB}{2}\right)\left(\frac{A}{4}\right)=\frac{ABA}{2\cdot 4}$$
44	39 43	eqtr4d	$$⊢\phi \to \frac{A^{2}B}{8}=\left(\frac{AB}{2}\right)\left(\frac{A}{4}\right)$$
45	29 44	oveq12d	$$⊢\phi \to \left(\frac{CA}{4}\right)-\left(\frac{A^{2}B}{8}\right)=C\left(\frac{A}{4}\right)-\left(\frac{AB}{2}\right)\left(\frac{A}{4}\right)$$
46	3 11 26	subdird	$$⊢\phi \to \left(C-\left(\frac{AB}{2}\right)\right)\left(\frac{A}{4}\right)=C\left(\frac{A}{4}\right)-\left(\frac{AB}{2}\right)\left(\frac{A}{4}\right)$$
47	45 46	eqtr4d	$$⊢\phi \to \left(\frac{CA}{4}\right)-\left(\frac{A^{2}B}{8}\right)=\left(C-\left(\frac{AB}{2}\right)\right)\left(\frac{A}{4}\right)$$
48		df-4	$$⊢4=3+1$$
49	48	oveq2i	$$⊢A^4=A^{3+1}$$
50		expp1	$$⊢\left(A\in ℂ\wedge 3\in {\mathbb{N}}_0\right)\to A^{3+1}=A^{3}A$$
51	1 13 50	sylancl	$$⊢\phi \to A^{3+1}=A^{3}A$$
52	49 51	eqtrid	$$⊢\phi \to A^4=A^{3}A$$
53	52	oveq1d	$$⊢\phi \to \frac{A^4}{8}=\frac{A^{3}A}{8}$$
54	15 1 17 20	div23d	$$⊢\phi \to \frac{A^{3}A}{8}=\left(\frac{A^3}{8}\right)A$$
55	53 54	eqtrd	$$⊢\phi \to \frac{A^4}{8}=\left(\frac{A^3}{8}\right)A$$
56	55	oveq1d	$$⊢\phi \to \frac{\frac{A^4}{8}}{4}=\frac{\left(\frac{A^3}{8}\right)A}{4}$$
57	21 1 23 25	divassd	$$⊢\phi \to \frac{\left(\frac{A^3}{8}\right)A}{4}=\left(\frac{A^3}{8}\right)\left(\frac{A}{4}\right)$$
58	56 57	eqtrd	$$⊢\phi \to \frac{\frac{A^4}{8}}{4}=\left(\frac{A^3}{8}\right)\left(\frac{A}{4}\right)$$
59	47 58	oveq12d	$$⊢\phi \to \left(\frac{CA}{4}\right)-\left(\frac{A^{2}B}{8}\right)+\left(\frac{\frac{A^4}{8}}{4}\right)=\left(C-\left(\frac{AB}{2}\right)\right)\left(\frac{A}{4}\right)+\left(\frac{A^3}{8}\right)\left(\frac{A}{4}\right)$$
60	27 28 59	3eqtr4d	$$⊢\phi \to Q\left(\frac{A}{4}\right)=\left(\frac{CA}{4}\right)-\left(\frac{A^{2}B}{8}\right)+\left(\frac{\frac{A^4}{8}}{4}\right)$$
61	3 1	mulcld	$$⊢\phi \to CA\in ℂ$$
62	61 23 25	divcld	$$⊢\phi \to \frac{CA}{4}\in ℂ$$
63	1	sqcld	$$⊢\phi \to A^2\in ℂ$$
64	63 2	mulcld	$$⊢\phi \to A^{2}B\in ℂ$$
65	64 17 20	divcld	$$⊢\phi \to \frac{A^{2}B}{8}\in ℂ$$
66		4nn0	$$⊢4\in {\mathbb{N}}_0$$
67		expcl	$$⊢\left(A\in ℂ\wedge 4\in {\mathbb{N}}_0\right)\to A^4\in ℂ$$
68	1 66 67	sylancl	$$⊢\phi \to A^4\in ℂ$$
69	68 17 20	divcld	$$⊢\phi \to \frac{A^4}{8}\in ℂ$$
70	69 23 25	divcld	$$⊢\phi \to \frac{\frac{A^4}{8}}{4}\in ℂ$$
71	62 65 70	subadd23d	$$⊢\phi \to \left(\frac{CA}{4}\right)-\left(\frac{A^{2}B}{8}\right)+\left(\frac{\frac{A^4}{8}}{4}\right)=\left(\frac{CA}{4}\right)+\left(\frac{\frac{A^4}{8}}{4}\right)-\left(\frac{A^{2}B}{8}\right)$$
72	70 65	subcld	$$⊢\phi \to \left(\frac{\frac{A^4}{8}}{4}\right)-\left(\frac{A^{2}B}{8}\right)\in ℂ$$
73	62 72	addcomd	$$⊢\phi \to \left(\frac{CA}{4}\right)+\left(\frac{\frac{A^4}{8}}{4}\right)-\left(\frac{A^{2}B}{8}\right)=\left(\frac{\frac{A^4}{8}}{4}\right)-\left(\frac{A^{2}B}{8}\right)+\left(\frac{CA}{4}\right)$$
74	60 71 73	3eqtrd	$$⊢\phi \to Q\left(\frac{A}{4}\right)=\left(\frac{\frac{A^4}{8}}{4}\right)-\left(\frac{A^{2}B}{8}\right)+\left(\frac{CA}{4}\right)$$
75		1nn0	$$⊢1\in {\mathbb{N}}_0$$
76		6nn	$$⊢6\in \mathbb{N}$$
77	75 76	decnncl	$$⊢16\in \mathbb{N}$$
78	77	nncni	$$⊢16\in ℂ$$
79	78	a1i	$$⊢\phi \to 16\in ℂ$$
80	77	nnne0i	$$⊢16\ne 0$$
81	80	a1i	$$⊢\phi \to 16\ne 0$$
82	64 79 81	divcld	$$⊢\phi \to \frac{A^{2}B}{16}\in ℂ$$
83		3cn	$$⊢3\in ℂ$$
84		2nn0	$$⊢2\in {\mathbb{N}}_0$$
85		5nn0	$$⊢5\in {\mathbb{N}}_0$$
86	84 85	deccl	$$⊢25\in {\mathbb{N}}_0$$
87	86 76	decnncl	$$⊢256\in \mathbb{N}$$
88	87	nncni	$$⊢256\in ℂ$$
89	87	nnne0i	$$⊢256\ne 0$$
90	83 88 89	divcli	$$⊢\frac{3}{256}\in ℂ$$
91		mulcl	$$⊢\left(\frac{3}{256}\in ℂ\wedge A^4\in ℂ\right)\to \left(\frac{3}{256}\right)A^4\in ℂ$$
92	90 68 91	sylancr	$$⊢\phi \to \left(\frac{3}{256}\right)A^4\in ℂ$$
93	82 92	subcld	$$⊢\phi \to \left(\frac{A^{2}B}{16}\right)-\left(\frac{3}{256}\right)A^4\in ℂ$$
94	4 93 62	addsubd	$$⊢\phi \to D+\left(\left(\frac{A^{2}B}{16}\right)-\left(\frac{3}{256}\right)A^4\right)-\left(\frac{CA}{4}\right)=\left(D-\left(\frac{CA}{4}\right)\right)+\left(\frac{A^{2}B}{16}\right)-\left(\frac{3}{256}\right)A^4$$
95	7 94	eqtr4d	$$⊢\phi \to R=D+\left(\left(\frac{A^{2}B}{16}\right)-\left(\frac{3}{256}\right)A^4\right)-\left(\frac{CA}{4}\right)$$
96	74 95	oveq12d	$$⊢\phi \to Q\left(\frac{A}{4}\right)+R=\left(\left(\frac{\frac{A^4}{8}}{4}\right)-\left(\frac{A^{2}B}{8}\right)\right)+\left(\frac{CA}{4}\right)+\left(D+\left(\left(\frac{A^{2}B}{16}\right)-\left(\frac{3}{256}\right)A^4\right)-\left(\frac{CA}{4}\right)\right)$$
97	4 93	addcld	$$⊢\phi \to D+\left(\frac{A^{2}B}{16}\right)-\left(\frac{3}{256}\right)A^4\in ℂ$$
98	72 62 97	ppncand	$$⊢\phi \to \left(\left(\frac{\frac{A^4}{8}}{4}\right)-\left(\frac{A^{2}B}{8}\right)\right)+\left(\frac{CA}{4}\right)+\left(D+\left(\left(\frac{A^{2}B}{16}\right)-\left(\frac{3}{256}\right)A^4\right)-\left(\frac{CA}{4}\right)\right)=\left(\left(\frac{\frac{A^4}{8}}{4}\right)-\left(\frac{A^{2}B}{8}\right)\right)+D+\left(\left(\frac{A^{2}B}{16}\right)-\left(\frac{3}{256}\right)A^4\right)$$
99	72 4 93	add12d	$$⊢\phi \to \left(\left(\frac{\frac{A^4}{8}}{4}\right)-\left(\frac{A^{2}B}{8}\right)\right)+D+\left(\left(\frac{A^{2}B}{16}\right)-\left(\frac{3}{256}\right)A^4\right)=D+\left(\left(\frac{\frac{A^4}{8}}{4}\right)-\left(\frac{A^{2}B}{8}\right)\right)+\left(\left(\frac{A^{2}B}{16}\right)-\left(\frac{3}{256}\right)A^4\right)$$
100	65 92	addcld	$$⊢\phi \to \left(\frac{A^{2}B}{8}\right)+\left(\frac{3}{256}\right)A^4\in ℂ$$
101	70 82	addcld	$$⊢\phi \to \left(\frac{\frac{A^4}{8}}{4}\right)+\left(\frac{A^{2}B}{16}\right)\in ℂ$$
102	100 101	negsubdi2d	$$⊢\phi \to -\left(\left(\frac{A^{2}B}{8}\right)+\left(\frac{3}{256}\right)A^4-\left(\left(\frac{\frac{A^4}{8}}{4}\right)+\left(\frac{A^{2}B}{16}\right)\right)\right)=\left(\frac{\frac{A^4}{8}}{4}\right)+\left(\frac{A^{2}B}{16}\right)-\left(\left(\frac{A^{2}B}{8}\right)+\left(\frac{3}{256}\right)A^4\right)$$
103	70 82	addcomd	$$⊢\phi \to \left(\frac{\frac{A^4}{8}}{4}\right)+\left(\frac{A^{2}B}{16}\right)=\left(\frac{A^{2}B}{16}\right)+\left(\frac{\frac{A^4}{8}}{4}\right)$$
104	103	oveq2d	$$⊢\phi \to \left(\frac{A^{2}B}{8}\right)+\left(\frac{3}{256}\right)A^4-\left(\left(\frac{\frac{A^4}{8}}{4}\right)+\left(\frac{A^{2}B}{16}\right)\right)=\left(\frac{A^{2}B}{8}\right)+\left(\frac{3}{256}\right)A^4-\left(\left(\frac{A^{2}B}{16}\right)+\left(\frac{\frac{A^4}{8}}{4}\right)\right)$$
105	65 92 82 70	addsub4d	$$⊢\phi \to \left(\frac{A^{2}B}{8}\right)+\left(\frac{3}{256}\right)A^4-\left(\left(\frac{A^{2}B}{16}\right)+\left(\frac{\frac{A^4}{8}}{4}\right)\right)=\left(\left(\frac{A^{2}B}{8}\right)-\left(\frac{A^{2}B}{16}\right)\right)+\left(\frac{3}{256}\right)A^4-\left(\frac{\frac{A^4}{8}}{4}\right)$$
106	83	a1i	$$⊢\phi \to 3\in ℂ$$
107	88	a1i	$$⊢\phi \to 256\in ℂ$$
108	89	a1i	$$⊢\phi \to 256\ne 0$$
109	106 68 107 108	divassd	$$⊢\phi \to \frac{3A^4}{256}=3\left(\frac{A^4}{256}\right)$$
110	106 68 107 108	div23d	$$⊢\phi \to \frac{3A^4}{256}=\left(\frac{3}{256}\right)A^4$$
111		1p2e3	$$⊢1+2=3$$
112	111	oveq1i	$$⊢\left(1+2\right)\left(\frac{A^4}{256}\right)=3\left(\frac{A^4}{256}\right)$$
113		1cnd	$$⊢\phi \to 1\in ℂ$$
114	68 107 108	divcld	$$⊢\phi \to \frac{A^4}{256}\in ℂ$$
115	113 40 114	adddird	$$⊢\phi \to \left(1+2\right)\left(\frac{A^4}{256}\right)=1\left(\frac{A^4}{256}\right)+2\left(\frac{A^4}{256}\right)$$
116	112 115	eqtr3id	$$⊢\phi \to 3\left(\frac{A^4}{256}\right)=1\left(\frac{A^4}{256}\right)+2\left(\frac{A^4}{256}\right)$$
117	114	mullidd	$$⊢\phi \to 1\left(\frac{A^4}{256}\right)=\frac{A^4}{256}$$
118	117	oveq1d	$$⊢\phi \to 1\left(\frac{A^4}{256}\right)+2\left(\frac{A^4}{256}\right)=\left(\frac{A^4}{256}\right)+2\left(\frac{A^4}{256}\right)$$
119	116 118	eqtrd	$$⊢\phi \to 3\left(\frac{A^4}{256}\right)=\left(\frac{A^4}{256}\right)+2\left(\frac{A^4}{256}\right)$$
120	109 110 119	3eqtr3d	$$⊢\phi \to \left(\frac{3}{256}\right)A^4=\left(\frac{A^4}{256}\right)+2\left(\frac{A^4}{256}\right)$$
121	48	oveq1i	$$⊢4\left(\frac{\frac{\frac{A^4}{8}}{4}}{4}\right)=\left(3+1\right)\left(\frac{\frac{\frac{A^4}{8}}{4}}{4}\right)$$
122	70 23 25	divcld	$$⊢\phi \to \frac{\frac{\frac{A^4}{8}}{4}}{4}\in ℂ$$
123	106 113 122	adddird	$$⊢\phi \to \left(3+1\right)\left(\frac{\frac{\frac{A^4}{8}}{4}}{4}\right)=3\left(\frac{\frac{\frac{A^4}{8}}{4}}{4}\right)+1\left(\frac{\frac{\frac{A^4}{8}}{4}}{4}\right)$$
124	121 123	eqtrid	$$⊢\phi \to 4\left(\frac{\frac{\frac{A^4}{8}}{4}}{4}\right)=3\left(\frac{\frac{\frac{A^4}{8}}{4}}{4}\right)+1\left(\frac{\frac{\frac{A^4}{8}}{4}}{4}\right)$$
125	70 23 25	divcan2d	$$⊢\phi \to 4\left(\frac{\frac{\frac{A^4}{8}}{4}}{4}\right)=\frac{\frac{A^4}{8}}{4}$$
126	122	mullidd	$$⊢\phi \to 1\left(\frac{\frac{\frac{A^4}{8}}{4}}{4}\right)=\frac{\frac{\frac{A^4}{8}}{4}}{4}$$
127	69 23 23 25 25	divdiv1d	$$⊢\phi \to \frac{\frac{\frac{A^4}{8}}{4}}{4}=\frac{\frac{A^4}{8}}{4\cdot 4}$$
128		4t4e16	$$⊢4\cdot 4=16$$
129	128	oveq2i	$$⊢\frac{\frac{A^4}{8}}{4\cdot 4}=\frac{\frac{A^4}{8}}{16}$$
130	127 129	eqtrdi	$$⊢\phi \to \frac{\frac{\frac{A^4}{8}}{4}}{4}=\frac{\frac{A^4}{8}}{16}$$
131	68 17 79 20 81	divdiv1d	$$⊢\phi \to \frac{\frac{A^4}{8}}{16}=\frac{A^4}{8\cdot 16}$$
132	16 78	mulcli	$$⊢8\cdot 16\in ℂ$$
133	132	a1i	$$⊢\phi \to 8\cdot 16\in ℂ$$
134	16 78 19 80	mulne0i	$$⊢8\cdot 16\ne 0$$
135	134	a1i	$$⊢\phi \to 8\cdot 16\ne 0$$
136	68 133 135	divcld	$$⊢\phi \to \frac{A^4}{8\cdot 16}\in ℂ$$
137	136 40 42	divcan2d	$$⊢\phi \to 2\left(\frac{\frac{A^4}{8\cdot 16}}{2}\right)=\frac{A^4}{8\cdot 16}$$
138	68 133 40 135 42	divdiv1d	$$⊢\phi \to \frac{\frac{A^4}{8\cdot 16}}{2}=\frac{A^4}{8\cdot 16\cdot 2}$$
139	16 78 35	mul32i	$$⊢8\cdot 16\cdot 2=8\cdot 2\cdot 16$$
140		2exp4	$$⊢2^4=16$$
141		8t2e16	$$⊢8\cdot 2=16$$
142	140 141	eqtr4i	$$⊢2^4=8\cdot 2$$
143	142 140	oveq12i	$$⊢2^4{2}^4=8\cdot 2\cdot 16$$
144		4p4e8	$$⊢4+4=8$$
145	144	oveq2i	$$⊢2^{4+4}=2^8$$
146		expadd	$$⊢\left(2\in ℂ\wedge 4\in {\mathbb{N}}_0\wedge 4\in {\mathbb{N}}_0\right)\to 2^{4+4}=2^4{2}^4$$
147	35 66 66 146	mp3an	$$⊢2^{4+4}=2^4{2}^4$$
148		2exp8	$$⊢2^8=256$$
149	145 147 148	3eqtr3i	$$⊢2^4{2}^4=256$$
150	139 143 149	3eqtr2i	$$⊢8\cdot 16\cdot 2=256$$
151	150	oveq2i	$$⊢\frac{A^4}{8\cdot 16\cdot 2}=\frac{A^4}{256}$$
152	138 151	eqtrdi	$$⊢\phi \to \frac{\frac{A^4}{8\cdot 16}}{2}=\frac{A^4}{256}$$
153	152	oveq2d	$$⊢\phi \to 2\left(\frac{\frac{A^4}{8\cdot 16}}{2}\right)=2\left(\frac{A^4}{256}\right)$$
154	131 137 153	3eqtr2d	$$⊢\phi \to \frac{\frac{A^4}{8}}{16}=2\left(\frac{A^4}{256}\right)$$
155	126 130 154	3eqtrd	$$⊢\phi \to 1\left(\frac{\frac{\frac{A^4}{8}}{4}}{4}\right)=2\left(\frac{A^4}{256}\right)$$
156	155	oveq2d	$$⊢\phi \to 3\left(\frac{\frac{\frac{A^4}{8}}{4}}{4}\right)+1\left(\frac{\frac{\frac{A^4}{8}}{4}}{4}\right)=3\left(\frac{\frac{\frac{A^4}{8}}{4}}{4}\right)+2\left(\frac{A^4}{256}\right)$$
157	124 125 156	3eqtr3d	$$⊢\phi \to \frac{\frac{A^4}{8}}{4}=3\left(\frac{\frac{\frac{A^4}{8}}{4}}{4}\right)+2\left(\frac{A^4}{256}\right)$$
158	120 157	oveq12d	$$⊢\phi \to \left(\frac{3}{256}\right)A^4-\left(\frac{\frac{A^4}{8}}{4}\right)=\left(\frac{A^4}{256}\right)+2\left(\frac{A^4}{256}\right)-\left(3\left(\frac{\frac{\frac{A^4}{8}}{4}}{4}\right)+2\left(\frac{A^4}{256}\right)\right)$$
159		mulcl	$$⊢\left(3\in ℂ\wedge \frac{\frac{\frac{A^4}{8}}{4}}{4}\in ℂ\right)\to 3\left(\frac{\frac{\frac{A^4}{8}}{4}}{4}\right)\in ℂ$$
160	83 122 159	sylancr	$$⊢\phi \to 3\left(\frac{\frac{\frac{A^4}{8}}{4}}{4}\right)\in ℂ$$
161		mulcl	$$⊢\left(2\in ℂ\wedge \frac{A^4}{256}\in ℂ\right)\to 2\left(\frac{A^4}{256}\right)\in ℂ$$
162	35 114 161	sylancr	$$⊢\phi \to 2\left(\frac{A^4}{256}\right)\in ℂ$$
163	114 160 162	pnpcan2d	$$⊢\phi \to \left(\frac{A^4}{256}\right)+2\left(\frac{A^4}{256}\right)-\left(3\left(\frac{\frac{\frac{A^4}{8}}{4}}{4}\right)+2\left(\frac{A^4}{256}\right)\right)=\left(\frac{A^4}{256}\right)-3\left(\frac{\frac{\frac{A^4}{8}}{4}}{4}\right)$$
164	158 163	eqtrd	$$⊢\phi \to \left(\frac{3}{256}\right)A^4-\left(\frac{\frac{A^4}{8}}{4}\right)=\left(\frac{A^4}{256}\right)-3\left(\frac{\frac{\frac{A^4}{8}}{4}}{4}\right)$$
165	164	oveq2d	$$⊢\phi \to \left(\frac{A^{2}B}{16}\right)+\left(\frac{3}{256}\right)A^4-\left(\frac{\frac{A^4}{8}}{4}\right)=\left(\frac{A^{2}B}{16}\right)+\left(\frac{A^4}{256}\right)-3\left(\frac{\frac{\frac{A^4}{8}}{4}}{4}\right)$$
166	82 114 160	addsub12d	$$⊢\phi \to \left(\frac{A^{2}B}{16}\right)+\left(\frac{A^4}{256}\right)-3\left(\frac{\frac{\frac{A^4}{8}}{4}}{4}\right)=\left(\frac{A^4}{256}\right)+\left(\frac{A^{2}B}{16}\right)-3\left(\frac{\frac{\frac{A^4}{8}}{4}}{4}\right)$$
167	165 166	eqtrd	$$⊢\phi \to \left(\frac{A^{2}B}{16}\right)+\left(\frac{3}{256}\right)A^4-\left(\frac{\frac{A^4}{8}}{4}\right)=\left(\frac{A^4}{256}\right)+\left(\frac{A^{2}B}{16}\right)-3\left(\frac{\frac{\frac{A^4}{8}}{4}}{4}\right)$$
168	64 17 40 20 42	divdiv1d	$$⊢\phi \to \frac{\frac{A^{2}B}{8}}{2}=\frac{A^{2}B}{8\cdot 2}$$
169	141	oveq2i	$$⊢\frac{A^{2}B}{8\cdot 2}=\frac{A^{2}B}{16}$$
170	168 169	eqtrdi	$$⊢\phi \to \frac{\frac{A^{2}B}{8}}{2}=\frac{A^{2}B}{16}$$
171	170	oveq2d	$$⊢\phi \to 2\left(\frac{\frac{A^{2}B}{8}}{2}\right)=2\left(\frac{A^{2}B}{16}\right)$$
172	65 40 42	divcan2d	$$⊢\phi \to 2\left(\frac{\frac{A^{2}B}{8}}{2}\right)=\frac{A^{2}B}{8}$$
173	82	2timesd	$$⊢\phi \to 2\left(\frac{A^{2}B}{16}\right)=\left(\frac{A^{2}B}{16}\right)+\left(\frac{A^{2}B}{16}\right)$$
174	171 172 173	3eqtr3d	$$⊢\phi \to \frac{A^{2}B}{8}=\left(\frac{A^{2}B}{16}\right)+\left(\frac{A^{2}B}{16}\right)$$
175	82 82 174	mvrladdd	$$⊢\phi \to \left(\frac{A^{2}B}{8}\right)-\left(\frac{A^{2}B}{16}\right)=\frac{A^{2}B}{16}$$
176	175	oveq1d	$$⊢\phi \to \left(\left(\frac{A^{2}B}{8}\right)-\left(\frac{A^{2}B}{16}\right)\right)+\left(\frac{3}{256}\right)A^4-\left(\frac{\frac{A^4}{8}}{4}\right)=\left(\frac{A^{2}B}{16}\right)+\left(\frac{3}{256}\right)A^4-\left(\frac{\frac{A^4}{8}}{4}\right)$$
177	5	oveq1d	$$⊢\phi \to P{\left(\frac{A}{4}\right)}^2=\left(B-\left(\frac{3}{8}\right)A^2\right){\left(\frac{A}{4}\right)}^2$$
178	83 16 19	divcli	$$⊢\frac{3}{8}\in ℂ$$
179		mulcl	$$⊢\left(\frac{3}{8}\in ℂ\wedge A^2\in ℂ\right)\to \left(\frac{3}{8}\right)A^2\in ℂ$$
180	178 63 179	sylancr	$$⊢\phi \to \left(\frac{3}{8}\right)A^2\in ℂ$$
181	26	sqcld	$$⊢\phi \to {\left(\frac{A}{4}\right)}^2\in ℂ$$
182	2 180 181	subdird	$$⊢\phi \to \left(B-\left(\frac{3}{8}\right)A^2\right){\left(\frac{A}{4}\right)}^2=B{\left(\frac{A}{4}\right)}^2-\left(\frac{3}{8}\right)A^2{\left(\frac{A}{4}\right)}^2$$
183	1 23 25	sqdivd	$$⊢\phi \to {\left(\frac{A}{4}\right)}^2=\frac{A^2}{4^2}$$
184	22	sqvali	$$⊢4^2=4\cdot 4$$
185	184 128	eqtri	$$⊢4^2=16$$
186	185	oveq2i	$$⊢\frac{A^2}{4^2}=\frac{A^2}{16}$$
187	183 186	eqtrdi	$$⊢\phi \to {\left(\frac{A}{4}\right)}^2=\frac{A^2}{16}$$
188	187	oveq2d	$$⊢\phi \to B{\left(\frac{A}{4}\right)}^2=B\left(\frac{A^2}{16}\right)$$
189	2 63 79 81	divassd	$$⊢\phi \to \frac{B{A}^2}{16}=B\left(\frac{A^2}{16}\right)$$
190	2 63	mulcomd	$$⊢\phi \to B{A}^2=A^{2}B$$
191	190	oveq1d	$$⊢\phi \to \frac{B{A}^2}{16}=\frac{A^{2}B}{16}$$
192	188 189 191	3eqtr2d	$$⊢\phi \to B{\left(\frac{A}{4}\right)}^2=\frac{A^{2}B}{16}$$
193	178	a1i	$$⊢\phi \to \frac{3}{8}\in ℂ$$
194	193 63 63	mulassd	$$⊢\phi \to \left(\frac{3}{8}\right)A^2{A}^2=\left(\frac{3}{8}\right)A^2{A}^2$$
195	106 68 17 20	div23d	$$⊢\phi \to \frac{3A^4}{8}=\left(\frac{3}{8}\right)A^4$$
196		2p2e4	$$⊢2+2=4$$
197	196	oveq2i	$$⊢A^{2+2}=A^4$$
198	84	a1i	$$⊢\phi \to 2\in {\mathbb{N}}_0$$
199	1 198 198	expaddd	$$⊢\phi \to A^{2+2}=A^2{A}^2$$
200	197 199	eqtr3id	$$⊢\phi \to A^4=A^2{A}^2$$
201	200	oveq2d	$$⊢\phi \to \left(\frac{3}{8}\right)A^4=\left(\frac{3}{8}\right)A^2{A}^2$$
202	195 201	eqtrd	$$⊢\phi \to \frac{3A^4}{8}=\left(\frac{3}{8}\right)A^2{A}^2$$
203	106 68 17 20	divassd	$$⊢\phi \to \frac{3A^4}{8}=3\left(\frac{A^4}{8}\right)$$
204	194 202 203	3eqtr2d	$$⊢\phi \to \left(\frac{3}{8}\right)A^2{A}^2=3\left(\frac{A^4}{8}\right)$$
205	204	oveq1d	$$⊢\phi \to \frac{\left(\frac{3}{8}\right)A^2{A}^2}{4^2}=\frac{3\left(\frac{A^4}{8}\right)}{4^2}$$
206	185 79	eqeltrid	$$⊢\phi \to 4^2\in ℂ$$
207	185 80	eqnetri	$$⊢4^2\ne 0$$
208	207	a1i	$$⊢\phi \to 4^2\ne 0$$
209	180 63 206 208	divassd	$$⊢\phi \to \frac{\left(\frac{3}{8}\right)A^2{A}^2}{4^2}=\left(\frac{3}{8}\right)A^2\left(\frac{A^2}{4^2}\right)$$
210	106 69 206 208	divassd	$$⊢\phi \to \frac{3\left(\frac{A^4}{8}\right)}{4^2}=3\left(\frac{\frac{A^4}{8}}{4^2}\right)$$
211	205 209 210	3eqtr3d	$$⊢\phi \to \left(\frac{3}{8}\right)A^2\left(\frac{A^2}{4^2}\right)=3\left(\frac{\frac{A^4}{8}}{4^2}\right)$$
212	183	oveq2d	$$⊢\phi \to \left(\frac{3}{8}\right)A^2{\left(\frac{A}{4}\right)}^2=\left(\frac{3}{8}\right)A^2\left(\frac{A^2}{4^2}\right)$$
213	185	oveq2i	$$⊢\frac{\frac{A^4}{8}}{4^2}=\frac{\frac{A^4}{8}}{16}$$
214	130 213	eqtr4di	$$⊢\phi \to \frac{\frac{\frac{A^4}{8}}{4}}{4}=\frac{\frac{A^4}{8}}{4^2}$$
215	214	oveq2d	$$⊢\phi \to 3\left(\frac{\frac{\frac{A^4}{8}}{4}}{4}\right)=3\left(\frac{\frac{A^4}{8}}{4^2}\right)$$
216	211 212 215	3eqtr4d	$$⊢\phi \to \left(\frac{3}{8}\right)A^2{\left(\frac{A}{4}\right)}^2=3\left(\frac{\frac{\frac{A^4}{8}}{4}}{4}\right)$$
217	192 216	oveq12d	$$⊢\phi \to B{\left(\frac{A}{4}\right)}^2-\left(\frac{3}{8}\right)A^2{\left(\frac{A}{4}\right)}^2=\left(\frac{A^{2}B}{16}\right)-3\left(\frac{\frac{\frac{A^4}{8}}{4}}{4}\right)$$
218	177 182 217	3eqtrd	$$⊢\phi \to P{\left(\frac{A}{4}\right)}^2=\left(\frac{A^{2}B}{16}\right)-3\left(\frac{\frac{\frac{A^4}{8}}{4}}{4}\right)$$
219	218	oveq2d	$$⊢\phi \to \left(\frac{A^4}{256}\right)+P{\left(\frac{A}{4}\right)}^2=\left(\frac{A^4}{256}\right)+\left(\frac{A^{2}B}{16}\right)-3\left(\frac{\frac{\frac{A^4}{8}}{4}}{4}\right)$$
220	167 176 219	3eqtr4d	$$⊢\phi \to \left(\left(\frac{A^{2}B}{8}\right)-\left(\frac{A^{2}B}{16}\right)\right)+\left(\frac{3}{256}\right)A^4-\left(\frac{\frac{A^4}{8}}{4}\right)=\left(\frac{A^4}{256}\right)+P{\left(\frac{A}{4}\right)}^2$$
221	104 105 220	3eqtrd	$$⊢\phi \to \left(\frac{A^{2}B}{8}\right)+\left(\frac{3}{256}\right)A^4-\left(\left(\frac{\frac{A^4}{8}}{4}\right)+\left(\frac{A^{2}B}{16}\right)\right)=\left(\frac{A^4}{256}\right)+P{\left(\frac{A}{4}\right)}^2$$
222	221	negeqd	$$⊢\phi \to -\left(\left(\frac{A^{2}B}{8}\right)+\left(\frac{3}{256}\right)A^4-\left(\left(\frac{\frac{A^4}{8}}{4}\right)+\left(\frac{A^{2}B}{16}\right)\right)\right)=-\left(\left(\frac{A^4}{256}\right)+P{\left(\frac{A}{4}\right)}^2\right)$$
223	70 82 65 92	addsub4d	$$⊢\phi \to \left(\frac{\frac{A^4}{8}}{4}\right)+\left(\frac{A^{2}B}{16}\right)-\left(\left(\frac{A^{2}B}{8}\right)+\left(\frac{3}{256}\right)A^4\right)=\left(\left(\frac{\frac{A^4}{8}}{4}\right)-\left(\frac{A^{2}B}{8}\right)\right)+\left(\frac{A^{2}B}{16}\right)-\left(\frac{3}{256}\right)A^4$$
224	102 222 223	3eqtr3rd	$$⊢\phi \to \left(\left(\frac{\frac{A^4}{8}}{4}\right)-\left(\frac{A^{2}B}{8}\right)\right)+\left(\frac{A^{2}B}{16}\right)-\left(\frac{3}{256}\right)A^4=-\left(\left(\frac{A^4}{256}\right)+P{\left(\frac{A}{4}\right)}^2\right)$$
225	224	oveq2d	$$⊢\phi \to D+\left(\left(\frac{\frac{A^4}{8}}{4}\right)-\left(\frac{A^{2}B}{8}\right)\right)+\left(\left(\frac{A^{2}B}{16}\right)-\left(\frac{3}{256}\right)A^4\right)=D+\left(-\left(\left(\frac{A^4}{256}\right)+P{\left(\frac{A}{4}\right)}^2\right)\right)$$
226	2 180	subcld	$$⊢\phi \to B-\left(\frac{3}{8}\right)A^2\in ℂ$$
227	5 226	eqeltrd	$$⊢\phi \to P\in ℂ$$
228	227 181	mulcld	$$⊢\phi \to P{\left(\frac{A}{4}\right)}^2\in ℂ$$
229	114 228	addcld	$$⊢\phi \to \left(\frac{A^4}{256}\right)+P{\left(\frac{A}{4}\right)}^2\in ℂ$$
230	4 229	negsubd	$$⊢\phi \to D+\left(-\left(\left(\frac{A^4}{256}\right)+P{\left(\frac{A}{4}\right)}^2\right)\right)=D-\left(\left(\frac{A^4}{256}\right)+P{\left(\frac{A}{4}\right)}^2\right)$$
231	99 225 230	3eqtrd	$$⊢\phi \to \left(\left(\frac{\frac{A^4}{8}}{4}\right)-\left(\frac{A^{2}B}{8}\right)\right)+D+\left(\left(\frac{A^{2}B}{16}\right)-\left(\frac{3}{256}\right)A^4\right)=D-\left(\left(\frac{A^4}{256}\right)+P{\left(\frac{A}{4}\right)}^2\right)$$
232	96 98 231	3eqtrd	$$⊢\phi \to Q\left(\frac{A}{4}\right)+R=D-\left(\left(\frac{A^4}{256}\right)+P{\left(\frac{A}{4}\right)}^2\right)$$
233	232	oveq2d	$$⊢\phi \to \left(\frac{A^4}{256}\right)+P{\left(\frac{A}{4}\right)}^2+Q\left(\frac{A}{4}\right)+R=\left(\frac{A^4}{256}\right)+P{\left(\frac{A}{4}\right)}^2+\left(D-\left(\left(\frac{A^4}{256}\right)+P{\left(\frac{A}{4}\right)}^2\right)\right)$$
234	229 4	pncan3d	$$⊢\phi \to \left(\frac{A^4}{256}\right)+P{\left(\frac{A}{4}\right)}^2+\left(D-\left(\left(\frac{A^4}{256}\right)+P{\left(\frac{A}{4}\right)}^2\right)\right)=D$$
235	233 234	eqtr2d	$$⊢\phi \to D=\left(\frac{A^4}{256}\right)+P{\left(\frac{A}{4}\right)}^2+Q\left(\frac{A}{4}\right)+R$$