Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  quartfull Unicode version

Theorem quartfull 23090
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.)
Hypotheses
Ref Expression
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 ) ) ) ) ) ) )  +  ( sqr `  (
( ( ( -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 ) ) ) ) ) ) )  +  ( sqr `  (
( ( ( -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 ) ) ) ) ) ) )  +  ( sqr `  (
( ( ( -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
Ref Expression
quartfull  |-  ( ph  ->  ( ( ( ( X ^ 4 )  +  ( A  x.  ( X ^ 3 ) ) )  +  ( ( B  x.  ( X ^ 2 ) )  +  ( ( C  x.  X )  +  D ) ) )  =  0  <->  ( ( X  =  ( ( -u ( A  /  4
)  -  ( ( sqr `  -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 ) ) ) ) ) ) )  +  ( sqr `  (
( ( ( -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 ) ) ) ) ) ) )  +  ( sqr `  (
( ( ( -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 ) )  +  ( sqr `  (
( -u ( ( ( sqr `  -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 ) ) ) ) ) ) )  +  ( sqr `  (
( ( ( -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 ) ) ) ) ) ) )  +  ( sqr `  (
( ( ( -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 )  / 
( ( sqr `  -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 ) ) ) ) ) ) )  +  ( sqr `  (
( ( ( -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 ) ) ) ) ) ) )  +  ( sqr `  (
( ( ( -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
)  -  ( ( sqr `  -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 ) ) ) ) ) ) )  +  ( sqr `  (
( ( ( -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 ) ) ) ) ) ) )  +  ( sqr `  (
( ( ( -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 ) )  -  ( sqr `  ( (
-u ( ( ( sqr `  -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 ) ) ) ) ) ) )  +  ( sqr `  (
( ( ( -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 ) ) ) ) ) ) )  +  ( sqr `  (
( ( ( -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 )  / 
( ( sqr `  -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 ) ) ) ) ) ) )  +  ( sqr `  (
( ( ( -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 ) ) ) ) ) ) )  +  ( sqr `  (
( ( ( -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 )  +  ( ( sqr `  -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 ) ) ) ) ) ) )  +  ( sqr `  (
( ( ( -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 ) ) ) ) ) ) )  +  ( sqr `  (
( ( ( -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 ) )  +  ( sqr `  (
( -u ( ( ( sqr `  -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 ) ) ) ) ) ) )  +  ( sqr `  (
( ( ( -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 ) ) ) ) ) ) )  +  ( sqr `  (
( ( ( -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 )  / 
( ( sqr `  -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 ) ) ) ) ) ) )  +  ( sqr `  (
( ( ( -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 ) ) ) ) ) ) )  +  ( sqr `  (
( ( ( -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
)  +  ( ( sqr `  -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 ) ) ) ) ) ) )  +  ( sqr `  (
( ( ( -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 ) ) ) ) ) ) )  +  ( sqr `  (
( ( ( -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 ) )  -  ( sqr `  ( (
-u ( ( ( sqr `  -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 ) ) ) ) ) ) )  +  ( sqr `  (
( ( ( -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 ) ) ) ) ) ) )  +  ( sqr `  (
( ( ( -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 )  / 
( ( sqr `  -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 ) ) ) ) ) ) )  +  ( sqr `  (
( ( ( -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 ) ) ) ) ) ) )  +  ( sqr `  (
( ( ( -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 of Theorem quartfull
StepHypRef Expression
1 quartfull.a . 2  |-  ( ph  ->  A  e.  CC )
2 quartfull.b . 2  |-  ( ph  ->  B  e.  CC )
3 quartfull.c . 2  |-  ( ph  ->  C  e.  CC )
4 quartfull.d . 2  |-  ( ph  ->  D  e.  CC )
5 quartfull.x . 2  |-  ( ph  ->  X  e.  CC )
6 eqidd 2285 . 2  |-  ( ph  -> 
-u ( A  / 
4 )  =  -u ( A  /  4
) )
7 eqidd 2285 . 2  |-  ( ph  ->  ( B  -  (
( 3  /  8
)  x.  ( A ^ 2 ) ) )  =  ( B  -  ( ( 3  /  8 )  x.  ( A ^ 2 ) ) ) )
8 eqidd 2285 . 2  |-  ( ph  ->  ( ( C  -  ( ( A  x.  B )  /  2
) )  +  ( ( A ^ 3 )  /  8 ) )  =  ( ( C  -  ( ( A  x.  B )  /  2 ) )  +  ( ( A ^ 3 )  / 
8 ) ) )
9 eqidd 2285 . 2  |-  ( 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 ) ) ) ) )
10 eqidd 2285 . 2  |-  ( 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 ) ) ) ) ) ) )
11 eqidd 2285 . 2  |-  ( 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 ) ) ) ) ) ) ) )
12 eqidd 2285 . 2  |-  ( ph  ->  ( sqr `  (
( ( ( -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 ) ) ) )  =  ( sqr `  ( ( ( (
-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 ) ) ) ) )
13 eqidd 2285 . 2  |-  ( ph  ->  ( ( sqr `  -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 ) ) ) ) ) ) )  +  ( sqr `  (
( ( ( -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 ) ) ) ) ) ) )  +  ( sqr `  (
( ( ( -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 )  =  ( ( sqr `  -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 ) ) ) ) ) ) )  +  ( sqr `  (
( ( ( -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 ) ) ) ) ) ) )  +  ( sqr `  (
( ( ( -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 ) )
14 eqidd 2285 . 2  |-  ( 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 ) ) ) ) ) ) )  +  ( sqr `  (
( ( ( -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 ) ) ) ) ) ) )  +  ( sqr `  (
( ( ( -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 ) ) ) ) ) ) )  +  ( sqr `  (
( ( ( -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 ) ) ) ) ) ) )  +  ( sqr `  (
( ( ( -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 ) )
15 eqidd 2285 . 2  |-  ( 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 ) ) ) ) ) ) )  +  ( sqr `  (
( ( ( -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 ) ) ) ) ) ) )  +  ( sqr `  (
( ( ( -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.  (