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