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