HomeHome Metamath Proof Explorer
Theorem List (p. 231 of 315)
< 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-21494)
  Hilbert Space Explorer  Hilbert Space Explorer
(21495-23017)
  Users' Mathboxes  Users' Mathboxes
(23018-31433)
 

Theorem List for Metamath Proof Explorer - 23001-23100   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremmdoc1i 23001 Orthocomplements form a modular pair. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
 |-  A  e.  CH   =>    |-  A  MH  ( _|_ `  A )
 
Theoremmdoc2i 23002 Orthocomplements form a modular pair. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
 |-  A  e.  CH   =>    |-  ( _|_ `  A )  MH  A
 
Theoremdmdoc1i 23003 Orthocomplements form a dual modular pair. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
 |-  A  e.  CH   =>    |-  A  MH*  ( _|_ `  A )
 
Theoremdmdoc2i 23004 Orthocomplements form a dual modular pair. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
 |-  A  e.  CH   =>    |-  ( _|_ `  A )  MH*  A
 
Theoremmdcompli 23005 A condition equivalent to the modular pair property. Part of proof of Theorem 1.14 of [MaedaMaeda] p. 4. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
 |-  A  e.  CH   &    |-  B  e.  CH   =>    |-  ( A  MH  B  <->  ( A  i^i  ( _|_ `  ( A  i^i  B ) ) )  MH  ( B  i^i  ( _|_ `  ( A  i^i  B ) ) ) )
 
Theoremdmdcompli 23006 A condition equivalent to the dual modular pair property. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
 |-  A  e.  CH   &    |-  B  e.  CH   =>    |-  ( A  MH*  B  <->  ( A  i^i  ( _|_ `  ( A  i^i  B ) ) ) 
 MH*  ( B  i^i  ( _|_ `  ( A  i^i  B ) ) ) )
 
Theoremmddmdin0i 23007* If dual modular implies modular whenever meet is zero, then dual modular implies modular for arbitrary lattice elements. This theorem is needed for the remark after Lemma 7 of [Holland] p. 1524 to hold. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
 |-  A  e.  CH   &    |-  B  e.  CH   &    |-  A. x  e.  CH  A. y  e. 
 CH  ( ( x 
 MH*  y  /\  ( x  i^i  y )  =  0H )  ->  x  MH  y )   =>    |-  ( A  MH*  B  ->  A  MH  B )
 
Theoremcdjreui 23008* A member of the sum of disjoint subspaces has a unique decomposition. Part of Lemma 5 of [Holland] p. 1520. (Contributed by NM, 20-May-2005.) (New usage is discouraged.)
 |-  A  e.  SH   &    |-  B  e.  SH   =>    |-  (
 ( C  e.  ( A  +H  B )  /\  ( A  i^i  B )  =  0H )  ->  E! x  e.  A  E. y  e.  B  C  =  ( x  +h  y ) )
 
Theoremcdj1i 23009* Two ways to express " A and  B are completely disjoint subspaces." (1) => (2) in Lemma 5 of [Holland] p. 1520. (Contributed by NM, 21-May-2005.) (New usage is discouraged.)
 |-  A  e.  SH   &    |-  B  e.  SH   =>    |-  ( E. w  e.  RR  ( 0  <  w  /\  A. y  e.  A  A. v  e.  B  ( ( normh `  y )  +  ( normh `  v )
 )  <_  ( w  x.  ( normh `  ( y  +h  v ) ) ) )  ->  E. x  e.  RR  ( 0  < 
 x  /\  A. y  e.  A  A. z  e.  B  ( ( normh `  y )  =  1 
 ->  x  <_  ( normh `  ( y  -h  z
 ) ) ) ) )
 
Theoremcdj3lem1 23010* A property of " A and  B are completely disjoint subspaces." Part of Lemma 5 of [Holland] p. 1520. (Contributed by NM, 23-May-2005.) (New usage is discouraged.)
 |-  A  e.  SH   &    |-  B  e.  SH   =>    |-  ( E. x  e.  RR  ( 0  <  x  /\  A. y  e.  A  A. z  e.  B  ( ( normh `  y )  +  ( normh `  z )
 )  <_  ( x  x.  ( normh `  ( y  +h  z ) ) ) )  ->  ( A  i^i  B )  =  0H )
 
Theoremcdj3lem2 23011* Lemma for cdj3i 23017. Value of the first-component function  S. (Contributed by NM, 23-May-2005.) (New usage is discouraged.)
 |-  A  e.  SH   &    |-  B  e.  SH   &    |-  S  =  ( x  e.  ( A  +H  B )  |->  (
 iota_ z  e.  A E. w  e.  B  x  =  ( z  +h  w ) ) )   =>    |-  ( ( C  e.  A  /\  D  e.  B  /\  ( A  i^i  B )  =  0H )  ->  ( S `  ( C  +h  D ) )  =  C )
 
Theoremcdj3lem2a 23012* Lemma for cdj3i 23017. Closure of the first-component function  S. (Contributed by NM, 25-May-2005.) (New usage is discouraged.)
 |-  A  e.  SH   &    |-  B  e.  SH   &    |-  S  =  ( x  e.  ( A  +H  B )  |->  (
 iota_ z  e.  A E. w  e.  B  x  =  ( z  +h  w ) ) )   =>    |-  ( ( C  e.  ( A  +H  B ) 
 /\  ( A  i^i  B )  =  0H )  ->  ( S `  C )  e.  A )
 
