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