Home | Metamath
Proof Explorer Theorem List (p. 141 of 466) | < 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-29289) |
Hilbert Space Explorer
(29290-30812) |
Users' Mathboxes
(30813-46532) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | facp1 14001 | The factorial of a successor. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.) |
⊢ (𝑁 ∈ ℕ0 → (!‘(𝑁 + 1)) = ((!‘𝑁) · (𝑁 + 1))) | ||
Theorem | fac2 14002 | The factorial of 2. (Contributed by NM, 17-Mar-2005.) |
⊢ (!‘2) = 2 | ||
Theorem | fac3 14003 | The factorial of 3. (Contributed by NM, 17-Mar-2005.) |
⊢ (!‘3) = 6 | ||
Theorem | fac4 14004 | The factorial of 4. (Contributed by Mario Carneiro, 18-Jun-2015.) |
⊢ (!‘4) = ;24 | ||
Theorem | facnn2 14005 | Value of the factorial function expressed recursively. (Contributed by NM, 2-Dec-2004.) |
⊢ (𝑁 ∈ ℕ → (!‘𝑁) = ((!‘(𝑁 − 1)) · 𝑁)) | ||
Theorem | faccl 14006 | Closure of the factorial function. (Contributed by NM, 2-Dec-2004.) |
⊢ (𝑁 ∈ ℕ0 → (!‘𝑁) ∈ ℕ) | ||
Theorem | faccld 14007 | Closure of the factorial function, deduction version of faccl 14006. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (!‘𝑁) ∈ ℕ) | ||
Theorem | facmapnn 14008 | 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 14009 | The factorial function is nonzero. (Contributed by NM, 26-Apr-2005.) |
⊢ (𝑁 ∈ ℕ0 → (!‘𝑁) ≠ 0) | ||
Theorem | facdiv 14010 | A positive integer divides the factorial of an equal or larger number. (Contributed by NM, 2-May-2005.) |
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑁 ≤ 𝑀) → ((!‘𝑀) / 𝑁) ∈ ℕ) | ||
Theorem | facndiv 14011 | 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 14012 | Ordering property of factorial. (Contributed by NM, 9-Dec-2005.) |
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁) → (!‘𝑀) ≤ (!‘𝑁)) | ||
Theorem | faclbnd 14013 | A lower bound for the factorial function. (Contributed by NM, 17-Dec-2005.) |
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀↑(𝑁 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑁))) | ||
Theorem | faclbnd2 14014 | A lower bound for the factorial function. (Contributed by NM, 17-Dec-2005.) |
⊢ (𝑁 ∈ ℕ0 → ((2↑𝑁) / 2) ≤ (!‘𝑁)) | ||
Theorem | faclbnd3 14015 | A lower bound for the factorial function. (Contributed by NM, 19-Dec-2005.) |
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀↑𝑁) ≤ ((𝑀↑𝑀) · (!‘𝑁))) | ||
Theorem | faclbnd4lem1 14016 | Lemma for faclbnd4 14020. Prepare the induction step. (Contributed by NM, 20-Dec-2005.) |
⊢ 𝑁 ∈ ℕ & ⊢ 𝐾 ∈ ℕ0 & ⊢ 𝑀 ∈ ℕ0 ⇒ ⊢ ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ≤ (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁))) | ||
Theorem | faclbnd4lem2 14017 | Lemma for faclbnd4 14020. Use the weak deduction theorem to convert the hypotheses of faclbnd4lem1 14016 to antecedents. (Contributed by NM, 23-Dec-2005.) |
⊢ ((𝑀 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ) → ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ≤ (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)))) | ||
Theorem | faclbnd4lem3 14018 | Lemma for faclbnd4 14020. The 𝑁 = 0 case. (Contributed by NM, 23-Dec-2005.) |
⊢ (((𝑀 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0) ∧ 𝑁 = 0) → ((𝑁↑𝐾) · (𝑀↑𝑁)) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁))) | ||
Theorem | faclbnd4lem4 14019 | Lemma for faclbnd4 14020. Prove the 0 < 𝑁 case by induction on 𝐾. (Contributed by NM, 19-Dec-2005.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0) → ((𝑁↑𝐾) · (𝑀↑𝑁)) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁))) | ||
Theorem | faclbnd4 14020 | Variant of faclbnd5 14021 providing a non-strict lower bound. (Contributed by NM, 23-Dec-2005.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0) → ((𝑁↑𝐾) · (𝑀↑𝑁)) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁))) | ||
Theorem | faclbnd5 14021 | 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 14022 | 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 14023 | An upper bound for the factorial function. (Contributed by Mario Carneiro, 15-Apr-2016.) |
⊢ (𝑁 ∈ ℕ0 → (!‘𝑁) ≤ (𝑁↑𝑁)) | ||
Theorem | facavg 14024 | 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 14025 | Extend class notation to include the binomial coefficient operation (combinatorial choose operation). |
class C | ||
Definition | df-bc 14026* |
Define the binomial coefficient operation. For example,
(5C3) = 10 (ex-bc 28825).
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 14027 | 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 14028 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 14028 | 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 14029 | 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 14030 | 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 14031 | Closure of the binomial coefficient in the positive reals. (This is mostly a lemma before we have bccl2 14046.) (Contributed by Mario Carneiro, 10-Mar-2014.) |
⊢ (𝐾 ∈ (0...𝑁) → (𝑁C𝐾) ∈ ℝ+) | ||
Theorem | bccmpl 14032 | "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 14033 | 𝑁 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 14034 | The binomial coefficient " 0 choose 𝐾 " is 0 for a positive integer K. Note that (0C0) = 1 (see bcn0 14033). (Contributed by Alexander van der Vekens, 1-Jan-2018.) |
⊢ (𝐾 ∈ ℕ → (0C𝐾) = 0) | ||
Theorem | bcnn 14035 | 𝑁 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 14036 | Binomial coefficient: 𝑁 choose 1. (Contributed by NM, 21-Jun-2005.) (Revised by Mario Carneiro, 8-Nov-2013.) |
⊢ (𝑁 ∈ ℕ0 → (𝑁C1) = 𝑁) | ||
Theorem | bcnp1n 14037 | Binomial coefficient: 𝑁 + 1 choose 𝑁. (Contributed by NM, 20-Jun-2005.) (Revised by Mario Carneiro, 8-Nov-2013.) |
⊢ (𝑁 ∈ ℕ0 → ((𝑁 + 1)C𝑁) = (𝑁 + 1)) | ||
Theorem | bcm1k 14038 | 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 14039 | 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 14040 | 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 14041 | 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 14042 | Binomial coefficient: 𝑁 choose 2. (Contributed by Mario Carneiro, 22-May-2014.) |
⊢ (𝑁 ∈ ℕ0 → (𝑁C2) = ((𝑁 · (𝑁 − 1)) / 2)) | ||
Theorem | bcp1m1 14043 | 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 14044 | 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 14045 | 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 14046 | 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 14047 | 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 14048 | 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 14049 | 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 14050 | The binomial coefficent of (𝑁 − 1) is 𝑁. (Contributed by Scott Fenton, 16-May-2014.) |
⊢ (𝑁 ∈ ℕ0 → (𝑁C(𝑁 − 1)) = 𝑁) | ||
Theorem | 4bc3eq4 14051 | The value of four choose three. (Contributed by Scott Fenton, 11-Jun-2016.) |
⊢ (4C3) = 4 | ||
Theorem | 4bc2eq6 14052 | The value of four choose two. (Contributed by Scott Fenton, 9-Jan-2017.) |
⊢ (4C2) = 6 | ||
Syntax | chash 14053 | Extend the definition of a class to include the set size function. |
class ♯ | ||
Definition | df-hash 14054 | 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 28826). (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ ♯ = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) ∘ card) ∪ ((V ∖ Fin) × {+∞})) | ||
Theorem | hashkf 14055 | 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 14056* | The value of the ♯ function in terms of the mapping 𝐺 from ω to ℕ0. The proof avoids the use of ax-ac 10224. (Contributed by Paul Chapman, 22-Jun-2011.) (Revised by Mario Carneiro, 26-Dec-2014.) |
⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) ⇒ ⊢ (𝐴 ∈ Fin → (𝐺‘(card‘𝐴)) = (♯‘𝐴)) | ||
Theorem | hashginv 14057* | 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 14058 | The value of the ♯ function on an infinite set. (Contributed by Mario Carneiro, 13-Jul-2014.) |
⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → (♯‘𝐴) = +∞) | ||
Theorem | hashbnd 14059 | If 𝐴 has size bounded by an integer 𝐵, then 𝐴 is finite. (Contributed by Mario Carneiro, 14-Jun-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ℕ0 ∧ (♯‘𝐴) ≤ 𝐵) → 𝐴 ∈ Fin) | ||
Theorem | hashfxnn0 14060 | 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 14061 | 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 14060? (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 14062 | 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 14063 | Restriction of the domain of the size function. (Contributed by Thierry Arnoux, 31-Jan-2017.) |
⊢ (♯ ↾ 𝐴) Fn 𝐴 | ||
Theorem | dmhashres 14064 | Restriction of the domain of the size function. (Contributed by Thierry Arnoux, 12-Jan-2017.) |
⊢ dom (♯ ↾ 𝐴) = 𝐴 | ||
Theorem | hashnn0pnf 14065 | 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 14062? (Contributed by Alexander van der Vekens, 6-Dec-2017.) |
⊢ (𝑀 ∈ 𝑉 → ((♯‘𝑀) ∈ ℕ0 ∨ (♯‘𝑀) = +∞)) | ||
Theorem | hashnnn0genn0 14066 | 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 14067 | The size of a set is never minus infinity. (Contributed by Alexander van der Vekens, 21-Dec-2017.) |
⊢ (𝐴 ∈ 𝑉 → (♯‘𝐴) ≠ -∞) | ||
Theorem | hashv01gt1 14068 | 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 14069 | The set (1...𝑁) has 𝑁 elements. (Contributed by Paul Chapman, 22-Jun-2011.) (Revised by Mario Carneiro, 15-Sep-2013.) |
⊢ (𝑁 ∈ ℕ0 → (♯‘(1...𝑁)) = 𝑁) | ||
Theorem | hashen 14070 | 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 14071 | Equinumerous sets have the same number of elements (even if they are not finite). (Contributed by Mario Carneiro, 15-Apr-2015.) |
⊢ (𝐴 ≈ 𝐵 → (♯‘𝐴) = (♯‘𝐵)) | ||
Theorem | hasheqf1o 14072* | 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 14073* | 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 | focdmex 14074 | The codomain of an onto function is a set if its domain is a set. (Contributed by AV, 4-May-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴–onto→𝐵) → 𝐵 ∈ V) | ||
Theorem | hasheqf1oi 14075* | 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 14076 | 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 14077 | 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 14078 | 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 14079 | 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 14080 | Closure of the ♯ function. (Contributed by Paul Chapman, 26-Oct-2012.) (Revised by Mario Carneiro, 13-Jul-2014.) |
⊢ (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℕ0) | ||
Theorem | hashxrcl 14081 | Extended real closure of the ♯ function. (Contributed by Mario Carneiro, 22-Apr-2015.) |
⊢ (𝐴 ∈ 𝑉 → (♯‘𝐴) ∈ ℝ*) | ||
Theorem | hashclb 14082 | Reverse closure of the ♯ function. (Contributed by Mario Carneiro, 15-Jan-2015.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Fin ↔ (♯‘𝐴) ∈ ℕ0)) | ||
Theorem | nfile 14083 | 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 14084 | A set of finite size is a finite set. (Contributed by Alexander van der Vekens, 8-Dec-2017.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → ((♯‘𝑆) = 𝑁 → 𝑆 ∈ Fin)) | ||
Theorem | hashnfinnn0 14085 | 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 14086 | 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 14087 | 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 14088 | Two ways of saying a set is not empty. (Contributed by Alexander van der Vekens, 23-Sep-2018.) |
⊢ (𝐴 ∈ 𝑉 → (0 < (♯‘𝐴) ↔ 𝐴 ≠ ∅)) | ||
Theorem | hashgt0n0 14089 | 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 14090 | Positive natural closure of the hash function. (Contributed by Mario Carneiro, 16-Jan-2015.) |
⊢ (𝐴 ∈ Fin → ((♯‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅)) | ||
Theorem | hash0 14091 | The empty set has size zero. (Contributed by Mario Carneiro, 8-Jul-2014.) |
⊢ (♯‘∅) = 0 | ||
Theorem | hashelne0d 14092 | A set with an element has nonzero size. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → ¬ (♯‘𝐴) = 0) | ||
Theorem | hashsng 14093 | The size of a singleton. (Contributed by Paul Chapman, 26-Oct-2012.) (Proof shortened by Mario Carneiro, 13-Feb-2013.) |
⊢ (𝐴 ∈ 𝑉 → (♯‘{𝐴}) = 1) | ||
Theorem | hashen1 14094 | 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 14095 | 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 14096* | 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 14097* | 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)) | ||
Theorem | hashrabsn1 14098* | If the size of a restricted class abstraction restricted to a singleton is 1, the condition of the class abstraction must hold for the singleton. (Contributed by Alexander van der Vekens, 3-Sep-2018.) |
⊢ ((♯‘{𝑥 ∈ {𝐴} ∣ 𝜑}) = 1 → [𝐴 / 𝑥]𝜑) | ||
Theorem | hashfn 14099 | A function is equinumerous to its domain. (Contributed by Mario Carneiro, 12-Mar-2015.) |
⊢ (𝐹 Fn 𝐴 → (♯‘𝐹) = (♯‘𝐴)) | ||
Theorem | fseq1hash 14100 | The value of the size function on a finite 1-based sequence. (Contributed by Paul Chapman, 26-Oct-2012.) (Proof shortened by Mario Carneiro, 12-Mar-2015.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹 Fn (1...𝑁)) → (♯‘𝐹) = 𝑁) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |