Home | Metamath
Proof ExplorerTheorem List
(p. 248 of 325)
| < Previous Next > |

Browser slow? Try the
Unicode version. |

Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs

Color key: | Metamath Proof Explorer
(1-22374) |
Hilbert Space Explorer
(22375-23897) |
Users' Mathboxes
(23898-32447) |

Type | Label | Description |
---|---|---|

Statement | ||

Theorem | ballotlemfelz 24701* | has values in . (Contributed by Thierry Arnoux, 23-Nov-2016.) |

Theorem | ballotlemfp1 24702* | If the th ballot is for A, goes up 1. If the th ballot is for B, goes down 1. (Contributed by Thierry Arnoux, 24-Nov-2016.) |

Theorem | ballotlemfc0 24703* | takes value 0 between negative and positive values. (Contributed by Thierry Arnoux, 24-Nov-2016.) |

Theorem | ballotlemfcc 24704* | takes value 0 between positive and negative values. (Contributed by Thierry Arnoux, 2-Apr-2017.) |

Theorem | ballotlemfmpn 24705* | finishes counting at . (Contributed by Thierry Arnoux, 25-Nov-2016.) |

Theorem | ballotlemfval0 24706* | always starts counting at 0 . (Contributed by Thierry Arnoux, 25-Nov-2016.) |

Theorem | ballotleme 24707* | Elements of . (Contributed by Thierry Arnoux, 14-Dec-2016.) |

Theorem | ballotlemodife 24708* | Elements of . (Contributed by Thierry Arnoux, 7-Dec-2016.) |

Theorem | ballotlem4 24709* | If the first pick is a vote for B, A is not ahead throughout the count (Contributed by Thierry Arnoux, 25-Nov-2016.) |

Theorem | ballotlem5 24710* | If A is not ahead throughout, there is a where votes are tied. (Contributed by Thierry Arnoux, 1-Dec-2016.) |

Theorem | ballotlemi 24711* | Value of for a given counting . (Contributed by Thierry Arnoux, 1-Dec-2016.) |

Theorem | ballotlemiex 24712* | Properties of . (Contributed by Thierry Arnoux, 12-Dec-2016.) |

Theorem | ballotlemi1 24713* | The first tie cannot be reached at the first pick. (Contributed by Thierry Arnoux, 12-Mar-2017.) |

Theorem | ballotlemii 24714* | The first tie cannot be reached at the first pick. (Contributed by Thierry Arnoux, 4-Apr-2017.) |

Theorem | ballotlemsup 24715* | The set of zeroes of satisfies the conditions to have a supremum (Contributed by Thierry Arnoux, 1-Dec-2016.) |

Theorem | ballotlemimin 24716* | is the first tie. (Contributed by Thierry Arnoux, 1-Dec-2016.) |

Theorem | ballotlemic 24717* | If the first vote is for B, the vote on the first tie is for A. (Contributed by Thierry Arnoux, 1-Dec-2016.) |

Theorem | ballotlem1c 24718* | If the first vote is for A, the vote on the first tie is for B. (Contributed by Thierry Arnoux, 4-Apr-2017.) |

Theorem | ballotlemsval 24719* | Value of (Contributed by Thierry Arnoux, 12-Apr-2017.) |

Theorem | ballotlemsv 24720* | Value of evaluated at for a given counting . (Contributed by Thierry Arnoux, 12-Apr-2017.) |

Theorem | ballotlemsgt1 24721* | maps values less than to values greater than 1. (Contributed by Thierry Arnoux, 28-Apr-2017.) |

Theorem | ballotlemsdom 24722* | Domain of for a given counting . (Contributed by Thierry Arnoux, 12-Apr-2017.) |

Theorem | ballotlemsel1i 24723* | The range is invariant under . (Contributed by Thierry Arnoux, 28-Apr-2017.) |

Theorem | ballotlemsf1o 24724* | The defined is a bijection, and an involution. (Contributed by Thierry Arnoux, 14-Apr-2017.) |

Theorem | ballotlemsi 24725* | The image by of the first tie pick is the first pick. (Contributed by Thierry Arnoux, 14-Apr-2017.) |

Theorem | ballotlemsima 24726* | The image by of an interval before the first pick. (Contributed by Thierry Arnoux, 5-May-2017.) |

Theorem | ballotlemieq 24727* | If two countings share the same first tie, they also have the same swap function. (Contributed by Thierry Arnoux, 18-Apr-2017.) |

Theorem | ballotlemrval 24728* | Value of . (Contributed by Thierry Arnoux, 14-Apr-2017.) |

Theorem | ballotlemscr 24729* | The image of by (Contributed by Thierry Arnoux, 21-Apr-2017.) |

Theorem | ballotlemrv 24730* | Value of evaluated at . (Contributed by Thierry Arnoux, 17-Apr-2017.) |

Theorem | ballotlemrv1 24731* | Value of before the tie. (Contributed by Thierry Arnoux, 11-Apr-2017.) |

Theorem | ballotlemrv2 24732* | Value of after the tie. (Contributed by Thierry Arnoux, 11-Apr-2017.) |

Theorem | ballotlemro 24733* | Range of is included in . (Contributed by Thierry Arnoux, 17-Apr-2017.) |

Theorem | ballotlemgval 24734* | Expand the value of . (Contributed by Thierry Arnoux, 21-Apr-2017.) |

Theorem | ballotlemgun 24735* | A property of the defined operator (Contributed by Thierry Arnoux, 26-Apr-2017.) |

Theorem | ballotlemfg 24736* | Express the value of in terms of . (Contributed by Thierry Arnoux, 21-Apr-2017.) |

Theorem | ballotlemfrc 24737* | Express the value of in terms of the newly defined . (Contributed by Thierry Arnoux, 21-Apr-2017.) |

Theorem | ballotlemfrci 24738* | Reverse counting preserves a tie at the first tie. (Contributed by Thierry Arnoux, 21-Apr-2017.) |

Theorem | ballotlemfrceq 24739* | Value of for a reverse counting . (Contributed by Thierry Arnoux, 27-Apr-2017.) |

Theorem | ballotlemfrcn0 24740* | Value of for a reversed counting , before the first tie, cannot be zero . (Contributed by Thierry Arnoux, 25-Apr-2017.) |

Theorem | ballotlemrc 24741* | Range of . (Contributed by Thierry Arnoux, 19-Apr-2017.) |

Theorem | ballotlemirc 24742* | Applying does not change first ties. (Contributed by Thierry Arnoux, 19-Apr-2017.) |

Theorem | ballotlemrinv0 24743* | Lemma for ballotlemrinv 24744. (Contributed by Thierry Arnoux, 18-Apr-2017.) |

Theorem | ballotlemrinv 24744* | is its own inverse : it is an involution. (Contributed by Thierry Arnoux, 10-Apr-2017.) |

Theorem | ballotlem1ri 24745* | 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.) |

Theorem | ballotlem7 24746* | is a bijection between two subsets of : 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.) |

Theorem | ballotlem8 24747* | 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.) |

Theorem | ballotth 24748* | Bertrand's ballot problem : the probability that A is ahead throughout the counting. (Contributed by Thierry Arnoux, 7-Dec-2016.) |

19.4 Mathbox for Mario
Carneiro | ||

19.4.1 Miscellaneous stuff | ||

Theorem | quartfull 24749 | 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.) |

; ; ; ;; ; ; ; ;; ; ; ;; ; ; ; ;; ; ; ; ;; ; ; ;; ; ; ;; ; ; ; ;; ; ; ; ;; ; ; ;; ; ; ; ;; ; ; ; ;; ; ; ;; ; ; ;; ; ; ; ;; ; ; ; ;; ; ; ;; ; ; ; ;; ; ; ; ;; ; ; ;; ; ; ;; ; ; ; ;; ; ; ; ;; ; ; ;; ; ; ; ;; ; ; ; ;; ; ; ;; ; ; ;; ; ; ; ;; ; ; ; ;; ; ; ;; |