Theorem quart1lem

Description: Lemma for quart1 . (Contributed by Mario Carneiro, 6-May-2015)

	Ref	Expression
Hypotheses	quart1.a	|- ( ph -> A e. CC )
	quart1.b	|- ( ph -> B e. CC )
	quart1.c	|- ( ph -> C e. CC )
	quart1.d	|- ( ph -> D e. CC )
	quart1.p	|- ( ph -> P = ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) )
	quart1.q	|- ( ph -> Q = ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) )
	quart1.r	|- ( ph -> R = ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) )
	quart1.x	|- ( ph -> X e. CC )
	quart1.y	|- ( ph -> Y = ( X + ( A / 4 ) ) )
Assertion	quart1lem	|- ( ph -> D = ( ( ( ( A ^ 4 ) / ; ; 2 5 6 ) + ( P x. ( ( A / 4 ) ^ 2 ) ) ) + ( ( Q x. ( A / 4 ) ) + R ) ) )

Proof

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