Theoremcdj3lem2b 23013* Lemma for cdj3i 23017. The first-component function  S is bounded if the subspaces are completely disjoint. (Contributed by NM, 26-May-2005.) (New usage is discouraged.)
 |-  A  e.  SH   &    |-  B  e.  SH   &    |-  S  =  ( x  e.  ( A  +H  B )  |->  (
 iota_ z  e.  A E. w  e.  B  x  =  ( z  +h  w ) ) )   =>    |-  ( E. v  e.  RR  ( 0  <  v  /\  A. x  e.  A  A. y  e.  B  ( ( normh `  x )  +  ( normh `  y )
 )  <_  ( v  x.  ( normh `  ( x  +h  y ) ) ) )  ->  E. v  e.  RR  ( 0  < 
 v  /\  A. u  e.  ( A  +H  B ) ( normh `  ( S `  u ) ) 
 <_  ( v  x.  ( normh `  u ) ) ) )
 
Theoremcdj3lem3 23014* Lemma for cdj3i 23017. Value of the second-component function  T. (Contributed by NM, 23-May-2005.) (New usage is discouraged.)
 |-  A  e.  SH   &    |-  B  e.  SH   &    |-  T  =  ( x  e.  ( A  +H  B )  |->  (
 iota_ w  e.  B E. z  e.  A  x  =  ( z  +h  w ) ) )   =>    |-  ( ( C  e.  A  /\  D  e.  B  /\  ( A  i^i  B )  =  0H )  ->  ( T `  ( C  +h  D ) )  =  D )
 
Theoremcdj3lem3a 23015* Lemma for cdj3i 23017. Closure of the second-component function  T. (Contributed by NM, 26-May-2005.) (New usage is discouraged.)
 |-  A  e.  SH   &    |-  B  e.  SH   &    |-  T  =  ( x  e.  ( A  +H  B )  |->  (
 iota_ w  e.  B E. z  e.  A  x  =  ( z  +h  w ) ) )   =>    |-  ( ( C  e.  ( A  +H  B ) 
 /\  ( A  i^i  B )  =  0H )  ->  ( T `  C )  e.  B )
 
Theoremcdj3lem3b 23016* Lemma for cdj3i 23017. The second-component function  T is bounded if the subspaces are completely disjoint. (Contributed by NM, 31-May-2005.) (New usage is discouraged.)
 |-  A  e.  SH   &    |-  B  e.  SH   &    |-  T  =  ( x  e.  ( A  +H  B )  |->  (
 iota_ w  e.  B E. z  e.  A  x  =  ( z  +h  w ) ) )   =>    |-  ( E. v  e.  RR  ( 0  <  v  /\  A. x  e.  A  A. y  e.  B  ( ( normh `  x )  +  ( normh `  y )
 )  <_  ( v  x.  ( normh `  ( x  +h  y ) ) ) )  ->  E. v  e.  RR  ( 0  < 
 v  /\  A. u  e.  ( A  +H  B ) ( normh `  ( T `  u ) ) 
 <_  ( v  x.  ( normh `  u ) ) ) )
 
Theoremcdj3i 23017* Two ways to express " A and  B are completely disjoint subspaces." (1) <=> (3) in Lemma 5 of [Holland] p. 1520. (Contributed by NM, 1-Jun-2005.) (New usage is discouraged.)
 |-  A  e.  SH   &    |-  B  e.  SH   &    |-  S  =  ( x  e.  ( A  +H  B )  |->  (
 iota_ z  e.  A E. w  e.  B  x  =  ( z  +h  w ) ) )   &    |-  T  =  ( x  e.  ( A  +H  B )  |->  ( iota_ w  e.  B E. z  e.  A  x  =  ( z  +h  w ) ) )   &    |-  ( ph  <->  E. v  e.  RR  ( 0  <  v  /\  A. u  e.  ( A  +H  B ) (
 normh `  ( S `  u ) )  <_  ( v  x.  ( normh `  u ) ) ) )   &    |-  ( ps  <->  E. v  e.  RR  ( 0  <  v  /\  A. u  e.  ( A  +H  B ) (
 normh `  ( T `  u ) )  <_  ( v  x.  ( normh `  u ) ) ) )   =>    |-  ( E. v  e. 
 RR  ( 0  < 
 v  /\  A. x  e.  A  A. y  e.  B  ( ( normh `  x )  +  ( normh `  y ) ) 
 <_  ( v  x.  ( normh `  ( x  +h  y ) ) ) )  <->  ( ( A  i^i  B )  =  0H  /\  ph  /\  ps ) )
 
PART 18  SUPPLEMENTARY MATERIAL (USER'S MATHBOXES)
 
18.1  Mathboxes for user contributions
 
18.1.1  Mathbox guidelines
 
Theoremmathbox 23018 (This theorem is a dummy placeholder for these guidelines. The name of this theorem, "mathbox", is hard-coded into the Metamath program to identify the start of the mathbox section for web page generation.)

A "mathbox" is a user-contributed section that is maintained by its contributor independently from the main part of set.mm.

For contributors:

By making a contribution, you agree to release it into the public domain, according to the statement at the beginning of set.mm.

Mathboxes are provided to help keep your work synchronized with changes in set.mm, but they shouldn't be depended on as a permanent archive. If you want to preserve your original contribution, it is your responsibility to keep your own copy of it along with the version of set.mm that works with it.

Guidelines:

1. If at all possible, please use only 0-ary class constants for new definitions, for example as in df-div 9420.

2. Try to follow the style of the rest of set.mm. Each $p and $a statement must be immediately preceded with the comment that will be shown on its web page description. The metamath program command "write source set.mm /rewrap" will take care of wrapping comment lines and indentation conventions. All mathbox content will be on public display and should hopefully reflect the overall quality of the web site.

3. Before submitting a revised mathbox, please make sure it verifies against the current set.mm.

4. Mathboxes should be independent i.e. the proofs should verify with all other mathboxes removed. If you need a theorem from another mathbox, that is fine (and encouraged), but let me know so I can move the theorem to the main section. One way avoid undesired accidental use of other mathbox theorems is to develop your mathbox using a modified set.mm that has mathboxes removed.

Notes:

1. I may decide to move some theorems to the main part of set.mm for general use. In that case, an author acknowledgment will be added to the description of the theorem.

2. I may make changes to mathboxes to maintain the overall quality of set.mm. Normally I will let you know if a change might impact what you are working on.

3. If you use theorems from another user's mathbox, I don't provide assurance that they are based on correct or consistent $a statements. (If you find such a problem, please let me know so it can be corrected.) (Contributed by NM, 20-Feb-2007.) (New usage is discouraged.)

 |-  x  =  x
 
18.2  Mathbox for Stefan Allan
 
Theoremfoo3 23019 A theorem about the universal class. (Contributed by Stefan Allan, 9-Dec-2008.)
 |-  ph   =>    |- 
 _V  =  { x  |  ph }
 
Theoremxfree 23020 A partial converse to 19.9t 1784. (Contributed by Stefan Allan, 21-Dec-2008.) (Revised by Mario Carneiro, 11-Dec-2016.)
 |-  ( A. x ( ph  ->  A. x ph )  <->  A. x ( E. x ph  ->  ph ) )
 
Theoremxfree2 23021 A partial converse to 19.9t 1784. (Contributed by Stefan Allan, 21-Dec-2008.)
 |-  ( A. x ( ph  ->  A. x ph )  <->  A. x ( -.  ph  ->  A. x  -.  ph ) )
 
TheoremaddltmulALT 23022 A proof readability experiment for addltmul 9943. (Contributed by Stefan Allan, 30-Oct-2010.) (Proof modification is discouraged.)
 |-  (
 ( ( A  e.  RR  /\  B  e.  RR )  /\  ( 2  <  A  /\  2  <  B ) )  ->  ( A  +  B )  < 
 ( A  x.  B ) )
 
18.3  Mathbox for Thierry Arnoux
 
Theoremmptcnv 23023* The converse of a mapping function. (Contributed by Thierry Arnoux, 16-Jan-2017.)
 |-  ( ph  ->  ( ( x  e.  A  /\  y  =  B )  <->  ( y  e.  C  /\  x  =  D ) ) )   =>    |-  ( ph  ->  `' ( x  e.  A  |->  B )  =  ( y  e.  C  |->  D ) )
 
Theoremreximddv 23024* Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Thierry Arnoux, 7-Dec-2016.)
 |-  (
 ( ph  /\  ( x  e.  A  /\  ps ) )  ->  ch )   &    |-  ( ph  ->  E. x  e.  A  ps )   =>    |-  ( ph  ->  E. x  e.  A  ch )
 
Theoreminfi 23025 If  A is finite,  ( A  i^i  B ) is finite. (Contributed by Thierry Arnoux, 17-Apr-2017.)
 |-  ( A  e.  Fin  ->  ( A  i^i  B )  e. 
 Fin )
 
Theoremfzspl 23026 Split the last element of a finite set of sequential integers. (more generic than fzsuc 10831) (Contributed by Thierry Arnoux, 7-Nov-2016.)
 |-  ( N  e.  ( ZZ>= `  M )  ->  ( M
 ... N )  =  ( ( M ... ( N  -  1
 ) )  u.  { N } ) )
 
Theoremfzsplit3 23027 Split a finite interval of integers into two parts. (Contributed by Thierry Arnoux, 2-May-2017.)
 |-  ( K  e.  ( M ... N )  ->  ( M ... N )  =  ( ( M ... ( K  -  1
 ) )  u.  ( K ... N ) ) )
 
Theorembcm1n 23028 The proportion of one binomial coefficient to another with  N decreased by 1. (Contributed by Thierry Arnoux, 9-Nov-2016.)
 |-  (
 ( K  e.  (
 0 ... ( N  -  1 ) )  /\  N  e.  NN )  ->  ( ( ( N  -  1 )  _C  K )  /  ( N  _C  K ) )  =  ( ( N  -  K )  /  N ) )
 
Theoremltesubnnd 23029 Subtracting an integer number from another number decreases it. See ltsubrpd 10414 (Contributed by Thierry Arnoux, 18-Apr-2017.)
 |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  N  e.  NN )   =>    |-  ( ph  ->  (
 ( M  +  1 )  -  N ) 
 <_  M )
 
Theoremifeqeqx 23030* An equality theorem tailored for ballotlemsf1o 23068 (Contributed by Thierry Arnoux, 14-Apr-2017.)
 |-  ( x  =  X  ->  A  =  C )   &    |-  ( x  =  Y  ->  B  =  a )   &    |-  ( x  =  X  ->  ( ch  <->  th ) )   &    |-  ( x  =  Y  ->  ( ch  <->  ps ) )   &    |-  ( ph  ->  a  =  C )   &    |-  ( ( ph  /\  ps )  ->  th )   &    |-  ( ph  ->  Y  e.  V )   &    |-  ( ph  ->  X  e.  W )   =>    |-  ( ( ph  /\  x  =  if ( ps ,  X ,  Y )
 )  ->  a  =  if ( ch ,  A ,  B ) )
 
Theoremfdmrn 23031 A different way to write  F is a function. (Contributed by Thierry Arnoux, 7-Dec-2016.)
 |-  ( Fun  F  <->  F :  dom  F --> ran  F )
 
Theoremnvof1o 23032 An involution is a bijection. (Contributed by Thierry Arnoux, 7-Dec-2016.)
 |-  (
 ( F  Fn  A  /\  `' F  =  F )  ->  F : A -1-1-onto-> A )
 
Theoremf1o3d 23033* Describe an implicit one-to-one onto function. (Contributed by Thierry Arnoux, 23-Apr-2017.)
 |-  ( ph  ->  F  =  ( x  e.  A  |->  C ) )   &    |-  ( ( ph  /\  x  e.  A ) 
 ->  C  e.  B )   &    |-  ( ( ph  /\  y  e.  B )  ->  D  e.  A )   &    |-  ( ( ph  /\  ( x  e.  A  /\  y  e.  B ) )  ->  ( x  =  D  <->  y  =  C ) )   =>    |-  ( ph  ->  ( F : A -1-1-onto-> B  /\  `' F  =  ( y  e.  B  |->  D ) ) )
 
Theoremrinvf1o 23034 Sufficient conditions for the restriction of an involution to be a bijection (Contributed by Thierry Arnoux, 7-Dec-2016.)
 |-  Fun  F   &    |-  `' F  =  F   &    |-  ( F " A )  C_  B   &    |-  ( F " B )  C_  A   &    |-  A  C_  dom  F   &    |-  B  C_ 
 dom  F   =>    |-  ( F  |`  A ) : A -1-1-onto-> B
 
Theoremelabreximd 23035* Class substitution in an image set. (Contributed by Thierry Arnoux, 30-Dec-2016.)
 |-  F/ x ph   &    |-  F/ x ch   &    |-  ( A  =  B  ->  ( ch  <->  ps ) )   &    |-  ( ph  ->  A  e.  V )   &    |-  ( ( ph  /\  x  e.  C )  ->  ps )   =>    |-  (
 ( ph  /\  A  e.  { y  |  E. x  e.  C  y  =  B } )  ->  ch )
 
Theoremabrexss 23036* A necessary condition for an image set to be a subset. (Contributed by Thierry Arnoux, 6-Feb-2017.)
 |-  F/_ x C   =>    |-  ( A. x  e.  A  B  e.  C  ->  { y  |  E. x  e.  A  y  =  B }  C_  C )
 
Theoremdfimafnf 23037* Alternate definition of the image of a function. (Contributed by Raph Levien, 20-Nov-2006.) (Revised by Thierry Arnoux, 24-Apr-2017.)
 |-  F/_ x A   &    |-  F/_ x F   =>    |-  ( ( Fun  F  /\  A  C_  dom  F ) 
 ->  ( F " A )  =  { y  |  E. x  e.  A  y  =  ( F `  x ) } )
 
Theoremfunimass4f 23038 Membership relation for the values of a function whose image is a subclass. (Contributed by Thierry Arnoux, 24-Apr-2017.)
 |-  F/_ x A   &    |-  F/_ x B   &    |-  F/_ x F   =>    |-  ( ( Fun 
 F  /\  A  C_  dom  F )  ->  ( ( F
 " A )  C_  B 
 <-> 
 A. x  e.  A  ( F `  x )  e.  B ) )
 
Theoremaddeq0 23039 Two complex which add up to zero are each other's negatives. (Contributed by Thierry Arnoux, 2-May-2017.)
 |-  (
 ( A  e.  CC  /\  B  e.  CC )  ->  ( ( A  +  B )  =  0  <->  A  =  -u B ) )
 
18.3.1  Bertrand's Ballot Problem
 
Theoremballotlemoex 23040*  O is a set. (Contributed by Thierry Arnoux, 7-Dec-2016.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   =>    |-  O  e.  _V
 
Theoremballotlem1 23041* The size of the universe is a binomial coefficient. (Contributed by Thierry Arnoux, 23-Nov-2016.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   =>    |-  ( # `  O )  =  ( ( M  +  N )  _C  M )
 
Theoremballotlemelo 23042* Elementhood in  O. (Contributed by Thierry Arnoux, 17-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   =>    |-  ( C  e.  O  <->  ( C  C_  ( 1 ... ( M  +  N ) )  /\  ( # `  C )  =  M ) )
 
Theoremballotlem2 23043* The probability that the first vote picked in a count is a B (Contributed by Thierry Arnoux, 23-Nov-2016.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   =>    |-  ( P `  { c  e.  O  |  -.  1  e.  c } )  =  ( N  /  ( M  +  N ) )
 
Theoremballotlemfval 23044* The value of F. (Contributed by Thierry Arnoux, 23-Nov-2016.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  ( ph  ->  C  e.  O )   &    |-  ( ph  ->  J  e.  ZZ )   =>    |-  ( ph  ->  (
 ( F `  C ) `  J )  =  ( ( # `  (
 ( 1 ... J )  i^i  C ) )  -  ( # `  (
 ( 1 ... J )  \  C ) ) ) )
 
Theoremballotlemfelz 23045*  ( F `  C ) has values in  ZZ. (Contributed by Thierry Arnoux, 23-Nov-2016.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  ( ph  ->  C  e.  O )   &    |-  ( ph  ->  J  e.  ZZ )   =>    |-  ( ph  ->  (
 ( F `  C ) `  J )  e. 
 ZZ )
 
Theoremballotlemfp1 23046* If the  J th ballot is for A,  ( F `  C ) goes up 1. If the  J th ballot is for B,  ( F `  C ) goes down 1. (Contributed by Thierry Arnoux, 24-Nov-2016.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  ( ph  ->  C  e.  O )   &    |-  ( ph  ->  J  e.  NN )   =>    |-  ( ph  ->  (
 ( -.  J  e.  C  ->  ( ( F `
  C ) `  J )  =  (
 ( ( F `  C ) `  ( J  -  1 ) )  -  1 ) ) 
 /\  ( J  e.  C  ->  ( ( F `
  C ) `  J )  =  (
 ( ( F `  C ) `  ( J  -  1 ) )  +  1 ) ) ) )
 
Theoremballotlemfc0 23047*  F takes value 0 between negative and positive values. (Contributed by Thierry Arnoux, 24-Nov-2016.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  ( ph  ->  C  e.  O )   &    |-  ( ph  ->  J  e.  NN )   &    |-  ( ph  ->  E. i  e.  ( 1 ... J ) ( ( F `
  C ) `  i )  <_  0 )   &    |-  ( ph  ->  0  <  ( ( F `  C ) `  J ) )   =>    |-  ( ph  ->  E. k  e.  ( 1 ... J ) ( ( F `
  C ) `  k )  =  0
 )
 
Theoremballotlemfcc 23048*  F takes value 0 between positive and negative values. (Contributed by Thierry Arnoux, 2-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  ( ph  ->  C  e.  O )   &    |-  ( ph  ->  J  e.  NN )   &    |-  ( ph  ->  E. i  e.  ( 1 ... J ) 0  <_  (
 ( F `  C ) `  i ) )   &    |-  ( ph  ->  ( ( F `  C ) `  J )  <  0 )   =>    |-  ( ph  ->  E. k  e.  ( 1 ... J ) ( ( F `
  C ) `  k )  =  0
 )
 
Theoremballotlemfmpn 23049*  ( F `  C ) finishes counting at  ( M  -  N ). (Contributed by Thierry Arnoux, 25-Nov-2016.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   =>    |-  ( C  e.  O  ->  ( ( F `  C ) `  ( M  +  N )
 )  =  ( M  -  N ) )
 
Theoremballotlemfval0 23050*  ( F `  C ) always starts counting at 0 . (Contributed by Thierry Arnoux, 25-Nov-2016.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   =>    |-  ( C  e.  O  ->  ( ( F `  C ) `  0
 )  =  0 )
 
Theoremballotleme 23051* Elements of  E. (Contributed by Thierry Arnoux, 14-Dec-2016.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   =>    |-  ( C  e.  E 
 <->  ( C  e.  O  /\  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  C ) `  i ) ) )
 
Theoremballotlemodife 23052* Elements of  ( O  \  E ). (Contributed by Thierry Arnoux, 7-Dec-2016.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   =>    |-  ( C  e.  ( O  \  E )  <-> 
 ( C  e.  O  /\  E. i  e.  (
 1 ... ( M  +  N ) ) ( ( F `  C ) `  i )  <_ 
 0 ) )
 
Theoremballotlem4 23053* If the first pick is a vote for B, A is not ahead throughout the count (Contributed by Thierry Arnoux, 25-Nov-2016.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   =>    |-  ( C  e.  O  ->  ( -.  1  e.  C  ->  -.  C  e.  E ) )
 
Theoremballotlem5 23054* If A is not ahead throughout, there is a  k where votes are tied. (Contributed by Thierry Arnoux, 1-Dec-2016.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   =>    |-  ( C  e.  ( O  \  E )  ->  E. k  e.  (
 1 ... ( M  +  N ) ) ( ( F `  C ) `  k )  =  0 )
 
Theoremballotlemi 23055* Value of  I for a given counting  C. (Contributed by Thierry Arnoux, 1-Dec-2016.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   =>    |-  ( C  e.  ( O  \  E ) 
 ->  ( I `  C )  =  sup ( {
 k  e.  ( 1
 ... ( M  +  N ) )  |  ( ( F `  C ) `  k
 )  =  0 } ,  RR ,  `'  <  ) )
 
Theoremballotlemiex 23056* Properties of  ( I `  C ). (Contributed by Thierry Arnoux, 12-Dec-2016.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   =>    |-  ( C  e.  ( O  \  E ) 
 ->  ( ( I `  C )  e.  (
 1 ... ( M  +  N ) )  /\  ( ( F `  C ) `  ( I `  C ) )  =  0 ) )
 
Theoremballotlemi1 23057* The first tie cannot be reached at the first pick. (Contributed by Thierry Arnoux, 12-Mar-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   =>    |-  ( ( C  e.  ( O  \  E )  /\  -.  1  e.  C )  ->  ( I `  C )  =/=  1 )
 
Theoremballotlemii 23058* The first tie cannot be reached at the first pick. (Contributed by Thierry Arnoux, 4-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   =>    |-  ( ( C  e.  ( O  \  E )  /\  1  e.  C )  ->  ( I `  C )  =/=  1 )
 
Theoremballotlemsup 23059* The set of zeroes of  F satisfies the conditions to have a supremum (Contributed by Thierry Arnoux, 1-Dec-2016.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   =>    |-  ( C  e.  ( O  \  E ) 
 ->  E. z  e.  RR  ( A. w  e.  {
 k  e.  ( 1
 ... ( M  +  N ) )  |  ( ( F `  C ) `  k
 )  =  0 }  -.  z `'  <  w 
 /\  A. w  e.  RR  ( w `'  <  z  ->  E. y  e.  {
 k  e.  ( 1
 ... ( M  +  N ) )  |  ( ( F `  C ) `  k
 )  =  0 } w `'  <  y
 ) ) )
 
Theoremballotlemimin 23060*  ( I `  C ) is the first tie. (Contributed by Thierry Arnoux, 1-Dec-2016.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   =>    |-  ( C  e.  ( O  \  E ) 
 ->  -.  E. k  e.  ( 1 ... (
 ( I `  C )  -  1 ) ) ( ( F `  C ) `  k
 )  =  0 )
 
Theoremballotlemic 23061* If the first vote is for B, the vote on the first tie is for A. (Contributed by Thierry Arnoux, 1-Dec-2016.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   =>    |-  ( ( C  e.  ( O  \  E )  /\  -.  1  e.  C )  ->  ( I `  C )  e.  C )
 
Theoremballotlem1c 23062* If the first vote is for A, the vote on the first tie is for B. (Contributed by Thierry Arnoux, 4-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   =>    |-  ( ( C  e.  ( O  \  E )  /\  1  e.  C )  ->  -.  ( I `  C )  e.  C )
 
Theoremballotlemsval 23063* Value of  S (Contributed by Thierry Arnoux, 12-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   =>    |-  ( C  e.  ( O  \  E )  ->  ( S `  C )  =  ( i  e.  ( 1 ... ( M  +  N )
 )  |->  if ( i  <_  ( I `  C ) ,  ( ( ( I `  C )  +  1 )  -  i ) ,  i
 ) ) )
 
Theoremballotlemsv 23064* Value of  S evaluated at  J for a given counting  C. (Contributed by Thierry Arnoux, 12-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   =>    |-  ( ( C  e.  ( O  \  E ) 
 /\  J  e.  (
 1 ... ( M  +  N ) ) ) 
 ->  ( ( S `  C ) `  J )  =  if ( J  <_  ( I `  C ) ,  (
 ( ( I `  C )  +  1
 )  -  J ) ,  J ) )
 
Theoremballotlemsgt1 23065*  S maps values less than  ( I `  C ) to values greater than 1. (Contributed by Thierry Arnoux, 28-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   =>    |-  ( ( C  e.  ( O  \  E ) 
 /\  J  e.  (
 1 ... ( M  +  N ) )  /\  J  <  ( I `  C ) )  -> 
 1  <  ( ( S `  C ) `  J ) )
 
Theoremballotlemsdom 23066* Domain of  S for a given counting  C. (Contributed by Thierry Arnoux, 12-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   =>    |-  ( ( C  e.  ( O  \  E ) 
 /\  J  e.  (
 1 ... ( M  +  N ) ) ) 
 ->  ( ( S `  C ) `  J )  e.  ( 1 ... ( M  +  N ) ) )
 
Theoremballotlemsel1i 23067* The range  ( 1 ... ( I `  C
) ) is invariant under  ( S `  C ). (Contributed by Thierry Arnoux, 28-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   =>    |-  ( ( C  e.  ( O  \  E ) 
 /\  J  e.  (
 1 ... ( I `  C ) ) ) 
 ->  ( ( S `  C ) `  J )  e.  ( 1 ... ( I `  C ) ) )
 
Theoremballotlemsf1o 23068* The defined  S is a bijection, and an involution. (Contributed by Thierry Arnoux, 14-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   =>    |-  ( C  e.  ( O  \  E )  ->  ( ( S `  C ) : ( 1 ... ( M  +  N ) ) -1-1-onto-> ( 1 ... ( M  +  N ) ) 
 /\  `' ( S `  C )  =  ( S `  C ) ) )
 
Theoremballotlemsi 23069* The image by  S of the first tie pick is the first pick. (Contributed by Thierry Arnoux, 14-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   =>    |-  ( C  e.  ( O  \  E )  ->  ( ( S `  C ) `  ( I `  C ) )  =  1 )
 
Theoremballotlemsima 23070* The image by  S of an interval before the first pick. (Contributed by Thierry Arnoux, 5-May-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   =>    |-  ( ( C  e.  ( O  \  E ) 
 /\  J  e.  (
 1 ... ( I `  C ) ) ) 
 ->  ( ( S `  C ) " (
 1 ... J ) )  =  ( ( ( S `  C ) `
  J ) ... ( I `  C ) ) )
 
Theoremballotlemieq 23071* If two countings share the same first tie, they also have the same swap function. (Contributed by Thierry Arnoux, 18-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   =>    |-  ( ( C  e.  ( O  \  E ) 
 /\  D  e.  ( O  \  E )  /\  ( I `  C )  =  ( I `  D ) )  ->  ( S `  C )  =  ( S `  D ) )
 
Theoremballotlemrval 23072* Value of  R. (Contributed by Thierry Arnoux, 14-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   &    |-  R  =  ( c  e.  ( O 
 \  E )  |->  ( ( S `  c
 ) " c ) )   =>    |-  ( C  e.  ( O  \  E )  ->  ( R `  C )  =  ( ( S `
  C ) " C ) )
 
Theoremballotlemscr 23073* The image of  ( R `  C ) by  ( S `  C ) (Contributed by Thierry Arnoux, 21-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   &    |-  R  =  ( c  e.  ( O 
 \  E )  |->  ( ( S `  c
 ) " c ) )   =>    |-  ( C  e.  ( O  \  E )  ->  ( ( S `  C ) " ( R `  C ) )  =  C )
 
Theoremballotlemrv 23074* Value of  R evaluated at  J. (Contributed by Thierry Arnoux, 17-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   &    |-  R  =  ( c  e.  ( O 
 \  E )  |->  ( ( S `  c
 ) " c ) )   =>    |-  ( ( C  e.  ( O  \  E ) 
 /\  J  e.  (
 1 ... ( M  +  N ) ) ) 
 ->  ( J  e.  ( R `  C )  <->  if ( J  <_  ( I `  C ) ,  ( ( ( I `  C )  +  1 )  -  J ) ,  J )  e.  C )
 )
 
Theoremballotlemrv1 23075* Value of  R before the tie. (Contributed by Thierry Arnoux, 11-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   &    |-  R  =  ( c  e.  ( O 
 \  E )  |->  ( ( S `  c
 ) " c ) )   =>    |-  ( ( C  e.  ( O  \  E ) 
 /\  J  e.  (
 1 ... ( M  +  N ) )  /\  J  <_  ( I `  C ) )  ->  ( J  e.  ( R `  C )  <->  ( ( ( I `  C )  +  1 )  -  J )  e.  C ) )
 
Theoremballotlemrv2 23076* Value of  R after the tie. (Contributed by Thierry Arnoux, 11-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   &    |-  R  =  ( c  e.  ( O 
 \  E )  |->  ( ( S `  c
 ) " c ) )   =>    |-  ( ( C  e.  ( O  \  E ) 
 /\  J  e.  (
 1 ... ( M  +  N ) )  /\  ( I `  C )  <  J )  ->  ( J  e.  ( R `  C )  <->  J  e.  C ) )
 
Theoremballotlemro 23077* Range of  R is included in  O. (Contributed by Thierry Arnoux, 17-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   &    |-  R  =  ( c  e.  ( O 
 \  E )  |->  ( ( S `  c
 ) " c ) )   =>    |-  ( C  e.  ( O  \  E )  ->  ( R `  C )  e.  O )
 
Theoremballotlemgval 23078* Expand the value of  .^. (Contributed by Thierry Arnoux, 21-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   &    |-  R  =  ( c  e.  ( O 
 \  E )  |->  ( ( S `  c
 ) " c ) )   &    |-  .^  =  ( u  e. 
 Fin ,  v  e.  Fin  |->  ( ( # `  (
 v  i^i  u )
 )  -  ( # `  ( v  \  u ) ) ) )   =>    |-  ( ( U  e.  Fin  /\  V  e.  Fin )  ->  ( U  .^  V )  =  ( ( # `
  ( V  i^i  U ) )  -  ( # `
  ( V  \  U ) ) ) )
 
Theoremballotlemgun 23079* A property of the defined  .^ operator (Contributed by Thierry Arnoux, 26-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   &    |-  R  =  ( c  e.  ( O 
 \  E )  |->  ( ( S `  c
 ) " c ) )   &    |-  .^  =  ( u  e. 
 Fin ,  v  e.  Fin  |->  ( ( # `  (
 v  i^i  u )
 )  -  ( # `  ( v  \  u ) ) ) )   &    |-  ( ph  ->  U  e.  Fin )   &    |-  ( ph  ->  V  e.  Fin )   &    |-  ( ph  ->  W  e.  Fin )   &    |-  ( ph  ->  ( V  i^i  W )  =  (/) )   =>    |-  ( ph  ->  ( U  .^  ( V  u.  W ) )  =  ( ( U  .^  V )  +  ( U  .^  W ) ) )
 
Theoremballotlemfg 23080* Express the value of  ( F `  C
) in terms of  .^. (Contributed by Thierry Arnoux, 21-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   &    |-  R  =  ( c  e.  ( O 
 \  E )  |->  ( ( S `  c
 ) " c ) )   &    |-  .^  =  ( u  e. 
 Fin ,  v  e.  Fin  |->  ( ( # `  (
 v  i^i  u )
 )  -  ( # `  ( v  \  u ) ) ) )   =>    |-  ( ( C  e.  ( O  \  E ) 
 /\  J  e.  (
 0 ... ( M  +  N ) ) ) 
 ->  ( ( F `  C ) `  J )  =  ( C  .^  ( 1 ... J ) ) )
 
Theoremballotlemfrc 23081* Express the value of  ( F `  ( R `  C )
) in terms of the newly defined  .^. (Contributed by Thierry Arnoux, 21-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   &    |-  R  =  ( c  e.  ( O 
 \  E )  |->  ( ( S `  c
 ) " c ) )   &    |-  .^  =  ( u  e. 
 Fin ,  v  e.  Fin  |->  ( ( # `  (
 v  i^i  u )
 )  -  ( # `  ( v  \  u ) ) ) )   =>    |-  ( ( C  e.  ( O  \  E ) 
 /\  J  e.  (
 1 ... ( I `  C ) ) ) 
 ->  ( ( F `  ( R `  C ) ) `  J )  =  ( C  .^  ( ( ( S `
  C ) `  J ) ... ( I `  C ) ) ) )
 
Theoremballotlemfrci 23082* Reverse counting preserves a tie at the first tie. (Contributed by Thierry Arnoux, 21-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   &    |-  R  =  ( c  e.  ( O 
 \  E )  |->  ( ( S `  c
 ) " c ) )   &    |-  .^  =  ( u  e. 
 Fin ,  v  e.  Fin  |->  ( ( # `  (
 v  i^i  u )
 )  -  ( # `  ( v  \  u ) ) ) )   =>    |-  ( C  e.  ( O  \  E )  ->  ( ( F `  ( R `  C ) ) `  ( I `
  C ) )  =  0 )
 
Theoremballotlemfrceq 23083* Value of  F for a reverse counting  ( R `  C ). (Contributed by Thierry Arnoux, 27-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   &    |-  R  =  ( c  e.  ( O 
 \  E )  |->  ( ( S `  c
 ) " c ) )   &    |-  .^  =  ( u  e. 
 Fin ,  v  e.  Fin  |->  ( ( # `  (
 v  i^i  u )
 )  -  ( # `  ( v  \  u ) ) ) )   =>    |-  ( ( C  e.  ( O  \  E ) 
 /\  J  e.  (
 1 ... ( I `  C ) ) ) 
 ->  ( ( F `  C ) `  (
 ( ( S `  C ) `  J )  -  1 ) )  =  -u ( ( F `
  ( R `  C ) ) `  J ) )
 
Theoremballotlemfrcn0 23084* Value of  F for a reversed counting  ( R `  C ), before the first tie, cannot be zero . (Contributed by Thierry Arnoux, 25-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   &    |-  R  =  ( c  e.  ( O 
 \  E )  |->  ( ( S `  c
 ) " c ) )   =>    |-  ( ( C  e.  ( O  \  E ) 
 /\  J  e.  (
 1 ... ( M  +  N ) )  /\  J  <  ( I `  C ) )  ->  ( ( F `  ( R `  C ) ) `  J )  =/=  0 )
 
Theoremballotlemrc 23085* Range of  R. (Contributed by Thierry Arnoux, 19-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   &    |-  R  =  ( c  e.  ( O 
 \  E )  |->  ( ( S `  c
 ) " c ) )   =>    |-  ( C  e.  ( O  \  E )  ->  ( R `  C )  e.  ( O  \  E ) )
 
Theoremballotlemirc 23086* Applying  R does not change first ties. (Contributed by Thierry Arnoux, 19-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   &    |-  R  =  ( c  e.  ( O 
 \  E )  |->  ( ( S `  c
 ) " c ) )   =>    |-  ( C  e.  ( O  \  E )  ->  ( I `  ( R `
  C ) )  =  ( I `  C ) )
 
Theoremballotlemrinv0 23087* Lemma for ballotlemrinv 23088. (Contributed by Thierry Arnoux, 18-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   &    |-  R  =  ( c  e.  ( O 
 \  E )  |->  ( ( S `  c
 ) " c ) )   =>    |-  ( ( C  e.  ( O  \  E ) 
 /\  D  =  ( ( S `  C ) " C ) ) 
 ->  ( D  e.  ( O  \  E )  /\  C  =  ( ( S `  D ) " D ) ) )
 
Theoremballotlemrinv 23088*  R is its own inverse : it is an involution. (Contributed by Thierry Arnoux, 10-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   &    |-  R  =  ( c  e.  ( O 
 \  E )  |->  ( ( S `  c
 ) " c ) )   =>    |-  `' R  =  R
 
Theoremballotlem1ri 23089* When the vote on the first tie is for A, the first vote is also for A on the reverse counting. (Contributed by Thierry Arnoux, 18-Apr-2017.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   &    |-  R  =  ( c  e.  ( O 
 \  E )  |->  ( ( S `  c
 ) " c ) )   =>    |-  ( C  e.  ( O  \  E )  ->  ( 1  e.  ( R `  C )  <->  ( I `  C )  e.  C ) )
 
Theoremballotlem7 23090*  R is a bijection between two subsets of  ( O  \  E
): one where a vote for A is picked first, and one where a vote for B is picked first (Contributed by Thierry Arnoux, 12-Dec-2016.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   &    |-  R  =  ( c  e.  ( O 
 \  E )  |->  ( ( S `  c
 ) " c ) )   =>    |-  ( R  |`  { c  e.  ( O  \  E )  |  1  e.  c } ) : {
 c  e.  ( O 
 \  E )  |  1  e.  c } -1-1-onto-> {
 c  e.  ( O 
 \  E )  |  -.  1  e.  c }
 
Theoremballotlem8 23091* There are as many countings with ties starting with a ballot for A as there are starting with a ballot for B. (Contributed by Thierry Arnoux, 7-Dec-2016.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   &    |-  R  =  ( c  e.  ( O 
 \  E )  |->  ( ( S `  c
 ) " c ) )   =>    |-  ( # `  { c  e.  ( O  \  E )  |  1  e.  c } )  =  ( # `  { c  e.  ( O  \  E )  |  -.  1  e.  c } )
 
Theoremballotth 23092* Bertrand's ballot problem : the probability that A is ahead throughout the counting. (Contributed by Thierry Arnoux, 7-Dec-2016.)
 |-  M  e.  NN   &    |-  N  e.  NN   &    |-  O  =  { c  e.  ~P ( 1 ... ( M  +  N )
 )  |  ( # `  c )  =  M }   &    |-  P  =  ( x  e.  ~P O  |->  ( ( # `  x )  /  ( # `  O ) ) )   &    |-  F  =  ( c  e.  O  |->  ( i  e.  ZZ  |->  ( ( # `  (
 ( 1 ... i
 )  i^i  c )
 )  -  ( # `  ( ( 1 ... i )  \  c
 ) ) ) ) )   &    |-  E  =  {
 c  e.  O  |  A. i  e.  (
 1 ... ( M  +  N ) ) 0  <  ( ( F `
  c ) `  i ) }   &    |-  N  <  M   &    |-  I  =  ( c  e.  ( O 
 \  E )  |->  sup ( { k  e.  ( 1 ... ( M  +  N )
 )  |  ( ( F `  c ) `
  k )  =  0 } ,  RR ,  `'  <  ) )   &    |-  S  =  ( c  e.  ( O  \  E )  |->  ( i  e.  ( 1
 ... ( M  +  N ) )  |->  if ( i  <_  ( I `  c ) ,  ( ( ( I `
  c )  +  1 )  -  i
 ) ,  i ) ) )   &    |-  R  =  ( c  e.  ( O 
 \  E )  |->  ( ( S `  c
 ) " c ) )   =>    |-  ( P `  E )  =  ( ( M  -  N )  /  ( M  +  N ) )
 
18.4  Mathbox for Mario Carneiro
 
18.4.1  Miscellaneous stuff
 
Theoremquartfull 23093 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.  (