![]() |
Metamath
Proof Explorer Theorem List (p. 143 of 481) | < 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-30603) |
![]() (30604-32126) |
![]() (32127-48013) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | bernneq3 14201 | A corollary of bernneq 14199. (Contributed by Mario Carneiro, 11-Mar-2014.) |
⊢ ((𝑃 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ0) → 𝑁 < (𝑃↑𝑁)) | ||
Theorem | expnbnd 14202* | Exponentiation with a base greater than 1 has no upper bound. (Contributed by NM, 20-Oct-2007.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → ∃𝑘 ∈ ℕ 𝐴 < (𝐵↑𝑘)) | ||
Theorem | expnlbnd 14203* | The reciprocal of exponentiation with a base greater than 1 has no positive lower bound. (Contributed by NM, 18-Jul-2008.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → ∃𝑘 ∈ ℕ (1 / (𝐵↑𝑘)) < 𝐴) | ||
Theorem | expnlbnd2 14204* | The reciprocal of exponentiation with a base greater than 1 has no positive lower bound. (Contributed by NM, 18-Jul-2008.) (Proof shortened by Mario Carneiro, 5-Jun-2014.) |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(1 / (𝐵↑𝑘)) < 𝐴) | ||
Theorem | expmulnbnd 14205* | Exponentiation with a base greater than 1 is not bounded by any linear function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → ∃𝑗 ∈ ℕ0 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐴 · 𝑘) < (𝐵↑𝑘)) | ||
Theorem | digit2 14206 | Two ways to express the 𝐾 th digit in the decimal (when base 𝐵 = 10) expansion of a number 𝐴. 𝐾 = 1 corresponds to the first digit after the decimal point. (Contributed by NM, 25-Dec-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) → ((⌊‘((𝐵↑𝐾) · 𝐴)) mod 𝐵) = ((⌊‘((𝐵↑𝐾) · 𝐴)) − (𝐵 · (⌊‘((𝐵↑(𝐾 − 1)) · 𝐴))))) | ||
Theorem | digit1 14207 | Two ways to express the 𝐾 th digit in the decimal expansion of a number 𝐴 (when base 𝐵 = 10). 𝐾 = 1 corresponds to the first digit after the decimal point. (Contributed by NM, 3-Jan-2009.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ) → ((⌊‘((𝐵↑𝐾) · 𝐴)) mod 𝐵) = (((⌊‘((𝐵↑𝐾) · 𝐴)) mod (𝐵↑𝐾)) − ((𝐵 · (⌊‘((𝐵↑(𝐾 − 1)) · 𝐴))) mod (𝐵↑𝐾)))) | ||
Theorem | modexp 14208 | Exponentiation property of the modulo operation, see theorem 5.2(c) in [ApostolNT] p. 107. (Contributed by Mario Carneiro, 28-Feb-2014.) |
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℝ+) ∧ (𝐴 mod 𝐷) = (𝐵 mod 𝐷)) → ((𝐴↑𝐶) mod 𝐷) = ((𝐵↑𝐶) mod 𝐷)) | ||
Theorem | discr1 14209* | A nonnegative quadratic form has nonnegative leading coefficient. (Contributed by Mario Carneiro, 4-Jun-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 0 ≤ (((𝐴 · (𝑥↑2)) + (𝐵 · 𝑥)) + 𝐶)) & ⊢ 𝑋 = if(1 ≤ (((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴), (((𝐵 + if(0 ≤ 𝐶, 𝐶, 0)) + 1) / -𝐴), 1) ⇒ ⊢ (𝜑 → 0 ≤ 𝐴) | ||
Theorem | discr 14210* | If a quadratic polynomial with real coefficients is nonnegative for all values, then its discriminant is nonpositive. (Contributed by NM, 10-Aug-1999.) (Revised by Mario Carneiro, 4-Jun-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 0 ≤ (((𝐴 · (𝑥↑2)) + (𝐵 · 𝑥)) + 𝐶)) ⇒ ⊢ (𝜑 → ((𝐵↑2) − (4 · (𝐴 · 𝐶))) ≤ 0) | ||
Theorem | expnngt1 14211 | If an integer power with a positive integer base is greater than 1, then the exponent is positive. (Contributed by AV, 28-Dec-2022.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ∧ 1 < (𝐴↑𝐵)) → 𝐵 ∈ ℕ) | ||
Theorem | expnngt1b 14212 | An integer power with an integer base greater than 1 is greater than 1 iff the exponent is positive. (Contributed by AV, 28-Dec-2022.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ ℤ) → (1 < (𝐴↑𝐵) ↔ 𝐵 ∈ ℕ)) | ||
Theorem | sqoddm1div8 14213 | A squared odd number minus 1 divided by 8 is the odd number multiplied with its successor divided by 2. (Contributed by AV, 19-Jul-2021.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 = ((2 · 𝑁) + 1)) → (((𝑀↑2) − 1) / 8) = ((𝑁 · (𝑁 + 1)) / 2)) | ||
Theorem | nnsqcld 14214 | The naturals are closed under squaring. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝐴↑2) ∈ ℕ) | ||
Theorem | nnexpcld 14215 | Closure of exponentiation of nonnegative integers. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐴↑𝑁) ∈ ℕ) | ||
Theorem | nn0expcld 14216 | Closure of exponentiation of nonnegative integers. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐴↑𝑁) ∈ ℕ0) | ||
Theorem | rpexpcld 14217 | Closure law for exponentiation of positive reals. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐴↑𝑁) ∈ ℝ+) | ||
Theorem | ltexp2rd 14218 | The power of a positive number smaller than 1 decreases as its exponent increases. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐴 < 1) ⇒ ⊢ (𝜑 → (𝑀 < 𝑁 ↔ (𝐴↑𝑁) < (𝐴↑𝑀))) | ||
Theorem | reexpclzd 14219 | Closure of exponentiation of reals. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐴↑𝑁) ∈ ℝ) | ||
Theorem | sqgt0d 14220 | The square of a nonzero real is positive. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → 0 < (𝐴↑2)) | ||
Theorem | ltexp2d 14221 | Ordering relationship for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 1 < 𝐴) ⇒ ⊢ (𝜑 → (𝑀 < 𝑁 ↔ (𝐴↑𝑀) < (𝐴↑𝑁))) | ||
Theorem | leexp2d 14222 | Ordering law for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 1 < 𝐴) ⇒ ⊢ (𝜑 → (𝑀 ≤ 𝑁 ↔ (𝐴↑𝑀) ≤ (𝐴↑𝑁))) | ||
Theorem | expcand 14223 | Ordering relationship for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 1 < 𝐴) & ⊢ (𝜑 → (𝐴↑𝑀) = (𝐴↑𝑁)) ⇒ ⊢ (𝜑 → 𝑀 = 𝑁) | ||
Theorem | leexp2ad 14224 | Ordering relationship for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 1 ≤ 𝐴) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) ⇒ ⊢ (𝜑 → (𝐴↑𝑀) ≤ (𝐴↑𝑁)) | ||
Theorem | leexp2rd 14225 | Ordering relationship for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐴 ≤ 1) ⇒ ⊢ (𝜑 → (𝐴↑𝑁) ≤ (𝐴↑𝑀)) | ||
Theorem | lt2sqd 14226 | The square function on nonnegative reals is strictly monotonic. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 0 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐴↑2) < (𝐵↑2))) | ||
Theorem | le2sqd 14227 | The square function on nonnegative reals is monotonic. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 0 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐴↑2) ≤ (𝐵↑2))) | ||
Theorem | sq11d 14228 | The square function is one-to-one for nonnegative reals. (Contributed by Mario Carneiro, 28-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 0 ≤ 𝐵) & ⊢ (𝜑 → (𝐴↑2) = (𝐵↑2)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | mulsubdivbinom2 14229 | 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 14230 | 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 14231 | The square of 10 is 100. (Contributed by AV, 14-Jun-2021.) (Revised by AV, 1-Aug-2021.) |
⊢ (;10↑2) = ;;100 | ||
Theorem | sq10e99m1 14232 | 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 14233 | 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 14234 | The square function on nonnegative integers is monotonic. (Contributed by Raph Levien, 10-Dec-2002.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 ⇒ ⊢ (𝐴 ≤ 𝐵 ↔ (𝐴 · 𝐴) ≤ (𝐵 · 𝐵)) | ||
Theorem | nn0opthlem1 14235 | A rather pretty lemma for nn0opthi 14237. (Contributed by Raph Levien, 10-Dec-2002.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 ⇒ ⊢ (𝐴 < 𝐶 ↔ ((𝐴 · 𝐴) + (2 · 𝐴)) < (𝐶 · 𝐶)) | ||
Theorem | nn0opthlem2 14236 | Lemma for nn0opthi 14237. (Contributed by Raph Levien, 10-Dec-2002.) (Revised by Scott Fenton, 8-Sep-2010.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 ⇒ ⊢ ((𝐴 + 𝐵) < 𝐶 → ((𝐶 · 𝐶) + 𝐷) ≠ (((𝐴 + 𝐵) · (𝐴 + 𝐵)) + 𝐵)) | ||
Theorem | nn0opthi 14237 | 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 4635 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 14238 | An ordered pair theorem for nonnegative integers. Theorem 17.3 of [Quine] p. 124. See comments for nn0opthi 14237. (Contributed by NM, 22-Jul-2004.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 ⇒ ⊢ ((((𝐴 + 𝐵)↑2) + 𝐵) = (((𝐶 + 𝐷)↑2) + 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
Theorem | nn0opth2 14239 | An ordered pair theorem for nonnegative integers. Theorem 17.3 of [Quine] p. 124. See nn0opthi 14237. (Contributed by NM, 22-Jul-2004.) |
⊢ (((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) ∧ (𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0)) → ((((𝐴 + 𝐵)↑2) + 𝐵) = (((𝐶 + 𝐷)↑2) + 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) | ||
Syntax | cfa 14240 | Extend class notation to include the factorial of nonnegative integers. |
class ! | ||
Definition | df-fac 14241 | Define the factorial function on nonnegative integers. For example, (!‘5) = 120 because 1 · 2 · 3 · 4 · 5 = 120 (ex-fac 30136). 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 14242 | 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 14243 | The factorial of 0. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.) |
⊢ (!‘0) = 1 | ||
Theorem | fac1 14244 | The factorial of 1. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.) |
⊢ (!‘1) = 1 | ||
Theorem | facp1 14245 | The factorial of a successor. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.) |
⊢ (𝑁 ∈ ℕ0 → (!‘(𝑁 + 1)) = ((!‘𝑁) · (𝑁 + 1))) | ||
Theorem | fac2 14246 | The factorial of 2. (Contributed by NM, 17-Mar-2005.) |
⊢ (!‘2) = 2 | ||
Theorem | fac3 14247 | The factorial of 3. (Contributed by NM, 17-Mar-2005.) |
⊢ (!‘3) = 6 | ||
Theorem | fac4 14248 | The factorial of 4. (Contributed by Mario Carneiro, 18-Jun-2015.) |
⊢ (!‘4) = ;24 | ||
Theorem | facnn2 14249 | Value of the factorial function expressed recursively. (Contributed by NM, 2-Dec-2004.) |
⊢ (𝑁 ∈ ℕ → (!‘𝑁) = ((!‘(𝑁 − 1)) · 𝑁)) | ||
Theorem | faccl 14250 | Closure of the factorial function. (Contributed by NM, 2-Dec-2004.) |
⊢ (𝑁 ∈ ℕ0 → (!‘𝑁) ∈ ℕ) | ||
Theorem | faccld 14251 | Closure of the factorial function, deduction version of faccl 14250. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (!‘𝑁) ∈ ℕ) | ||
Theorem | facmapnn 14252 | 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 14253 | The factorial function is nonzero. (Contributed by NM, 26-Apr-2005.) |
⊢ (𝑁 ∈ ℕ0 → (!‘𝑁) ≠ 0) | ||
Theorem | facdiv 14254 | A positive integer divides the factorial of an equal or larger number. (Contributed by NM, 2-May-2005.) |
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑁 ≤ 𝑀) → ((!‘𝑀) / 𝑁) ∈ ℕ) | ||
Theorem | facndiv 14255 | 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 14256 | Ordering property of factorial. (Contributed by NM, 9-Dec-2005.) |
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁) → (!‘𝑀) ≤ (!‘𝑁)) | ||
Theorem | faclbnd 14257 | A lower bound for the factorial function. (Contributed by NM, 17-Dec-2005.) |
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀↑(𝑁 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑁))) | ||
Theorem | faclbnd2 14258 | A lower bound for the factorial function. (Contributed by NM, 17-Dec-2005.) |
⊢ (𝑁 ∈ ℕ0 → ((2↑𝑁) / 2) ≤ (!‘𝑁)) | ||
Theorem | faclbnd3 14259 | A lower bound for the factorial function. (Contributed by NM, 19-Dec-2005.) |
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀↑𝑁) ≤ ((𝑀↑𝑀) · (!‘𝑁))) | ||
Theorem | faclbnd4lem1 14260 | Lemma for faclbnd4 14264. Prepare the induction step. (Contributed by NM, 20-Dec-2005.) |
⊢ 𝑁 ∈ ℕ & ⊢ 𝐾 ∈ ℕ0 & ⊢ 𝑀 ∈ ℕ0 ⇒ ⊢ ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ≤ (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁))) | ||
Theorem | faclbnd4lem2 14261 | Lemma for faclbnd4 14264. Use the weak deduction theorem to convert the hypotheses of faclbnd4lem1 14260 to antecedents. (Contributed by NM, 23-Dec-2005.) |
⊢ ((𝑀 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ) → ((((𝑁 − 1)↑𝐾) · (𝑀↑(𝑁 − 1))) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘(𝑁 − 1))) → ((𝑁↑(𝐾 + 1)) · (𝑀↑𝑁)) ≤ (((2↑((𝐾 + 1)↑2)) · (𝑀↑(𝑀 + (𝐾 + 1)))) · (!‘𝑁)))) | ||
Theorem | faclbnd4lem3 14262 | Lemma for faclbnd4 14264. The 𝑁 = 0 case. (Contributed by NM, 23-Dec-2005.) |
⊢ (((𝑀 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0) ∧ 𝑁 = 0) → ((𝑁↑𝐾) · (𝑀↑𝑁)) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁))) | ||
Theorem | faclbnd4lem4 14263 | Lemma for faclbnd4 14264. Prove the 0 < 𝑁 case by induction on 𝐾. (Contributed by NM, 19-Dec-2005.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0) → ((𝑁↑𝐾) · (𝑀↑𝑁)) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁))) | ||
Theorem | faclbnd4 14264 | Variant of faclbnd5 14265 providing a non-strict lower bound. (Contributed by NM, 23-Dec-2005.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0) → ((𝑁↑𝐾) · (𝑀↑𝑁)) ≤ (((2↑(𝐾↑2)) · (𝑀↑(𝑀 + 𝐾))) · (!‘𝑁))) | ||
Theorem | faclbnd5 14265 | 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 14266 | 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 14267 | An upper bound for the factorial function. (Contributed by Mario Carneiro, 15-Apr-2016.) |
⊢ (𝑁 ∈ ℕ0 → (!‘𝑁) ≤ (𝑁↑𝑁)) | ||
Theorem | facavg 14268 | 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 14269 | Extend class notation to include the binomial coefficient operation (combinatorial choose operation). |
class C | ||
Definition | df-bc 14270* |
Define the binomial coefficient operation. For example,
(5C3) = 10 (ex-bc 30137).
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 14271 | 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 14272 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 14272 | 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 14273 | 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 14274 | 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 14275 | Closure of the binomial coefficient in the positive reals. (This is mostly a lemma before we have bccl2 14290.) (Contributed by Mario Carneiro, 10-Mar-2014.) |
⊢ (𝐾 ∈ (0...𝑁) → (𝑁C𝐾) ∈ ℝ+) | ||
Theorem | bccmpl 14276 | "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 14277 | 𝑁 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 14278 | The binomial coefficient " 0 choose 𝐾 " is 0 for a positive integer K. Note that (0C0) = 1 (see bcn0 14277). (Contributed by Alexander van der Vekens, 1-Jan-2018.) |
⊢ (𝐾 ∈ ℕ → (0C𝐾) = 0) | ||
Theorem | bcnn 14279 | 𝑁 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 14280 | Binomial coefficient: 𝑁 choose 1. (Contributed by NM, 21-Jun-2005.) (Revised by Mario Carneiro, 8-Nov-2013.) |
⊢ (𝑁 ∈ ℕ0 → (𝑁C1) = 𝑁) | ||
Theorem | bcnp1n 14281 | Binomial coefficient: 𝑁 + 1 choose 𝑁. (Contributed by NM, 20-Jun-2005.) (Revised by Mario Carneiro, 8-Nov-2013.) |
⊢ (𝑁 ∈ ℕ0 → ((𝑁 + 1)C𝑁) = (𝑁 + 1)) | ||
Theorem | bcm1k 14282 | 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 14283 | 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 14284 | 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 14285 | 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 14286 | Binomial coefficient: 𝑁 choose 2. (Contributed by Mario Carneiro, 22-May-2014.) |
⊢ (𝑁 ∈ ℕ0 → (𝑁C2) = ((𝑁 · (𝑁 − 1)) / 2)) | ||
Theorem | bcp1m1 14287 | 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 14288 | 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 14289 | 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 14290 | 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 14291 | 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 14292 | 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 14293 | 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 14294 | The binomial coefficent of (𝑁 − 1) is 𝑁. (Contributed by Scott Fenton, 16-May-2014.) |
⊢ (𝑁 ∈ ℕ0 → (𝑁C(𝑁 − 1)) = 𝑁) | ||
Theorem | 4bc3eq4 14295 | The value of four choose three. (Contributed by Scott Fenton, 11-Jun-2016.) |
⊢ (4C3) = 4 | ||
Theorem | 4bc2eq6 14296 | The value of four choose two. (Contributed by Scott Fenton, 9-Jan-2017.) |
⊢ (4C2) = 6 | ||
Syntax | chash 14297 | Extend the definition of a class to include the set size function. |
class ♯ | ||
Definition | df-hash 14298 | 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 30138). (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ ♯ = (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) ∘ card) ∪ ((V ∖ Fin) × {+∞})) | ||
Theorem | hashkf 14299 | 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 14300* | The value of the ♯ function in terms of the mapping 𝐺 from ω to ℕ0. The proof avoids the use of ax-ac 10460. (Contributed by Paul Chapman, 22-Jun-2011.) (Revised by Mario Carneiro, 26-Dec-2014.) |
⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 0) ↾ ω) ⇒ ⊢ (𝐴 ∈ Fin → (𝐺‘(card‘𝐴)) = (♯‘𝐴)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |