Theorem quart1

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