P. 270 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 26901-27000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	atantan 26901	The arctangent function is an inverse to tan. (Contributed by Mario Carneiro, 5-Apr-2015.)
⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (arctan‘(tan‘𝐴)) = 𝐴)
Theorem	atantanb 26902	Relationship between tangent and arctangent. (Contributed by Mario Carneiro, 5-Apr-2015.)
⊢ ((𝐴 ∈ dom arctan ∧ 𝐵 ∈ ℂ ∧ (ℜ‘𝐵) ∈ (-(π / 2)(,)(π / 2))) → ((arctan‘𝐴) = 𝐵 ↔ (tan‘𝐵) = 𝐴))
Theorem	atanbndlem 26903	Lemma for atanbnd 26904. (Contributed by Mario Carneiro, 5-Apr-2015.)
⊢ (𝐴 ∈ ℝ+ → (arctan‘𝐴) ∈ (-(π / 2)(,)(π / 2)))
Theorem	atanbnd 26904	The arctangent function is bounded by π / 2 on the reals. (Contributed by Mario Carneiro, 5-Apr-2015.)
⊢ (𝐴 ∈ ℝ → (arctan‘𝐴) ∈ (-(π / 2)(,)(π / 2)))
Theorem	atanord 26905	The arctangent function is strictly increasing. (Contributed by Mario Carneiro, 5-Apr-2015.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ (arctan‘𝐴) < (arctan‘𝐵)))
Theorem	atan1 26906	The arctangent of 1 is π / 4. (Contributed by Mario Carneiro, 2-Apr-2015.)
⊢ (arctan‘1) = (π / 4)
Theorem	bndatandm 26907	A point in the open unit disk is in the domain of the arctangent. (Contributed by Mario Carneiro, 5-Apr-2015.)
⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → 𝐴 ∈ dom arctan)
Theorem	atans 26908*	The "domain of continuity" of the arctangent. (Contributed by Mario Carneiro, 7-Apr-2015.)
⊢ 𝐷 = (ℂ ∖ (-∞(,]0))    &   ⊢ 𝑆 = {𝑦 ∈ ℂ ∣ (1 + (𝑦↑2)) ∈ 𝐷}    ⇒   ⊢ (𝐴 ∈ 𝑆 ↔ (𝐴 ∈ ℂ ∧ (1 + (𝐴↑2)) ∈ 𝐷))
Theorem	atans2 26909*	It suffices to show that 1 − i𝐴 and 1 + i𝐴 are in the continuity domain of log to show that 𝐴 is in the continuity domain of arctangent. (Contributed by Mario Carneiro, 7-Apr-2015.)
⊢ 𝐷 = (ℂ ∖ (-∞(,]0))    &   ⊢ 𝑆 = {𝑦 ∈ ℂ ∣ (1 + (𝑦↑2)) ∈ 𝐷}    ⇒   ⊢ (𝐴 ∈ 𝑆 ↔ (𝐴 ∈ ℂ ∧ (1 − (i · 𝐴)) ∈ 𝐷 ∧ (1 + (i · 𝐴)) ∈ 𝐷))
Theorem	atansopn 26910*	The domain of continuity of the arctangent is an open set. (Contributed by Mario Carneiro, 7-Apr-2015.)
⊢ 𝐷 = (ℂ ∖ (-∞(,]0))    &   ⊢ 𝑆 = {𝑦 ∈ ℂ ∣ (1 + (𝑦↑2)) ∈ 𝐷}    ⇒   ⊢ 𝑆 ∈ (TopOpen‘ℂfld)
Theorem	atansssdm 26911*	The domain of continuity of the arctangent is a subset of the actual domain of the arctangent. (Contributed by Mario Carneiro, 7-Apr-2015.)
⊢ 𝐷 = (ℂ ∖ (-∞(,]0))    &   ⊢ 𝑆 = {𝑦 ∈ ℂ ∣ (1 + (𝑦↑2)) ∈ 𝐷}    ⇒   ⊢ 𝑆 ⊆ dom arctan
Theorem	ressatans 26912*	The real number line is a subset of the domain of continuity of the arctangent. (Contributed by Mario Carneiro, 7-Apr-2015.)
⊢ 𝐷 = (ℂ ∖ (-∞(,]0))    &   ⊢ 𝑆 = {𝑦 ∈ ℂ ∣ (1 + (𝑦↑2)) ∈ 𝐷}    ⇒   ⊢ ℝ ⊆ 𝑆
Theorem	dvatan 26913*	The derivative of the arctangent. (Contributed by Mario Carneiro, 7-Apr-2015.)
⊢ 𝐷 = (ℂ ∖ (-∞(,]0))    &   ⊢ 𝑆 = {𝑦 ∈ ℂ ∣ (1 + (𝑦↑2)) ∈ 𝐷}    ⇒   ⊢ (ℂ D (arctan ↾ 𝑆)) = (𝑥 ∈ 𝑆 ↦ (1 / (1 + (𝑥↑2))))
Theorem	atancn 26914*	The arctangent is a continuous function. (Contributed by Mario Carneiro, 7-Apr-2015.)
⊢ 𝐷 = (ℂ ∖ (-∞(,]0))    &   ⊢ 𝑆 = {𝑦 ∈ ℂ ∣ (1 + (𝑦↑2)) ∈ 𝐷}    ⇒   ⊢ (arctan ↾ 𝑆) ∈ (𝑆–cn→ℂ)
Theorem	atantayl 26915*	The Taylor series for arctan(𝐴). (Contributed by Mario Carneiro, 1-Apr-2015.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (((i · ((-i↑𝑛) − (i↑𝑛))) / 2) · ((𝐴↑𝑛) / 𝑛)))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq1( + , 𝐹) ⇝ (arctan‘𝐴))
Theorem	atantayl2 26916*	The Taylor series for arctan(𝐴). (Contributed by Mario Carneiro, 1-Apr-2015.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, ((-1↑((𝑛 − 1) / 2)) · ((𝐴↑𝑛) / 𝑛))))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq1( + , 𝐹) ⇝ (arctan‘𝐴))
Theorem	atantayl3 26917*	The Taylor series for arctan(𝐴). (Contributed by Mario Carneiro, 7-Apr-2015.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((-1↑𝑛) · ((𝐴↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1))))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq0( + , 𝐹) ⇝ (arctan‘𝐴))
Theorem	leibpilem1 26918	Lemma for leibpi 26920. (Contributed by Mario Carneiro, 7-Apr-2015.) (Proof shortened by Steven Nguyen, 23-Mar-2023.)
⊢ ((𝑁 ∈ ℕ0 ∧ (¬ 𝑁 = 0 ∧ ¬ 2 ∥ 𝑁)) → (𝑁 ∈ ℕ ∧ ((𝑁 − 1) / 2) ∈ ℕ0))
Theorem	leibpilem2 26919*	The Leibniz formula for π. (Contributed by Mario Carneiro, 7-Apr-2015.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((-1↑𝑛) / ((2 · 𝑛) + 1)))    &   ⊢ 𝐺 = (𝑘 ∈ ℕ0 ↦ if((𝑘 = 0 ∨ 2 ∥ 𝑘), 0, ((-1↑((𝑘 − 1) / 2)) / 𝑘)))    &   ⊢ 𝐴 ∈ V    ⇒   ⊢ (seq0( + , 𝐹) ⇝ 𝐴 ↔ seq0( + , 𝐺) ⇝ 𝐴)
Theorem	leibpi 26920	The Leibniz formula for π. This proof depends on three main facts: (1) the series 𝐹 is convergent, because it is an alternating series (iseralt 15620). (2) Using leibpilem2 26919 to rewrite the series as a power series, it is the 𝑥 = 1 special case of the Taylor series for arctan (atantayl2 26916). (3) Although we cannot directly plug 𝑥 = 1 into atantayl2 26916, Abel's theorem (abelth2 26420) says that the limit along any sequence converging to 1, such as 1 − 1 / 𝑛, of the power series converges to the power series extended to 1, and then since arctan is continuous at 1 (atancn 26914) we get the desired result. This is Metamath 100 proof #26. (Contributed by Mario Carneiro, 7-Apr-2015.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((-1↑𝑛) / ((2 · 𝑛) + 1)))    ⇒   ⊢ seq0( + , 𝐹) ⇝ (π / 4)
Theorem	leibpisum 26921	The Leibniz formula for π. This version of leibpi 26920 looks nicer but does not assert that the series is convergent so is not as practically useful. (Contributed by Mario Carneiro, 7-Apr-2015.)
⊢ Σ𝑛 ∈ ℕ0 ((-1↑𝑛) / ((2 · 𝑛) + 1)) = (π / 4)
Theorem	log2cnv 26922	Using the Taylor series for arctan(i / 3), produce a rapidly convergent series for log2. (Contributed by Mario Carneiro, 7-Apr-2015.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))    ⇒   ⊢ seq0( + , 𝐹) ⇝ (log‘2)
Theorem	log2tlbnd 26923*	Bound the error term in the series of log2cnv 26922. (Contributed by Mario Carneiro, 7-Apr-2015.)
⊢ (𝑁 ∈ ℕ0 → ((log‘2) − Σ𝑛 ∈ (0...(𝑁 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ∈ (0[,](3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁)))))
14.3.9  The Birthday Problem
Theorem	log2ublem1 26924	Lemma for log2ub 26927. The proof of log2ub 26927, which is simply the evaluation of log2tlbnd 26923 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 26925*	Lemma for log2ub 26927. (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 26926	Lemma for log2ub 26927. 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	log2ub 26927	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. (Contributed by Mario Carneiro, 7-Apr-2015.) (Proof shortened by AV, 16-Sep-2021.)
⊢ (log‘2) < (;;253 / ;;365)
Theorem	log2le1 26928	log2 is less than 1. This is just a weaker form of log2ub 26927 when no tight upper bound is required. (Contributed by Thierry Arnoux, 27-Sep-2017.)
⊢ (log‘2) < 1
Theorem	birthdaylem1 26929*	Lemma for birthday 26932. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ 𝑆 = {𝑓 ∣ 𝑓:(1...𝐾)⟶(1...𝑁)}    &   ⊢ 𝑇 = {𝑓 ∣ 𝑓:(1...𝐾)–1-1→(1...𝑁)}    ⇒   ⊢ (𝑇 ⊆ 𝑆 ∧ 𝑆 ∈ Fin ∧ (𝑁 ∈ ℕ → 𝑆 ≠ ∅))
Theorem	birthdaylem2 26930*	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 26931*	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	birthday 26932*	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. This is Metamath 100 proof #93. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ 𝑆 = {𝑓 ∣ 𝑓:(1...𝐾)⟶(1...𝑁)}    &   ⊢ 𝑇 = {𝑓 ∣ 𝑓:(1...𝐾)–1-1→(1...𝑁)}    &   ⊢ 𝐾 = ;23    &   ⊢ 𝑁 = ;;365    ⇒   ⊢ ((♯‘𝑇) / (♯‘𝑆)) < (1 / 2)
14.3.10  Areas in R^2
Syntax	carea 26933	Area of regions in the complex plane.
class area
Definition	df-area 26934*	Define the area of a subset of ℝ × ℝ. (Contributed by Mario Carneiro, 21-Jun-2015.)
⊢ area = (𝑠 ∈ {𝑡 ∈ 𝒫 (ℝ × ℝ) ∣ (∀𝑥 ∈ ℝ (𝑡 “ {𝑥}) ∈ (◡vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦ (vol‘(𝑡 “ {𝑥}))) ∈ 𝐿1)} ↦ ∫ℝ(vol‘(𝑠 “ {𝑥})) d𝑥)
Theorem	dmarea 26935*	The domain of the area function is the set of finitely measurable subsets of ℝ × ℝ. (Contributed by Mario Carneiro, 21-Jun-2015.)
⊢ (𝐴 ∈ dom area ↔ (𝐴 ⊆ (ℝ × ℝ) ∧ ∀𝑥 ∈ ℝ (𝐴 “ {𝑥}) ∈ (◡vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦ (vol‘(𝐴 “ {𝑥}))) ∈ 𝐿1))
Theorem	areambl 26936	The fibers of a measurable region are finitely measurable subsets of ℝ. (Contributed by Mario Carneiro, 21-Jun-2015.)
⊢ ((𝑆 ∈ dom area ∧ 𝐴 ∈ ℝ) → ((𝑆 “ {𝐴}) ∈ dom vol ∧ (vol‘(𝑆 “ {𝐴})) ∈ ℝ))
Theorem	areass 26937	A measurable region is a subset of ℝ × ℝ. (Contributed by Mario Carneiro, 21-Jun-2015.)
⊢ (𝑆 ∈ dom area → 𝑆 ⊆ (ℝ × ℝ))
Theorem	dfarea 26938*	Rewrite df-area 26934 self-referentially. (Contributed by Mario Carneiro, 21-Jun-2015.)
⊢ area = (𝑠 ∈ dom area ↦ ∫ℝ(vol‘(𝑠 “ {𝑥})) d𝑥)
Theorem	areaf 26939	Area measurement is a function whose values are nonnegative reals. (Contributed by Mario Carneiro, 21-Jun-2015.)
⊢ area:dom area⟶(0[,)+∞)
Theorem	areacl 26940	The area of a measurable region is a real number. (Contributed by Mario Carneiro, 21-Jun-2015.)
⊢ (𝑆 ∈ dom area → (area‘𝑆) ∈ ℝ)
Theorem	areage0 26941	The area of a measurable region is greater than or equal to zero. (Contributed by Mario Carneiro, 21-Jun-2015.)
⊢ (𝑆 ∈ dom area → 0 ≤ (area‘𝑆))
Theorem	areaval 26942*	The area of a measurable region is greater than or equal to zero. (Contributed by Mario Carneiro, 21-Jun-2015.)
⊢ (𝑆 ∈ dom area → (area‘𝑆) = ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥)
14.3.11  More miscellaneous converging sequences
Theorem	rlimcnp 26943*	Relate a limit of a real-valued sequence at infinity to the continuity of the function 𝑆(𝑦) = 𝑅(1 / 𝑦) at zero. (Contributed by Mario Carneiro, 1-Mar-2015.)
⊢ (𝜑 → 𝐴 ⊆ (0[,)+∞))    &   ⊢ (𝜑 → 0 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐵 ⊆ ℝ+)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑅 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥 ∈ 𝐴 ↔ (1 / 𝑥) ∈ 𝐵))    &   ⊢ (𝑥 = 0 → 𝑅 = 𝐶)    &   ⊢ (𝑥 = (1 / 𝑦) → 𝑅 = 𝑆)    &   ⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝐾 = (𝐽 ↾t 𝐴)    ⇒   ⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ⇝𝑟 𝐶 ↔ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘0)))
Theorem	rlimcnp2 26944*	Relate a limit of a real-valued sequence at infinity to the continuity of the function 𝑆(𝑦) = 𝑅(1 / 𝑦) at zero. (Contributed by Mario Carneiro, 1-Mar-2015.)
⊢ (𝜑 → 𝐴 ⊆ (0[,)+∞))    &   ⊢ (𝜑 → 0 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐵 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑆 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (𝑦 ∈ 𝐵 ↔ (1 / 𝑦) ∈ 𝐴))    &   ⊢ (𝑦 = (1 / 𝑥) → 𝑆 = 𝑅)    &   ⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝐾 = (𝐽 ↾t 𝐴)    ⇒   ⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ⇝𝑟 𝐶 ↔ (𝑥 ∈ 𝐴 ↦ if(𝑥 = 0, 𝐶, 𝑅)) ∈ ((𝐾 CnP 𝐽)‘0)))
Theorem	rlimcnp3 26945*	Relate a limit of a real-valued sequence at infinity to the continuity of the function 𝑆(𝑦) = 𝑅(1 / 𝑦) at zero. (Contributed by Mario Carneiro, 1-Mar-2015.)
⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 𝑆 ∈ ℂ)    &   ⊢ (𝑦 = (1 / 𝑥) → 𝑆 = 𝑅)    &   ⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝐾 = (𝐽 ↾t (0[,)+∞))    ⇒   ⊢ (𝜑 → ((𝑦 ∈ ℝ+ ↦ 𝑆) ⇝𝑟 𝐶 ↔ (𝑥 ∈ (0[,)+∞) ↦ if(𝑥 = 0, 𝐶, 𝑅)) ∈ ((𝐾 CnP 𝐽)‘0)))
Theorem	xrlimcnp 26946*	Relate a limit of a real-valued sequence at infinity to the continuity of the corresponding extended real function at +∞. Since any ⇝𝑟 limit can be written in the form on the left side of the implication, this shows that real limits are a special case of topological continuity at a point. (Contributed by Mario Carneiro, 8-Sep-2015.)
⊢ (𝜑 → 𝐴 = (𝐵 ∪ {+∞}))    &   ⊢ (𝜑 → 𝐵 ⊆ ℝ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑅 ∈ ℂ)    &   ⊢ (𝑥 = +∞ → 𝑅 = 𝐶)    &   ⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝐾 = ((ordTop‘ ≤ ) ↾t 𝐴)    ⇒   ⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶 ↔ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)))
Theorem	efrlim 26947*	The limit of the sequence (1 + 𝐴 / 𝑘)↑𝑘 is the exponential function. This is often taken as an alternate definition of the exponential function (see also dfef2 26949). (Contributed by Mario Carneiro, 1-Mar-2015.) Avoid ax-mulf 11118. (Revised by GG, 19-Apr-2025.)
⊢ 𝑆 = (0(ball‘(abs ∘ − ))(1 / ((abs‘𝐴) + 1)))    ⇒   ⊢ (𝐴 ∈ ℂ → (𝑘 ∈ ℝ+ ↦ ((1 + (𝐴 / 𝑘))↑𝑐𝑘)) ⇝𝑟 (exp‘𝐴))
Theorem	efrlimOLD 26948*	Obsolete version of efrlim 26947 as of 19-Apr-2025. (Contributed by Mario Carneiro, 1-Mar-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑆 = (0(ball‘(abs ∘ − ))(1 / ((abs‘𝐴) + 1)))    ⇒   ⊢ (𝐴 ∈ ℂ → (𝑘 ∈ ℝ+ ↦ ((1 + (𝐴 / 𝑘))↑𝑐𝑘)) ⇝𝑟 (exp‘𝐴))
Theorem	dfef2 26949*	The limit of the sequence (1 + 𝐴 / 𝑘)↑𝑘 as 𝑘 goes to +∞ is (exp‘𝐴). This is another common definition of e. (Contributed by Mario Carneiro, 1-Mar-2015.)
⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) = ((1 + (𝐴 / 𝑘))↑𝑘))    ⇒   ⊢ (𝜑 → 𝐹 ⇝ (exp‘𝐴))
Theorem	cxplim 26950*	A power to a negative exponent goes to zero as the base becomes large. (Contributed by Mario Carneiro, 15-Sep-2014.) (Revised by Mario Carneiro, 18-May-2016.)
⊢ (𝐴 ∈ ℝ+ → (𝑛 ∈ ℝ+ ↦ (1 / (𝑛↑𝑐𝐴))) ⇝𝑟 0)
Theorem	sqrtlim 26951	The inverse square root function converges to zero. (Contributed by Mario Carneiro, 18-May-2016.)
⊢ (𝑛 ∈ ℝ+ ↦ (1 / (√‘𝑛))) ⇝𝑟 0
Theorem	rlimcxp 26952*	Any power to a positive exponent of a converging sequence also converges. (Contributed by Mario Carneiro, 18-Sep-2014.)
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑛 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 0)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝑛 ∈ 𝐴 ↦ (𝐵↑𝑐𝐶)) ⇝𝑟 0)
Theorem	o1cxp 26953*	An eventually bounded function taken to a nonnegative power is eventually bounded. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 0 ≤ (ℜ‘𝐶))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝑂(1))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵↑𝑐𝐶)) ∈ 𝑂(1))
Theorem	cxp2limlem 26954*	A linear factor grows slower than any exponential with base greater than 1. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 1 < 𝐴) → (𝑛 ∈ ℝ+ ↦ (𝑛 / (𝐴↑𝑐𝑛))) ⇝𝑟 0)
Theorem	cxp2lim 26955*	Any power grows slower than any exponential with base greater than 1. (Contributed by Mario Carneiro, 18-Sep-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → (𝑛 ∈ ℝ+ ↦ ((𝑛↑𝑐𝐴) / (𝐵↑𝑐𝑛))) ⇝𝑟 0)
Theorem	cxploglim 26956*	The logarithm grows slower than any positive power. (Contributed by Mario Carneiro, 18-Sep-2014.)
⊢ (𝐴 ∈ ℝ+ → (𝑛 ∈ ℝ+ ↦ ((log‘𝑛) / (𝑛↑𝑐𝐴))) ⇝𝑟 0)
Theorem	cxploglim2 26957*	Every power of the logarithm grows slower than any positive power. (Contributed by Mario Carneiro, 20-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+) → (𝑛 ∈ ℝ+ ↦ (((log‘𝑛)↑𝑐𝐴) / (𝑛↑𝑐𝐵))) ⇝𝑟 0)
Theorem	divsqrtsumlem 26958*	Lemma for divsqrsum 26960 and divsqrtsum2 26961. (Contributed by Mario Carneiro, 18-May-2016.)
⊢ 𝐹 = (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑛)) − (2 · (√‘𝑥))))    ⇒   ⊢ (𝐹:ℝ+⟶ℝ ∧ 𝐹 ∈ dom ⇝𝑟 ∧ ((𝐹 ⇝𝑟 𝐿 ∧ 𝐴 ∈ ℝ+) → (abs‘((𝐹‘𝐴) − 𝐿)) ≤ (1 / (√‘𝐴))))
Theorem	divsqrsumf 26959*	The function 𝐹 used in divsqrsum 26960 is a real function. (Contributed by Mario Carneiro, 12-May-2016.)
⊢ 𝐹 = (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑛)) − (2 · (√‘𝑥))))    ⇒   ⊢ 𝐹:ℝ+⟶ℝ
Theorem	divsqrsum 26960*	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 26961*	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 26962*	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 26963*	Closure of a 0-1 linear combination in a convex set. (Contributed by Mario Carneiro, 21-Jun-2015.)
⊢ (𝜑 → 𝐷 ⊆ ℝ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) → (𝑥[,]𝑦) ⊆ 𝐷)    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)) ∈ 𝐷)
Theorem	scvxcvx 26964*	A strictly convex function is convex. (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ (𝜑 → 𝐷 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹:𝐷⟶ℝ)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐷 ∧ 𝑏 ∈ 𝐷)) → (𝑎[,]𝑏) ⊆ 𝐷)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))))    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) ≤ ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))
Theorem	jensenlem1 26965*	Lemma for jensen 26967. (Contributed by Mario Carneiro, 4-Jun-2016.)
⊢ (𝜑 → 𝐷 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹:𝐷⟶ℝ)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐷 ∧ 𝑏 ∈ 𝐷)) → (𝑎[,]𝑏) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝑇:𝐴⟶(0[,)+∞))    &   ⊢ (𝜑 → 𝑋:𝐴⟶𝐷)    &   ⊢ (𝜑 → 0 < (ℂfld Σg 𝑇))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑡 ∈ (0[,]1))) → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ≤ ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))))    &   ⊢ (𝜑 → ¬ 𝑧 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐵 ∪ {𝑧}) ⊆ 𝐴)    &   ⊢ 𝑆 = (ℂfld Σg (𝑇 ↾ 𝐵))    &   ⊢ 𝐿 = (ℂfld Σg (𝑇 ↾ (𝐵 ∪ {𝑧})))    ⇒   ⊢ (𝜑 → 𝐿 = (𝑆 + (𝑇‘𝑧)))
Theorem	jensenlem2 26966*	Lemma for jensen 26967. (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 26967*	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 26968	Lemma for amgm 26969. (Contributed by Mario Carneiro, 21-Jun-2015.)
⊢ 𝑀 = (mulGrp‘ℂfld)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ+)    ⇒   ⊢ (𝜑 → ((𝑀 Σg 𝐹)↑𝑐(1 / (♯‘𝐴))) ≤ ((ℂfld Σg 𝐹) / (♯‘𝐴)))
Theorem	amgm 26969	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 26970	The Euler-Mascheroni constant. (The label abbreviates Euler-Mascheroni.)
class γ
Definition	df-em 26971	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 26981. (Contributed by Mario Carneiro, 11-Jul-2014.)
⊢ γ = Σ𝑘 ∈ ℕ ((1 / 𝑘) − (log‘(1 + (1 / 𝑘))))
Theorem	logdifbnd 26972	Bound on the difference of logs. (Contributed by Mario Carneiro, 23-May-2016.)
⊢ (𝐴 ∈ ℝ+ → ((log‘(𝐴 + 1)) − (log‘𝐴)) ≤ (1 / 𝐴))
Theorem	logdiflbnd 26973	Lower bound on the difference of logs. (Contributed by Mario Carneiro, 3-Jul-2017.)
⊢ (𝐴 ∈ ℝ+ → (1 / (𝐴 + 1)) ≤ ((log‘(𝐴 + 1)) − (log‘𝐴)))
Theorem	emcllem1 26974*	Lemma for emcl 26981. 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 26975*	Lemma for emcl 26981. 𝐹 is increasing, and 𝐺 is decreasing. (Contributed by Mario Carneiro, 11-Jul-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘𝑛)))    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘(𝑛 + 1))))    ⇒   ⊢ (𝑁 ∈ ℕ → ((𝐹‘(𝑁 + 1)) ≤ (𝐹‘𝑁) ∧ (𝐺‘𝑁) ≤ (𝐺‘(𝑁 + 1))))
Theorem	emcllem3 26976*	Lemma for emcl 26981. 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 26977*	Lemma for emcl 26981. 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 26978*	Lemma for emcl 26981. The partial sums of the series 𝑇, which is used in Definition df-em 26971, 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 26979*	Lemma for emcl 26981. 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 26980*	Lemma for emcl 26981 and harmonicbnd 26982. 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 26981	Closure and bounds for the Euler-Mascheroni constant. (Contributed by Mario Carneiro, 11-Jul-2014.)
⊢ γ ∈ ((1 − (log‘2))[,]1)
Theorem	harmonicbnd 26982*	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 26983*	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 26984	The Euler-Mascheroni constant is a real number. (Contributed by Mario Carneiro, 11-Jul-2014.)
⊢ γ ∈ ℝ
Theorem	emgt0 26985	The Euler-Mascheroni constant is positive. (Contributed by Mario Carneiro, 11-Jul-2014.)
⊢ 0 < γ
Theorem	harmonicbnd3 26986*	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 26987*	A bound on the harmonic series, as compared to the natural logarithm. (Contributed by Mario Carneiro, 13-Apr-2016.)
⊢ (𝐴 ∈ ℝ+ → (log‘𝐴) ≤ Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚))
Theorem	harmonicubnd 26988*	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 26989*	The asymptotic behavior of Σ𝑚 ≤ 𝐴, 1 / 𝑚 = log𝐴 + γ + 𝑂(1 / 𝐴). (Contributed by Mario Carneiro, 14-May-2016.)
⊢ (𝐴 ∈ ℝ+ → (abs‘(Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − ((log‘𝐴) + γ))) ≤ (1 / 𝐴))
Theorem	fsumharmonic 26990*	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 26991	The Riemann zeta function.
class ζ
Definition	df-zeta 26992*	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 26993*	The zeta series is convergent. (Contributed by Mario Carneiro, 18-Jul-2014.)
⊢ (𝜑 → 𝑆 ∈ ℂ)    &   ⊢ (𝜑 → 1 < (ℜ‘𝑆))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) = (𝑘↑𝑐-𝑆))    ⇒   ⊢ (𝜑 → seq1( + , 𝐹) ∈ dom ⇝ )
14.3.15  Gamma function
Syntax	clgam 26994	Logarithm of the Gamma function.
class log Γ
Syntax	cgam 26995	The Gamma function.
class Γ
Syntax	cigam 26996	The inverse Gamma function.
class 1/Γ
Definition	df-lgam 26997*	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 26998	Define the Gamma function. See df-lgam 26997 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 26999	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 27000	Elementhood in the set of non-nonpositive integers. (Contributed by Mario Carneiro, 12-Jul-2014.)
⊢ (𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)) ↔ (𝐴 ∈ ℂ ∧ ¬ -𝐴 ∈ ℕ0))