Metamath Proof Explorer

Theorem quartfull

Description: The quartic equation, written out in full. This actually makes a fairly good Metamath stress test. Note that the length of this formula could be shortened significantly if the intermediate expressions were expanded and simplified, but it's not like this theorem will be used anyway. (Contributed by Mario Carneiro, 6-May-2015)

Ref Expression
Hypotheses quartfull.a 
|- ( ph -> A e. CC )
quartfull.b 
|- ( ph -> B e. CC )
quartfull.c 
|- ( ph -> C e. CC )
quartfull.d 
|- ( ph -> D e. CC )
quartfull.x 
|- ( ph -> X e. CC )
quartfull.t0 
|- ( ph -> ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) =/= 0 )
quartfull.m0 
|- ( ph -> -u ( ( ( ( 2 x. ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ) + ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) + ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) / ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) ) / 3 ) =/= 0 )
Assertion quartfull 
|- ( ph -> ( ( ( ( X ^ 4 ) + ( A x. ( X ^ 3 ) ) ) + ( ( B x. ( X ^ 2 ) ) + ( ( C x. X ) + D ) ) ) = 0 <-> ( ( X = ( ( -u ( A / 4 ) - ( ( sqrt ` -u ( ( ( ( 2 x. ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ) + ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) + ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) / ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) ) / 3 ) ) / 2 ) ) + ( sqrt ` ( ( -u ( ( ( sqrt ` -u ( ( ( ( 2 x. ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ) + ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) + ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) / ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) ) / 3 ) ) / 2 ) ^ 2 ) - ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) / 2 ) ) + ( ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) / 4 ) / ( ( sqrt ` -u ( ( ( ( 2 x. ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ) + ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) + ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) / ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) ) / 3 ) ) / 2 ) ) ) ) ) \/ X = ( ( -u ( A / 4 ) - ( ( sqrt ` -u ( ( ( ( 2 x. ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ) + ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) + ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) / ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) ) / 3 ) ) / 2 ) ) - ( sqrt ` ( ( -u ( ( ( sqrt ` -u ( ( ( ( 2 x. ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ) + ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) + ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) / ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) ) / 3 ) ) / 2 ) ^ 2 ) - ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) / 2 ) ) + ( ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) / 4 ) / ( ( sqrt ` -u ( ( ( ( 2 x. ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ) + ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) + ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) / ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) ) / 3 ) ) / 2 ) ) ) ) ) ) \/ ( X = ( ( -u ( A / 4 ) + ( ( sqrt ` -u ( ( ( ( 2 x. ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ) + ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) + ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) / ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) ) / 3 ) ) / 2 ) ) + ( sqrt ` ( ( -u ( ( ( sqrt ` -u ( ( ( ( 2 x. ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ) + ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) + ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) / ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) ) / 3 ) ) / 2 ) ^ 2 ) - ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) / 2 ) ) - ( ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) / 4 ) / ( ( sqrt ` -u ( ( ( ( 2 x. ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ) + ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) + ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) / ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) ) / 3 ) ) / 2 ) ) ) ) ) \/ X = ( ( -u ( A / 4 ) + ( ( sqrt ` -u ( ( ( ( 2 x. ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ) + ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) + ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) / ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) ) / 3 ) ) / 2 ) ) - ( sqrt ` ( ( -u ( ( ( sqrt ` -u ( ( ( ( 2 x. ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ) + ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) + ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) / ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) ) / 3 ) ) / 2 ) ^ 2 ) - ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) / 2 ) ) - ( ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) / 4 ) / ( ( sqrt ` -u ( ( ( ( 2 x. ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ) + ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) + ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) / ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) ) / 3 ) ) / 2 ) ) ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 quartfull.a 
 |-  ( ph -> A e. CC )
2 quartfull.b 
 |-  ( ph -> B e. CC )
3 quartfull.c 
 |-  ( ph -> C e. CC )
4 quartfull.d 
 |-  ( ph -> D e. CC )
5 quartfull.x 
 |-  ( ph -> X e. CC )
6 quartfull.t0 
 |-  ( ph -> ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) =/= 0 )
7 quartfull.m0 
 |-  ( ph -> -u ( ( ( ( 2 x. ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ) + ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) + ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) / ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) ) / 3 ) =/= 0 )
8 eqidd 
 |-  ( ph -> -u ( A / 4 ) = -u ( A / 4 ) )
9 eqidd 
 |-  ( ph -> ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) = ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) )
10 eqidd 
 |-  ( ph -> ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) = ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) )
11 eqidd 
 |-  ( ph -> ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) = ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) )
12 eqidd 
 |-  ( ph -> ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) = ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) )
13 eqidd 
 |-  ( ph -> ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) = ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) )
14 eqidd 
 |-  ( ph -> ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) = ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) )
15 eqidd 
 |-  ( ph -> ( ( sqrt ` -u ( ( ( ( 2 x. ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ) + ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) + ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) / ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) ) / 3 ) ) / 2 ) = ( ( sqrt ` -u ( ( ( ( 2 x. ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ) + ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) + ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) / ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) ) / 3 ) ) / 2 ) )
16 eqidd 
 |-  ( ph -> -u ( ( ( ( 2 x. ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ) + ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) + ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) / ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) ) / 3 ) = -u ( ( ( ( 2 x. ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ) + ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) + ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) / ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) ) / 3 ) )
17 eqidd 
 |-  ( ph -> ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) = ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) )
