P. 271 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 27001-27100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sqrtlim 27001	The inverse square root function converges to zero. (Contributed by Mario Carneiro, 18-May-2016.)
⊢ (𝑛 ∈ ℝ+ ↦ (1 / (√‘𝑛))) ⇝𝑟 0
Theorem	rlimcxp 27002*	Any power to a positive exponent of a converging sequence also converges. (Contributed by Mario Carneiro, 18-Sep-2014.)
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑛 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 0)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝑛 ∈ 𝐴 ↦ (𝐵↑𝑐𝐶)) ⇝𝑟 0)
Theorem	o1cxp 27003*	An eventually bounded function taken to a nonnegative power is eventually bounded. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 0 ≤ (ℜ‘𝐶))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝑂(1))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵↑𝑐𝐶)) ∈ 𝑂(1))
Theorem	cxp2limlem 27004*	A linear factor grows slower than any exponential with base greater than 1. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 1 < 𝐴) → (𝑛 ∈ ℝ+ ↦ (𝑛 / (𝐴↑𝑐𝑛))) ⇝𝑟 0)
Theorem	cxp2lim 27005*	Any power grows slower than any exponential with base greater than 1. (Contributed by Mario Carneiro, 18-Sep-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → (𝑛 ∈ ℝ+ ↦ ((𝑛↑𝑐𝐴) / (𝐵↑𝑐𝑛))) ⇝𝑟 0)
Theorem	cxploglim 27006*	The logarithm grows slower than any positive power. (Contributed by Mario Carneiro, 18-Sep-2014.)
⊢ (𝐴 ∈ ℝ+ → (𝑛 ∈ ℝ+ ↦ ((log‘𝑛) / (𝑛↑𝑐𝐴))) ⇝𝑟 0)
Theorem	cxploglim2 27007*	Every power of the logarithm grows slower than any positive power. (Contributed by Mario Carneiro, 20-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+) → (𝑛 ∈ ℝ+ ↦ (((log‘𝑛)↑𝑐𝐴) / (𝑛↑𝑐𝐵))) ⇝𝑟 0)
Theorem	divsqrtsumlem 27008*	Lemma for divsqrsum 27010 and divsqrtsum2 27011. (Contributed by Mario Carneiro, 18-May-2016.)
⊢ 𝐹 = (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑛)) − (2 · (√‘𝑥))))    ⇒   ⊢ (𝐹:ℝ+⟶ℝ ∧ 𝐹 ∈ dom ⇝𝑟 ∧ ((𝐹 ⇝𝑟 𝐿 ∧ 𝐴 ∈ ℝ+) → (abs‘((𝐹‘𝐴) − 𝐿)) ≤ (1 / (√‘𝐴))))
Theorem	divsqrsumf 27009*	The function 𝐹 used in divsqrsum 27010 is a real function. (Contributed by Mario Carneiro, 12-May-2016.)
⊢ 𝐹 = (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑛)) − (2 · (√‘𝑥))))    ⇒   ⊢ 𝐹:ℝ+⟶ℝ
Theorem	divsqrsum 27010*	The sum Σ𝑛 ≤ 𝑥(1 / √𝑛) is asymptotic to 2√𝑥 + 𝐿 with a finite limit 𝐿. (In fact, this limit is ζ(1 / 2) ≈ -1.46....) (Contributed by Mario Carneiro, 9-May-2016.)
⊢ 𝐹 = (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑛)) − (2 · (√‘𝑥))))    ⇒   ⊢ 𝐹 ∈ dom ⇝𝑟
Theorem	divsqrtsum2 27011*	A bound on the distance of the sum Σ𝑛 ≤ 𝑥(1 / √𝑛) from its asymptotic value 2√𝑥 + 𝐿. (Contributed by Mario Carneiro, 18-May-2016.)
⊢ 𝐹 = (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑛)) − (2 · (√‘𝑥))))    &   ⊢ (𝜑 → 𝐹 ⇝𝑟 𝐿)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ ℝ+) → (abs‘((𝐹‘𝐴) − 𝐿)) ≤ (1 / (√‘𝐴)))
Theorem	divsqrtsumo1 27012*	The sum Σ𝑛 ≤ 𝑥(1 / √𝑛) has the asymptotic expansion 2√𝑥 + 𝐿 + 𝑂(1 / √𝑥), for some 𝐿. (Contributed by Mario Carneiro, 10-May-2016.)
⊢ 𝐹 = (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑛)) − (2 · (√‘𝑥))))    &   ⊢ (𝜑 → 𝐹 ⇝𝑟 𝐿)    ⇒   ⊢ (𝜑 → (𝑦 ∈ ℝ+ ↦ (((𝐹‘𝑦) − 𝐿) · (√‘𝑦))) ∈ 𝑂(1))
14.3.12  Inequality of arithmetic and geometric means
Theorem	cvxcl 27013*	Closure of a 0-1 linear combination in a convex set. (Contributed by Mario Carneiro, 21-Jun-2015.)
⊢ (𝜑 → 𝐷 ⊆ ℝ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) → (𝑥[,]𝑦) ⊆ 𝐷)    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)) ∈ 𝐷)
Theorem	scvxcvx 27014*	A strictly convex function is convex. (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ (𝜑 → 𝐷 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹:𝐷⟶ℝ)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐷 ∧ 𝑏 ∈ 𝐷)) → (𝑎[,]𝑏) ⊆ 𝐷)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))))    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) ≤ ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))
Theorem	jensenlem1 27015*	Lemma for jensen 27017. (Contributed by Mario Carneiro, 4-Jun-2016.)
⊢ (𝜑 → 𝐷 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹:𝐷⟶ℝ)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐷 ∧ 𝑏 ∈ 𝐷)) → (𝑎[,]𝑏) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝑇:𝐴⟶(0[,)+∞))    &   ⊢ (𝜑 → 𝑋:𝐴⟶𝐷)    &   ⊢ (𝜑 → 0 < (ℂfld Σg 𝑇))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑡 ∈ (0[,]1))) → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ≤ ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))))    &   ⊢ (𝜑 → ¬ 𝑧 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐵 ∪ {𝑧}) ⊆ 𝐴)    &   ⊢ 𝑆 = (ℂfld Σg (𝑇 ↾ 𝐵))    &   ⊢ 𝐿 = (ℂfld Σg (𝑇 ↾ (𝐵 ∪ {𝑧})))    ⇒   ⊢ (𝜑 → 𝐿 = (𝑆 + (𝑇‘𝑧)))
Theorem	jensenlem2 27016*	Lemma for jensen 27017. (Contributed by Mario Carneiro, 21-Jun-2015.)
⊢ (𝜑 → 𝐷 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹:𝐷⟶ℝ)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐷 ∧ 𝑏 ∈ 𝐷)) → (𝑎[,]𝑏) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝑇:𝐴⟶(0[,)+∞))    &   ⊢ (𝜑 → 𝑋:𝐴⟶𝐷)    &   ⊢ (𝜑 → 0 < (ℂfld Σg 𝑇))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑡 ∈ (0[,]1))) → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ≤ ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))))    &   ⊢ (𝜑 → ¬ 𝑧 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐵 ∪ {𝑧}) ⊆ 𝐴)    &   ⊢ 𝑆 = (ℂfld Σg (𝑇 ↾ 𝐵))    &   ⊢ 𝐿 = (ℂfld Σg (𝑇 ↾ (𝐵 ∪ {𝑧})))    &   ⊢ (𝜑 → 𝑆 ∈ ℝ+)    &   ⊢ (𝜑 → ((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆) ∈ 𝐷)    &   ⊢ (𝜑 → (𝐹‘((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ 𝐵)) / 𝑆)) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ 𝐵)) / 𝑆))    ⇒   ⊢ (𝜑 → (((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝐵 ∪ {𝑧}))) / 𝐿) ∈ 𝐷 ∧ (𝐹‘((ℂfld Σg ((𝑇 ∘f · 𝑋) ↾ (𝐵 ∪ {𝑧}))) / 𝐿)) ≤ ((ℂfld Σg ((𝑇 ∘f · (𝐹 ∘ 𝑋)) ↾ (𝐵 ∪ {𝑧}))) / 𝐿)))
Theorem	jensen 27017*	Jensen's inequality, a finite extension of the definition of convexity (the last hypothesis). (Contributed by Mario Carneiro, 21-Jun-2015.) (Proof shortened by AV, 27-Jul-2019.)
⊢ (𝜑 → 𝐷 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹:𝐷⟶ℝ)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐷 ∧ 𝑏 ∈ 𝐷)) → (𝑎[,]𝑏) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝑇:𝐴⟶(0[,)+∞))    &   ⊢ (𝜑 → 𝑋:𝐴⟶𝐷)    &   ⊢ (𝜑 → 0 < (ℂfld Σg 𝑇))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑡 ∈ (0[,]1))) → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ≤ ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))))    ⇒   ⊢ (𝜑 → (((ℂfld Σg (𝑇 ∘f · 𝑋)) / (ℂfld Σg 𝑇)) ∈ 𝐷 ∧ (𝐹‘((ℂfld Σg (𝑇 ∘f · 𝑋)) / (ℂfld Σg 𝑇))) ≤ ((ℂfld Σg (𝑇 ∘f · (𝐹 ∘ 𝑋))) / (ℂfld Σg 𝑇))))
Theorem	amgmlem 27018	Lemma for amgm 27019. (Contributed by Mario Carneiro, 21-Jun-2015.)
⊢ 𝑀 = (mulGrp‘ℂfld)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ+)    ⇒   ⊢ (𝜑 → ((𝑀 Σg 𝐹)↑𝑐(1 / (♯‘𝐴))) ≤ ((ℂfld Σg 𝐹) / (♯‘𝐴)))
Theorem	amgm 27019	Inequality of arithmetic and geometric means. Here (𝑀 Σg 𝐹) calculates the group sum within the multiplicative monoid of the complex numbers (or in other words, it multiplies the elements 𝐹(𝑥), 𝑥 ∈ 𝐴 together), and (ℂfld Σg 𝐹) calculates the group sum in the additive group (i.e. the sum of the elements). This is Metamath 100 proof #38. (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ 𝑀 = (mulGrp‘ℂfld)    ⇒   ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(0[,)+∞)) → ((𝑀 Σg 𝐹)↑𝑐(1 / (♯‘𝐴))) ≤ ((ℂfld Σg 𝐹) / (♯‘𝐴)))
14.3.13  Euler-Mascheroni constant
Syntax	cem 27020	The Euler-Mascheroni constant. (The label abbreviates Euler-Mascheroni.)
class γ
Definition	df-em 27021	Define the Euler-Mascheroni constant, γ = 0.57721.... This is the limit of the series Σ𝑘 ∈ (1...𝑚)(1 / 𝑘) − (log‘𝑚), with a proof that the limit exists in emcl 27031. (Contributed by Mario Carneiro, 11-Jul-2014.)
⊢ γ = Σ𝑘 ∈ ℕ ((1 / 𝑘) − (log‘(1 + (1 / 𝑘))))
Theorem	logdifbnd 27022	Bound on the difference of logs. (Contributed by Mario Carneiro, 23-May-2016.)
⊢ (𝐴 ∈ ℝ+ → ((log‘(𝐴 + 1)) − (log‘𝐴)) ≤ (1 / 𝐴))
Theorem	logdiflbnd 27023	Lower bound on the difference of logs. (Contributed by Mario Carneiro, 3-Jul-2017.)
⊢ (𝐴 ∈ ℝ+ → (1 / (𝐴 + 1)) ≤ ((log‘(𝐴 + 1)) − (log‘𝐴)))
Theorem	emcllem1 27024*	Lemma for emcl 27031. The series 𝐹 and 𝐺 are sequences of real numbers that approach γ from above and below, respectively. (Contributed by Mario Carneiro, 11-Jul-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘𝑛)))    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘(𝑛 + 1))))    ⇒   ⊢ (𝐹:ℕ⟶ℝ ∧ 𝐺:ℕ⟶ℝ)
Theorem	emcllem2 27025*	Lemma for emcl 27031. 𝐹 is increasing, and 𝐺 is decreasing. (Contributed by Mario Carneiro, 11-Jul-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘𝑛)))    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘(𝑛 + 1))))    ⇒   ⊢ (𝑁 ∈ ℕ → ((𝐹‘(𝑁 + 1)) ≤ (𝐹‘𝑁) ∧ (𝐺‘𝑁) ≤ (𝐺‘(𝑁 + 1))))
Theorem	emcllem3 27026*	Lemma for emcl 27031. The function 𝐻 is the difference between 𝐹 and 𝐺. (Contributed by Mario Carneiro, 11-Jul-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘𝑛)))    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘(𝑛 + 1))))    &   ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ (log‘(1 + (1 / 𝑛))))    ⇒   ⊢ (𝑁 ∈ ℕ → (𝐻‘𝑁) = ((𝐹‘𝑁) − (𝐺‘𝑁)))
Theorem	emcllem4 27027*	Lemma for emcl 27031. The difference between series 𝐹 and 𝐺 tends to zero. (Contributed by Mario Carneiro, 11-Jul-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘𝑛)))    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘(𝑛 + 1))))    &   ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ (log‘(1 + (1 / 𝑛))))    ⇒   ⊢ 𝐻 ⇝ 0
Theorem	emcllem5 27028*	Lemma for emcl 27031. The partial sums of the series 𝑇, which is used in Definition df-em 27021, is in fact the same as 𝐺. (Contributed by Mario Carneiro, 11-Jul-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘𝑛)))    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘(𝑛 + 1))))    &   ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ (log‘(1 + (1 / 𝑛))))    &   ⊢ 𝑇 = (𝑛 ∈ ℕ ↦ ((1 / 𝑛) − (log‘(1 + (1 / 𝑛)))))    ⇒   ⊢ 𝐺 = seq1( + , 𝑇)
Theorem	emcllem6 27029*	Lemma for emcl 27031. By the previous lemmas, 𝐹 and 𝐺 must approach a common limit, which is γ by definition. (Contributed by Mario Carneiro, 11-Jul-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘𝑛)))    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘(𝑛 + 1))))    &   ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ (log‘(1 + (1 / 𝑛))))    &   ⊢ 𝑇 = (𝑛 ∈ ℕ ↦ ((1 / 𝑛) − (log‘(1 + (1 / 𝑛)))))    ⇒   ⊢ (𝐹 ⇝ γ ∧ 𝐺 ⇝ γ)
Theorem	emcllem7 27030*	Lemma for emcl 27031 and harmonicbnd 27032. Derive bounds on γ as 𝐹(1) and 𝐺(1). (Contributed by Mario Carneiro, 11-Jul-2014.) (Revised by Mario Carneiro, 9-Apr-2016.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘𝑛)))    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘(𝑛 + 1))))    &   ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ (log‘(1 + (1 / 𝑛))))    &   ⊢ 𝑇 = (𝑛 ∈ ℕ ↦ ((1 / 𝑛) − (log‘(1 + (1 / 𝑛)))))    ⇒   ⊢ (γ ∈ ((1 − (log‘2))[,]1) ∧ 𝐹:ℕ⟶(γ[,]1) ∧ 𝐺:ℕ⟶((1 − (log‘2))[,]γ))
Theorem	emcl 27031	Closure and bounds for the Euler-Mascheroni constant. (Contributed by Mario Carneiro, 11-Jul-2014.)
⊢ γ ∈ ((1 − (log‘2))[,]1)
Theorem	harmonicbnd 27032*	A bound on the harmonic series, as compared to the natural logarithm. (Contributed by Mario Carneiro, 9-Apr-2016.)
⊢ (𝑁 ∈ ℕ → (Σ𝑚 ∈ (1...𝑁)(1 / 𝑚) − (log‘𝑁)) ∈ (γ[,]1))
Theorem	harmonicbnd2 27033*	A bound on the harmonic series, as compared to the natural logarithm. (Contributed by Mario Carneiro, 13-Apr-2016.)
⊢ (𝑁 ∈ ℕ → (Σ𝑚 ∈ (1...𝑁)(1 / 𝑚) − (log‘(𝑁 + 1))) ∈ ((1 − (log‘2))[,]γ))
Theorem	emre 27034	The Euler-Mascheroni constant is a real number. (Contributed by Mario Carneiro, 11-Jul-2014.)
⊢ γ ∈ ℝ
Theorem	emgt0 27035	The Euler-Mascheroni constant is positive. (Contributed by Mario Carneiro, 11-Jul-2014.)
⊢ 0 < γ
Theorem	harmonicbnd3 27036*	A bound on the harmonic series, as compared to the natural logarithm. (Contributed by Mario Carneiro, 13-Apr-2016.)
⊢ (𝑁 ∈ ℕ0 → (Σ𝑚 ∈ (1...𝑁)(1 / 𝑚) − (log‘(𝑁 + 1))) ∈ (0[,]γ))
Theorem	harmoniclbnd 27037*	A bound on the harmonic series, as compared to the natural logarithm. (Contributed by Mario Carneiro, 13-Apr-2016.)
⊢ (𝐴 ∈ ℝ+ → (log‘𝐴) ≤ Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚))
Theorem	harmonicubnd 27038*	A bound on the harmonic series, as compared to the natural logarithm. (Contributed by Mario Carneiro, 13-Apr-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) ≤ ((log‘𝐴) + 1))
Theorem	harmonicbnd4 27039*	The asymptotic behavior of Σ𝑚 ≤ 𝐴, 1 / 𝑚 = log𝐴 + γ + 𝑂(1 / 𝐴). (Contributed by Mario Carneiro, 14-May-2016.)
⊢ (𝐴 ∈ ℝ+ → (abs‘(Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − ((log‘𝐴) + γ))) ≤ (1 / 𝐴))
Theorem	fsumharmonic 27040*	Bound a finite sum based on the harmonic series, where the "strong" bound 𝐶 only applies asymptotically, and there is a "weak" bound 𝑅 for the remaining values. (Contributed by Mario Carneiro, 18-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → (𝑇 ∈ ℝ ∧ 1 ≤ 𝑇))    &   ⊢ (𝜑 → (𝑅 ∈ ℝ ∧ 0 ≤ 𝑅))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 𝐵 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 𝐶 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 0 ≤ 𝐶)    &   ⊢ (((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) ∧ 𝑇 ≤ (𝐴 / 𝑛)) → (abs‘𝐵) ≤ (𝐶 · 𝑛))    &   ⊢ (((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) ∧ (𝐴 / 𝑛) < 𝑇) → (abs‘𝐵) ≤ 𝑅)    ⇒   ⊢ (𝜑 → (abs‘Σ𝑛 ∈ (1...(⌊‘𝐴))(𝐵 / 𝑛)) ≤ (Σ𝑛 ∈ (1...(⌊‘𝐴))𝐶 + (𝑅 · ((log‘𝑇) + 1))))
14.3.14  Zeta function
Syntax	czeta 27041	The Riemann zeta function.
class ζ
Definition	df-zeta 27042*	Define the Riemann zeta function. This definition uses a series expansion of the alternating zeta function ~? zetaalt that is convergent everywhere except 1, but going from the alternating zeta function to the regular zeta function requires dividing by 1 − 2↑(1 − 𝑠), which has zeroes other than 1. To extract the correct value of the zeta function at these points, we extend the divided alternating zeta function by continuity. (Contributed by Mario Carneiro, 18-Jul-2014.)
⊢ ζ = (℩𝑓 ∈ ((ℂ ∖ {1})–cn→ℂ)∀𝑠 ∈ (ℂ ∖ {1})((1 − (2↑𝑐(1 − 𝑠))) · (𝑓‘𝑠)) = Σ𝑛 ∈ ℕ0 (Σ𝑘 ∈ (0...𝑛)(((-1↑𝑘) · (𝑛C𝑘)) · ((𝑘 + 1)↑𝑐𝑠)) / (2↑(𝑛 + 1))))
Theorem	zetacvg 27043*	The zeta series is convergent. (Contributed by Mario Carneiro, 18-Jul-2014.)
⊢ (𝜑 → 𝑆 ∈ ℂ)    &   ⊢ (𝜑 → 1 < (ℜ‘𝑆))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) = (𝑘↑𝑐-𝑆))    ⇒   ⊢ (𝜑 → seq1( + , 𝐹) ∈ dom ⇝ )
14.3.15  Gamma function
Syntax	clgam 27044	Logarithm of the Gamma function.
class log Γ
Syntax	cgam 27045	The Gamma function.
class Γ
Syntax	cigam 27046	The inverse Gamma function.
class 1/Γ
Definition	df-lgam 27047*	Define the log-Gamma function. We can work with this form of the gamma function a bit easier than the equivalent expression for the gamma function itself, and moreover this function is not actually equal to log(Γ(𝑥)) because the branch cuts are placed differently (we do have exp(log Γ(𝑥)) = Γ(𝑥), though). This definition is attributed to Euler, and unlike the usual integral definition is defined on the entire complex plane except the nonpositive integers ℤ ∖ ℕ, where the function has simple poles. (Contributed by Mario Carneiro, 12-Jul-2014.)
⊢ log Γ = (𝑧 ∈ (ℂ ∖ (ℤ ∖ ℕ)) ↦ (Σ𝑚 ∈ ℕ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))) − (log‘𝑧)))
Definition	df-gam 27048	Define the Gamma function. See df-lgam 27047 for more information about the reason for this definition in terms of the log-gamma function. (Contributed by Mario Carneiro, 12-Jul-2014.)
⊢ Γ = (exp ∘ log Γ)
Definition	df-igam 27049	Define the inverse Gamma function, which is defined everywhere, unlike the Gamma function itself. (Contributed by Mario Carneiro, 16-Jul-2017.)
⊢ 1/Γ = (𝑥 ∈ ℂ ↦ if(𝑥 ∈ (ℤ ∖ ℕ), 0, (1 / (Γ‘𝑥))))
Theorem	eldmgm 27050	Elementhood in the set of non-nonpositive integers. (Contributed by Mario Carneiro, 12-Jul-2014.)
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) ↔ (𝐴 ∈ ℂ ∧ ¬ -𝐴 ∈ ℕ0))
Theorem	dmgmaddn0 27051	If 𝐴 is not a nonpositive integer, then 𝐴 + 𝑁 is nonzero for any nonnegative integer 𝑁. (Contributed by Mario Carneiro, 12-Jul-2014.)
⊢ ((𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) ∧ 𝑁 ∈ ℕ0) → (𝐴 + 𝑁) ≠ 0)
Theorem	dmlogdmgm 27052	If 𝐴 is in the continuous domain of the logarithm, then it is in the domain of the Gamma function. (Contributed by Mario Carneiro, 8-Jul-2017.)
⊢ (𝐴 ∈ (ℂ ∖ (-∞(,]0)) → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
Theorem	rpdmgm 27053	A positive real number is in the domain of the Gamma function. (Contributed by Mario Carneiro, 9-Jul-2017.)
⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
Theorem	dmgmn0 27054	If 𝐴 is not a nonpositive integer, then 𝐴 is nonzero. (Contributed by Mario Carneiro, 3-Jul-2017.)
⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))    ⇒   ⊢ (𝜑 → 𝐴 ≠ 0)
Theorem	dmgmaddnn0 27055	If 𝐴 is not a nonpositive integer and 𝑁 is a nonnegative integer, then 𝐴 + 𝑁 is also not a nonpositive integer. (Contributed by Mario Carneiro, 6-Jul-2017.)
⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐴 + 𝑁) ∈ (ℂ ∖ (ℤ ∖ ℕ)))
Theorem	dmgmdivn0 27056	Lemma for lgamf 27070. (Contributed by Mario Carneiro, 3-Jul-2017.)
⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝑀) + 1) ≠ 0)
Theorem	lgamgulmlem1 27057*	Lemma for lgamgulm 27063. (Contributed by Mario Carneiro, 3-Jul-2017.)
⊢ (𝜑 → 𝑅 ∈ ℕ)    &   ⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)))}    ⇒   ⊢ (𝜑 → 𝑈 ⊆ (ℂ ∖ (ℤ ∖ ℕ)))
Theorem	lgamgulmlem2 27058*	Lemma for lgamgulm 27063. (Contributed by Mario Carneiro, 3-Jul-2017.)
⊢ (𝜑 → 𝑅 ∈ ℕ)    &   ⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)))}    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → (2 · 𝑅) ≤ 𝑁)    ⇒   ⊢ (𝜑 → (abs‘((𝐴 / 𝑁) − (log‘((𝐴 / 𝑁) + 1)))) ≤ (𝑅 · ((1 / (𝑁 − 𝑅)) − (1 / 𝑁))))
Theorem	lgamgulmlem3 27059*	Lemma for lgamgulm 27063. (Contributed by Mario Carneiro, 3-Jul-2017.)
⊢ (𝜑 → 𝑅 ∈ ℕ)    &   ⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)))}    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ (𝜑 → (2 · 𝑅) ≤ 𝑁)    ⇒   ⊢ (𝜑 → (abs‘((𝐴 · (log‘((𝑁 + 1) / 𝑁))) − (log‘((𝐴 / 𝑁) + 1)))) ≤ (𝑅 · ((2 · (𝑅 + 1)) / (𝑁↑2))))
Theorem	lgamgulmlem4 27060*	Lemma for lgamgulm 27063. (Contributed by Mario Carneiro, 3-Jul-2017.)
⊢ (𝜑 → 𝑅 ∈ ℕ)    &   ⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)))}    &   ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))    &   ⊢ 𝑇 = (𝑚 ∈ ℕ ↦ if((2 · 𝑅) ≤ 𝑚, (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))), ((𝑅 · (log‘((𝑚 + 1) / 𝑚))) + ((log‘((𝑅 + 1) · 𝑚)) + π))))    ⇒   ⊢ (𝜑 → seq1( + , 𝑇) ∈ dom ⇝ )
Theorem	lgamgulmlem5 27061*	Lemma for lgamgulm 27063. (Contributed by Mario Carneiro, 3-Jul-2017.)
⊢ (𝜑 → 𝑅 ∈ ℕ)    &   ⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)))}    &   ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))    &   ⊢ 𝑇 = (𝑚 ∈ ℕ ↦ if((2 · 𝑅) ≤ 𝑚, (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))), ((𝑅 · (log‘((𝑚 + 1) / 𝑚))) + ((log‘((𝑅 + 1) · 𝑚)) + π))))    ⇒   ⊢ ((𝜑 ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑈)) → (abs‘((𝐺‘𝑛)‘𝑦)) ≤ (𝑇‘𝑛))
Theorem	lgamgulmlem6 27062*	The series 𝐺 is uniformly convergent on the compact region 𝑈, which describes a circle of radius 𝑅 with holes of size 1 / 𝑅 around the poles of the gamma function. (Contributed by Mario Carneiro, 9-Jul-2017.)
⊢ (𝜑 → 𝑅 ∈ ℕ)    &   ⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)))}    &   ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))    &   ⊢ 𝑇 = (𝑚 ∈ ℕ ↦ if((2 · 𝑅) ≤ 𝑚, (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))), ((𝑅 · (log‘((𝑚 + 1) / 𝑚))) + ((log‘((𝑅 + 1) · 𝑚)) + π))))    ⇒   ⊢ (𝜑 → (seq1( ∘f + , 𝐺) ∈ dom (⇝𝑢‘𝑈) ∧ (seq1( ∘f + , 𝐺)(⇝𝑢‘𝑈)(𝑧 ∈ 𝑈 ↦ 𝑂) → ∃𝑟 ∈ ℝ ∀𝑧 ∈ 𝑈 (abs‘𝑂) ≤ 𝑟)))
Theorem	lgamgulm 27063*	The series 𝐺 is uniformly convergent on the compact region 𝑈, which describes a circle of radius 𝑅 with holes of size 1 / 𝑅 around the poles of the gamma function. (Contributed by Mario Carneiro, 3-Jul-2017.)
⊢ (𝜑 → 𝑅 ∈ ℕ)    &   ⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)))}    &   ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))    ⇒   ⊢ (𝜑 → seq1( ∘f + , 𝐺) ∈ dom (⇝𝑢‘𝑈))
Theorem	lgamgulm2 27064*	Rewrite the limit of the sequence 𝐺 in terms of the log-Gamma function. (Contributed by Mario Carneiro, 6-Jul-2017.)
⊢ (𝜑 → 𝑅 ∈ ℕ)    &   ⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)))}    &   ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))    ⇒   ⊢ (𝜑 → (∀𝑧 ∈ 𝑈 (log Γ‘𝑧) ∈ ℂ ∧ seq1( ∘f + , 𝐺)(⇝𝑢‘𝑈)(𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧)))))
Theorem	lgambdd 27065*	The log-Gamma function is bounded on the region 𝑈. (Contributed by Mario Carneiro, 9-Jul-2017.)
⊢ (𝜑 → 𝑅 ∈ ℕ)    &   ⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)))}    &   ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))    ⇒   ⊢ (𝜑 → ∃𝑟 ∈ ℝ ∀𝑧 ∈ 𝑈 (abs‘(log Γ‘𝑧)) ≤ 𝑟)
Theorem	lgamucov 27066*	The 𝑈 regions used in the proof of lgamgulm 27063 have interiors which cover the entire domain of the Gamma function. (Contributed by Mario Carneiro, 6-Jul-2017.)
⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))}    &   ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))    &   ⊢ 𝐽 = (TopOpen‘ℂfld)    ⇒   ⊢ (𝜑 → ∃𝑟 ∈ ℕ 𝐴 ∈ ((int‘𝐽)‘𝑈))
Theorem	lgamucov2 27067*	The 𝑈 regions used in the proof of lgamgulm 27063 have interiors which cover the entire domain of the Gamma function. (Contributed by Mario Carneiro, 8-Jul-2017.)
⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))}    &   ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))    ⇒   ⊢ (𝜑 → ∃𝑟 ∈ ℕ 𝐴 ∈ 𝑈)
Theorem	lgamcvglem 27068*	Lemma for lgamf 27070 and lgamcvg 27082. (Contributed by Mario Carneiro, 8-Jul-2017.)
⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ0 (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))}    &   ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))    &   ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1))))    ⇒   ⊢ (𝜑 → ((log Γ‘𝐴) ∈ ℂ ∧ seq1( + , 𝐺) ⇝ ((log Γ‘𝐴) + (log‘𝐴))))
Theorem	lgamcl 27069	The log-Gamma function is a complex function defined on the whole complex plane except for the negative integers. (Contributed by Mario Carneiro, 8-Jul-2017.)
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (log Γ‘𝐴) ∈ ℂ)
Theorem	lgamf 27070	The log-Gamma function is a complex function defined on the whole complex plane except for the negative integers. (Contributed by Mario Carneiro, 6-Jul-2017.)
⊢ log Γ:(ℂ ∖ (ℤ ∖ ℕ))⟶ℂ
Theorem	gamf 27071	The Gamma function is a complex function defined on the whole complex plane except for the negative integers. (Contributed by Mario Carneiro, 6-Jul-2017.)
⊢ Γ:(ℂ ∖ (ℤ ∖ ℕ))⟶ℂ
Theorem	gamcl 27072	The exponential of the log-Gamma function is the Gamma function (by definition). (Contributed by Mario Carneiro, 8-Jul-2017.)
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (Γ‘𝐴) ∈ ℂ)
Theorem	eflgam 27073	The exponential of the log-Gamma function is the Gamma function (by definition). (Contributed by Mario Carneiro, 8-Jul-2017.)
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (exp‘(log Γ‘𝐴)) = (Γ‘𝐴))
Theorem	gamne0 27074	The Gamma function is never zero. (Contributed by Mario Carneiro, 9-Jul-2017.)
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (Γ‘𝐴) ≠ 0)
Theorem	igamval 27075	Value of the inverse Gamma function. (Contributed by Mario Carneiro, 16-Jul-2017.)
⊢ (𝐴 ∈ ℂ → (1/Γ‘𝐴) = if(𝐴 ∈ (ℤ ∖ ℕ), 0, (1 / (Γ‘𝐴))))
Theorem	igamz 27076	Value of the inverse Gamma function on nonpositive integers. (Contributed by Mario Carneiro, 16-Jul-2017.)
⊢ (𝐴 ∈ (ℤ ∖ ℕ) → (1/Γ‘𝐴) = 0)
Theorem	igamgam 27077	Value of the inverse Gamma function in terms of the Gamma function. (Contributed by Mario Carneiro, 16-Jul-2017.)
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (1/Γ‘𝐴) = (1 / (Γ‘𝐴)))
Theorem	igamlgam 27078	Value of the inverse Gamma function in terms of the log-Gamma function. (Contributed by Mario Carneiro, 16-Jul-2017.)
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (1/Γ‘𝐴) = (exp‘-(log Γ‘𝐴)))
Theorem	igamf 27079	Closure of the inverse Gamma function. (Contributed by Mario Carneiro, 16-Jul-2017.)
⊢ 1/Γ:ℂ⟶ℂ
Theorem	igamcl 27080	Closure of the inverse Gamma function. (Contributed by Mario Carneiro, 16-Jul-2017.)
⊢ (𝐴 ∈ ℂ → (1/Γ‘𝐴) ∈ ℂ)
Theorem	gamigam 27081	The Gamma function is the inverse of the inverse Gamma function. (Contributed by Mario Carneiro, 16-Jul-2017.)
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (Γ‘𝐴) = (1 / (1/Γ‘𝐴)))
Theorem	lgamcvg 27082*	The series 𝐺 converges to log Γ(𝐴) + log(𝐴). (Contributed by Mario Carneiro, 6-Jul-2017.)
⊢ 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1))))    &   ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))    ⇒   ⊢ (𝜑 → seq1( + , 𝐺) ⇝ ((log Γ‘𝐴) + (log‘𝐴)))
Theorem	lgamcvg2 27083*	The series 𝐺 converges to log Γ(𝐴 + 1). (Contributed by Mario Carneiro, 9-Jul-2017.)
⊢ 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1))))    &   ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))    ⇒   ⊢ (𝜑 → seq1( + , 𝐺) ⇝ (log Γ‘(𝐴 + 1)))
Theorem	gamcvg 27084*	The pointwise exponential of the series 𝐺 converges to Γ(𝐴) · 𝐴. (Contributed by Mario Carneiro, 6-Jul-2017.)
⊢ 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1))))    &   ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))    ⇒   ⊢ (𝜑 → (exp ∘ seq1( + , 𝐺)) ⇝ ((Γ‘𝐴) · 𝐴))
Theorem	lgamp1 27085	The functional equation of the (log) Gamma function. (Contributed by Mario Carneiro, 9-Jul-2017.)
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (log Γ‘(𝐴 + 1)) = ((log Γ‘𝐴) + (log‘𝐴)))
Theorem	gamp1 27086	The functional equation of the Gamma function. (Contributed by Mario Carneiro, 9-Jul-2017.)
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) → (Γ‘(𝐴 + 1)) = ((Γ‘𝐴) · 𝐴))
Theorem	gamcvg2lem 27087*	Lemma for gamcvg2 27088. (Contributed by Mario Carneiro, 10-Jul-2017.)
⊢ 𝐹 = (𝑚 ∈ ℕ ↦ ((((𝑚 + 1) / 𝑚)↑𝑐𝐴) / ((𝐴 / 𝑚) + 1)))    &   ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))    &   ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1))))    ⇒   ⊢ (𝜑 → (exp ∘ seq1( + , 𝐺)) = seq1( · , 𝐹))
Theorem	gamcvg2 27088*	An infinite product expression for the gamma function. (Contributed by Mario Carneiro, 9-Jul-2017.)
⊢ 𝐹 = (𝑚 ∈ ℕ ↦ ((((𝑚 + 1) / 𝑚)↑𝑐𝐴) / ((𝐴 / 𝑚) + 1)))    &   ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))    ⇒   ⊢ (𝜑 → seq1( · , 𝐹) ⇝ ((Γ‘𝐴) · 𝐴))
Theorem	regamcl 27089	The Gamma function is real for real input. (Contributed by Mario Carneiro, 9-Jul-2017.)
⊢ (𝐴 ∈ (ℝ ∖ (ℤ ∖ ℕ)) → (Γ‘𝐴) ∈ ℝ)
Theorem	relgamcl 27090	The log-Gamma function is real for positive real input. (Contributed by Mario Carneiro, 9-Jul-2017.)
⊢ (𝐴 ∈ ℝ+ → (log Γ‘𝐴) ∈ ℝ)
Theorem	rpgamcl 27091	The log-Gamma function is positive real for positive real input. (Contributed by Mario Carneiro, 9-Jul-2017.)
⊢ (𝐴 ∈ ℝ+ → (Γ‘𝐴) ∈ ℝ+)
Theorem	lgam1 27092	The log-Gamma function at one. (Contributed by Mario Carneiro, 9-Jul-2017.)
⊢ (log Γ‘1) = 0
Theorem	gam1 27093	The log-Gamma function at one. (Contributed by Mario Carneiro, 9-Jul-2017.)
⊢ (Γ‘1) = 1
Theorem	facgam 27094	The Gamma function generalizes the factorial. (Contributed by Mario Carneiro, 9-Jul-2017.)
⊢ (𝑁 ∈ ℕ0 → (!‘𝑁) = (Γ‘(𝑁 + 1)))
Theorem	gamfac 27095	The Gamma function generalizes the factorial. (Contributed by Mario Carneiro, 9-Jul-2017.)
⊢ (𝑁 ∈ ℕ → (Γ‘𝑁) = (!‘(𝑁 − 1)))
14.4  Basic number theory
14.4.1  Wilson's theorem
Theorem	wilthlem1 27096	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 16788, (𝑁↑(𝑃 − 2)) mod 𝑃 is the modular inverse of 𝑁 in ℤ / 𝑃ℤ. (Contributed by Mario Carneiro, 24-Jan-2015.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑁 = ((𝑁↑(𝑃 − 2)) mod 𝑃) ↔ (𝑁 = 1 ∨ 𝑁 = (𝑃 − 1))))
Theorem	wilthlem2 27097*	Lemma for wilth 27099: induction step. The "hand proof" version of this theorem works by writing out the list of all numbers from 1 to 𝑃 − 1 in pairs such that a number is paired with its inverse. Every number has a unique inverse different from itself except 1 and 𝑃 − 1, and so each pair multiplies to 1, and 1 and 𝑃 − 1≡-1 multiply to -1, so the full product is equal to -1. Here we make this precise by doing the product pair by pair. The induction hypothesis says that every subset 𝑆 of 1...(𝑃 − 1) that is closed under inverse (i.e. all pairs are matched up) and contains 𝑃 − 1 multiplies to -1 mod 𝑃. Given such a set, we take out one element 𝑧 ≠ 𝑃 − 1. If there are no such elements, then 𝑆 = {𝑃 − 1} which forms the base case. Otherwise, 𝑆 ∖ {𝑧, 𝑧↑-1} is also closed under inverse and contains 𝑃 − 1, so the induction hypothesis says that this equals -1; and the remaining two elements are either equal to each other, in which case wilthlem1 27096 gives that 𝑧 = 1 or 𝑃 − 1, and we've already excluded the second case, so the product gives 1; or 𝑧 ≠ 𝑧↑-1 and their product is 1. In either case the accumulated product is unaffected. (Contributed by Mario Carneiro, 24-Jan-2015.) (Proof shortened by AV, 27-Jul-2019.)
⊢ 𝑇 = (mulGrp‘ℂfld)    &   ⊢ 𝐴 = {𝑥 ∈ 𝒫 (1...(𝑃 − 1)) ∣ ((𝑃 − 1) ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥)}    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 𝑆 ∈ 𝐴)    &   ⊢ (𝜑 → ∀𝑠 ∈ 𝐴 (𝑠 ⊊ 𝑆 → ((𝑇 Σg ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))    ⇒   ⊢ (𝜑 → ((𝑇 Σg ( I ↾ 𝑆)) mod 𝑃) = (-1 mod 𝑃))
Theorem	wilthlem3 27098*	Lemma for wilth 27099. Here we round out the argument of wilthlem2 27097 with the final step of the induction. The induction argument shows that every subset of 1...(𝑃 − 1) that is closed under inverse and contains 𝑃 − 1 multiplies to -1 mod 𝑃, and clearly 1...(𝑃 − 1) itself is such a set. Thus, the product of all the elements is -1, and all that is left is to translate the group sum notation (which we used for its unordered summing capabilities) into an ordered sequence to match the definition of the factorial. (Contributed by Mario Carneiro, 24-Jan-2015.) (Proof shortened by AV, 27-Jul-2019.)
⊢ 𝑇 = (mulGrp‘ℂfld)    &   ⊢ 𝐴 = {𝑥 ∈ 𝒫 (1...(𝑃 − 1)) ∣ ((𝑃 − 1) ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥)}    ⇒   ⊢ (𝑃 ∈ ℙ → 𝑃 ∥ ((!‘(𝑃 − 1)) + 1))
Theorem	wilth 27099	Wilson's theorem. A number is prime iff it is greater than or equal to 2 and (𝑁 − 1)! is congruent to -1, mod 𝑁, or alternatively if 𝑁 divides (𝑁 − 1)! + 1. In this part of the proof we show the relatively simple reverse implication; see wilthlem3 27098 for the forward implication. This is Metamath 100 proof #51. (Contributed by Mario Carneiro, 24-Jan-2015.) (Proof shortened by Fan Zheng, 16-Jun-2016.)
⊢ (𝑁 ∈ ℙ ↔ (𝑁 ∈ (ℤ≥‘2) ∧ 𝑁 ∥ ((!‘(𝑁 − 1)) + 1)))
Theorem	wilthimp 27100	The forward implication of Wilson's theorem wilth 27099 (see wilthlem3 27098), expressed using the modulo operation: For any prime 𝑝 we have (𝑝 − 1)!≡ − 1 (mod 𝑝), see theorem 5.24 in [ApostolNT] p. 116. (Contributed by AV, 21-Jul-2021.)
⊢ (𝑃 ∈ ℙ → ((!‘(𝑃 − 1)) mod 𝑃) = (-1 mod 𝑃))