P. 111 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 11001-11100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nnexpcld 11001	Closure of exponentiation of nonnegative integers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐴↑𝑁) ∈ ℕ)
Theorem	nn0expcld 11002	Closure of exponentiation of nonnegative integers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐴↑𝑁) ∈ ℕ0)
Theorem	rpexpcld 11003	Closure law for exponentiation of positive reals. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝐴↑𝑁) ∈ ℝ+)
Theorem	reexpclzapd 11004	Closure of exponentiation of reals. (Contributed by Jim Kingdon, 13-Jun-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 # 0)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝐴↑𝑁) ∈ ℝ)
Theorem	resqcld 11005	Closure of square in reals. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴↑2) ∈ ℝ)
Theorem	sqge0d 11006	A square of a real is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → 0 ≤ (𝐴↑2))
Theorem	sqgt0apd 11007	The square of a real apart from zero is positive. (Contributed by Jim Kingdon, 13-Jun-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 # 0)    ⇒   ⊢ (𝜑 → 0 < (𝐴↑2))
Theorem	leexp2ad 11008	Ordering relationship for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 1 ≤ 𝐴)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    ⇒   ⊢ (𝜑 → (𝐴↑𝑀) ≤ (𝐴↑𝑁))
Theorem	leexp2rd 11009	Ordering relationship for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐴 ≤ 1)    ⇒   ⊢ (𝜑 → (𝐴↑𝑁) ≤ (𝐴↑𝑀))
Theorem	lt2sqd 11010	The square function on nonnegative reals is strictly monotonic. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 0 ≤ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐴↑2) < (𝐵↑2)))
Theorem	le2sqd 11011	The square function on nonnegative reals is monotonic. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 0 ≤ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐴↑2) ≤ (𝐵↑2)))
Theorem	sq11d 11012	The square function is one-to-one for nonnegative reals. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 0 ≤ 𝐵)    &   ⊢ (𝜑 → (𝐴↑2) = (𝐵↑2))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	sq11ap 11013	Analogue to sq11 10918 but for apartness. (Contributed by Jim Kingdon, 12-Aug-2021.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴↑2) # (𝐵↑2) ↔ 𝐴 # 𝐵))
Theorem	zzlesq 11014	An integer is less than or equal to its square. (Contributed by BJ, 6-Feb-2025.)
⊢ (𝑁 ∈ ℤ → 𝑁 ≤ (𝑁↑2))
Theorem	nn0ltexp2 11015	Special case of ltexp2 15732 which we use here because we haven't yet defined df-rpcxp 15650 which is used in the current proof of ltexp2 15732. (Contributed by Jim Kingdon, 7-Oct-2024.)
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 1 < 𝐴) → (𝑀 < 𝑁 ↔ (𝐴↑𝑀) < (𝐴↑𝑁)))
Theorem	nn0leexp2 11016	Ordering law for exponentiation. (Contributed by Jim Kingdon, 9-Oct-2024.)
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 1 < 𝐴) → (𝑀 ≤ 𝑁 ↔ (𝐴↑𝑀) ≤ (𝐴↑𝑁)))
Theorem	mulsubdivbinom2ap 11017	The square of a binomial with factor minus a number divided by a number apart from zero. (Contributed by AV, 19-Jul-2021.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → (((((𝐶 · 𝐴) + 𝐵)↑2) − 𝐷) / 𝐶) = (((𝐶 · (𝐴↑2)) + (2 · (𝐴 · 𝐵))) + (((𝐵↑2) − 𝐷) / 𝐶)))
Theorem	sq10 11018	The square of 10 is 100. (Contributed by AV, 14-Jun-2021.) (Revised by AV, 1-Aug-2021.)
⊢ (;10↑2) = ;;100
Theorem	sq10e99m1 11019	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 11020	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	expcanlem 11021	Lemma for expcan 11022. Proving the order in one direction. (Contributed by Jim Kingdon, 29-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 1 < 𝐴)    ⇒   ⊢ (𝜑 → ((𝐴↑𝑀) ≤ (𝐴↑𝑁) → 𝑀 ≤ 𝑁))
Theorem	expcan 11022	Cancellation law for exponentiation. (Contributed by NM, 2-Aug-2006.) (Revised by Mario Carneiro, 4-Jun-2014.)
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 1 < 𝐴) → ((𝐴↑𝑀) = (𝐴↑𝑁) ↔ 𝑀 = 𝑁))
Theorem	expcand 11023	Ordering relationship for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 1 < 𝐴)    &   ⊢ (𝜑 → (𝐴↑𝑀) = (𝐴↑𝑁))    ⇒   ⊢ (𝜑 → 𝑀 = 𝑁)
Theorem	apexp1 11024	Exponentiation and apartness. (Contributed by Jim Kingdon, 9-Jul-2024.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ) → ((𝐴↑𝑁) # (𝐵↑𝑁) → 𝐴 # 𝐵))
4.6.7  Ordered pair theorem for nonnegative integers
Theorem	nn0le2msqd 11025	The square function on nonnegative integers is monotonic. (Contributed by Jim Kingdon, 31-Oct-2021.)
⊢ (𝜑 → 𝐴 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐴 · 𝐴) ≤ (𝐵 · 𝐵)))
Theorem	nn0opthlem1d 11026	A rather pretty lemma for nn0opth2 11030. (Contributed by Jim Kingdon, 31-Oct-2021.)
⊢ (𝜑 → 𝐴 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐴 < 𝐶 ↔ ((𝐴 · 𝐴) + (2 · 𝐴)) < (𝐶 · 𝐶)))
Theorem	nn0opthlem2d 11027	Lemma for nn0opth2 11030. (Contributed by Jim Kingdon, 31-Oct-2021.)
⊢ (𝜑 → 𝐴 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐷 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) < 𝐶 → ((𝐶 · 𝐶) + 𝐷) ≠ (((𝐴 + 𝐵) · (𝐴 + 𝐵)) + 𝐵)))
Theorem	nn0opthd 11028	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 3682 that works for any set. (Contributed by Jim Kingdon, 31-Oct-2021.)
⊢ (𝜑 → 𝐴 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐷 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((((𝐴 + 𝐵) · (𝐴 + 𝐵)) + 𝐵) = (((𝐶 + 𝐷) · (𝐶 + 𝐷)) + 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
Theorem	nn0opth2d 11029	An ordered pair theorem for nonnegative integers. Theorem 17.3 of [Quine] p. 124. See comments for nn0opthd 11028. (Contributed by Jim Kingdon, 31-Oct-2021.)
⊢ (𝜑 → 𝐴 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐷 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((((𝐴 + 𝐵)↑2) + 𝐵) = (((𝐶 + 𝐷)↑2) + 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
Theorem	nn0opth2 11030	An ordered pair theorem for nonnegative integers. Theorem 17.3 of [Quine] p. 124. See nn0opthd 11028. (Contributed by NM, 22-Jul-2004.)
⊢ (((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) ∧ (𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0)) → ((((𝐴 + 𝐵)↑2) + 𝐵) = (((𝐶 + 𝐷)↑2) + 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
4.6.8  Factorial function
Syntax	cfa 11031	Extend class notation to include the factorial of nonnegative integers.
class !
Definition	df-fac 11032	Define the factorial function on nonnegative integers. For example, (!‘5) = 120 because 1 · 2 · 3 · 4 · 5 = 120 (ex-fac 16422). 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 11033	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 11034	The factorial of 0. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.)
⊢ (!‘0) = 1
Theorem	fac1 11035	The factorial of 1. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.)
⊢ (!‘1) = 1
Theorem	facp1 11036	The factorial of a successor. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.)
⊢ (𝑁 ∈ ℕ0 → (!‘(𝑁 + 1)) = ((!‘𝑁) · (𝑁 + 1)))
Theorem	fac2 11037	The factorial of 2. (Contributed by NM, 17-Mar-2005.)
⊢ (!‘2) = 2
Theorem	fac3 11038	The factorial of 3. (Contributed by NM, 17-Mar-2005.)
⊢ (!‘3) = 6
Theorem	fac4 11039	The factorial of 4. (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ (!‘4) = ;24
Theorem	facnn2 11040	Value of the factorial function expressed recursively. (Contributed by NM, 2-Dec-2004.)
⊢ (𝑁 ∈ ℕ → (!‘𝑁) = ((!‘(𝑁 − 1)) · 𝑁))
Theorem	faccl 11041	Closure of the factorial function. (Contributed by NM, 2-Dec-2004.)
⊢ (𝑁 ∈ ℕ0 → (!‘𝑁) ∈ ℕ)
Theorem	faccld 11042	Closure of the factorial function, deduction version of faccl 11041. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (!‘𝑁) ∈ ℕ)
Theorem	facne0 11043	The factorial function is nonzero. (Contributed by NM, 26-Apr-2005.)
⊢ (𝑁 ∈ ℕ0 → (!‘𝑁) ≠ 0)
Theorem	facdiv 11044	A positive integer divides the factorial of an equal or larger number. (Contributed by NM, 2-May-2005.)
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑁 ≤ 𝑀) → ((!‘𝑀) / 𝑁) ∈ ℕ)
Theorem	facndiv 11045	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 11046	Ordering property of factorial. (Contributed by NM, 9-Dec-2005.)
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁) → (!‘𝑀) ≤ (!‘𝑁))
Theorem	faclbnd 11047	A lower bound for the factorial function. (Contributed by NM, 17-Dec-2005.)
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀↑(𝑁 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑁)))
Theorem	faclbnd2 11048	A lower bound for the factorial function. (Contributed by NM, 17-Dec-2005.)
⊢ (𝑁 ∈ ℕ0 → ((2↑𝑁) / 2) ≤ (!‘𝑁))
Theorem	faclbnd3 11049	A lower bound for the factorial function. (Contributed by NM, 19-Dec-2005.)
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀↑𝑁) ≤ ((𝑀↑𝑀) · (!‘𝑁)))
Theorem	faclbnd6 11050	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 11051	An upper bound for the factorial function. (Contributed by Mario Carneiro, 15-Apr-2016.)
⊢ (𝑁 ∈ ℕ0 → (!‘𝑁) ≤ (𝑁↑𝑁))
Theorem	facavg 11052	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))) ≤ ((!‘𝑀) · (!‘𝑁)))
4.6.9  The binomial coefficient operation
Syntax	cbc 11053	Extend class notation to include the binomial coefficient operation (combinatorial choose operation).
class C
Definition	df-bc 11054*	Define the binomial coefficient operation. For example, (5C3) = 10 (ex-bc 16423). 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". (𝑁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 11055	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 11056 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 11056	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 11057	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 11058	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 11059	Closure of the binomial coefficient in the positive reals. (This is mostly a lemma before we have bccl2 11074.) (Contributed by Mario Carneiro, 10-Mar-2014.)
⊢ (𝐾 ∈ (0...𝑁) → (𝑁C𝐾) ∈ ℝ+)
Theorem	bccmpl 11060	"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 11061	𝑁 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 11062	The binomial coefficient " 0 choose 𝐾 " is 0 for a positive integer K. Note that (0C0) = 1 (see bcn0 11061). (Contributed by Alexander van der Vekens, 1-Jan-2018.)
⊢ (𝐾 ∈ ℕ → (0C𝐾) = 0)
Theorem	bcnn 11063	𝑁 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 11064	Binomial coefficient: 𝑁 choose 1. (Contributed by NM, 21-Jun-2005.) (Revised by Mario Carneiro, 8-Nov-2013.)
⊢ (𝑁 ∈ ℕ0 → (𝑁C1) = 𝑁)
Theorem	bcnp1n 11065	Binomial coefficient: 𝑁 + 1 choose 𝑁. (Contributed by NM, 20-Jun-2005.) (Revised by Mario Carneiro, 8-Nov-2013.)
⊢ (𝑁 ∈ ℕ0 → ((𝑁 + 1)C𝑁) = (𝑁 + 1))
Theorem	bcm1k 11066	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 11067	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 11068	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 11069	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.) (Revised by Jim Kingdon, 23-Apr-2023.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ) → (𝑁C𝐾) = ((seq((𝑁 − 𝐾) + 1)( · , I )‘𝑁) / (!‘𝐾)))
Theorem	bcn2 11070	Binomial coefficient: 𝑁 choose 2. (Contributed by Mario Carneiro, 22-May-2014.)
⊢ (𝑁 ∈ ℕ0 → (𝑁C2) = ((𝑁 · (𝑁 − 1)) / 2))
Theorem	bcp1m1 11071	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 11072	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 11073	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 11074	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 11075	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 11076	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 11077	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 11078	The binomial coefficent of (𝑁 − 1) is 𝑁. (Contributed by Scott Fenton, 16-May-2014.)
⊢ (𝑁 ∈ ℕ0 → (𝑁C(𝑁 − 1)) = 𝑁)
Theorem	4bc3eq4 11079	The value of four choose three. (Contributed by Scott Fenton, 11-Jun-2016.)
⊢ (4C3) = 4
Theorem	4bc2eq6 11080	The value of four choose two. (Contributed by Scott Fenton, 9-Jan-2017.)
⊢ (4C2) = 6
4.6.10  The ` # ` (set size) function
Syntax	chash 11081	Extend the definition of a class to include the set size function.
class ♯
Definition	df-ihash 11082*	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. Since we don't know that an arbitrary set is either finite or infinite (by inffiexmid 7141), the behavior beyond finite sets is not as useful as it might appear. For example, we wouldn't expect to be able to define this function in a meaningful way on 𝒫 1o, which cannot be shown to be finite (per pw1fin 7145). Note that we use the sharp sign (♯) for this function and we use the different character octothorpe (#) for the apartness relation (see df-ap 8805). We adopt the former notation from Corollary 8.2.4 of [AczelRathjen], p. 80 (although that work only defines it for finite sets). This definition (in terms of ∪ and ≼) is not taken directly from the literature, but for finite sets should be equivalent to the conventional definition that the size of a finite set is the unique natural number which is equinumerous to the given set. (Contributed by Jim Kingdon, 19-Feb-2022.)
⊢ ♯ = ((frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) ∪ {⟨ω, +∞⟩}) ∘ (𝑥 ∈ V ↦ ∪ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦 ≼ 𝑥}))
Theorem	hashinfuni 11083*	The ordinal size of an infinite set is ω. (Contributed by Jim Kingdon, 20-Feb-2022.)
⊢ (ω ≼ 𝐴 → ∪ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦 ≼ 𝐴} = ω)
Theorem	hashinfom 11084	The value of the ♯ function on an infinite set. (Contributed by Jim Kingdon, 20-Feb-2022.)
⊢ (ω ≼ 𝐴 → (♯‘𝐴) = +∞)
Theorem	hashennnuni 11085*	The ordinal size of a set equinumerous to an element of ω is that element of ω. (Contributed by Jim Kingdon, 20-Feb-2022.)
⊢ ((𝑁 ∈ ω ∧ 𝑁 ≈ 𝐴) → ∪ {𝑦 ∈ (ω ∪ {ω}) ∣ 𝑦 ≼ 𝐴} = 𝑁)
Theorem	hashennn 11086*	The size of a set equinumerous to an element of ω. (Contributed by Jim Kingdon, 21-Feb-2022.)
⊢ ((𝑁 ∈ ω ∧ 𝑁 ≈ 𝐴) → (♯‘𝐴) = (frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)‘𝑁))
Theorem	hashcl 11087	Closure of the ♯ function. (Contributed by Paul Chapman, 26-Oct-2012.) (Revised by Mario Carneiro, 13-Jul-2014.)
⊢ (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℕ0)
Theorem	hashfiv01gt1 11088	The size of a finite set is either 0 or 1 or greater than 1. (Contributed by Jim Kingdon, 21-Feb-2022.)
⊢ (𝑀 ∈ Fin → ((♯‘𝑀) = 0 ∨ (♯‘𝑀) = 1 ∨ 1 < (♯‘𝑀)))
Theorem	hashfz1 11089	The set (1...𝑁) has 𝑁 elements. (Contributed by Paul Chapman, 22-Jun-2011.) (Revised by Mario Carneiro, 15-Sep-2013.)
⊢ (𝑁 ∈ ℕ0 → (♯‘(1...𝑁)) = 𝑁)
Theorem	hashen 11090	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	hasheqf1o 11091*	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 11092*	There is no bijection between a finite set and an infinite set. By infnfi 7127 the theorem would also hold if "infinite" were expressed as ω ≼ 𝐵. (Contributed by Alexander van der Vekens, 25-Dec-2017.)
⊢ ((𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin) → ¬ ∃𝑓 𝑓:𝐴–1-1-onto→𝐵)
Theorem	fihasheqf1oi 11093	The size of two finite sets is equal if there is a bijection mapping one of the sets onto the other. (Contributed by Jim Kingdon, 21-Feb-2022.)
⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴–1-1-onto→𝐵) → (♯‘𝐴) = (♯‘𝐵))
Theorem	fihashf1rn 11094	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 Jim Kingdon, 21-Feb-2022.)
⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴–1-1→𝐵) → (♯‘𝐹) = (♯‘ran 𝐹))
Theorem	fihasheqf1od 11095	The size of two finite sets is equal if there is a bijection mapping one of the sets onto the other. (Contributed by Jim Kingdon, 21-Feb-2022.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵)    ⇒   ⊢ (𝜑 → (♯‘𝐴) = (♯‘𝐵))
Theorem	fz1eqb 11096	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	filtinf 11097	The size of an infinite set is greater than the size of a finite set. (Contributed by Jim Kingdon, 21-Feb-2022.)
⊢ ((𝐴 ∈ Fin ∧ ω ≼ 𝐵) → (♯‘𝐴) < (♯‘𝐵))
Theorem	isfinite4im 11098	A finite set is equinumerous to the range of integers from one up to the hash value of the set. (Contributed by Jim Kingdon, 22-Feb-2022.)
⊢ (𝐴 ∈ Fin → (1...(♯‘𝐴)) ≈ 𝐴)
Theorem	fihasheq0 11099	Two ways of saying a finite set is empty. (Contributed by Paul Chapman, 26-Oct-2012.) (Revised by Mario Carneiro, 27-Jul-2014.) (Intuitionized by Jim Kingdon, 23-Feb-2022.)
⊢ (𝐴 ∈ Fin → ((♯‘𝐴) = 0 ↔ 𝐴 = ∅))
Theorem	fihashneq0 11100	Two ways of saying a finite set is not empty. Also, "A is inhabited" would be equivalent by fin0 7117. (Contributed by Alexander van der Vekens, 23-Sep-2018.) (Intuitionized by Jim Kingdon, 23-Feb-2022.)
⊢ (𝐴 ∈ Fin → (0 < (♯‘𝐴) ↔ 𝐴 ≠ ∅))