Home | Metamath
Proof Explorer Theorem List (p. 142 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-fac 14101 | Define the factorial function on nonnegative integers. For example, (!‘5) = 120 because 1 · 2 · 3 · 4 · 5 = 120 (ex-fac 29193). In the literature, the factorial function is written as a postscript exclamation point. (Contributed by NM, 2-Dec-2004.) |
⊢ ! = ({⟨0, 1⟩} ∪ seq1( · , I )) | ||
Theorem | facnn 14102 | Value of the factorial function for positive integers. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.) |
⊢ (𝑁 ∈ ℕ → (!‘𝑁) = (seq1( · , I )‘𝑁)) | ||
Theorem | fac0 14103 | The factorial of 0. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.) |
⊢ (!‘0) = 1 | ||
Theorem | fac1 14104 | The factorial of 1. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.) |
⊢ (!‘1) = 1 | ||
Theorem | facp1 14105 | The factorial of a successor. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.) |
⊢ (𝑁 ∈ ℕ0 → (!‘(𝑁 + 1)) = ((!‘𝑁) · (𝑁 + 1))) | ||
Theorem | fac2 14106 | The factorial of 2. (Contributed by NM, 17-Mar-2005.) |
⊢ (!‘2) = 2 | ||
Theorem | fac3 14107 | The factorial of 3. (Contributed by NM, 17-Mar-2005.) |
⊢ (!‘3) = 6 | ||
Theorem | fac4 14108 | The factorial of 4. (Contributed by Mario Carneiro, 18-Jun-2015.) |
⊢ (!‘4) = ;24 | ||
Theorem | facnn2 14109 | Value of the factorial function expressed recursively. (Contributed by NM, 2-Dec-2004.) |
⊢ (𝑁 ∈ ℕ → (!‘𝑁) = ((!‘(𝑁 − 1)) · 𝑁)) | ||
Theorem | faccl 14110 | Closure of the factorial function. (Contributed by NM, 2-Dec-2004.) |
⊢ (𝑁 ∈ ℕ0 → (!‘𝑁) ∈ ℕ) | ||
Theorem | faccld 14111 | Closure of the factorial function, deduction version of faccl 14110. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (!‘𝑁) ∈ ℕ) | ||
Theorem | facmapnn 14112 | The factorial function restricted to positive integers is a mapping from the positive integers to the positive integers. (Contributed by AV, 8-Aug-2020.) |
⊢ (𝑛 ∈ ℕ ↦ (!‘𝑛)) ∈ (ℕ ↑m ℕ) | ||
Theorem | facne0 14113 | The factorial function is nonzero. (Contributed by NM, 26-Apr-2005.) |
⊢ (𝑁 ∈ ℕ0 → (!‘𝑁) ≠ 0) | ||
Theorem | facdiv 14114 | A positive integer divides the factorial of an equal or larger number. (Contributed by NM, 2-May-2005.) |
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑁 ≤ 𝑀) → ((!‘𝑀) / 𝑁) ∈ ℕ) | ||
Theorem | facndiv 14115 | No positive integer (greater than one) divides the factorial plus one of an equal or larger number. (Contributed by NM, 3-May-2005.) |
⊢ (((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ) ∧ (1 < 𝑁 ∧ 𝑁 ≤ 𝑀)) → ¬ (((!‘𝑀) + 1) / 𝑁) ∈ ℤ) | ||
Theorem | facwordi 14116 | Ordering property of factorial. (Contributed by NM, 9-Dec-2005.) |
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁) → (!‘𝑀) ≤ (!‘𝑁)) | ||
Theorem | faclbnd 14117 | A lower bound for the factorial function. (Contributed by NM, 17-Dec-2005.) |
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀↑(𝑁 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑁))) | ||
Theorem | faclbnd2 14118 | A lower bound for the factorial function. (Contributed by NM, 17-Dec-2005.) |
⊢ (𝑁 ∈ ℕ0 → ((2↑𝑁) / 2) ≤ (!‘𝑁)) | ||
Theorem | faclbnd3 14119 | A lower bound for the factorial function. (Contributed by NM, 19-Dec-2005.) |
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀↑𝑁) ≤ ((𝑀↑𝑀) · (!‘𝑁))) | ||
Theorem | faclbnd4lem1 14120 | Lemma for faclbnd4 14124. Prepare the induction step. (Contributed by NM, 20-Dec-2005.) |
⊢ 𝑁 ∈ ℕ & ⊢ 𝐾 ∈ ℕ0 & ⊢ 𝑀 ∈ ℕ0 ⇒ ⊢ ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ≤ (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁))) | ||
Theorem | faclbnd4lem2 14121 | Lemma for faclbnd4 14124. Use the weak deduction theorem to convert the hypotheses of faclbnd4lem1 14120 to antecedents. (Contributed by NM, 23-Dec-2005.) |
⊢ ((𝑀 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ) → ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ≤ (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)))) | ||
Theorem | faclbnd4lem3 14122 | Lemma for faclbnd4 14124. The 𝑁 = 0 case. (Contributed by NM, 23-Dec-2005.) |
⊢ (((𝑀 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0) ∧ 𝑁 = 0) → ((𝑁↑𝐾) · (𝑀↑𝑁)) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁))) | ||
Theorem | faclbnd4lem4 14123 | Lemma for faclbnd4 14124. Prove the 0 < 𝑁 case by induction on 𝐾. (Contributed by NM, 19-Dec-2005.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0) → ((𝑁↑𝐾) · (𝑀↑𝑁)) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁))) | ||
Theorem | faclbnd4 14124 | Variant of faclbnd5 14125 providing a non-strict lower bound. (Contributed by NM, 23-Dec-2005.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0) → ((𝑁↑𝐾) · (𝑀↑𝑁)) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁))) | ||
Theorem | faclbnd5 14125 | The factorial function grows faster than powers and exponentiations. If we consider 𝐾 and 𝑀 to be constants, the right-hand side of the inequality is a constant times 𝑁-factorial. (Contributed by NM, 24-Dec-2005.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ) → ((𝑁↑𝐾) · (𝑀↑𝑁)) < ((2 · ((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾)))) · (!‘𝑁))) | ||
Theorem | faclbnd6 14126 | Geometric lower bound for the factorial function, where N is usually held constant. (Contributed by Paul Chapman, 28-Dec-2007.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0) → ((!‘𝑁) · ((𝑁 + 1)↑𝑀)) ≤ (!‘(𝑁 + 𝑀))) | ||
Theorem | facubnd 14127 | An upper bound for the factorial function. (Contributed by Mario Carneiro, 15-Apr-2016.) |
⊢ (𝑁 ∈ ℕ0 → (!‘𝑁) ≤ (𝑁↑𝑁)) | ||
Theorem | facavg 14128 | The product of two factorials is greater than or equal to the factorial of (the floor of) their average. (Contributed by NM, 9-Dec-2005.) |
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (!‘(⌊‘((𝑀 + 𝑁) / 2))) ≤ ((!‘𝑀) · (!‘𝑁))) | ||
Syntax | cbc 14129 | Extend class notation to include the binomial coefficient operation (combinatorial choose operation). |
class C | ||
Definition | df-bc 14130* |
Define the binomial coefficient operation. For example,
(5C3) = 10 (ex-bc 29194).
In the literature, this function is often written as a column vector of the two arguments, or with the arguments as subscripts before and after the letter "C". The expression (𝑁C𝐾) is read "𝑁 choose 𝐾". Definition of binomial coefficient in [Gleason] p. 295. As suggested by Gleason, we define it to be 0 when 0 ≤ 𝑘 ≤ 𝑛 does not hold. (Contributed by NM, 10-Jul-2005.) |
⊢ C = (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0)) | ||
Theorem | bcval 14131 | Value of the binomial coefficient, 𝑁 choose 𝐾. Definition of binomial coefficient in [Gleason] p. 295. As suggested by Gleason, we define it to be 0 when 0 ≤ 𝐾 ≤ 𝑁 does not hold. See bcval2 14132 for the value in the standard domain. (Contributed by NM, 10-Jul-2005.) (Revised by Mario Carneiro, 7-Nov-2013.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ) → (𝑁C𝐾) = if(𝐾 ∈ (0...𝑁), ((!‘𝑁) / ((!‘(𝑁 − 𝐾)) · (!‘𝐾))), 0)) | ||
Theorem | bcval2 14132 | Value of the binomial coefficient, 𝑁 choose 𝐾, in its standard domain. (Contributed by NM, 9-Jun-2005.) (Revised by Mario Carneiro, 7-Nov-2013.) |
⊢ (𝐾 ∈ (0...𝑁) → (𝑁C𝐾) = ((!‘𝑁) / ((!‘(𝑁 − 𝐾)) · (!‘𝐾)))) | ||
Theorem | bcval3 14133 | Value of the binomial coefficient, 𝑁 choose 𝐾, outside of its standard domain. Remark in [Gleason] p. 295. (Contributed by NM, 14-Jul-2005.) (Revised by Mario Carneiro, 8-Nov-2013.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ∧ ¬ 𝐾 ∈ (0...𝑁)) → (𝑁C𝐾) = 0) | ||
Theorem | bcval4 14134 | Value of the binomial coefficient, 𝑁 choose 𝐾, outside of its standard domain. Remark in [Gleason] p. 295. (Contributed by NM, 14-Jul-2005.) (Revised by Mario Carneiro, 7-Nov-2013.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ∧ (𝐾 < 0 ∨ 𝑁 < 𝐾)) → (𝑁C𝐾) = 0) | ||
Theorem | bcrpcl 14135 | Closure of the binomial coefficient in the positive reals. (This is mostly a lemma before we have bccl2 14150.) (Contributed by Mario Carneiro, 10-Mar-2014.) |
⊢ (𝐾 ∈ (0...𝑁) → (𝑁C𝐾) ∈ ℝ+) | ||
Theorem | bccmpl 14136 | "Complementing" its second argument doesn't change a binary coefficient. (Contributed by NM, 21-Jun-2005.) (Revised by Mario Carneiro, 5-Mar-2014.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ) → (𝑁C𝐾) = (𝑁C(𝑁 − 𝐾))) | ||
Theorem | bcn0 14137 | 𝑁 choose 0 is 1. Remark in [Gleason] p. 296. (Contributed by NM, 17-Jun-2005.) (Revised by Mario Carneiro, 8-Nov-2013.) |
⊢ (𝑁 ∈ ℕ0 → (𝑁C0) = 1) | ||
Theorem | bc0k 14138 | The binomial coefficient " 0 choose 𝐾 " is 0 for a positive integer K. Note that (0C0) = 1 (see bcn0 14137). (Contributed by Alexander van der Vekens, 1-Jan-2018.) |
⊢ (𝐾 ∈ ℕ → (0C𝐾) = 0) | ||
Theorem | bcnn 14139 | 𝑁 choose 𝑁 is 1. Remark in [Gleason] p. 296. (Contributed by NM, 17-Jun-2005.) (Revised by Mario Carneiro, 8-Nov-2013.) |
⊢ (𝑁 ∈ ℕ0 → (𝑁C𝑁) = 1) | ||
Theorem | bcn1 14140 | Binomial coefficient: 𝑁 choose 1. (Contributed by NM, 21-Jun-2005.) (Revised by Mario Carneiro, 8-Nov-2013.) |
⊢ (𝑁 ∈ ℕ0 → (𝑁C1) = 𝑁) | ||
Theorem | bcnp1n 14141 | Binomial coefficient: 𝑁 + 1 choose 𝑁. (Contributed by NM, 20-Jun-2005.) (Revised by Mario Carneiro, 8-Nov-2013.) |
⊢ (𝑁 ∈ ℕ0 → ((𝑁 + 1)C𝑁) = (𝑁 + 1)) | ||
Theorem | bcm1k 14142 | The proportion of one binomial coefficient to another with 𝐾 decreased by 1. (Contributed by Mario Carneiro, 10-Mar-2014.) |
⊢ (𝐾 ∈ (1...𝑁) → (𝑁C𝐾) = ((𝑁C(𝐾 − 1)) · ((𝑁 − (𝐾 − 1)) / 𝐾))) | ||
Theorem | bcp1n 14143 | The proportion of one binomial coefficient to another with 𝑁 increased by 1. (Contributed by Mario Carneiro, 10-Mar-2014.) |
⊢ (𝐾 ∈ (0...𝑁) → ((𝑁 + 1)C𝐾) = ((𝑁C𝐾) · ((𝑁 + 1) / ((𝑁 + 1) − 𝐾)))) | ||
Theorem | bcp1nk 14144 | The proportion of one binomial coefficient to another with 𝑁 and 𝐾 increased by 1. (Contributed by Mario Carneiro, 16-Jan-2015.) |
⊢ (𝐾 ∈ (0...𝑁) → ((𝑁 + 1)C(𝐾 + 1)) = ((𝑁C𝐾) · ((𝑁 + 1) / (𝐾 + 1)))) | ||
Theorem | bcval5 14145 | Write out the top and bottom parts of the binomial coefficient (𝑁C𝐾) = (𝑁 · (𝑁 − 1) · ... · ((𝑁 − 𝐾) + 1)) / 𝐾! explicitly. In this form, it is valid even for 𝑁 < 𝐾, although it is no longer valid for nonpositive 𝐾. (Contributed by Mario Carneiro, 22-May-2014.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ) → (𝑁C𝐾) = ((seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁) / (!‘𝐾))) | ||
Theorem | bcn2 14146 | Binomial coefficient: 𝑁 choose 2. (Contributed by Mario Carneiro, 22-May-2014.) |
⊢ (𝑁 ∈ ℕ0 → (𝑁C2) = ((𝑁 · (𝑁 − 1)) / 2)) | ||
Theorem | bcp1m1 14147 | Compute the binomial coefficient of (𝑁 + 1) over (𝑁 − 1) (Contributed by Scott Fenton, 11-May-2014.) (Revised by Mario Carneiro, 22-May-2014.) |
⊢ (𝑁 ∈ ℕ0 → ((𝑁 + 1)C(𝑁 − 1)) = (((𝑁 + 1) · 𝑁) / 2)) | ||
Theorem | bcpasc 14148 | Pascal's rule for the binomial coefficient, generalized to all integers 𝐾. Equation 2 of [Gleason] p. 295. (Contributed by NM, 13-Jul-2005.) (Revised by Mario Carneiro, 10-Mar-2014.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾)) | ||
Theorem | bccl 14149 | A binomial coefficient, in its extended domain, is a nonnegative integer. (Contributed by NM, 10-Jul-2005.) (Revised by Mario Carneiro, 9-Nov-2013.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ) → (𝑁C𝐾) ∈ ℕ0) | ||
Theorem | bccl2 14150 | A binomial coefficient, in its standard domain, is a positive integer. (Contributed by NM, 3-Jan-2006.) (Revised by Mario Carneiro, 10-Mar-2014.) |
⊢ (𝐾 ∈ (0...𝑁) → (𝑁C𝐾) ∈ ℕ) | ||
Theorem | bcn2m1 14151 | Compute the binomial coefficient "𝑁 choose 2 " from "(𝑁 − 1) choose 2 ": (N-1) + ( (N-1) 2 ) = ( N 2 ). (Contributed by Alexander van der Vekens, 7-Jan-2018.) |
⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) + ((𝑁 − 1)C2)) = (𝑁C2)) | ||
Theorem | bcn2p1 14152 | Compute the binomial coefficient "(𝑁 + 1) choose 2 " from "𝑁 choose 2 ": N + ( N 2 ) = ( (N+1) 2 ). (Contributed by Alexander van der Vekens, 8-Jan-2018.) |
⊢ (𝑁 ∈ ℕ0 → (𝑁 + (𝑁C2)) = ((𝑁 + 1)C2)) | ||
Theorem | permnn 14153 | The number of permutations of 𝑁 − 𝑅 objects from a collection of 𝑁 objects is a positive integer. (Contributed by Jason Orendorff, 24-Jan-2007.) |
⊢ (𝑅 ∈ (0...𝑁) → ((!‘𝑁) / (!‘𝑅)) ∈ ℕ) | ||
Theorem | bcnm1 14154 | The binomial coefficent of (𝑁 − 1) is 𝑁. (Contributed by Scott Fenton, 16-May-2014.) |
⊢ (𝑁 ∈ ℕ0 → (𝑁C(𝑁 − 1)) = 𝑁) | ||
Theorem | 4bc3eq4 14155 | The value of four choose three. (Contributed by Scott Fenton, 11-Jun-2016.) |
⊢ (4C3) = 4 | ||
Theorem | 4bc2eq6 14156 | The value of four choose two. (Contributed by Scott Fenton, 9-Jan-2017.) |
⊢ (4C2) = 6 | ||
Syntax | chash 14157 | Extend the definition of a class to include the set size function. |
class ♯ | ||
Definition | df-hash 14158 | Define the set size function ♯, which gives the cardinality of a finite set as a member of ℕ0, and assigns all infinite sets the value +∞. For example, (♯‘{0, 1, 2}) = 3 (ex-hash 29195). (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ ♯ = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) ∘ card) ∪ ((V ∖ Fin) × {+∞})) | ||
Theorem | hashkf 14159 | The finite part of the size function maps all finite sets to their cardinality, as members of ℕ0. (Contributed by Mario Carneiro, 13-Sep-2013.) (Revised by Mario Carneiro, 26-Dec-2014.) |
⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) & ⊢ 𝐾 = (𝐺 ∘ card) ⇒ ⊢ 𝐾:Fin⟶ℕ0 | ||
Theorem | hashgval 14160* | The value of the ♯ function in terms of the mapping 𝐺 from ω to ℕ0. The proof avoids the use of ax-ac 10328. (Contributed by Paul Chapman, 22-Jun-2011.) (Revised by Mario Carneiro, 26-Dec-2014.) |
⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) ⇒ ⊢ (𝐴 ∈ Fin → (𝐺‘(card‘𝐴)) = (♯‘𝐴)) | ||
Theorem | hashginv 14161* | The converse of 𝐺 maps the size function's value to card. (Contributed by Paul Chapman, 22-Jun-2011.) (Revised by Mario Carneiro, 15-Sep-2013.) |
⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) ⇒ ⊢ (𝐴 ∈ Fin → (◡𝐺‘(♯‘𝐴)) = (card‘𝐴)) | ||
Theorem | hashinf 14162 | The value of the ♯ function on an infinite set. (Contributed by Mario Carneiro, 13-Jul-2014.) |
⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → (♯‘𝐴) = +∞) | ||
Theorem | hashbnd 14163 | If 𝐴 has size bounded by an integer 𝐵, then 𝐴 is finite. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ℕ0 ∧ (♯‘𝐴) ≤ 𝐵) → 𝐴 ∈ Fin) | ||
Theorem | hashfxnn0 14164 | The size function is a function into the extended nonnegative integers. (Contributed by Mario Carneiro, 13-Sep-2013.) (Revised by AV, 10-Dec-2020.) |
⊢ ♯:V⟶ℕ0* | ||
Theorem | hashf 14165 | The size function maps all finite sets to their cardinality, as members of ℕ0, and infinite sets to +∞. TODO-AV: mark as OBSOLETE and replace it by hashfxnn0 14164? (Contributed by Mario Carneiro, 13-Sep-2013.) (Revised by Mario Carneiro, 13-Jul-2014.) (Proof shortened by AV, 24-Oct-2021.) |
⊢ ♯:V⟶(ℕ0 ∪ {+∞}) | ||
Theorem | hashxnn0 14166 | The value of the hash function for a set is an extended nonnegative integer. (Contributed by Alexander van der Vekens, 6-Dec-2017.) (Revised by AV, 10-Dec-2020.) |
⊢ (𝑀 ∈ 𝑉 → (♯‘𝑀) ∈ ℕ0*) | ||
Theorem | hashresfn 14167 | Restriction of the domain of the size function. (Contributed by Thierry Arnoux, 31-Jan-2017.) |
⊢ (♯ ↾ 𝐴) Fn 𝐴 | ||
Theorem | dmhashres 14168 | Restriction of the domain of the size function. (Contributed by Thierry Arnoux, 12-Jan-2017.) |
⊢ dom (♯ ↾ 𝐴) = 𝐴 | ||
Theorem | hashnn0pnf 14169 | The value of the hash function for a set is either a nonnegative integer or positive infinity. TODO-AV: mark as OBSOLETE and replace it by hashxnn0 14166? (Contributed by Alexander van der Vekens, 6-Dec-2017.) |
⊢ (𝑀 ∈ 𝑉 → ((♯‘𝑀) ∈ ℕ0 ∨ (♯‘𝑀) = +∞)) | ||
Theorem | hashnnn0genn0 14170 | If the size of a set is not a nonnegative integer, it is greater than or equal to any nonnegative integer. (Contributed by Alexander van der Vekens, 6-Dec-2017.) |
⊢ ((𝑀 ∈ 𝑉 ∧ (♯‘𝑀) ∉ ℕ0 ∧ 𝑁 ∈ ℕ0) → 𝑁 ≤ (♯‘𝑀)) | ||
Theorem | hashnemnf 14171 | The size of a set is never minus infinity. (Contributed by Alexander van der Vekens, 21-Dec-2017.) |
⊢ (𝐴 ∈ 𝑉 → (♯‘𝐴) ≠ -∞) | ||
Theorem | hashv01gt1 14172 | The size of a set is either 0 or 1 or greater than 1. (Contributed by Alexander van der Vekens, 29-Dec-2017.) |
⊢ (𝑀 ∈ 𝑉 → ((♯‘𝑀) = 0 ∨ (♯‘𝑀) = 1 ∨ 1 < (♯‘𝑀))) | ||
Theorem | hashfz1 14173 | The set (1...𝑁) has 𝑁 elements. (Contributed by Paul Chapman, 22-Jun-2011.) (Revised by Mario Carneiro, 15-Sep-2013.) |
⊢ (𝑁 ∈ ℕ0 → (♯‘(1...𝑁)) = 𝑁) | ||
Theorem | hashen 14174 | Two finite sets have the same number of elements iff they are equinumerous. (Contributed by Paul Chapman, 22-Jun-2011.) (Revised by Mario Carneiro, 15-Sep-2013.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((♯‘𝐴) = (♯‘𝐵) ↔ 𝐴 ≈ 𝐵)) | ||
Theorem | hasheni 14175 | Equinumerous sets have the same number of elements (even if they are not finite). (Contributed by Mario Carneiro, 15-Apr-2015.) |
⊢ (𝐴 ≈ 𝐵 → (♯‘𝐴) = (♯‘𝐵)) | ||
Theorem | hasheqf1o 14176* | The size of two finite sets is equal if and only if there is a bijection mapping one of the sets onto the other. (Contributed by Alexander van der Vekens, 17-Dec-2017.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((♯‘𝐴) = (♯‘𝐵) ↔ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵)) | ||
Theorem | fiinfnf1o 14177* | There is no bijection between a finite set and an infinite set. (Contributed by Alexander van der Vekens, 25-Dec-2017.) |
⊢ ((𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin) → ¬ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵) | ||
Theorem | hasheqf1oi 14178* | The size of two sets is equal if there is a bijection mapping one of the sets onto the other. (Contributed by Alexander van der Vekens, 25-Dec-2017.) (Revised by AV, 4-May-2021.) |
⊢ (𝐴 ∈ 𝑉 → (∃𝑓 𝑓:𝐴–1-1-onto→𝐵 → (♯‘𝐴) = (♯‘𝐵))) | ||
Theorem | hashf1rn 14179 | The size of a finite set which is a one-to-one function is equal to the size of the function's range. (Contributed by Alexander van der Vekens, 12-Jan-2018.) (Revised by AV, 4-May-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴–1-1→𝐵) → (♯‘𝐹) = (♯‘ran 𝐹)) | ||
Theorem | hasheqf1od 14180 | The size of two sets is equal if there is a bijection mapping one of the sets onto the other. (Contributed by AV, 4-May-2021.) |
⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵) ⇒ ⊢ (𝜑 → (♯‘𝐴) = (♯‘𝐵)) | ||
Theorem | fz1eqb 14181 | Two possibly-empty 1-based finite sets of sequential integers are equal iff their endpoints are equal. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Mario Carneiro, 29-Mar-2014.) |
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → ((1...𝑀) = (1...𝑁) ↔ 𝑀 = 𝑁)) | ||
Theorem | hashcard 14182 | The size function of the cardinality function. (Contributed by Mario Carneiro, 19-Sep-2013.) (Revised by Mario Carneiro, 4-Nov-2013.) |
⊢ (𝐴 ∈ Fin → (♯‘(card‘𝐴)) = (♯‘𝐴)) | ||
Theorem | hashcl 14183 | Closure of the ♯ function. (Contributed by Paul Chapman, 26-Oct-2012.) (Revised by Mario Carneiro, 13-Jul-2014.) |
⊢ (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℕ0) | ||
Theorem | hashxrcl 14184 | Extended real closure of the ♯ function. (Contributed by Mario Carneiro, 22-Apr-2015.) |
⊢ (𝐴 ∈ 𝑉 → (♯‘𝐴) ∈ ℝ*) | ||
Theorem | hashclb 14185 | Reverse closure of the ♯ function. (Contributed by Mario Carneiro, 15-Jan-2015.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Fin ↔ (♯‘𝐴) ∈ ℕ0)) | ||
Theorem | nfile 14186 | The size of any infinite set is always greater than or equal to the size of any set. (Contributed by AV, 13-Nov-2020.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ ¬ 𝐵 ∈ Fin) → (♯‘𝐴) ≤ (♯‘𝐵)) | ||
Theorem | hashvnfin 14187 | A set of finite size is a finite set. (Contributed by Alexander van der Vekens, 8-Dec-2017.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → ((♯‘𝑆) = 𝑁 → 𝑆 ∈ Fin)) | ||
Theorem | hashnfinnn0 14188 | The size of an infinite set is not a nonnegative integer. (Contributed by Alexander van der Vekens, 21-Dec-2017.) (Proof shortened by Alexander van der Vekens, 18-Jan-2018.) |
⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → (♯‘𝐴) ∉ ℕ0) | ||
Theorem | isfinite4 14189 | A finite set is equinumerous to the range of integers from one up to the hash value of the set. In other words, counting objects with natural numbers works if and only if it is a finite collection. (Contributed by Richard Penner, 26-Feb-2020.) |
⊢ (𝐴 ∈ Fin ↔ (1...(♯‘𝐴)) ≈ 𝐴) | ||
Theorem | hasheq0 14190 | Two ways of saying a finite set is empty. (Contributed by Paul Chapman, 26-Oct-2012.) (Revised by Mario Carneiro, 27-Jul-2014.) |
⊢ (𝐴 ∈ 𝑉 → ((♯‘𝐴) = 0 ↔ 𝐴 = ∅)) | ||
Theorem | hashneq0 14191 | Two ways of saying a set is not empty. (Contributed by Alexander van der Vekens, 23-Sep-2018.) |
⊢ (𝐴 ∈ 𝑉 → (0 < (♯‘𝐴) ↔ 𝐴 ≠ ∅)) | ||
Theorem | hashgt0n0 14192 | If the size of a set is greater than 0, the set is not empty. (Contributed by AV, 5-Aug-2018.) (Proof shortened by AV, 18-Nov-2018.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 0 < (♯‘𝐴)) → 𝐴 ≠ ∅) | ||
Theorem | hashnncl 14193 | Positive natural closure of the hash function. (Contributed by Mario Carneiro, 16-Jan-2015.) |
⊢ (𝐴 ∈ Fin → ((♯‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅)) | ||
Theorem | hash0 14194 | The empty set has size zero. (Contributed by Mario Carneiro, 8-Jul-2014.) |
⊢ (♯‘∅) = 0 | ||
Theorem | hashelne0d 14195 | A set with an element has nonzero size. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → ¬ (♯‘𝐴) = 0) | ||
Theorem | hashsng 14196 | The size of a singleton. (Contributed by Paul Chapman, 26-Oct-2012.) (Proof shortened by Mario Carneiro, 13-Feb-2013.) |
⊢ (𝐴 ∈ 𝑉 → (♯‘{𝐴}) = 1) | ||
Theorem | hashen1 14197 | A set has size 1 if and only if it is equinumerous to the ordinal 1. (Contributed by AV, 14-Apr-2019.) |
⊢ (𝐴 ∈ 𝑉 → ((♯‘𝐴) = 1 ↔ 𝐴 ≈ 1o)) | ||
Theorem | hash1elsn 14198 | A set of size 1 with a known element is the singleton of that element. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ (𝜑 → (♯‘𝐴) = 1) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐴 = {𝐵}) | ||
Theorem | hashrabrsn 14199* | The size of a restricted class abstraction restricted to a singleton is a nonnegative integer. (Contributed by Alexander van der Vekens, 22-Dec-2017.) |
⊢ (♯‘{𝑥 ∈ {𝐴} ∣ 𝜑}) ∈ ℕ0 | ||
Theorem | hashrabsn01 14200* | The size of a restricted class abstraction restricted to a singleton is either 0 or 1. (Contributed by Alexander van der Vekens, 3-Sep-2018.) |
⊢ ((♯‘{𝑥 ∈ {𝐴} ∣ 𝜑}) = 𝑁 → (𝑁 = 0 ∨ 𝑁 = 1)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |