Metamath Proof Explorer


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 syl5eq
 |-  ( 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 mulid2d
 |-  ( 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 ) ) )