| Metamath
Proof Explorer Theorem List (p. 144 of 494) | < 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: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | mulsubdivbinom2 14301 | The square of a binomial with factor minus a number divided by a nonzero number. (Contributed by AV, 19-Jul-2021.) |
| ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → (((((𝐶 · 𝐴) + 𝐵)↑2) − 𝐷) / 𝐶) = (((𝐶 · (𝐴↑2)) + (2 · (𝐴 · 𝐵))) + (((𝐵↑2) − 𝐷) / 𝐶))) | ||
| Theorem | muldivbinom2 14302 | The square of a binomial with factor divided by a nonzero number. (Contributed by AV, 19-Jul-2021.) |
| ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 ≠ 0)) → ((((𝐶 · 𝐴) + 𝐵)↑2) / 𝐶) = (((𝐶 · (𝐴↑2)) + (2 · (𝐴 · 𝐵))) + ((𝐵↑2) / 𝐶))) | ||
| Theorem | sq10 14303 | The square of 10 is 100. (Contributed by AV, 14-Jun-2021.) (Revised by AV, 1-Aug-2021.) |
| ⊢ (;10↑2) = ;;100 | ||
| Theorem | sq10e99m1 14304 | The square of 10 is 99 plus 1. (Contributed by AV, 14-Jun-2021.) (Revised by AV, 1-Aug-2021.) |
| ⊢ (;10↑2) = (;99 + 1) | ||
| Theorem | 3dec 14305 | A "decimal constructor" which is used to build up "decimal integers" or "numeric terms" in base 10 with 3 "digits". (Contributed by AV, 14-Jun-2021.) (Revised by AV, 1-Aug-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 ⇒ ⊢ ;;𝐴𝐵𝐶 = ((((;10↑2) · 𝐴) + (;10 · 𝐵)) + 𝐶) | ||
| Theorem | nn0le2msqi 14306 | The square function on nonnegative integers is monotonic. (Contributed by Raph Levien, 10-Dec-2002.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 ⇒ ⊢ (𝐴 ≤ 𝐵 ↔ (𝐴 · 𝐴) ≤ (𝐵 · 𝐵)) | ||
| Theorem | nn0opthlem1 14307 | A rather pretty lemma for nn0opthi 14309. (Contributed by Raph Levien, 10-Dec-2002.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 ⇒ ⊢ (𝐴 < 𝐶 ↔ ((𝐴 · 𝐴) + (2 · 𝐴)) < (𝐶 · 𝐶)) | ||
| Theorem | nn0opthlem2 14308 | Lemma for nn0opthi 14309. (Contributed by Raph Levien, 10-Dec-2002.) (Revised by Scott Fenton, 8-Sep-2010.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 ⇒ ⊢ ((𝐴 + 𝐵) < 𝐶 → ((𝐶 · 𝐶) + 𝐷) ≠ (((𝐴 + 𝐵) · (𝐴 + 𝐵)) + 𝐵)) | ||
| Theorem | nn0opthi 14309 | An ordered pair theorem for nonnegative integers. Theorem 17.3 of [Quine] p. 124. We can represent an ordered pair of nonnegative integers 𝐴 and 𝐵 by (((𝐴 + 𝐵) · (𝐴 + 𝐵)) + 𝐵). If two such ordered pairs are equal, their first elements are equal and their second elements are equal. Contrast this ordered pair representation with the standard one df-op 4633 that works for any set. (Contributed by Raph Levien, 10-Dec-2002.) (Proof shortened by Scott Fenton, 8-Sep-2010.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 ⇒ ⊢ ((((𝐴 + 𝐵) · (𝐴 + 𝐵)) + 𝐵) = (((𝐶 + 𝐷) · (𝐶 + 𝐷)) + 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
| Theorem | nn0opth2i 14310 | An ordered pair theorem for nonnegative integers. Theorem 17.3 of [Quine] p. 124. See comments for nn0opthi 14309. (Contributed by NM, 22-Jul-2004.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 ⇒ ⊢ ((((𝐴 + 𝐵)↑2) + 𝐵) = (((𝐶 + 𝐷)↑2) + 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
| Theorem | nn0opth2 14311 | An ordered pair theorem for nonnegative integers. Theorem 17.3 of [Quine] p. 124. See nn0opthi 14309. (Contributed by NM, 22-Jul-2004.) |
| ⊢ (((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) ∧ (𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0)) → ((((𝐴 + 𝐵)↑2) + 𝐵) = (((𝐶 + 𝐷)↑2) + 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) | ||
| Syntax | cfa 14312 | Extend class notation to include the factorial of nonnegative integers. |
| class ! | ||
| Definition | df-fac 14313 | Define the factorial function on nonnegative integers. For example, (!‘5) = 120 because 1 · 2 · 3 · 4 · 5 = 120 (ex-fac 30470). 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 14314 | 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 14315 | The factorial of 0. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.) |
| ⊢ (!‘0) = 1 | ||
| Theorem | fac1 14316 | The factorial of 1. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.) |
| ⊢ (!‘1) = 1 | ||
| Theorem | facp1 14317 | The factorial of a successor. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.) |
| ⊢ (𝑁 ∈ ℕ0 → (!‘(𝑁 + 1)) = ((!‘𝑁) · (𝑁 + 1))) | ||
| Theorem | fac2 14318 | The factorial of 2. (Contributed by NM, 17-Mar-2005.) |
| ⊢ (!‘2) = 2 | ||
| Theorem | fac3 14319 | The factorial of 3. (Contributed by NM, 17-Mar-2005.) |
| ⊢ (!‘3) = 6 | ||
| Theorem | fac4 14320 | The factorial of 4. (Contributed by Mario Carneiro, 18-Jun-2015.) |
| ⊢ (!‘4) = ;24 | ||
| Theorem | facnn2 14321 | Value of the factorial function expressed recursively. (Contributed by NM, 2-Dec-2004.) |
| ⊢ (𝑁 ∈ ℕ → (!‘𝑁) = ((!‘(𝑁 − 1)) · 𝑁)) | ||
| Theorem | faccl 14322 | Closure of the factorial function. (Contributed by NM, 2-Dec-2004.) |
| ⊢ (𝑁 ∈ ℕ0 → (!‘𝑁) ∈ ℕ) | ||
| Theorem | faccld 14323 | Closure of the factorial function, deduction version of faccl 14322. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (!‘𝑁) ∈ ℕ) | ||
| Theorem | facmapnn 14324 | 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 14325 | The factorial function is nonzero. (Contributed by NM, 26-Apr-2005.) |
| ⊢ (𝑁 ∈ ℕ0 → (!‘𝑁) ≠ 0) | ||
| Theorem | facdiv 14326 | A positive integer divides the factorial of an equal or larger number. (Contributed by NM, 2-May-2005.) |
| ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑁 ≤ 𝑀) → ((!‘𝑀) / 𝑁) ∈ ℕ) | ||
| Theorem | facndiv 14327 | 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 14328 | Ordering property of factorial. (Contributed by NM, 9-Dec-2005.) |
| ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁) → (!‘𝑀) ≤ (!‘𝑁)) | ||
| Theorem | faclbnd 14329 | A lower bound for the factorial function. (Contributed by NM, 17-Dec-2005.) |
| ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀↑(𝑁 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑁))) | ||
| Theorem | faclbnd2 14330 | A lower bound for the factorial function. (Contributed by NM, 17-Dec-2005.) |
| ⊢ (𝑁 ∈ ℕ0 → ((2↑𝑁) / 2) ≤ (!‘𝑁)) | ||
| Theorem | faclbnd3 14331 | A lower bound for the factorial function. (Contributed by NM, 19-Dec-2005.) |
| ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀↑𝑁) ≤ ((𝑀↑𝑀) · (!‘𝑁))) | ||
| Theorem | faclbnd4lem1 14332 | Lemma for faclbnd4 14336. Prepare the induction step. (Contributed by NM, 20-Dec-2005.) |
| ⊢ 𝑁 ∈ ℕ & ⊢ 𝐾 ∈ ℕ0 & ⊢ 𝑀 ∈ ℕ0 ⇒ ⊢ ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ≤ (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁))) | ||
| Theorem | faclbnd4lem2 14333 | Lemma for faclbnd4 14336. Use the weak deduction theorem to convert the hypotheses of faclbnd4lem1 14332 to antecedents. (Contributed by NM, 23-Dec-2005.) |
| ⊢ ((𝑀 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ) → ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ≤ (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)))) | ||
| Theorem | faclbnd4lem3 14334 | Lemma for faclbnd4 14336. The 𝑁 = 0 case. (Contributed by NM, 23-Dec-2005.) |
| ⊢ (((𝑀 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0) ∧ 𝑁 = 0) → ((𝑁↑𝐾) · (𝑀↑𝑁)) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁))) | ||
| Theorem | faclbnd4lem4 14335 | Lemma for faclbnd4 14336. Prove the 0 < 𝑁 case by induction on 𝐾. (Contributed by NM, 19-Dec-2005.) |
| ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0) → ((𝑁↑𝐾) · (𝑀↑𝑁)) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁))) | ||
| Theorem | faclbnd4 14336 | Variant of faclbnd5 14337 providing a non-strict lower bound. (Contributed by NM, 23-Dec-2005.) |
| ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0) → ((𝑁↑𝐾) · (𝑀↑𝑁)) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁))) | ||
| Theorem | faclbnd5 14337 | 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 14338 | 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 14339 | An upper bound for the factorial function. (Contributed by Mario Carneiro, 15-Apr-2016.) |
| ⊢ (𝑁 ∈ ℕ0 → (!‘𝑁) ≤ (𝑁↑𝑁)) | ||
| Theorem | facavg 14340 | 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 14341 | Extend class notation to include the binomial coefficient operation (combinatorial choose operation). |
| class C | ||
| Definition | df-bc 14342* |
Define the binomial coefficient operation. For example,
(5C3) = 10 (ex-bc 30471).
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 14343 | 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 14344 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 14344 | 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 14345 | 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 14346 | 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 14347 | Closure of the binomial coefficient in the positive reals. (This is mostly a lemma before we have bccl2 14362.) (Contributed by Mario Carneiro, 10-Mar-2014.) |
| ⊢ (𝐾 ∈ (0...𝑁) → (𝑁C𝐾) ∈ ℝ+) | ||
| Theorem | bccmpl 14348 | "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 14349 | 𝑁 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 14350 | The binomial coefficient " 0 choose 𝐾 " is 0 for a positive integer K. Note that (0C0) = 1 (see bcn0 14349). (Contributed by Alexander van der Vekens, 1-Jan-2018.) |
| ⊢ (𝐾 ∈ ℕ → (0C𝐾) = 0) | ||
| Theorem | bcnn 14351 | 𝑁 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 14352 | Binomial coefficient: 𝑁 choose 1. (Contributed by NM, 21-Jun-2005.) (Revised by Mario Carneiro, 8-Nov-2013.) |
| ⊢ (𝑁 ∈ ℕ0 → (𝑁C1) = 𝑁) | ||
| Theorem | bcnp1n 14353 | Binomial coefficient: 𝑁 + 1 choose 𝑁. (Contributed by NM, 20-Jun-2005.) (Revised by Mario Carneiro, 8-Nov-2013.) |
| ⊢ (𝑁 ∈ ℕ0 → ((𝑁 + 1)C𝑁) = (𝑁 + 1)) | ||
| Theorem | bcm1k 14354 | 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 14355 | 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 14356 | 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 14357 | 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 14358 | Binomial coefficient: 𝑁 choose 2. (Contributed by Mario Carneiro, 22-May-2014.) |
| ⊢ (𝑁 ∈ ℕ0 → (𝑁C2) = ((𝑁 · (𝑁 − 1)) / 2)) | ||
| Theorem | bcp1m1 14359 | 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 14360 | 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 14361 | 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 14362 | 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 14363 | 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 14364 | 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 14365 | 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 14366 | The binomial coefficient of (𝑁 − 1) is 𝑁. (Contributed by Scott Fenton, 16-May-2014.) |
| ⊢ (𝑁 ∈ ℕ0 → (𝑁C(𝑁 − 1)) = 𝑁) | ||
| Theorem | 4bc3eq4 14367 | The value of four choose three. (Contributed by Scott Fenton, 11-Jun-2016.) |
| ⊢ (4C3) = 4 | ||
| Theorem | 4bc2eq6 14368 | The value of four choose two. (Contributed by Scott Fenton, 9-Jan-2017.) |
| ⊢ (4C2) = 6 | ||
| Syntax | chash 14369 | Extend the definition of a class to include the set size function. |
| class ♯ | ||
| Definition | df-hash 14370 | 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 30472). (Contributed by Paul Chapman, 22-Jun-2011.) |
| ⊢ ♯ = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) ∘ card) ∪ ((V ∖ Fin) × {+∞})) | ||
| Theorem | hashkf 14371 | 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 14372* | The value of the ♯ function in terms of the mapping 𝐺 from ω to ℕ0. The proof avoids the use of ax-ac 10499. (Contributed by Paul Chapman, 22-Jun-2011.) (Revised by Mario Carneiro, 26-Dec-2014.) |
| ⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) ⇒ ⊢ (𝐴 ∈ Fin → (𝐺‘(card‘𝐴)) = (♯‘𝐴)) | ||
| Theorem | hashginv 14373* | 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 14374 | The value of the ♯ function on an infinite set. (Contributed by Mario Carneiro, 13-Jul-2014.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin) → (♯‘𝐴) = +∞) | ||
| Theorem | hashbnd 14375 | If 𝐴 has size bounded by an integer 𝐵, then 𝐴 is finite. (Contributed by Mario Carneiro, 14-Jun-2015.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ℕ0 ∧ (♯‘𝐴) ≤ 𝐵) → 𝐴 ∈ Fin) | ||
| Theorem | hashfxnn0 14376 | 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 14377 | 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 14376? (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 14378 | 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 14379 | Restriction of the domain of the size function. (Contributed by Thierry Arnoux, 31-Jan-2017.) |
| ⊢ (♯ ↾ 𝐴) Fn 𝐴 | ||
| Theorem | dmhashres 14380 | Restriction of the domain of the size function. (Contributed by Thierry Arnoux, 12-Jan-2017.) |
| ⊢ dom (♯ ↾ 𝐴) = 𝐴 | ||
| Theorem | hashnn0pnf 14381 | 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 14378? (Contributed by Alexander van der Vekens, 6-Dec-2017.) |
| ⊢ (𝑀 ∈ 𝑉 → ((♯‘𝑀) ∈ ℕ0 ∨ (♯‘𝑀) = +∞)) | ||
| Theorem | hashnnn0genn0 14382 | 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 14383 | The size of a set is never minus infinity. (Contributed by Alexander van der Vekens, 21-Dec-2017.) |
| ⊢ (𝐴 ∈ 𝑉 → (♯‘𝐴) ≠ -∞) | ||
| Theorem | hashv01gt1 14384 | 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 14385 | The set (1...𝑁) has 𝑁 elements. (Contributed by Paul Chapman, 22-Jun-2011.) (Revised by Mario Carneiro, 15-Sep-2013.) |
| ⊢ (𝑁 ∈ ℕ0 → (♯‘(1...𝑁)) = 𝑁) | ||
| Theorem | hashen 14386 | 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 14387 | Equinumerous sets have the same number of elements (even if they are not finite). (Contributed by Mario Carneiro, 15-Apr-2015.) |
| ⊢ (𝐴 ≈ 𝐵 → (♯‘𝐴) = (♯‘𝐵)) | ||
| Theorem | hasheqf1o 14388* | 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 14389* | 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 14390* | 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 14391 | 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 14392 | 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 14393 | 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 14394 | 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 14395 | Closure of the ♯ function. (Contributed by Paul Chapman, 26-Oct-2012.) (Revised by Mario Carneiro, 13-Jul-2014.) |
| ⊢ (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℕ0) | ||
| Theorem | hashxrcl 14396 | Extended real closure of the ♯ function. (Contributed by Mario Carneiro, 22-Apr-2015.) |
| ⊢ (𝐴 ∈ 𝑉 → (♯‘𝐴) ∈ ℝ*) | ||
| Theorem | hashclb 14397 | Reverse closure of the ♯ function. (Contributed by Mario Carneiro, 15-Jan-2015.) |
| ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Fin ↔ (♯‘𝐴) ∈ ℕ0)) | ||
| Theorem | nfile 14398 | 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 14399 | A set of finite size is a finite set. (Contributed by Alexander van der Vekens, 8-Dec-2017.) |
| ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → ((♯‘𝑆) = 𝑁 → 𝑆 ∈ Fin)) | ||
| Theorem | hashnfinnn0 14400 | 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) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |