Home Metamath Proof ExplorerTheorem List (p. 248 of 325) < Previous  Next > Browser slow? Try the Unicode version.

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

Theorem List for Metamath Proof Explorer - 24701-24800   *Has distinct variable group(s)
TypeLabelDescription
Statement

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

Theoremballotlemfp1 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.)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theoremballotlem1ri 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.)

Theoremballotlem7 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.)

Theoremballotlem8 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.)

Theoremballotth 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

Theoremquartfull 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.)
; ; ; ;; ; ; ; ;; ; ; ;;        ; ; ; ;; ; ; ; ;; ; ; ;; ; ; ;; ; ; ; ;; ; ; ; ;; ; ; ;;        ; ; ; ;; ; ; ; ;; ; ; ;; ; ; ;; ; ; ; ;; ; ; ; ;; ; ; ;; ; ; ; ;; ; ; ; ;; ; ; ;; ; ; ;; ; ; ; ;; ; ; ; ;; ; ; ;; ; ; ; ;; ; ; ; ;; ; ; ;; ; ; ;; ; ; ; ;; ; ; ; ;; ; ; ;;