Home | Metamath
Proof ExplorerTheorem 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

Color key: | Metamath Proof Explorer
(1-21459) |
Hilbert Space Explorer
(21460-22982) |
Users' Mathboxes
(22983-31404) |

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

Statement | ||

Theorem | elabreximd 23001* | Class substitution in an image set. (Contributed by Thierry Arnoux, 30-Dec-2016.) |

Theorem | abrexss 23002* | A necessary condition for an image set to be a subset. (Contributed by Thierry Arnoux, 6-Feb-2017.) |

Theorem | dfimafnf 23003* | Alternate definition of the image of a function. (Contributed by Raph Levien, 20-Nov-2006.) (Revised by Thierry Arnoux, 24-Apr-2017.) |

Theorem | funimass4f 23004 | Membership relation for the values of a function whose image is a subclass. (Contributed by Thierry Arnoux, 24-Apr-2017.) |

Theorem | addeq0 23005 | Two complex which add up to zero are each other's negatives. (Contributed by Thierry Arnoux, 2-May-2017.) |

18.3.1 Bertrand's Ballot Problem | ||

Theorem | ballotlemoex 23006* | is a set. (Contributed by Thierry Arnoux, 7-Dec-2016.) |

Theorem | ballotlem1 23007* | The size of the universe is a binomial coefficient. (Contributed by Thierry Arnoux, 23-Nov-2016.) |

Theorem | ballotlemelo 23008* | Elementhood in . (Contributed by Thierry Arnoux, 17-Apr-2017.) |

Theorem | ballotlem2 23009* | The probability that the first vote picked in a count is a B (Contributed by Thierry Arnoux, 23-Nov-2016.) |

Theorem | ballotlemfval 23010* | The value of F. (Contributed by Thierry Arnoux, 23-Nov-2016.) |

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

Theorem | ballotlemfp1 23012* | 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 23013* | takes value 0 between negative and positive values. (Contributed by Thierry Arnoux, 24-Nov-2016.) |

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

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

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

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

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

Theorem | ballotlem4 23019* | 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 23020* | If A is not ahead throughout, there is a where votes are tied. (Contributed by Thierry Arnoux, 1-Dec-2016.) |

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

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

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

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

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

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

Theorem | ballotlemic 23027* | 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 23028* | 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 23029* | Value of (Contributed by Thierry Arnoux, 12-Apr-2017.) |

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem | ballotlem1ri 23055* | 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 23056* | 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 23057* | 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 23058* | Bertrand's ballot problem : the probability that A is ahead throughout the counting. (Contributed by Thierry Arnoux, 7-Dec-2016.) |

18.4 Mathbox for Mario
Carneiro | ||

18.4.1 Miscellaneous stuff | ||

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

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