P. 143 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 14201-14300   *Has distinct variable group(s)

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 · 𝐵)) + 𝐶)
5.6.8  Ordered pair theorem for nonnegative integers
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) + 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
5.6.9  Factorial function
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))) ≤ ((!‘𝑀) · (!‘𝑁)))
5.6.10  The binomial coefficient operation
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
5.6.11  The ` # ` (set size) function
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‘𝐴)) = (♯‘𝐴))