Metamath Proof Explorer

Theorem quart1lem

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

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

Proof

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