18 eqidd 
 |-  ( ph -> ( sqrt ` ( ( -u ( ( ( sqrt ` -u ( ( ( ( 2 x. ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ) + ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) + ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) / ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) ) / 3 ) ) / 2 ) ^ 2 ) - ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) / 2 ) ) + ( ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) / 4 ) / ( ( sqrt ` -u ( ( ( ( 2 x. ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ) + ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) + ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) / ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) ) / 3 ) ) / 2 ) ) ) ) = ( sqrt ` ( ( -u ( ( ( sqrt ` -u ( ( ( ( 2 x. ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ) + ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) + ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) / ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) ) / 3 ) ) / 2 ) ^ 2 ) - ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) / 2 ) ) + ( ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) / 4 ) / ( ( sqrt ` -u ( ( ( ( 2 x. ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ) + ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) + ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) / ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) ) / 3 ) ) / 2 ) ) ) ) )
19 eqidd 
 |-  ( ph -> ( sqrt ` ( ( -u ( ( ( sqrt ` -u ( ( ( ( 2 x. ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ) + ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) + ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) / ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) ) / 3 ) ) / 2 ) ^ 2 ) - ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) / 2 ) ) - ( ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) / 4 ) / ( ( sqrt ` -u ( ( ( ( 2 x. ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ) + ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) + ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) / ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) ) / 3 ) ) / 2 ) ) ) ) = ( sqrt ` ( ( -u ( ( ( sqrt ` -u ( ( ( ( 2 x. ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ) + ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) + ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) / ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) ) / 3 ) ) / 2 ) ^ 2 ) - ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) / 2 ) ) - ( ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) / 4 ) / ( ( sqrt ` -u ( ( ( ( 2 x. ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ) + ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) + ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) / ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) ) / 3 ) ) / 2 ) ) ) ) )
20 1 2 3 4 5 8 9 10 11 12 13 14 15 16 17 6 7 18 19 quart 
 |-  ( ph -> ( ( ( ( X ^ 4 ) + ( A x. ( X ^ 3 ) ) ) + ( ( B x. ( X ^ 2 ) ) + ( ( C x. X ) + D ) ) ) = 0 <-> ( ( X = ( ( -u ( A / 4 ) - ( ( sqrt ` -u ( ( ( ( 2 x. ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ) + ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) + ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) / ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) ) / 3 ) ) / 2 ) ) + ( sqrt ` ( ( -u ( ( ( sqrt ` -u ( ( ( ( 2 x. ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ) + ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) + ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) / ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) ) / 3 ) ) / 2 ) ^ 2 ) - ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) / 2 ) ) + ( ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) / 4 ) / ( ( sqrt ` -u ( ( ( ( 2 x. ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ) + ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) + ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) / ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) ) / 3 ) ) / 2 ) ) ) ) ) \/ X = ( ( -u ( A / 4 ) - ( ( sqrt ` -u ( ( ( ( 2 x. ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ) + ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) + ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) / ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) ) / 3 ) ) / 2 ) ) - ( sqrt ` ( ( -u ( ( ( sqrt ` -u ( ( ( ( 2 x. ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ) + ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) + ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) / ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) ) / 3 ) ) / 2 ) ^ 2 ) - ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) / 2 ) ) + ( ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) / 4 ) / ( ( sqrt ` -u ( ( ( ( 2 x. ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ) + ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) + ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) / ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) ) / 3 ) ) / 2 ) ) ) ) ) ) \/ ( X = ( ( -u ( A / 4 ) + ( ( sqrt ` -u ( ( ( ( 2 x. ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ) + ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) + ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) / ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) ) / 3 ) ) / 2 ) ) + ( sqrt ` ( ( -u ( ( ( sqrt ` -u ( ( ( ( 2 x. ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ) + ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) + ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) / ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) ) / 3 ) ) / 2 ) ^ 2 ) - ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) / 2 ) ) - ( ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) / 4 ) / ( ( sqrt ` -u ( ( ( ( 2 x. ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ) + ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) + ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) / ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) ) / 3 ) ) / 2 ) ) ) ) ) \/ X = ( ( -u ( A / 4 ) + ( ( sqrt ` -u ( ( ( ( 2 x. ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ) + ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) + ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) / ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) ) / 3 ) ) / 2 ) ) - ( sqrt ` ( ( -u ( ( ( sqrt ` -u ( ( ( ( 2 x. ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ) + ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) + ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) / ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) ) / 3 ) ) / 2 ) ^ 2 ) - ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) / 2 ) ) - ( ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) / 4 ) / ( ( sqrt ` -u ( ( ( ( 2 x. ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ) + ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) + ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) / ( ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) + ( sqrt ` ( ( ( ( -u ( 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 3 ) ) - ( ; 2 7 x. ( ( ( C - ( ( A x. B ) / 2 ) ) + ( ( A ^ 3 ) / 8 ) ) ^ 2 ) ) ) + ( ; 7 2 x. ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ) ^ 2 ) - ( 4 x. ( ( ( ( B - ( ( 3 / 8 ) x. ( A ^ 2 ) ) ) ^ 2 ) + ( ; 1 2 x. ( ( D - ( ( C x. A ) / 4 ) ) + ( ( ( ( A ^ 2 ) x. B ) / ; 1 6 ) - ( ( 3 / ; ; 2 5 6 ) x. ( A ^ 4 ) ) ) ) ) ) ^ 3 ) ) ) ) ) / 2 ) ^c ( 1 / 3 ) ) ) ) / 3 ) ) / 2 ) ) ) ) ) ) ) ) )