P. 109 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 10801-10900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	subsqi 10801	Factor the difference of two squares. (Contributed by NM, 7-Feb-2005.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ ((𝐴↑2) − (𝐵↑2)) = ((𝐴 + 𝐵) · (𝐴 − 𝐵))
Theorem	qsqeqor 10802	The squares of two rational numbers are equal iff one number equals the other or its negative. (Contributed by Jim Kingdon, 1-Nov-2024.)
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → ((𝐴↑2) = (𝐵↑2) ↔ (𝐴 = 𝐵 ∨ 𝐴 = -𝐵)))
Theorem	binom2 10803	The square of a binomial. (Contributed by FL, 10-Dec-2006.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑2) = (((𝐴↑2) + (2 · (𝐴 · 𝐵))) + (𝐵↑2)))
Theorem	binom21 10804	Special case of binom2 10803 where 𝐵 = 1. (Contributed by Scott Fenton, 11-May-2014.)
⊢ (𝐴 ∈ ℂ → ((𝐴 + 1)↑2) = (((𝐴↑2) + (2 · 𝐴)) + 1))
Theorem	binom2sub 10805	Expand the square of a subtraction. (Contributed by Scott Fenton, 10-Jun-2013.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵)↑2) = (((𝐴↑2) − (2 · (𝐴 · 𝐵))) + (𝐵↑2)))
Theorem	binom2sub1 10806	Special case of binom2sub 10805 where 𝐵 = 1. (Contributed by AV, 2-Aug-2021.)
⊢ (𝐴 ∈ ℂ → ((𝐴 − 1)↑2) = (((𝐴↑2) − (2 · 𝐴)) + 1))
Theorem	binom2subi 10807	Expand the square of a subtraction. (Contributed by Scott Fenton, 13-Jun-2013.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ ((𝐴 − 𝐵)↑2) = (((𝐴↑2) − (2 · (𝐴 · 𝐵))) + (𝐵↑2))
Theorem	mulbinom2 10808	The square of a binomial with factor. (Contributed by AV, 19-Jul-2021.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (((𝐶 · 𝐴) + 𝐵)↑2) = ((((𝐶 · 𝐴)↑2) + ((2 · 𝐶) · (𝐴 · 𝐵))) + (𝐵↑2)))
Theorem	binom3 10809	The cube of a binomial. (Contributed by Mario Carneiro, 24-Apr-2015.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑3) = (((𝐴↑3) + (3 · ((𝐴↑2) · 𝐵))) + ((3 · (𝐴 · (𝐵↑2))) + (𝐵↑3))))
Theorem	zesq 10810	An integer is even iff its square is even. (Contributed by Mario Carneiro, 12-Sep-2015.)
⊢ (𝑁 ∈ ℤ → ((𝑁 / 2) ∈ ℤ ↔ ((𝑁↑2) / 2) ∈ ℤ))
Theorem	nnesq 10811	A positive integer is even iff its square is even. (Contributed by NM, 20-Aug-2001.) (Revised by Mario Carneiro, 12-Sep-2015.)
⊢ (𝑁 ∈ ℕ → ((𝑁 / 2) ∈ ℕ ↔ ((𝑁↑2) / 2) ∈ ℕ))
Theorem	bernneq 10812	Bernoulli's inequality, due to Johan Bernoulli (1667-1748). (Contributed by NM, 21-Feb-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ -1 ≤ 𝐴) → (1 + (𝐴 · 𝑁)) ≤ ((1 + 𝐴)↑𝑁))
Theorem	bernneq2 10813	Variation of Bernoulli's inequality bernneq 10812. (Contributed by NM, 18-Oct-2007.)
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ∧ 0 ≤ 𝐴) → (((𝐴 − 1) · 𝑁) + 1) ≤ (𝐴↑𝑁))
Theorem	bernneq3 10814	A corollary of bernneq 10812. (Contributed by Mario Carneiro, 11-Mar-2014.)
⊢ ((𝑃 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ0) → 𝑁 < (𝑃↑𝑁))
Theorem	expnbnd 10815*	Exponentiation with a base greater than 1 has no upper bound. (Contributed by NM, 20-Oct-2007.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → ∃𝑘 ∈ ℕ 𝐴 < (𝐵↑𝑘))
Theorem	expnlbnd 10816*	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 10817*	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	modqexp 10818	Exponentiation property of the modulo operation, see theorem 5.2(c) in [ApostolNT] p. 107. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 7-Sep-2024.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐷 ∈ ℚ)    &   ⊢ (𝜑 → 0 < 𝐷)    &   ⊢ (𝜑 → (𝐴 mod 𝐷) = (𝐵 mod 𝐷))    ⇒   ⊢ (𝜑 → ((𝐴↑𝐶) mod 𝐷) = ((𝐵↑𝐶) mod 𝐷))
Theorem	exp0d 10819	Value of a complex number raised to the 0th power. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴↑0) = 1)
Theorem	exp1d 10820	Value of a complex number raised to the first power. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴↑1) = 𝐴)
Theorem	expeq0d 10821	Positive integer exponentiation is 0 iff its base is 0. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → (𝐴↑𝑁) = 0)    ⇒   ⊢ (𝜑 → 𝐴 = 0)
Theorem	sqvald 10822	Value of square. Inference version. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴↑2) = (𝐴 · 𝐴))
Theorem	sqcld 10823	Closure of square. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴↑2) ∈ ℂ)
Theorem	sqeq0d 10824	A number is zero iff its square is zero. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴↑2) = 0)    ⇒   ⊢ (𝜑 → 𝐴 = 0)
Theorem	expcld 10825	Closure law for nonnegative integer exponentiation. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐴↑𝑁) ∈ ℂ)
Theorem	expp1d 10826	Value of a complex number raised to a nonnegative integer power plus one. Part of Definition 10-4.1 of [Gleason] p. 134. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐴↑(𝑁 + 1)) = ((𝐴↑𝑁) · 𝐴))
Theorem	expaddd 10827	Sum of exponents law for nonnegative integer exponentiation. Proposition 10-4.2(a) of [Gleason] p. 135. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐴↑(𝑀 + 𝑁)) = ((𝐴↑𝑀) · (𝐴↑𝑁)))
Theorem	expmuld 10828	Product of exponents law for positive integer exponentiation. Proposition 10-4.2(b) of [Gleason] p. 135, restricted to nonnegative integer exponents. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐴↑(𝑀 · 𝑁)) = ((𝐴↑𝑀)↑𝑁))
Theorem	sqrecapd 10829	Square of reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    ⇒   ⊢ (𝜑 → ((1 / 𝐴)↑2) = (1 / (𝐴↑2)))
Theorem	expclzapd 10830	Closure law for integer exponentiation. (Contributed by Jim Kingdon, 12-Jun-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝐴↑𝑁) ∈ ℂ)
Theorem	expap0d 10831	Nonnegative integer exponentiation is nonzero if its base is nonzero. (Contributed by Jim Kingdon, 12-Jun-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝐴↑𝑁) # 0)
Theorem	expnegapd 10832	Value of a complex number raised to a negative power. (Contributed by Jim Kingdon, 12-Jun-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝐴↑-𝑁) = (1 / (𝐴↑𝑁)))
Theorem	exprecapd 10833	Nonnegative integer exponentiation of a reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    ⇒   ⊢ (𝜑 → ((1 / 𝐴)↑𝑁) = (1 / (𝐴↑𝑁)))
Theorem	expp1zapd 10834	Value of a nonzero complex number raised to an integer power plus one. (Contributed by Jim Kingdon, 12-Jun-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝐴↑(𝑁 + 1)) = ((𝐴↑𝑁) · 𝐴))
Theorem	expm1apd 10835	Value of a complex number raised to an integer power minus one. (Contributed by Jim Kingdon, 12-Jun-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝐴↑(𝑁 − 1)) = ((𝐴↑𝑁) / 𝐴))
Theorem	expsubapd 10836	Exponent subtraction law for nonnegative integer exponentiation. (Contributed by Jim Kingdon, 12-Jun-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝐴↑(𝑀 − 𝑁)) = ((𝐴↑𝑀) / (𝐴↑𝑁)))
Theorem	sqmuld 10837	Distribution of square over multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵)↑2) = ((𝐴↑2) · (𝐵↑2)))
Theorem	sqdivapd 10838	Distribution of square over division. (Contributed by Jim Kingdon, 13-Jun-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵)↑2) = ((𝐴↑2) / (𝐵↑2)))
Theorem	expdivapd 10839	Nonnegative integer exponentiation of a quotient. (Contributed by Jim Kingdon, 13-Jun-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵)↑𝑁) = ((𝐴↑𝑁) / (𝐵↑𝑁)))
Theorem	mulexpd 10840	Positive integer exponentiation of a product. Proposition 10-4.2(c) of [Gleason] p. 135, restricted to nonnegative integer exponents. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵)↑𝑁) = ((𝐴↑𝑁) · (𝐵↑𝑁)))
Theorem	0expd 10841	Value of zero raised to a positive integer power. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → (0↑𝑁) = 0)
Theorem	reexpcld 10842	Closure of exponentiation of reals. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐴↑𝑁) ∈ ℝ)
Theorem	expge0d 10843	A nonnegative real raised to a nonnegative integer is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    ⇒   ⊢ (𝜑 → 0 ≤ (𝐴↑𝑁))
Theorem	expge1d 10844	A real greater than or equal to 1 raised to a nonnegative integer is greater than or equal to 1. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 1 ≤ 𝐴)    ⇒   ⊢ (𝜑 → 1 ≤ (𝐴↑𝑁))
Theorem	sqoddm1div8 10845	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 10846	The naturals are closed under squaring. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝐴↑2) ∈ ℕ)
Theorem	nnexpcld 10847	Closure of exponentiation of nonnegative integers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐴↑𝑁) ∈ ℕ)
Theorem	nn0expcld 10848	Closure of exponentiation of nonnegative integers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐴↑𝑁) ∈ ℕ0)
Theorem	rpexpcld 10849	Closure law for exponentiation of positive reals. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝐴↑𝑁) ∈ ℝ+)
Theorem	reexpclzapd 10850	Closure of exponentiation of reals. (Contributed by Jim Kingdon, 13-Jun-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 # 0)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝐴↑𝑁) ∈ ℝ)
Theorem	resqcld 10851	Closure of square in reals. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴↑2) ∈ ℝ)
Theorem	sqge0d 10852	A square of a real is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → 0 ≤ (𝐴↑2))
Theorem	sqgt0apd 10853	The square of a real apart from zero is positive. (Contributed by Jim Kingdon, 13-Jun-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 # 0)    ⇒   ⊢ (𝜑 → 0 < (𝐴↑2))
Theorem	leexp2ad 10854	Ordering relationship for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 1 ≤ 𝐴)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    ⇒   ⊢ (𝜑 → (𝐴↑𝑀) ≤ (𝐴↑𝑁))
Theorem	leexp2rd 10855	Ordering relationship for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐴 ≤ 1)    ⇒   ⊢ (𝜑 → (𝐴↑𝑁) ≤ (𝐴↑𝑀))
Theorem	lt2sqd 10856	The square function on nonnegative reals is strictly monotonic. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 0 ≤ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 < 𝐵 ↔ (𝐴↑2) < (𝐵↑2)))
Theorem	le2sqd 10857	The square function on nonnegative reals is monotonic. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 0 ≤ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐴↑2) ≤ (𝐵↑2)))
Theorem	sq11d 10858	The square function is one-to-one for nonnegative reals. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 0 ≤ 𝐵)    &   ⊢ (𝜑 → (𝐴↑2) = (𝐵↑2))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	sq11ap 10859	Analogue to sq11 10764 but for apartness. (Contributed by Jim Kingdon, 12-Aug-2021.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → ((𝐴↑2) # (𝐵↑2) ↔ 𝐴 # 𝐵))
Theorem	zzlesq 10860	An integer is less than or equal to its square. (Contributed by BJ, 6-Feb-2025.)
⊢ (𝑁 ∈ ℤ → 𝑁 ≤ (𝑁↑2))
Theorem	nn0ltexp2 10861	Special case of ltexp2 15457 which we use here because we haven't yet defined df-rpcxp 15375 which is used in the current proof of ltexp2 15457. (Contributed by Jim Kingdon, 7-Oct-2024.)
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 1 < 𝐴) → (𝑀 < 𝑁 ↔ (𝐴↑𝑀) < (𝐴↑𝑁)))
Theorem	nn0leexp2 10862	Ordering law for exponentiation. (Contributed by Jim Kingdon, 9-Oct-2024.)
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 1 < 𝐴) → (𝑀 ≤ 𝑁 ↔ (𝐴↑𝑀) ≤ (𝐴↑𝑁)))
Theorem	mulsubdivbinom2ap 10863	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 10864	The square of 10 is 100. (Contributed by AV, 14-Jun-2021.) (Revised by AV, 1-Aug-2021.)
⊢ (;10↑2) = ;;100
Theorem	sq10e99m1 10865	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 10866	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 10867	Lemma for expcan 10868. Proving the order in one direction. (Contributed by Jim Kingdon, 29-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 1 < 𝐴)    ⇒   ⊢ (𝜑 → ((𝐴↑𝑀) ≤ (𝐴↑𝑁) → 𝑀 ≤ 𝑁))
Theorem	expcan 10868	Cancellation law for exponentiation. (Contributed by NM, 2-Aug-2006.) (Revised by Mario Carneiro, 4-Jun-2014.)
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 1 < 𝐴) → ((𝐴↑𝑀) = (𝐴↑𝑁) ↔ 𝑀 = 𝑁))
Theorem	expcand 10869	Ordering relationship for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 1 < 𝐴)    &   ⊢ (𝜑 → (𝐴↑𝑀) = (𝐴↑𝑁))    ⇒   ⊢ (𝜑 → 𝑀 = 𝑁)
Theorem	apexp1 10870	Exponentiation and apartness. (Contributed by Jim Kingdon, 9-Jul-2024.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ) → ((𝐴↑𝑁) # (𝐵↑𝑁) → 𝐴 # 𝐵))
4.6.7  Ordered pair theorem for nonnegative integers
Theorem	nn0le2msqd 10871	The square function on nonnegative integers is monotonic. (Contributed by Jim Kingdon, 31-Oct-2021.)
⊢ (𝜑 → 𝐴 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐴 · 𝐴) ≤ (𝐵 · 𝐵)))
Theorem	nn0opthlem1d 10872	A rather pretty lemma for nn0opth2 10876. (Contributed by Jim Kingdon, 31-Oct-2021.)
⊢ (𝜑 → 𝐴 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐴 < 𝐶 ↔ ((𝐴 · 𝐴) + (2 · 𝐴)) < (𝐶 · 𝐶)))
Theorem	nn0opthlem2d 10873	Lemma for nn0opth2 10876. (Contributed by Jim Kingdon, 31-Oct-2021.)
⊢ (𝜑 → 𝐴 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐷 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) < 𝐶 → ((𝐶 · 𝐶) + 𝐷) ≠ (((𝐴 + 𝐵) · (𝐴 + 𝐵)) + 𝐵)))
Theorem	nn0opthd 10874	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 3643 that works for any set. (Contributed by Jim Kingdon, 31-Oct-2021.)
⊢ (𝜑 → 𝐴 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐷 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((((𝐴 + 𝐵) · (𝐴 + 𝐵)) + 𝐵) = (((𝐶 + 𝐷) · (𝐶 + 𝐷)) + 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
Theorem	nn0opth2d 10875	An ordered pair theorem for nonnegative integers. Theorem 17.3 of [Quine] p. 124. See comments for nn0opthd 10874. (Contributed by Jim Kingdon, 31-Oct-2021.)
⊢ (𝜑 → 𝐴 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐷 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((((𝐴 + 𝐵)↑2) + 𝐵) = (((𝐶 + 𝐷)↑2) + 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
Theorem	nn0opth2 10876	An ordered pair theorem for nonnegative integers. Theorem 17.3 of [Quine] p. 124. See nn0opthd 10874. (Contributed by NM, 22-Jul-2004.)
⊢ (((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) ∧ (𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0)) → ((((𝐴 + 𝐵)↑2) + 𝐵) = (((𝐶 + 𝐷)↑2) + 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
4.6.8  Factorial function
Syntax	cfa 10877	Extend class notation to include the factorial of nonnegative integers.
class !
Definition	df-fac 10878	Define the factorial function on nonnegative integers. For example, (!‘5) = 120 because 1 · 2 · 3 · 4 · 5 = 120 (ex-fac 15738). 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 10879	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 10880	The factorial of 0. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.)
⊢ (!‘0) = 1
Theorem	fac1 10881	The factorial of 1. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.)
⊢ (!‘1) = 1
Theorem	facp1 10882	The factorial of a successor. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.)
⊢ (𝑁 ∈ ℕ0 → (!‘(𝑁 + 1)) = ((!‘𝑁) · (𝑁 + 1)))
Theorem	fac2 10883	The factorial of 2. (Contributed by NM, 17-Mar-2005.)
⊢ (!‘2) = 2
Theorem	fac3 10884	The factorial of 3. (Contributed by NM, 17-Mar-2005.)
⊢ (!‘3) = 6
Theorem	fac4 10885	The factorial of 4. (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ (!‘4) = ;24
Theorem	facnn2 10886	Value of the factorial function expressed recursively. (Contributed by NM, 2-Dec-2004.)
⊢ (𝑁 ∈ ℕ → (!‘𝑁) = ((!‘(𝑁 − 1)) · 𝑁))
Theorem	faccl 10887	Closure of the factorial function. (Contributed by NM, 2-Dec-2004.)
⊢ (𝑁 ∈ ℕ0 → (!‘𝑁) ∈ ℕ)
Theorem	faccld 10888	Closure of the factorial function, deduction version of faccl 10887. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (!‘𝑁) ∈ ℕ)
Theorem	facne0 10889	The factorial function is nonzero. (Contributed by NM, 26-Apr-2005.)
⊢ (𝑁 ∈ ℕ0 → (!‘𝑁) ≠ 0)
Theorem	facdiv 10890	A positive integer divides the factorial of an equal or larger number. (Contributed by NM, 2-May-2005.)
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑁 ≤ 𝑀) → ((!‘𝑀) / 𝑁) ∈ ℕ)
Theorem	facndiv 10891	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 10892	Ordering property of factorial. (Contributed by NM, 9-Dec-2005.)
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁) → (!‘𝑀) ≤ (!‘𝑁))
Theorem	faclbnd 10893	A lower bound for the factorial function. (Contributed by NM, 17-Dec-2005.)
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀↑(𝑁 + 1)) ≤ ((𝑀↑𝑀) · (!‘𝑁)))
Theorem	faclbnd2 10894	A lower bound for the factorial function. (Contributed by NM, 17-Dec-2005.)
⊢ (𝑁 ∈ ℕ0 → ((2↑𝑁) / 2) ≤ (!‘𝑁))
Theorem	faclbnd3 10895	A lower bound for the factorial function. (Contributed by NM, 19-Dec-2005.)
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀↑𝑁) ≤ ((𝑀↑𝑀) · (!‘𝑁)))
Theorem	faclbnd6 10896	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 10897	An upper bound for the factorial function. (Contributed by Mario Carneiro, 15-Apr-2016.)
⊢ (𝑁 ∈ ℕ0 → (!‘𝑁) ≤ (𝑁↑𝑁))
Theorem	facavg 10898	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 10899	Extend class notation to include the binomial coefficient operation (combinatorial choose operation).
class C
Definition	df-bc 10900*	Define the binomial coefficient operation. For example, (5C3) = 10 (ex-bc 15739). 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))