P. 162 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 16101-16200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rpcncxpcl 16101	Closure of the complex power function. (Contributed by Jim Kingdon, 12-Jun-2024.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑐𝐵) ∈ ℂ)
Theorem	rpcxpcl 16102	Positive real closure of the complex power function. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ) → (𝐴↑𝑐𝐵) ∈ ℝ+)
Theorem	cxpap0 16103	Complex exponentiation is apart from zero. (Contributed by Mario Carneiro, 2-Aug-2014.) (Revised by Jim Kingdon, 12-Jun-2024.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑐𝐵) # 0)
Theorem	rpcxpadd 16104	Sum of exponents law for complex exponentiation. (Contributed by Mario Carneiro, 2-Aug-2014.) (Revised by Jim Kingdon, 13-Jun-2024.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴↑𝑐(𝐵 + 𝐶)) = ((𝐴↑𝑐𝐵) · (𝐴↑𝑐𝐶)))
Theorem	rpcxpp1 16105	Value of a nonzero complex number raised to a complex power plus one. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑐(𝐵 + 1)) = ((𝐴↑𝑐𝐵) · 𝐴))
Theorem	rpcxpneg 16106	Value of a complex number raised to a negative power. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ) → (𝐴↑𝑐-𝐵) = (1 / (𝐴↑𝑐𝐵)))
Theorem	rpcxpsub 16107	Exponent subtraction law for complex exponentiation. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴↑𝑐(𝐵 − 𝐶)) = ((𝐴↑𝑐𝐵) / (𝐴↑𝑐𝐶)))
Theorem	rpmulcxp 16108	Complex exponentiation of a product. Proposition 10-4.2(c) of [Gleason] p. 135. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵)↑𝑐𝐶) = ((𝐴↑𝑐𝐶) · (𝐵↑𝑐𝐶)))
Theorem	cxprec 16109	Complex exponentiation of a reciprocal. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ) → ((1 / 𝐴)↑𝑐𝐵) = (1 / (𝐴↑𝑐𝐵)))
Theorem	rpdivcxp 16110	Complex exponentiation of a quotient. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℂ) → ((𝐴 / 𝐵)↑𝑐𝐶) = ((𝐴↑𝑐𝐶) / (𝐵↑𝑐𝐶)))
Theorem	cxpmul 16111	Product of exponents law for complex exponentiation. Proposition 10-4.2(b) of [Gleason] p. 135. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℂ) → (𝐴↑𝑐(𝐵 · 𝐶)) = ((𝐴↑𝑐𝐵)↑𝑐𝐶))
Theorem	rpcxpmul2 16112	Product of exponents law for complex exponentiation. Variation on cxpmul 16111 with more general conditions on 𝐴 and 𝐵 when 𝐶 is a nonnegative integer. (Contributed by Mario Carneiro, 9-Aug-2014.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℕ0) → (𝐴↑𝑐(𝐵 · 𝐶)) = ((𝐴↑𝑐𝐵)↑𝐶))
Theorem	rpcxproot 16113	The complex power function allows us to write n-th roots via the idiom 𝐴↑𝑐(1 / 𝑁). (Contributed by Mario Carneiro, 6-May-2015.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℕ) → ((𝐴↑𝑐(1 / 𝑁))↑𝑁) = 𝐴)
Theorem	rpcxpmul2z 16114	Generalize rpcxpmul2 16112 to negative integers. (Contributed by Mario Carneiro, 23-Apr-2015.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℤ) → (𝐴↑𝑐(𝐵 · 𝐶)) = ((𝐴↑𝑐𝐵)↑𝐶))
Theorem	rpcxpmul2zd 16115	Generalize rpcxpmul2 16112 to negative integers. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝐴↑𝑐(𝐵 · 𝐶)) = ((𝐴↑𝑐𝐵)↑𝐶))
Theorem	abscxp 16116	Absolute value of a power, when the base is real. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℂ) → (abs‘(𝐴↑𝑐𝐵)) = (𝐴↑𝑐(ℜ‘𝐵)))
Theorem	cxplt 16117	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ (((𝐴 ∈ ℝ ∧ 1 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ)) → (𝐵 < 𝐶 ↔ (𝐴↑𝑐𝐵) < (𝐴↑𝑐𝐶)))
Theorem	cxple 16118	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 2-Aug-2014.)
⊢ (((𝐴 ∈ ℝ ∧ 1 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ)) → (𝐵 ≤ 𝐶 ↔ (𝐴↑𝑐𝐵) ≤ (𝐴↑𝑐𝐶)))
Theorem	rpcxple2 16119	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+) → (𝐴 ≤ 𝐵 ↔ (𝐴↑𝑐𝐶) ≤ (𝐵↑𝑐𝐶)))
Theorem	rpcxplt2 16120	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+) → (𝐴 < 𝐵 ↔ (𝐴↑𝑐𝐶) < (𝐵↑𝑐𝐶)))
Theorem	cxplt3 16121	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 2-May-2016.)
⊢ (((𝐴 ∈ ℝ+ ∧ 𝐴 < 1) ∧ (𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ)) → (𝐵 < 𝐶 ↔ (𝐴↑𝑐𝐶) < (𝐴↑𝑐𝐵)))
Theorem	cxple3 16122	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 2-May-2016.)
⊢ (((𝐴 ∈ ℝ+ ∧ 𝐴 < 1) ∧ (𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ)) → (𝐵 ≤ 𝐶 ↔ (𝐴↑𝑐𝐶) ≤ (𝐴↑𝑐𝐵)))
Theorem	rpcxpsqrt 16123	The exponential function with exponent 1 / 2 exactly matches the square root function, and thus serves as a suitable generalization to other 𝑛-th roots and irrational roots. (Contributed by Mario Carneiro, 2-Aug-2014.) (Revised by Jim Kingdon, 16-Jun-2024.)
⊢ (𝐴 ∈ ℝ+ → (𝐴↑𝑐(1 / 2)) = (√‘𝐴))
Theorem	logsqrt 16124	Logarithm of a square root. (Contributed by Mario Carneiro, 5-May-2016.)
⊢ (𝐴 ∈ ℝ+ → (log‘(√‘𝐴)) = ((log‘𝐴) / 2))
Theorem	rpcxp0d 16125	Value of the complex power function when the second argument is zero. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴↑𝑐0) = 1)
Theorem	rpcxp1d 16126	Value of the complex power function at one. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴↑𝑐1) = 𝐴)
Theorem	1cxpd 16127	Value of the complex power function at one. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (1↑𝑐𝐴) = 1)
Theorem	rpcncxpcld 16128	Closure of the complex power function. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴↑𝑐𝐵) ∈ ℂ)
Theorem	cxpltd 16129	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 1 < 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐵 < 𝐶 ↔ (𝐴↑𝑐𝐵) < (𝐴↑𝑐𝐶)))
Theorem	cxpled 16130	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 1 < 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐵 ≤ 𝐶 ↔ (𝐴↑𝑐𝐵) ≤ (𝐴↑𝑐𝐶)))
Theorem	rpcxpsqrtth 16131	Square root theorem over the complex numbers for the complex power function. Compare with resqrtth 11813. (Contributed by AV, 23-Dec-2022.)
⊢ (𝐴 ∈ ℝ+ → ((√‘𝐴)↑𝑐2) = 𝐴)
Theorem	cxprecd 16132	Complex exponentiation of a reciprocal. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((1 / 𝐴)↑𝑐𝐵) = (1 / (𝐴↑𝑐𝐵)))
Theorem	rpcxpmul2d 16133	Product of exponents law for complex exponentiation. Variation on cxpmul 16111 with more general conditions on 𝐴 and 𝐵 when 𝐶 is a nonnegative integer. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐴↑𝑐(𝐵 · 𝐶)) = ((𝐴↑𝑐𝐵)↑𝐶))
Theorem	rpcxpcld 16134	Positive real closure of the complex power function. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐴↑𝑐𝐵) ∈ ℝ+)
Theorem	logcxpd 16135	Logarithm of a complex power. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (log‘(𝐴↑𝑐𝐵)) = (𝐵 · (log‘𝐴)))
Theorem	cxplt3d 16136	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 1)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐵 < 𝐶 ↔ (𝐴↑𝑐𝐶) < (𝐴↑𝑐𝐵)))
Theorem	cxple3d 16137	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 1)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝐵 ≤ 𝐶 ↔ (𝐴↑𝑐𝐶) ≤ (𝐴↑𝑐𝐵)))
Theorem	cxpmuld 16138	Product of exponents law for complex exponentiation. Proposition 10-4.2(b) of [Gleason] p. 135. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴↑𝑐(𝐵 · 𝐶)) = ((𝐴↑𝑐𝐵)↑𝑐𝐶))
Theorem	cxpcom 16139	Commutative law for real exponentiation. (Contributed by AV, 29-Dec-2022.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴↑𝑐𝐵)↑𝑐𝐶) = ((𝐴↑𝑐𝐶)↑𝑐𝐵))
Theorem	apcxp2 16140	Apartness and real exponentiation. (Contributed by Jim Kingdon, 10-Jul-2024.)
⊢ (((𝐴 ∈ ℝ+ ∧ 𝐴 # 1) ∧ (𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ)) → (𝐵 # 𝐶 ↔ (𝐴↑𝑐𝐵) # (𝐴↑𝑐𝐶)))
Theorem	rpabscxpbnd 16141	Bound on the absolute value of a complex power. (Contributed by Mario Carneiro, 15-Sep-2014.) (Revised by Jim Kingdon, 19-Jun-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 0 < (ℜ‘𝐵))    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ (𝜑 → (abs‘𝐴) ≤ 𝑀)    ⇒   ⊢ (𝜑 → (abs‘(𝐴↑𝑐𝐵)) ≤ ((𝑀↑𝑐(ℜ‘𝐵)) · (exp‘((abs‘𝐵) · π))))
Theorem	efnthr 16142*	An equation involving an 𝑁-th power. The expression exp(2πi / 𝑁) is a way to write the primitive 𝑁-th root of unity with the smallest positive argument. We could write it as -1↑𝑐(2 / 𝑁) except that we only support positive real numbers as the base for ↑𝑐. The converse is presumably also provable but we do not have a proof yet. (Contributed by Mario Carneiro, 23-Apr-2015.) (Revised by Jim Kingdon, 18-Sep-2026.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝐵 ∈ ℝ+) → (∃𝑛 ∈ (0...(𝑁 − 1))𝐴 = ((𝐵↑𝑐(1 / 𝑁)) · ((exp‘((i · (2 · π)) / 𝑁))↑𝑛)) → (𝐴↑𝑁) = 𝐵))
Theorem	ltexp2 16143	Ordering law for exponentiation. (Contributed by NM, 2-Aug-2006.) (Revised by Mario Carneiro, 5-Jun-2014.)
⊢ (((𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 1 < 𝐴) → (𝑀 < 𝑁 ↔ (𝐴↑𝑀) < (𝐴↑𝑁)))
Theorem	ltexp2d 16144	Ordering relationship for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 1 < 𝐴)    ⇒   ⊢ (𝜑 → (𝑀 < 𝑁 ↔ (𝐴↑𝑀) < (𝐴↑𝑁)))
11.2.4  Logarithms to an arbitrary base Define "log using an arbitrary base" function and then prove some of its properties. As with df-relog 16053 this is for real logarithms rather than complex logarithms. Metamath doesn't care what letters are used to represent classes. Usually classes begin with the letter "A", but here we use "B" and "X" to more clearly distinguish between "base" and "other parameter of log". There are different ways this could be defined in Metamath. The approach used here is intentionally similar to existing 2-parameter Metamath functions (operations): (𝐵 logb 𝑋) where 𝐵 is the base and 𝑋 is the argument of the logarithm function. An alternative would be to support the notational form (( logb ‘𝐵)‘𝑋); that looks a little more like traditional notation.
Syntax	clogb 16145	Extend class notation to include the logarithm generalized to an arbitrary base.
class logb
Definition	df-logb 16146*	Define the logb operator. This is the logarithm generalized to an arbitrary base. It can be used as (𝐵 logb 𝑋) for "log base B of X". In the most common traditional notation, base B is a subscript of "log". The definition will only be useful where 𝑥 is a positive real apart from one and where 𝑦 is a positive real, so the choice of (ℂ ∖ {0, 1}) and (ℂ ∖ {0}) is somewhat arbitrary (we adopt the definition used in set.mm). (Contributed by David A. Wheeler, 21-Jan-2017.)
⊢ logb = (𝑥 ∈ (ℂ ∖ {0, 1}), 𝑦 ∈ (ℂ ∖ {0}) ↦ ((log‘𝑦) / (log‘𝑥)))
Theorem	rplogbval 16147	Define the value of the logb function, the logarithm generalized to an arbitrary base, when used as infix. Most Metamath statements select variables in order of their use, but to make the order clearer we use "B" for base and "X" for the argument of the logarithm function here. (Contributed by David A. Wheeler, 21-Jan-2017.) (Revised by Jim Kingdon, 3-Jul-2024.)
⊢ ((𝐵 ∈ ℝ+ ∧ 𝐵 # 1 ∧ 𝑋 ∈ ℝ+) → (𝐵 logb 𝑋) = ((log‘𝑋) / (log‘𝐵)))
Theorem	rplogbcl 16148	General logarithm closure. (Contributed by David A. Wheeler, 17-Jul-2017.)
⊢ ((𝐵 ∈ ℝ+ ∧ 𝐵 # 1 ∧ 𝑋 ∈ ℝ+) → (𝐵 logb 𝑋) ∈ ℝ)
Theorem	rplogbid1 16149	General logarithm is 1 when base and arg match. Property 1(a) of [Cohen4] p. 361. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Revised by David A. Wheeler, 22-Jul-2017.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐴 # 1) → (𝐴 logb 𝐴) = 1)
Theorem	rplogb1 16150	The logarithm of 1 to an arbitrary base 𝐵 is 0. Property 1(b) of [Cohen4] p. 361. See log1 16061. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Revised by Thierry Arnoux, 27-Sep-2017.)
⊢ ((𝐵 ∈ ℝ+ ∧ 𝐵 # 1) → (𝐵 logb 1) = 0)
Theorem	rpelogb 16151	The general logarithm of a number to the base being Euler's constant is the natural logarithm of the number. Put another way, using e as the base in logb is the same as log. Definition in [Cohen4] p. 352. (Contributed by David A. Wheeler, 17-Oct-2017.) (Revised by David A. Wheeler and AV, 16-Jun-2020.)
⊢ (𝐴 ∈ ℝ+ → (e logb 𝐴) = (log‘𝐴))
Theorem	rplogbchbase 16152	Change of base for logarithms. Property in [Cohen4] p. 367. (Contributed by AV, 11-Jun-2020.)
⊢ (((𝐴 ∈ ℝ+ ∧ 𝐴 # 1) ∧ (𝐵 ∈ ℝ+ ∧ 𝐵 # 1) ∧ 𝑋 ∈ ℝ+) → (𝐴 logb 𝑋) = ((𝐵 logb 𝑋) / (𝐵 logb 𝐴)))
Theorem	relogbval 16153	Value of the general logarithm with integer base. (Contributed by Thierry Arnoux, 27-Sep-2017.)
⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝑋 ∈ ℝ+) → (𝐵 logb 𝑋) = ((log‘𝑋) / (log‘𝐵)))
Theorem	relogbzcl 16154	Closure of the general logarithm with integer base on positive reals. (Contributed by Thierry Arnoux, 27-Sep-2017.) (Proof shortened by AV, 9-Jun-2020.)
⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝑋 ∈ ℝ+) → (𝐵 logb 𝑋) ∈ ℝ)
Theorem	rplogbreexp 16155	Power law for the general logarithm for real powers: The logarithm of a positive real number to the power of a real number is equal to the product of the exponent and the logarithm of the base of the power. Property 4 of [Cohen4] p. 361. (Contributed by AV, 9-Jun-2020.)
⊢ (((𝐵 ∈ ℝ+ ∧ 𝐵 # 1) ∧ 𝐶 ∈ ℝ+ ∧ 𝐸 ∈ ℝ) → (𝐵 logb (𝐶↑𝑐𝐸)) = (𝐸 · (𝐵 logb 𝐶)))
Theorem	rplogbzexp 16156	Power law for the general logarithm for integer powers: The logarithm of a positive real number to the power of an integer is equal to the product of the exponent and the logarithm of the base of the power. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Revised by AV, 9-Jun-2020.)
⊢ (((𝐵 ∈ ℝ+ ∧ 𝐵 # 1) ∧ 𝐶 ∈ ℝ+ ∧ 𝑁 ∈ ℤ) → (𝐵 logb (𝐶↑𝑁)) = (𝑁 · (𝐵 logb 𝐶)))
Theorem	rprelogbmul 16157	The logarithm of the product of two positive real numbers is the sum of logarithms. Property 2 of [Cohen4] p. 361. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Revised by AV, 29-May-2020.)
⊢ (((𝐵 ∈ ℝ+ ∧ 𝐵 # 1) ∧ (𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+)) → (𝐵 logb (𝐴 · 𝐶)) = ((𝐵 logb 𝐴) + (𝐵 logb 𝐶)))
Theorem	rprelogbmulexp 16158	The logarithm of the product of a positive real and a positive real number to the power of a real number is the sum of the logarithm of the first real number and the scaled logarithm of the second real number. (Contributed by AV, 29-May-2020.)
⊢ (((𝐵 ∈ ℝ+ ∧ 𝐵 # 1) ∧ (𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+ ∧ 𝐸 ∈ ℝ)) → (𝐵 logb (𝐴 · (𝐶↑𝑐𝐸))) = ((𝐵 logb 𝐴) + (𝐸 · (𝐵 logb 𝐶))))
Theorem	rprelogbdiv 16159	The logarithm of the quotient of two positive real numbers is the difference of logarithms. Property 3 of [Cohen4] p. 361. (Contributed by AV, 29-May-2020.)
⊢ (((𝐵 ∈ ℝ+ ∧ 𝐵 # 1) ∧ (𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ+)) → (𝐵 logb (𝐴 / 𝐶)) = ((𝐵 logb 𝐴) − (𝐵 logb 𝐶)))
Theorem	relogbexpap 16160	Identity law for general logarithm: the logarithm of a power to the base is the exponent. Property 6 of [Cohen4] p. 361. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Revised by AV, 9-Jun-2020.)
⊢ ((𝐵 ∈ ℝ+ ∧ 𝐵 # 1 ∧ 𝑀 ∈ ℤ) → (𝐵 logb (𝐵↑𝑀)) = 𝑀)
Theorem	nnlogbexp 16161	Identity law for general logarithm with integer base. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Revised by Thierry Arnoux, 27-Sep-2017.)
⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ) → (𝐵 logb (𝐵↑𝑀)) = 𝑀)
Theorem	logbrec 16162	Logarithm of a reciprocal changes sign. Particular case of Property 3 of [Cohen4] p. 361. (Contributed by Thierry Arnoux, 27-Sep-2017.)
⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝐴 ∈ ℝ+) → (𝐵 logb (1 / 𝐴)) = -(𝐵 logb 𝐴))
Theorem	logbleb 16163	The general logarithm function is monotone/increasing. See logleb 16071. (Contributed by Stefan O'Rear, 19-Oct-2014.) (Revised by AV, 31-May-2020.)
⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ+) → (𝑋 ≤ 𝑌 ↔ (𝐵 logb 𝑋) ≤ (𝐵 logb 𝑌)))
Theorem	logblt 16164	The general logarithm function is strictly monotone/increasing. Property 2 of [Cohen4] p. 377. See logltb 16070. (Contributed by Stefan O'Rear, 19-Oct-2014.) (Revised by Thierry Arnoux, 27-Sep-2017.)
⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ+) → (𝑋 < 𝑌 ↔ (𝐵 logb 𝑋) < (𝐵 logb 𝑌)))
Theorem	rplogbcxp 16165	Identity law for the general logarithm for real numbers. (Contributed by AV, 22-May-2020.)
⊢ ((𝐵 ∈ ℝ+ ∧ 𝐵 # 1 ∧ 𝑋 ∈ ℝ) → (𝐵 logb (𝐵↑𝑐𝑋)) = 𝑋)
Theorem	rpcxplogb 16166	Identity law for the general logarithm. (Contributed by AV, 22-May-2020.)
⊢ ((𝐵 ∈ ℝ+ ∧ 𝐵 # 1 ∧ 𝑋 ∈ ℝ+) → (𝐵↑𝑐(𝐵 logb 𝑋)) = 𝑋)
Theorem	relogbcxpbap 16167	The logarithm is the inverse of the exponentiation. Observation in [Cohen4] p. 348. (Contributed by AV, 11-Jun-2020.)
⊢ (((𝐵 ∈ ℝ+ ∧ 𝐵 # 1) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ) → ((𝐵 logb 𝑋) = 𝑌 ↔ (𝐵↑𝑐𝑌) = 𝑋))
Theorem	logbgt0b 16168	The logarithm of a positive real number to a real base greater than 1 is positive iff the number is greater than 1. (Contributed by AV, 29-Dec-2022.)
⊢ ((𝐴 ∈ ℝ+ ∧ (𝐵 ∈ ℝ+ ∧ 1 < 𝐵)) → (0 < (𝐵 logb 𝐴) ↔ 1 < 𝐴))
Theorem	logbgcd1irr 16169	The logarithm of an integer greater than 1 to an integer base greater than 1 is not rational if the argument and the base are relatively prime. For example, (2 logb 9) ∈ (ℝ ∖ ℚ). (Contributed by AV, 29-Dec-2022.)
⊢ ((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2) ∧ (𝑋 gcd 𝐵) = 1) → (𝐵 logb 𝑋) ∈ (ℝ ∖ ℚ))
Theorem	logbgcd1irraplemexp 16170	Lemma for logbgcd1irrap 16172. Apartness of 𝑋↑𝑁 and 𝐵↑𝑀. (Contributed by Jim Kingdon, 11-Jul-2024.)
⊢ (𝜑 → 𝑋 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → 𝐵 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → (𝑋 gcd 𝐵) = 1)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝑋↑𝑁) # (𝐵↑𝑀))
Theorem	logbgcd1irraplemap 16171	Lemma for logbgcd1irrap 16172. The result, with the rational number expressed as numerator and denominator. (Contributed by Jim Kingdon, 9-Jul-2024.)
⊢ (𝜑 → 𝑋 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → 𝐵 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → (𝑋 gcd 𝐵) = 1)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝐵 logb 𝑋) # (𝑀 / 𝑁))
Theorem	logbgcd1irrap 16172	The logarithm of an integer greater than 1 to an integer base greater than 1 is irrational (in the sense of being apart from any rational number) if the argument and the base are relatively prime. For example, (2 logb 9) # 𝑄 where 𝑄 is rational. (Contributed by AV, 29-Dec-2022.)
⊢ (((𝑋 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) ∧ ((𝑋 gcd 𝐵) = 1 ∧ 𝑄 ∈ ℚ)) → (𝐵 logb 𝑋) # 𝑄)
Theorem	2logb9irr 16173	Example for logbgcd1irr 16169. The logarithm of nine to base two is not rational. Also see 2logb9irrap 16179 which says that it is irrational (in the sense of being apart from any rational number). (Contributed by AV, 29-Dec-2022.)
⊢ (2 logb 9) ∈ (ℝ ∖ ℚ)
Theorem	logbprmirr 16174	The logarithm of a prime to a different prime base is not rational. For example, (2 logb 3) ∈ (ℝ ∖ ℚ) (see 2logb3irr 16175). (Contributed by AV, 31-Dec-2022.)
⊢ ((𝑋 ∈ ℙ ∧ 𝐵 ∈ ℙ ∧ 𝑋 ≠ 𝐵) → (𝐵 logb 𝑋) ∈ (ℝ ∖ ℚ))
Theorem	2logb3irr 16175	Example for logbprmirr 16174. The logarithm of three to base two is not rational. (Contributed by AV, 31-Dec-2022.)
⊢ (2 logb 3) ∈ (ℝ ∖ ℚ)
Theorem	2logb9irrALT 16176	Alternate proof of 2logb9irr 16173: The logarithm of nine to base two is not rational. (Contributed by AV, 31-Dec-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (2 logb 9) ∈ (ℝ ∖ ℚ)
Theorem	sqrt2cxp2logb9e3 16177	The square root of two to the power of the logarithm of nine to base two is three. (√‘2) and (2 logb 9) are not rational (see sqrt2irr0 12962 resp. 2logb9irr 16173), satisfying the statement in 2irrexpq 16178. (Contributed by AV, 29-Dec-2022.)
⊢ ((√‘2)↑𝑐(2 logb 9)) = 3
Theorem	2irrexpq 16178*	There exist real numbers 𝑎 and 𝑏 which are not rational such that (𝑎↑𝑏) is rational. Statement in the Metamath book, section 1.1.5, footnote 27 on page 17, and the "constructive proof" for theorem 1.2 of [Bauer], p. 483. This is a constructive proof because it is based on two explicitly named non-rational numbers (√‘2) and (2 logb 9), see sqrt2irr0 12962, 2logb9irr 16173 and sqrt2cxp2logb9e3 16177. Therefore, this proof is acceptable/usable in intuitionistic logic. For a theorem which is the same but proves that 𝑎 and 𝑏 are irrational (in the sense of being apart from any rational number), see 2irrexpqap 16180. (Contributed by AV, 23-Dec-2022.)
⊢ ∃𝑎 ∈ (ℝ ∖ ℚ)∃𝑏 ∈ (ℝ ∖ ℚ)(𝑎↑𝑐𝑏) ∈ ℚ
Theorem	2logb9irrap 16179	Example for logbgcd1irrap 16172. The logarithm of nine to base two is irrational (in the sense of being apart from any rational number). (Contributed by Jim Kingdon, 12-Jul-2024.)
⊢ (𝑄 ∈ ℚ → (2 logb 9) # 𝑄)
Theorem	2irrexpqap 16180*	There exist real numbers 𝑎 and 𝑏 which are irrational (in the sense of being apart from any rational number) such that (𝑎↑𝑏) is rational. Statement in the Metamath book, section 1.1.5, footnote 27 on page 17, and the "constructive proof" for theorem 1.2 of [Bauer], p. 483. This is a constructive proof because it is based on two explicitly named irrational numbers (√‘2) and (2 logb 9), see sqrt2irrap 12979, 2logb9irrap 16179 and sqrt2cxp2logb9e3 16177. Therefore, this proof is acceptable/usable in intuitionistic logic. (Contributed by Jim Kingdon, 12-Jul-2024.)
⊢ ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ (∀𝑝 ∈ ℚ 𝑎 # 𝑝 ∧ ∀𝑞 ∈ ℚ 𝑏 # 𝑞 ∧ (𝑎↑𝑐𝑏) ∈ ℚ)
Theorem	zprmlogbaplem1 16181	Lemma for zprmlogbap 16184. Rearranging an expression involving logarithms. (Contributed by Jim Kingdon, 20-Aug-2026.)
⊢ (𝜑 → 𝐵 ∈ ℙ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → ¬ 𝐵 ∥ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐵 logb ((𝐵↑𝐴) · 𝑀)) = (𝐴 + (𝐵 logb 𝑀)))
Theorem	zprmlogbaplem2 16182*	Lemma for zprmlogbap 16184. The logarithm is either rational or irrational. (Contributed by Jim Kingdon, 20-Aug-2026.)
⊢ (𝜑 → 𝐵 ∈ ℙ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → ¬ 𝐵 ∥ 𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ ℕ0)    &   ⊢ 𝑋 = ((𝐵↑𝐴) · 𝑀)    ⇒   ⊢ (𝜑 → ((𝐵 logb 𝑋) ∈ ℚ ∨ ((𝐵 logb 𝑋) ∈ ℝ ∧ ∀𝑞 ∈ ℚ (𝐵 logb 𝑋) # 𝑞)))
Theorem	zprmlogbaplem3 16183*	Lemma for zprmlogbap 16184. Decomposing a natural number into a power of a prime base and a factor not divisible by that prime. (Contributed by Jim Kingdon, 20-Aug-2026.)
⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 𝐵 ∥ 𝑧}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((𝐵↑𝑦) · 𝑥))    ⇒   ⊢ ((𝑋 ∈ ℕ ∧ 𝐵 ∈ ℙ) → ∃𝑚 ∈ ℕ ∃𝑎 ∈ ℕ0 (¬ 𝐵 ∥ 𝑚 ∧ 𝑋 = ((𝐵↑𝑎) · 𝑚)))
Theorem	zprmlogbap 16184*	The logarithm of a natural number to a prime base is either rational or irrational. The proof decomposes 𝑋 into 𝑚 ∈ ℕ and 𝑎 ∈ ℕ0 such that 𝑋 = ((𝐵↑𝑎) · 𝑚) (using nnmaxpw 12972). If 𝑚 = 1 the logarithm is 𝑎, which is rational. If 1 < 𝑚 then we can apply logbgcd1irrap 16172 to show that the logarithm is irrational. (Contributed by Jim Kingdon and Taylor Barrella, 20-Aug-2026.)
⊢ ((𝑋 ∈ ℕ ∧ 𝐵 ∈ ℙ) → ((𝐵 logb 𝑋) ∈ ℚ ∨ ((𝐵 logb 𝑋) ∈ ℝ ∧ ∀𝑞 ∈ ℚ (𝐵 logb 𝑋) # 𝑞)))
11.2.5  Quartic binomial expansion
Theorem	binom4 16185	Work out a quartic binomial. (You would think that by this point it would be faster to use binom 12270, but it turns out to be just as much work to put it into this form after clearing all the sums and calculating binomial coefficients.) (Contributed by Mario Carneiro, 6-May-2015.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵)↑4) = (((𝐴↑4) + (4 · ((𝐴↑3) · 𝐵))) + ((6 · ((𝐴↑2) · (𝐵↑2))) + ((4 · (𝐴 · (𝐵↑3))) + (𝐵↑4)))))
11.2.6  Logarithms (cont.)
Theorem	log2tlbndlog2 16186*	Bound the error term in the series of the hypothesis. The presence of the hypothesis here is a temporary measure until it can be proved as log2cnv . (Contributed by Mario Carneiro, 7-Apr-2015.)
⊢ seq0( + , (𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))) ⇝ (log‘2)    ⇒   ⊢ (𝑁 ∈ ℕ0 → ((log‘2) − Σ𝑛 ∈ (0...(𝑁 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ∈ (0[,](3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁)))))
11.2.7  The Birthday Problem
Theorem	log2ublem1 16187	Lemma for log2ublog2 16190. The proof of log2ublog2 16190, which is simply the evaluation of log2tlbndlog2 16186 for 𝑁 = 4, takes the form of the addition of five fractions and showing this is less than another fraction. We could just perform exact arithmetic on these fractions, get a large rational number, and just multiply everything to verify the claim, but as anyone who uses decimal numbers for this task knows, it is often better to pick a common denominator 𝑑 (usually a large power of 10) and work with the closest approximations of the form 𝑛 / 𝑑 for some integer 𝑛 instead. It turns out that for our purposes it is sufficient to take 𝑑 = (3↑7) · 5 · 7, which is also nice because it shares many factors in common with the fractions in question. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ (((3↑7) · (5 · 7)) · 𝐴) ≤ 𝐵    &   ⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝐸 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐹 ∈ ℕ0    &   ⊢ 𝐶 = (𝐴 + (𝐷 / 𝐸))    &   ⊢ (𝐵 + 𝐹) = 𝐺    &   ⊢ (((3↑7) · (5 · 7)) · 𝐷) ≤ (𝐸 · 𝐹)    ⇒   ⊢ (((3↑7) · (5 · 7)) · 𝐶) ≤ 𝐺
Theorem	log2ublem2 16188*	Lemma for log2ublog2 16190. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...𝐾)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ (2 · 𝐵)    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐹 ∈ ℕ0    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ (𝑁 − 1) = 𝐾    &   ⊢ (𝐵 + 𝐹) = 𝐺    &   ⊢ 𝑀 ∈ ℕ0    &   ⊢ (𝑀 + 𝑁) = 3    &   ⊢ ((5 · 7) · (9↑𝑀)) = (((2 · 𝑁) + 1) · 𝐹)    ⇒   ⊢ (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ (2 · 𝐺)
Theorem	log2ublem3 16189	Lemma for log2ublog2 16190. In decimal, this is a proof that the first four terms of the series for log2 is less than 53056 / 76545. (Contributed by Mario Carneiro, 17-Apr-2015.) (Proof shortened by AV, 15-Sep-2021.)
⊢ (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ ;;;;53056
Theorem	log2ublog2 16190	log2 is less than 253 / 365. If written in decimal, this is because log2 = 0.693147... is less than 253/365 = 0.693151... , so this is a very tight bound, at five decimal places. The presence of the hypothesis here is a temporary measure until it can be proved as log2cnv . (Contributed by Mario Carneiro, 7-Apr-2015.) (Proof shortened by AV, 16-Sep-2021.)
⊢ seq0( + , (𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))) ⇝ (log‘2)    ⇒   ⊢ (log‘2) < (;;253 / ;;365)
Theorem	birthdaylem1g 16191*	Lemma for birthdaylog2 16194. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ 𝑆 = {𝑓 ∣ 𝑓:(1...𝐾)⟶(1...𝑁)}    &   ⊢ 𝑇 = {𝑓 ∣ 𝑓:(1...𝐾)–1-1→(1...𝑁)}    ⇒   ⊢ ((𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ) → (𝑇 ⊆ 𝑆 ∧ 𝑆 ∈ Fin ∧ 𝑆 ≠ ∅))
Theorem	birthdaylem2 16192*	For general 𝑁 and 𝐾, count the fraction of injective functions from 1...𝐾 to 1...𝑁. (Contributed by Mario Carneiro, 7-May-2015.)
⊢ 𝑆 = {𝑓 ∣ 𝑓:(1...𝐾)⟶(1...𝑁)}    &   ⊢ 𝑇 = {𝑓 ∣ 𝑓:(1...𝐾)–1-1→(1...𝑁)}    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁)) → ((♯‘𝑇) / (♯‘𝑆)) = (exp‘Σ𝑘 ∈ (0...(𝐾 − 1))(log‘(1 − (𝑘 / 𝑁)))))
Theorem	birthdaylem3 16193*	For general 𝑁 and 𝐾, upper-bound the fraction of injective functions from 1...𝐾 to 1...𝑁. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ 𝑆 = {𝑓 ∣ 𝑓:(1...𝐾)⟶(1...𝑁)}    &   ⊢ 𝑇 = {𝑓 ∣ 𝑓:(1...𝐾)–1-1→(1...𝑁)}    ⇒   ⊢ ((𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ) → ((♯‘𝑇) / (♯‘𝑆)) ≤ (exp‘-((((𝐾↑2) − 𝐾) / 2) / 𝑁)))
Theorem	birthdaylog2 16194*	The Birthday Problem. There is a more than even chance that out of 23 people in a room, at least two of them have the same birthday. Mathematically, this is asserting that for 𝐾 = 23 and 𝑁 = 365, fewer than half of the set of all functions from 1...𝐾 to 1...𝑁 are injective. The presence of the hypothesis giving a series which converges to (log‘2) is a temporary measure until it can be proved as log2cnv . Although this is Metamath 100 proof #93, we cannot consider it proved until we prove the missing log2cnv piece (or prove the theorem another way which does not require it). (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ 𝑆 = {𝑓 ∣ 𝑓:(1...𝐾)⟶(1...𝑁)}    &   ⊢ 𝑇 = {𝑓 ∣ 𝑓:(1...𝐾)–1-1→(1...𝑁)}    &   ⊢ 𝐾 = ;23    &   ⊢ 𝑁 = ;;365    &   ⊢ seq0( + , (𝑘 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))) ⇝ (log‘2)    ⇒   ⊢ ((♯‘𝑇) / (♯‘𝑆)) < (1 / 2)
11.3  Pell equations
11.3.1  Pell equations 1: A nontrivial solution always exists
Theorem	pellexlem1 16195	Lemma for pellex . Arithmetical core of pellexlem3, norm lower bound. This begins Dirichlet's proof of the Pell equation solution existence; the proof here follows theorem 62 of [vandenDries] p. 43. (Contributed by Stefan O'Rear, 14-Sep-2014.)
⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ ¬ (√‘𝐷) ∈ ℚ) → ((𝐴↑2) − (𝐷 · (𝐵↑2))) ≠ 0)
Theorem	pellexlem2 16196	Lemma for pellex . Arithmetical core of pellexlem3, norm upper bound. (Contributed by Stefan O'Rear, 14-Sep-2014.)
⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))) < (1 + (2 · (√‘𝐷))))
Theorem	pellexlem3 16197*	Lemma for pellex . To each good rational approximation of (√‘𝐷), there exists a near-solution. (Contributed by Stefan O'Rear, 14-Sep-2014.)
⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → {𝑥 ∈ ℚ ∣ (0 < 𝑥 ∧ (abs‘(𝑥 − (√‘𝐷))) < ((denom‘𝑥)↑-2))} ≼ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))})
11.4  Basic number theory
11.4.1  Wilson's theorem
Theorem	wilthlem1 16198	The only elements that are equal to their own inverses in the multiplicative group of nonzero elements in ℤ / 𝑃ℤ are 1 and -1≡𝑃 − 1. (Note that from prmdiveq 13037, (𝑁↑(𝑃 − 2)) mod 𝑃 is the modular inverse of 𝑁 in ℤ / 𝑃ℤ. (Contributed by Mario Carneiro, 24-Jan-2015.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑁 = ((𝑁↑(𝑃 − 2)) mod 𝑃) ↔ (𝑁 = 1 ∨ 𝑁 = (𝑃 − 1))))
11.4.2  Number-theoretical functions
Syntax	ccht 16199	Extend class notation with the first Chebyshev function.
class θ
Syntax	cppi 16200	Extend class notation with the prime-counting function pi.
class π