HomeHome Metamath Proof Explorer
Theorem List (p. 238 of 328)
< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Color key:    Metamath Proof Explorer  Metamath Proof Explorer
(1-21514)
  Hilbert Space Explorer  Hilbert Space Explorer
(21515-23037)
  Users' Mathboxes  Users' Mathboxes
(23038-32776)
 

Theorem List for Metamath Proof Explorer - 23701-23800   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
18.4  Mathbox for Mario Carneiro
 
18.4.1  Miscellaneous stuff
 
Theoremquartfull 23701 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.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  C  e.  CC )   &    |-  ( ph  ->  D  e.  CC )   &    |-  ( ph  ->  X  e.  CC )   &    |-  ( 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 )   &    |-  ( 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 )   =>    |-  ( 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
 ) ) ) ) ) ) ) ) )
 
18.4.2  Zeta function
 
Syntaxczeta 23702 The Riemann zeta function.
 class  zeta
 
Definitiondf-zeta 23703* Define the Riemann zeta function. This definition uses a series expansion of the alternating zeta function ~? zetaalt that is convergent everywhere except  1, but going from the alternating zeta function to the regular zeta function requires dividing by  1  -  2 ^ ( 1  -  s ), which has zeroes other than  1. To extract the correct value of the zeta function at these points, we extend the divided alternating zeta function by continuity. (Contributed by Mario Carneiro, 18-Jul-2014.)
 |-  zeta  =  ( iota_ f  e.  (
 ( CC  \  {
 1 } ) -cn-> CC ) A. s  e.  ( CC  \  { 1 } ) ( ( 1  -  ( 2  ^ c  ( 1  -  s
 ) ) )  x.  ( f `  s
 ) )  =  sum_ n  e.  NN0  ( sum_ k  e.  ( 0 ... n ) ( ( ( -u 1 ^ k
 )  x.  ( n  _C  k ) )  x.  ( ( k  +  1 )  ^ c  s ) )  /  ( 2 ^ ( n  +  1 )
 ) ) )
 
Theoremzetacvg 23704* The zeta series is convergent. (Contributed by Mario Carneiro, 18-Jul-2014.)
 |-  ( ph  ->  S  e.  CC )   &    |-  ( ph  ->  1  <  ( Re `  S ) )   &    |-  ( ( ph  /\  k  e.  NN )  ->  ( F `  k
 )  =  ( k 
 ^ c  -u S ) )   =>    |-  ( ph  ->  seq  1
 (  +  ,  F )  e.  dom  ~~>  )
 
18.4.3  Gamma function
 
Syntaxclgam 23705 Logarithm of the Gamma function.
 class  log  _G
 
Syntaxcgam 23706 The Gamma function.
 class  _G
 
Definitiondf-lgam 23707* Define the log-Gamma function. We can work with this form of the gamma function a bit easier than the equivalent expression for the gamma function itself, and moreover this function is not actually equal to  log ( _G ( x ) ) because the branch cuts are placed differently (we do have  exp ( log  _G ( x ) )  =  _G ( x ), though). This definition is attributed to Euler, and unlike the usual integral definition is defined on the entire complex plane except the nonpositive integers  ZZ  \  NN, where the function has simple poles. (Contributed by Mario Carneiro, 12-Jul-2014.)
 |-  log  _G  =  ( z  e.  ( CC  \  ( ZZ  \  NN ) ) 
 |->  (  ~~>  `  ( n  e.  NN  |->  ( ( ( z  x.  ( log `  n ) )  -  ( log `  z )
 )  -  sum_ m  e.  ( 1 ... n ) ( log `  (
 ( z  /  m )  +  1 )
 ) ) ) ) )
 
Definitiondf-gam 23708 Define the Gamma function. See df-lgam 23707 for more information about the reason for this definition in terms of the log-gamma function. (Contributed by Mario Carneiro, 12-Jul-2014.)
 |-  _G  =  ( exp  o.  log  _G )
 
Theoremeldmgm 23709 Elementhood in the set of non-nonpositive integers. (Contributed by Mario Carneiro, 12-Jul-2014.)
 |-  ( A  e.  ( CC  \  ( ZZ  \  NN ) )  <->  ( A  e.  CC  /\  -.  -u A  e.  NN0 ) )
 
Theoremdmgmaddn0 23710 If  A is not a nonpositive integer, then  A  +  N is nonzero for any nonnegative integer  N. (Contributed by Mario Carneiro, 12-Jul-2014.)
 |-  (
 ( A  e.  ( CC  \  ( ZZ  \  NN ) )  /\  N  e.  NN0 )  ->  ( A  +  N )  =/=  0 )
 
Theoremdmgmseqn0 23711* If  A is not a nonpositive integer, then  prod_ m  e.  ( 1 ... N
) A  +  m is nonzero for any  N. (Contributed by Mario Carneiro, 12-Jul-2014.)
 |-  S  =  seq  0 (  x. 
 ,  ( m  e. 
 _V  |->  ( A  +  m ) ) )   =>    |-  ( ( A  e.  ( CC  \  ( ZZ  \  NN ) )  /\  N  e.  NN0 )  ->  ( S `  N )  =/=  0 )
 
18.4.4  Derangements and the Subfactorial
 
Theoremderanglem 23712* Lemma for derangements. (Contributed by Mario Carneiro, 19-Jan-2015.)
 |-  ( A  e.  Fin  ->  { f  |  ( f : A -1-1-onto-> A  /\  ph ) }  e.  Fin )
 
Theoremderangval 23713* Define the derangement function, which counts the number of bijections from a set to itself such that no element is mapped to itself. (Contributed by Mario Carneiro, 19-Jan-2015.)
 |-  D  =  ( x  e.  Fin  |->  ( # `  { f  |  ( f : x -1-1-onto-> x  /\  A. y  e.  x  ( f `  y
 )  =/=  y ) } ) )   =>    |-  ( A  e.  Fin 
 ->  ( D `  A )  =  ( # `  { f  |  ( f : A -1-1-onto-> A  /\  A. y  e.  A  ( f `  y
 )  =/=  y ) } ) )
 
Theoremderangf 23714* The derangement number is a function from finite sets to nonnegative integers. (Contributed by Mario Carneiro, 19-Jan-2015.)
 |-  D  =  ( x  e.  Fin  |->  ( # `  { f  |  ( f : x -1-1-onto-> x  /\  A. y  e.  x  ( f `  y
 )  =/=  y ) } ) )   =>    |-  D : Fin --> NN0
 
Theoremderang0 23715* The derangement number of the empty set. (Contributed by Mario Carneiro, 19-Jan-2015.)
 |-  D  =  ( x  e.  Fin  |->  ( # `  { f  |  ( f : x -1-1-onto-> x  /\  A. y  e.  x  ( f `  y
 )  =/=  y ) } ) )   =>    |-  ( D `  (/) )  =  1
 
Theoremderangsn 23716* The derangement number of a singleton. (Contributed by Mario Carneiro, 19-Jan-2015.)
 |-  D  =  ( x  e.  Fin  |->  ( # `  { f  |  ( f : x -1-1-onto-> x  /\  A. y  e.  x  ( f `  y
 )  =/=  y ) } ) )   =>    |-  ( A  e.  V  ->  ( D `  { A } )  =  0 )
 
Theoremderangenlem 23717* One half of derangen 23718. (Contributed by Mario Carneiro, 22-Jan-2015.)
 |-  D  =  ( x  e.  Fin  |->  ( # `  { f  |  ( f : x -1-1-onto-> x  /\  A. y  e.  x  ( f `  y
 )  =/=  y ) } ) )   =>    |-  ( ( A 
 ~~  B  /\  B  e.  Fin )  ->  ( D `  A )  <_  ( D `  B ) )
 
Theoremderangen 23718* The derangement number is a cardinal invariant, i.e. it only depends on the size of a set and not on its contents. (Contributed by Mario Carneiro, 22-Jan-2015.)
 |-  D  =  ( x  e.  Fin  |->  ( # `  { f  |  ( f : x -1-1-onto-> x  /\  A. y  e.  x  ( f `  y
 )  =/=  y ) } ) )   =>    |-  ( ( A 
 ~~  B  /\  B  e.  Fin )  ->  ( D `  A )  =  ( D `  B ) )
 
Theoremsubfacval 23719* The subfactorial is defined as the number of derangements (see derangval 23713) of the set  ( 1 ... N ). (Contributed by Mario Carneiro, 21-Jan-2015.)
 |-  D  =  ( x  e.  Fin  |->  ( # `  { f  |  ( f : x -1-1-onto-> x  /\  A. y  e.  x  ( f `  y
 )  =/=  y ) } ) )   &    |-  S  =  ( n  e.  NN0  |->  ( D `  ( 1
 ... n ) ) )   =>    |-  ( N  e.  NN0  ->  ( S `  N )  =  ( D `  ( 1 ... N ) ) )
 
Theoremderangen2 23720* Write the derangement number in terms of the subfactorial. (Contributed by Mario Carneiro, 22-Jan-2015.)
 |-  D  =  ( x  e.  Fin  |->  ( # `  { f  |  ( f : x -1-1-onto-> x  /\  A. y  e.  x  ( f `  y
 )  =/=  y ) } ) )   &    |-  S  =  ( n  e.  NN0  |->  ( D `  ( 1
 ... n ) ) )   =>    |-  ( A  e.  Fin  ->  ( D `  A )  =  ( S `  ( # `  A ) ) )
 
Theoremsubfacf 23721* The subfactorial is a function from nonnegative integers to nonnegative integers. (Contributed by Mario Carneiro, 19-Jan-2015.)
 |-  D  =  ( x  e.  Fin  |->  ( # `  { f  |  ( f : x -1-1-onto-> x  /\  A. y  e.  x  ( f `  y
 )  =/=  y ) } ) )   &    |-  S  =  ( n  e.  NN0  |->  ( D `  ( 1
 ... n ) ) )   =>    |-  S : NN0 --> NN0
 
Theoremsubfaclefac 23722* The subfactorial is less than the factorial. (Contributed by Mario Carneiro, 19-Jan-2015.)
 |-  D  =  ( x  e.  Fin  |->  ( # `  { f  |  ( f : x -1-1-onto-> x  /\  A. y  e.  x  ( f `  y
 )  =/=  y ) } ) )   &    |-  S  =  ( n  e.  NN0  |->  ( D `  ( 1
 ... n ) ) )   =>    |-  ( N  e.  NN0  ->  ( S `  N ) 
 <_  ( ! `  N ) )
 
Theoremsubfac0 23723* The subfactorial at zero. (Contributed by Mario Carneiro, 19-Jan-2015.)
 |-  D  =  ( x  e.  Fin  |->  ( # `  { f  |  ( f : x -1-1-onto-> x  /\  A. y  e.  x  ( f `  y
 )  =/=  y ) } ) )   &    |-  S  =  ( n  e.  NN0  |->  ( D `  ( 1
 ... n ) ) )   =>    |-  ( S `  0
 )  =  1
 
Theoremsubfac1 23724* The subfactorial at one. (Contributed by Mario Carneiro, 19-Jan-2015.)
 |-  D  =  ( x  e.  Fin  |->  ( # `  { f  |  ( f : x -1-1-onto-> x  /\  A. y  e.  x  ( f `  y
 )  =/=  y ) } ) )   &    |-  S  =  ( n  e.  NN0  |->  ( D `  ( 1
 ... n ) ) )   =>    |-  ( S `  1
 )  =  0
 
Theoremsubfacp1lem1 23725* Lemma for subfacp1 23732. The set  K together with  { 1 ,  M } partitions the set  1 ... ( N  +  1 ). (Contributed by Mario Carneiro, 23-Jan-2015.)
 |-  D  =  ( x  e.  Fin  |->  ( # `  { f  |  ( f : x -1-1-onto-> x  /\  A. y  e.  x  ( f `  y
 )  =/=  y ) } ) )   &    |-  S  =  ( n  e.  NN0  |->  ( D `  ( 1
 ... n ) ) )   &    |-  A  =  {
 f  |  ( f : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 )
 )  /\  A. y  e.  ( 1 ... ( N  +  1 )
 ) ( f `  y )  =/=  y
 ) }   &    |-  ( ph  ->  N  e.  NN )   &    |-  ( ph  ->  M  e.  (
 2 ... ( N  +  1 ) ) )   &    |-  M  e.  _V   &    |-  K  =  ( ( 2 ... ( N  +  1 )
 )  \  { M } )   =>    |-  ( ph  ->  (
 ( K  i^i  {
 1 ,  M }
 )  =  (/)  /\  ( K  u.  { 1 ,  M } )  =  ( 1 ... ( N  +  1 )
 )  /\  ( # `  K )  =  ( N  -  1 ) ) )
 
Theoremsubfacp1lem2a 23726* Lemma for subfacp1 23732. Properties of a bijection on  K augmented with the two-element flip to get a bijection on  K  u.  {
1 ,  M }. (Contributed by Mario Carneiro, 23-Jan-2015.)
 |-  D  =  ( x  e.  Fin  |->  ( # `  { f  |  ( f : x -1-1-onto-> x  /\  A. y  e.  x  ( f `  y
 )  =/=  y ) } ) )   &    |-  S  =  ( n  e.  NN0  |->  ( D `  ( 1
 ... n ) ) )   &    |-  A  =  {
 f  |  ( f : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 )
 )  /\  A. y  e.  ( 1 ... ( N  +  1 )
 ) ( f `  y )  =/=  y
 ) }   &    |-  ( ph  ->  N  e.  NN )   &    |-  ( ph  ->  M  e.  (
 2 ... ( N  +  1 ) ) )   &    |-  M  e.  _V   &    |-  K  =  ( ( 2 ... ( N  +  1 )
 )  \  { M } )   &    |-  F  =  ( G  u.  { <. 1 ,  M >. ,  <. M ,  1 >. } )   &    |-  ( ph  ->  G : K -1-1-onto-> K )   =>    |-  ( ph  ->  ( F : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 )
 )  /\  ( F `  1 )  =  M  /\  ( F `  M )  =  1 )
 )
 
Theoremsubfacp1lem2b 23727* Lemma for subfacp1 23732. Properties of a bijection on  K augmented with the two-element flip to get a bijection on  K  u.  {
1 ,  M }. (Contributed by Mario Carneiro, 23-Jan-2015.)
 |-  D  =  ( x  e.  Fin  |->  ( # `  { f  |  ( f : x -1-1-onto-> x  /\  A. y  e.  x  ( f `  y
 )  =/=  y ) } ) )   &    |-  S  =  ( n  e.  NN0  |->  ( D `  ( 1
 ... n ) ) )   &    |-  A  =  {
 f  |  ( f : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 )
 )  /\  A. y  e.  ( 1 ... ( N  +  1 )
 ) ( f `  y )  =/=  y
 ) }   &    |-  ( ph  ->  N  e.  NN )   &    |-  ( ph  ->  M  e.  (
 2 ... ( N  +  1 ) ) )   &    |-  M  e.  _V   &    |-  K  =  ( ( 2 ... ( N  +  1 )
 )  \  { M } )   &    |-  F  =  ( G  u.  { <. 1 ,  M >. ,  <. M ,  1 >. } )   &    |-  ( ph  ->  G : K -1-1-onto-> K )   =>    |-  ( ( ph  /\  X  e.  K )  ->  ( F `  X )  =  ( G `  X ) )
 
Theoremsubfacp1lem3 23728* Lemma for subfacp1 23732. In subfacp1lem6 23731 we cut up the set of all derangements on  1 ... ( N  +  1 ) first according to the value at  1, and then by whether or not  ( f `  ( f `  1
) )  =  1. In this lemma, we show that the subset of all  N  +  1 derangements that satisfy this for fixed  M  =  ( f `  1 ) is in bijection with  N  -  1 derangements, by simply dropping the  x  =  1 and  x  =  M points from the function to get a derangement on  K  =  ( 1 ... ( N  -  1 ) ) 
\  { 1 ,  M }. (Contributed by Mario Carneiro, 23-Jan-2015.)
 |-  D  =  ( x  e.  Fin  |->  ( # `  { f  |  ( f : x -1-1-onto-> x  /\  A. y  e.  x  ( f `  y
 )  =/=  y ) } ) )   &    |-  S  =  ( n  e.  NN0  |->  ( D `  ( 1
 ... n ) ) )   &    |-  A  =  {
 f  |  ( f : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 )
 )  /\  A. y  e.  ( 1 ... ( N  +  1 )
 ) ( f `  y )  =/=  y
 ) }   &    |-  ( ph  ->  N  e.  NN )   &    |-  ( ph  ->  M  e.  (
 2 ... ( N  +  1 ) ) )   &    |-  M  e.  _V   &    |-  K  =  ( ( 2 ... ( N  +  1 )
 )  \  { M } )   &    |-  B  =  {
 g  e.  A  |  ( ( g `  1 )  =  M  /\  ( g `  M )  =  1 ) }   &    |-  C  =  { f  |  ( f : K -1-1-onto-> K  /\  A. y  e.  K  ( f `  y
 )  =/=  y ) }   =>    |-  ( ph  ->  ( # `
  B )  =  ( S `  ( N  -  1 ) ) )
 
Theoremsubfacp1lem4 23729* Lemma for subfacp1 23732. The function  F, which swaps  1 with  M and leaves all other elements alone, is a bijection of order  2, i.e. it is its own inverse. (Contributed by Mario Carneiro, 19-Jan-2015.)
 |-  D  =  ( x  e.  Fin  |->  ( # `  { f  |  ( f : x -1-1-onto-> x  /\  A. y  e.  x  ( f `  y
 )  =/=  y ) } ) )   &    |-  S  =  ( n  e.  NN0  |->  ( D `  ( 1
 ... n ) ) )   &    |-  A  =  {
 f  |  ( f : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 )
 )  /\  A. y  e.  ( 1 ... ( N  +  1 )
 ) ( f `  y )  =/=  y
 ) }   &    |-  ( ph  ->  N  e.  NN )   &    |-  ( ph  ->  M  e.  (
 2 ... ( N  +  1 ) ) )   &    |-  M  e.  _V   &    |-  K  =  ( ( 2 ... ( N  +  1 )
 )  \  { M } )   &    |-  B  =  {
 g  e.  A  |  ( ( g `  1 )  =  M  /\  ( g `  M )  =/=  1 ) }   &    |-  F  =  ( (  _I  |`  K )  u.  { <. 1 ,  M >. ,  <. M , 
 1 >. } )   =>    |-  ( ph  ->  `' F  =  F )
 
Theoremsubfacp1lem5 23730* Lemma for subfacp1 23732. In subfacp1lem6 23731 we cut up the set of all derangements on  1 ... ( N  +  1 ) first according to the value at  1, and then by whether or not  ( f `  ( f `  1
) )  =  1. In this lemma, we show that the subset of all  N  +  1 derangements with  ( f `  ( f `  1
) )  =/=  1 for fixed  M  =  ( f ` 
1 ) is in bijection with derangements of  2 ... ( N  + 
1 ), because pre-composing with the function  F swaps  1 and  M and turns the function into a bijection with  ( f `  1 )  =  1 and  ( f `  x )  =/=  x for all other  x, so dropping the point at  1 yields a derangement on the  N remaining points. (Contributed by Mario Carneiro, 23-Jan-2015.)
 |-  D  =  ( x  e.  Fin  |->  ( # `  { f  |  ( f : x -1-1-onto-> x  /\  A. y  e.  x  ( f `  y
 )  =/=  y ) } ) )   &    |-  S  =  ( n  e.  NN0  |->  ( D `  ( 1
 ... n ) ) )   &    |-  A  =  {
 f  |  ( f : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 )
 )  /\  A. y  e.  ( 1 ... ( N  +  1 )
 ) ( f `  y )  =/=  y
 ) }   &    |-  ( ph  ->  N  e.  NN )   &    |-  ( ph  ->  M  e.  (
 2 ... ( N  +  1 ) ) )   &    |-  M  e.  _V   &    |-  K  =  ( ( 2 ... ( N  +  1 )
 )  \  { M } )   &    |-  B  =  {
 g  e.  A  |  ( ( g `  1 )  =  M  /\  ( g `  M )  =/=  1 ) }   &    |-  F  =  ( (  _I  |`  K )  u.  { <. 1 ,  M >. ,  <. M , 
 1 >. } )   &    |-  C  =  { f  |  ( f : ( 2
 ... ( N  +  1 ) ) -1-1-onto-> ( 2
 ... ( N  +  1 ) )  /\  A. y  e.  ( 2
 ... ( N  +  1 ) ) ( f `  y )  =/=  y ) }   =>    |-  ( ph  ->  ( # `  B )  =  ( S `  N ) )
 
Theoremsubfacp1lem6 23731* Lemma for subfacp1 23732. By induction, we cut up the set of all derangements on  N  +  1 according to the  N possible values of  ( f ` 
1 ) (since  ( f `  1 )  =/=  1), and for each set for fixed  M  =  ( f `  1 ), the subset of derangements with  ( f `  M )  =  1 has size  S ( N  - 
1 ) (by subfacp1lem3 23728), while the subset with  ( f `  M
)  =/=  1 has size  S
( N ) (by subfacp1lem5 23730). Adding it all up yields the desired equation  N ( S ( N )  +  S ( N  - 
1 ) ) for the number of derangements on  N  +  1. (Contributed by Mario Carneiro, 22-Jan-2015.)
 |-  D  =  ( x  e.  Fin  |->  ( # `  { f  |  ( f : x -1-1-onto-> x  /\  A. y  e.  x  ( f `  y
 )  =/=  y ) } ) )   &    |-  S  =  ( n  e.  NN0  |->  ( D `  ( 1
 ... n ) ) )   &    |-  A  =  {
 f  |  ( f : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 )
 )  /\  A. y  e.  ( 1 ... ( N  +  1 )
 ) ( f `  y )  =/=  y
 ) }   =>    |-  ( N  e.  NN  ->  ( S `  ( N  +  1 )
 )  =  ( N  x.  ( ( S `
  N )  +  ( S `  ( N  -  1 ) ) ) ) )
 
Theoremsubfacp1 23732* A two-term recurrence for the subfactorial. This theorem allows us to forget the combinatorial definition of the derangement number in favor of the recursive definition provided by this theorem and subfac0 23723, subfac1 23724. (Contributed by Mario Carneiro, 23-Jan-2015.)
 |-  D  =  ( x  e.  Fin  |->  ( # `  { f  |  ( f : x -1-1-onto-> x  /\  A. y  e.  x  ( f `  y
 )  =/=  y ) } ) )   &    |-  S  =  ( n  e.  NN0  |->  ( D `  ( 1
 ... n ) ) )   =>    |-  ( N  e.  NN  ->  ( S `  ( N  +  1 )
 )  =  ( N  x.  ( ( S `
  N )  +  ( S `  ( N  -  1 ) ) ) ) )
 
Theoremsubfacval2 23733* A closed-form expression for the subfactorial. (Contributed by Mario Carneiro, 23-Jan-2015.)
 |-  D  =  ( x  e.  Fin  |->  ( # `  { f  |  ( f : x -1-1-onto-> x  /\  A. y  e.  x  ( f `  y
 )  =/=  y ) } ) )   &    |-  S  =  ( n  e.  NN0  |->  ( D `  ( 1
 ... n ) ) )   =>    |-  ( N  e.  NN0  ->  ( S `  N )  =  ( ( ! `
  N )  x. 
 sum_ k  e.  (
 0 ... N ) ( ( -u 1 ^ k
 )  /  ( ! `  k ) ) ) )
 
Theoremsubfaclim 23734* The subfactorial converges rapidly to  N !  /  _e. (Contributed by Mario Carneiro, 23-Jan-2015.)
 |-  D  =  ( x  e.  Fin  |->  ( # `  { f  |  ( f : x -1-1-onto-> x  /\  A. y  e.  x  ( f `  y
 )  =/=  y ) } ) )   &    |-  S  =  ( n  e.  NN0  |->  ( D `  ( 1
 ... n ) ) )   =>    |-  ( N  e.  NN  ->  ( abs `  (
 ( ( ! `  N )  /  _e )  -  ( S `  N ) ) )  <  ( 1  /  N ) )
 
Theoremsubfacval3 23735* Another closed form expression for the subfactorial. The expression  |_ `  (
x  +  1  / 
2 ) is a way of saying "rounded to the nearest integer". (Contributed by Mario Carneiro, 23-Jan-2015.)
 |-  D  =  ( x  e.  Fin  |->  ( # `  { f  |  ( f : x -1-1-onto-> x  /\  A. y  e.  x  ( f `  y
 )  =/=  y ) } ) )   &    |-  S  =  ( n  e.  NN0  |->  ( D `  ( 1
 ... n ) ) )   =>    |-  ( N  e.  NN  ->  ( S `  N )  =  ( |_ `  ( ( ( ! `
  N )  /  _e )  +  (
 1  /  2 )
 ) ) )
 
Theoremderangfmla 23736* The derangements formula, which expresses the number of derangements of a finite nonempty set in terms of the factorial. The expression  |_ `  (
x  +  1  / 
2 ) is a way of saying "rounded to the nearest integer". (Contributed by Mario Carneiro, 23-Jan-2015.)
 |-  D  =  ( x  e.  Fin  |->  ( # `  { f  |  ( f : x -1-1-onto-> x  /\  A. y  e.  x  ( f `  y
 )  =/=  y ) } ) )   =>    |-  ( ( A  e.  Fin  /\  A  =/=  (/) )  ->  ( D `  A )  =  ( |_ `  ( ( ( ! `  ( # `
  A ) ) 
 /  _e )  +  ( 1  /  2
 ) ) ) )
 
18.4.5  The Erdős-Szekeres theorem
 
Theoremerdszelem1 23737* Lemma for erdsze 23748. (Contributed by Mario Carneiro, 22-Jan-2015.)
 |-  S  =  { y  e.  ~P ( 1 ... A )  |  ( ( F  |`  y )  Isom  <  ,  O  ( y ,  ( F " y
 ) )  /\  A  e.  y ) }   =>    |-  ( X  e.  S 
 <->  ( X  C_  (
 1 ... A )  /\  ( F  |`  X ) 
 Isom  <  ,  O  ( X ,  ( F
 " X ) ) 
 /\  A  e.  X ) )
 
Theoremerdszelem2 23738* Lemma for erdsze 23748. (Contributed by Mario Carneiro, 22-Jan-2015.)
 |-  S  =  { y  e.  ~P ( 1 ... A )  |  ( ( F  |`  y )  Isom  <  ,  O  ( y ,  ( F " y
 ) )  /\  A  e.  y ) }   =>    |-  ( ( # " S )  e.  Fin  /\  ( # " S )  C_  NN )
 
Theoremerdszelem3 23739* Lemma for erdsze 23748. (Contributed by Mario Carneiro, 22-Jan-2015.)
 |-  ( ph  ->  N  e.  NN )   &    |-  ( ph  ->  F : ( 1 ...
 N ) -1-1-> RR )   &    |-  K  =  ( x  e.  (
 1 ... N )  |->  sup ( ( # " {
 y  e.  ~P (
 1 ... x )  |  ( ( F  |`  y ) 
 Isom  <  ,  O  ( y ,  ( F
 " y ) ) 
 /\  x  e.  y
 ) } ) ,  RR ,  <  )
 )   =>    |-  ( A  e.  (
 1 ... N )  ->  ( K `  A )  =  sup ( ( # " { y  e. 
 ~P ( 1 ...
 A )  |  ( ( F  |`  y ) 
 Isom  <  ,  O  ( y ,  ( F
 " y ) ) 
 /\  A  e.  y
 ) } ) ,  RR ,  <  )
 )
 
Theoremerdszelem4 23740* Lemma for erdsze 23748. (Contributed by Mario Carneiro, 22-Jan-2015.)
 |-  ( ph  ->  N  e.  NN )   &    |-  ( ph  ->  F : ( 1 ...
 N ) -1-1-> RR )   &    |-  K  =  ( x  e.  (
 1 ... N )  |->  sup ( ( # " {
 y  e.  ~P (
 1 ... x )  |  ( ( F  |`  y ) 
 Isom  <  ,  O  ( y ,  ( F
 " y ) ) 
 /\  x  e.  y
 ) } ) ,  RR ,  <  )
 )   &    |-  O  Or  RR   =>    |-  ( ( ph  /\  A  e.  ( 1
 ... N ) ) 
 ->  { A }  e.  { y  e.  ~P (
 1 ... A )  |  ( ( F  |`  y ) 
 Isom  <  ,  O  ( y ,  ( F
 " y ) ) 
 /\  A  e.  y
 ) } )
 
Theoremerdszelem5 23741* Lemma for erdsze 23748. (Contributed by Mario Carneiro, 22-Jan-2015.)
 |-  ( ph  ->  N  e.  NN )   &    |-  ( ph  ->  F : ( 1 ...
 N ) -1-1-> RR )   &    |-  K  =  ( x  e.  (
 1 ... N )  |->  sup ( ( # " {
 y  e.  ~P (
 1 ... x )  |  ( ( F  |`  y ) 
 Isom  <  ,  O  ( y ,  ( F
 " y ) ) 
 /\  x  e.  y
 ) } ) ,  RR ,  <  )
 )   &    |-  O  Or  RR   =>    |-  ( ( ph  /\  A  e.  ( 1
 ... N ) ) 
 ->  ( K `  A )  e.  ( # " {
 y  e.  ~P (
 1 ... A )  |  ( ( F  |`  y ) 
 Isom  <  ,  O  ( y ,  ( F
 " y ) ) 
 /\  A  e.  y
 ) } ) )
 
Theoremerdszelem6 23742* Lemma for erdsze 23748. (Contributed by Mario Carneiro, 22-Jan-2015.)
 |-  ( ph  ->  N  e.  NN )   &    |-  ( ph  ->  F : ( 1 ...
 N ) -1-1-> RR )   &    |-  K  =  ( x  e.  (
 1 ... N )  |->  sup ( ( # " {
 y  e.  ~P (
 1 ... x )  |  ( ( F  |`  y ) 
 Isom  <  ,  O  ( y ,  ( F
 " y ) ) 
 /\  x  e.  y
 ) } ) ,  RR ,  <  )
 )   &    |-  O  Or  RR   =>    |-  ( ph  ->  K : ( 1 ...
 N ) --> NN )
 
Theoremerdszelem7 23743* Lemma for erdsze 23748. (Contributed by Mario Carneiro, 22-Jan-2015.)
 |-  ( ph  ->  N  e.  NN )   &    |-  ( ph  ->  F : ( 1 ...
 N ) -1-1-> RR )   &    |-  K  =  ( x  e.  (
 1 ... N )  |->  sup ( ( # " {
 y  e.  ~P (
 1 ... x )  |  ( ( F  |`  y ) 
 Isom  <  ,  O  ( y ,  ( F
 " y ) ) 
 /\  x  e.  y
 ) } ) ,  RR ,  <  )
 )   &    |-  O  Or  RR   &    |-  ( ph  ->  A  e.  (
 1 ... N ) )   &    |-  ( ph  ->  R  e.  NN )   &    |-  ( ph  ->  -.  ( K `  A )  e.  ( 1 ... ( R  -  1
 ) ) )   =>    |-  ( ph  ->  E. s  e.  ~P  (
 1 ... N ) ( R  <_  ( # `  s
 )  /\  ( F  |`  s )  Isom  <  ,  O  ( s ,  ( F " s
 ) ) ) )
 
Theoremerdszelem8 23744* Lemma for erdsze 23748. (Contributed by Mario Carneiro, 22-Jan-2015.)
 |-  ( ph  ->  N  e.  NN )   &    |-  ( ph  ->  F : ( 1 ...
 N ) -1-1-> RR )   &    |-  K  =  ( x  e.  (
 1 ... N )  |->  sup ( ( # " {
 y  e.  ~P (
 1 ... x )  |  ( ( F  |`  y ) 
 Isom  <  ,  O  ( y ,  ( F
 " y ) ) 
 /\  x  e.  y
 ) } ) ,  RR ,  <  )
 )   &    |-  O  Or  RR   &    |-  ( ph  ->  A  e.  (
 1 ... N ) )   &    |-  ( ph  ->  B  e.  ( 1 ... N ) )   &    |-  ( ph  ->  A  <  B )   =>    |-  ( ph  ->  ( ( K `  A )  =  ( K `  B )  ->  -.  ( F `  A ) O ( F `  B ) ) )
 
Theoremerdszelem9 23745* Lemma for erdsze 23748. (Contributed by Mario Carneiro, 22-Jan-2015.)
 |-  ( ph  ->  N  e.  NN )   &    |-  ( ph  ->  F : ( 1 ...
 N ) -1-1-> RR )   &    |-  I  =  ( x  e.  (
 1 ... N )  |->  sup ( ( # " {
 y  e.  ~P (
 1 ... x )  |  ( ( F  |`  y ) 
 Isom  <  ,  <  (
 y ,  ( F
 " y ) ) 
 /\  x  e.  y
 ) } ) ,  RR ,  <  )
 )   &    |-  J  =  ( x  e.  ( 1 ...
 N )  |->  sup (
 ( # " { y  e.  ~P ( 1 ... x )  |  ( ( F  |`  y ) 
 Isom  <  ,  `'  <  ( y ,  ( F
 " y ) ) 
 /\  x  e.  y
 ) } ) ,  RR ,  <  )
 )   &    |-  T  =  ( n  e.  ( 1 ...
 N )  |->  <. ( I `
  n ) ,  ( J `  n ) >. )   =>    |-  ( ph  ->  T : ( 1 ...
 N ) -1-1-> ( NN 
 X.  NN ) )
 
Theoremerdszelem10 23746* Lemma for erdsze 23748. (Contributed by Mario Carneiro, 22-Jan-2015.)
 |-  ( ph  ->  N  e.  NN )   &    |-  ( ph  ->  F : ( 1 ...
 N ) -1-1-> RR )   &    |-  I  =  ( x  e.  (
 1 ... N )  |->  sup ( ( # " {
 y  e.  ~P (
 1 ... x )  |  ( ( F  |`  y ) 
 Isom  <  ,  <  (
 y ,  ( F
 " y ) ) 
 /\  x  e.  y
 ) } ) ,  RR ,  <  )
 )   &    |-  J  =  ( x  e.  ( 1 ...
 N )  |->  sup (