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	efiatan 26901	Value of the exponential of an arctangent. (Contributed by Mario Carneiro, 2-Apr-2015.)
⊢ (𝐴 ∈ dom arctan → (exp‘(i · (arctan‘𝐴))) = ((√‘(1 + (i · 𝐴))) / (√‘(1 − (i · 𝐴)))))
Theorem	atanlogaddlem 26902	Lemma for atanlogadd 26903. (Contributed by Mario Carneiro, 3-Apr-2015.)
⊢ ((𝐴 ∈ dom arctan ∧ 0 ≤ (ℜ‘𝐴)) → ((log‘(1 + (i · 𝐴))) + (log‘(1 − (i · 𝐴)))) ∈ ran log)
Theorem	atanlogadd 26903	The rule √(𝑧𝑤) = (√𝑧)(√𝑤) is not always true on the complex numbers, but it is true when the arguments of 𝑧 and 𝑤 sum to within the interval (-π, π], so there are some cases such as this one with 𝑧 = 1 + i𝐴 and 𝑤 = 1 − i𝐴 which are true unconditionally. This result can also be stated as "√(1 + 𝑧) + √(1 − 𝑧) is analytic". (Contributed by Mario Carneiro, 3-Apr-2015.)
⊢ (𝐴 ∈ dom arctan → ((log‘(1 + (i · 𝐴))) + (log‘(1 − (i · 𝐴)))) ∈ ran log)
Theorem	atanlogsublem 26904	Lemma for atanlogsub 26905. (Contributed by Mario Carneiro, 4-Apr-2015.)
⊢ ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i · 𝐴))))) ∈ (-π(,)π))
Theorem	atanlogsub 26905	A variation on atanlogadd 26903, to show that √(1 + i𝑧) / √(1 − i𝑧) = √((1 + i𝑧) / (1 − i𝑧)) under more limited conditions. (Contributed by Mario Carneiro, 4-Apr-2015.)
⊢ ((𝐴 ∈ dom arctan ∧ (ℜ‘𝐴) ≠ 0) → ((log‘(1 + (i · 𝐴))) − (log‘(1 − (i · 𝐴)))) ∈ ran log)
Theorem	efiatan2 26906	Value of the exponential of an arctangent. (Contributed by Mario Carneiro, 3-Apr-2015.)
⊢ (𝐴 ∈ dom arctan → (exp‘(i · (arctan‘𝐴))) = ((1 + (i · 𝐴)) / (√‘(1 + (𝐴↑2)))))
Theorem	2efiatan 26907	Value of the exponential of an arctangent. (Contributed by Mario Carneiro, 2-Apr-2015.)
⊢ (𝐴 ∈ dom arctan → (exp‘(2 · (i · (arctan‘𝐴)))) = (((2 · i) / (𝐴 + i)) − 1))
Theorem	tanatan 26908	The arctangent function is an inverse to tan. (Contributed by Mario Carneiro, 2-Apr-2015.)
⊢ (𝐴 ∈ dom arctan → (tan‘(arctan‘𝐴)) = 𝐴)
Theorem	atandmtan 26909	The tangent function has range contained in the domain of the arctangent. (Contributed by Mario Carneiro, 31-Mar-2015.)
⊢ ((𝐴 ∈ ℂ ∧ (cos‘𝐴) ≠ 0) → (tan‘𝐴) ∈ dom arctan)
Theorem	cosatan 26910	The cosine of an arctangent. (Contributed by Mario Carneiro, 3-Apr-2015.)
⊢ (𝐴 ∈ dom arctan → (cos‘(arctan‘𝐴)) = (1 / (√‘(1 + (𝐴↑2)))))
Theorem	cosatanne0 26911	The arctangent function has range contained in the domain of the tangent. (Contributed by Mario Carneiro, 3-Apr-2015.)
⊢ (𝐴 ∈ dom arctan → (cos‘(arctan‘𝐴)) ≠ 0)
Theorem	atantan 26912	The arctangent function is an inverse to tan. (Contributed by Mario Carneiro, 5-Apr-2015.)
⊢ ((𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ (-(π / 2)(,)(π / 2))) → (arctan‘(tan‘𝐴)) = 𝐴)
Theorem	atantanb 26913	Relationship between tangent and arctangent. (Contributed by Mario Carneiro, 5-Apr-2015.)
⊢ ((𝐴 ∈ dom arctan ∧ 𝐵 ∈ ℂ ∧ (ℜ‘𝐵) ∈ (-(π / 2)(,)(π / 2))) → ((arctan‘𝐴) = 𝐵 ↔ (tan‘𝐵) = 𝐴))
Theorem	atanbndlem 26914	Lemma for atanbnd 26915. (Contributed by Mario Carneiro, 5-Apr-2015.)
⊢ (𝐴 ∈ ℝ+ → (arctan‘𝐴) ∈ (-(π / 2)(,)(π / 2)))
Theorem	atanbnd 26915	The arctangent function is bounded by π / 2 on the reals. (Contributed by Mario Carneiro, 5-Apr-2015.)
⊢ (𝐴 ∈ ℝ → (arctan‘𝐴) ∈ (-(π / 2)(,)(π / 2)))
Theorem	atanord 26916	The arctangent function is strictly increasing. (Contributed by Mario Carneiro, 5-Apr-2015.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ (arctan‘𝐴) < (arctan‘𝐵)))
Theorem	atan1 26917	The arctangent of 1 is π / 4. (Contributed by Mario Carneiro, 2-Apr-2015.)
⊢ (arctan‘1) = (π / 4)
Theorem	bndatandm 26918	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 26919*	The "domain of continuity" of the arctangent. (Contributed by Mario Carneiro, 7-Apr-2015.)
⊢ 𝐷 = (ℂ ∖ (-∞(,]0))    &   ⊢ 𝑆 = {𝑦 ∈ ℂ ∣ (1 + (𝑦↑2)) ∈ 𝐷}    ⇒   ⊢ (𝐴 ∈ 𝑆 ↔ (𝐴 ∈ ℂ ∧ (1 + (𝐴↑2)) ∈ 𝐷))
Theorem	atans2 26920*	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 26921*	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 26922*	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 26923*	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 26924*	The derivative of the arctangent. (Contributed by Mario Carneiro, 7-Apr-2015.)
⊢ 𝐷 = (ℂ ∖ (-∞(,]0))    &   ⊢ 𝑆 = {𝑦 ∈ ℂ ∣ (1 + (𝑦↑2)) ∈ 𝐷}    ⇒   ⊢ (ℂ D (arctan ↾ 𝑆)) = (𝑥 ∈ 𝑆 ↦ (1 / (1 + (𝑥↑2))))
Theorem	atancn 26925*	The arctangent is a continuous function. (Contributed by Mario Carneiro, 7-Apr-2015.)
⊢ 𝐷 = (ℂ ∖ (-∞(,]0))    &   ⊢ 𝑆 = {𝑦 ∈ ℂ ∣ (1 + (𝑦↑2)) ∈ 𝐷}    ⇒   ⊢ (arctan ↾ 𝑆) ∈ (𝑆–cn→ℂ)
Theorem	atantayl 26926*	The Taylor series for arctan(𝐴). (Contributed by Mario Carneiro, 1-Apr-2015.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (((i · ((-i↑𝑛) − (i↑𝑛))) / 2) · ((𝐴↑𝑛) / 𝑛)))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq1( + , 𝐹) ⇝ (arctan‘𝐴))
Theorem	atantayl2 26927*	The Taylor series for arctan(𝐴). (Contributed by Mario Carneiro, 1-Apr-2015.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, ((-1↑((𝑛 − 1) / 2)) · ((𝐴↑𝑛) / 𝑛))))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq1( + , 𝐹) ⇝ (arctan‘𝐴))
Theorem	atantayl3 26928*	The Taylor series for arctan(𝐴). (Contributed by Mario Carneiro, 7-Apr-2015.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ ((-1↑𝑛) · ((𝐴↑((2 · 𝑛) + 1)) / ((2 · 𝑛) + 1))))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) < 1) → seq0( + , 𝐹) ⇝ (arctan‘𝐴))
Theorem	leibpilem1 26929	Lemma for leibpi 26931. (Contributed by Mario Carneiro, 7-Apr-2015.) (Proof shortened by Steven Nguyen, 23-Mar-2023.)
⊢ ((𝑁 ∈ ℕ0 ∧ (¬ 𝑁 = 0 ∧ ¬ 2 ∥ 𝑁)) → (𝑁 ∈ ℕ ∧ ((𝑁 − 1) / 2) ∈ ℕ0))
Theorem	leibpilem2 26930*	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 26931	The Leibniz formula for π. This proof depends on three main facts: (1) the series 𝐹 is convergent, because it is an alternating series (iseralt 15645). (2) Using leibpilem2 26930 to rewrite the series as a power series, it is the 𝑥 = 1 special case of the Taylor series for arctan (atantayl2 26927). (3) Although we cannot directly plug 𝑥 = 1 into atantayl2 26927, Abel's theorem (abelth2 26432) 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 26925) 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 26932	The Leibniz formula for π. This version of leibpi 26931 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 26933	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 26934*	Bound the error term in the series of log2cnv 26933. (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 26935	Lemma for log2ub 26938. The proof of log2ub 26938, which is simply the evaluation of log2tlbnd 26934 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 26936*	Lemma for log2ub 26938. (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 26937	Lemma for log2ub 26938. 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 26938	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 26939	log2 is less than 1. This is just a weaker form of log2ub 26938 when no tight upper bound is required. (Contributed by Thierry Arnoux, 27-Sep-2017.)
⊢ (log‘2) < 1
Theorem	birthdaylem1 26940*	Lemma for birthday 26943. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ 𝑆 = {𝑓 ∣ 𝑓:(1...𝐾)⟶(1...𝑁)}    &   ⊢ 𝑇 = {𝑓 ∣ 𝑓:(1...𝐾)–1-1→(1...𝑁)}    ⇒   ⊢ (𝑇 ⊆ 𝑆 ∧ 𝑆 ∈ Fin ∧ (𝑁 ∈ ℕ → 𝑆 ≠ ∅))
Theorem	birthdaylem2 26941*	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 26942*	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 26943*	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 26944	Area of regions in the complex plane.
class area
Definition	df-area 26945*	Define the area of a subset of ℝ × ℝ. (Contributed by Mario Carneiro, 21-Jun-2015.)
⊢ area = (𝑠 ∈ {𝑡 ∈ 𝒫 (ℝ × ℝ) ∣ (∀𝑥 ∈ ℝ (𝑡 “ {𝑥}) ∈ (◡vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦ (vol‘(𝑡 “ {𝑥}))) ∈ 𝐿1)} ↦ ∫ℝ(vol‘(𝑠 “ {𝑥})) d𝑥)
Theorem	dmarea 26946*	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 26947	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 26948	A measurable region is a subset of ℝ × ℝ. (Contributed by Mario Carneiro, 21-Jun-2015.)
⊢ (𝑆 ∈ dom area → 𝑆 ⊆ (ℝ × ℝ))
Theorem	dfarea 26949*	Rewrite df-area 26945 self-referentially. (Contributed by Mario Carneiro, 21-Jun-2015.)
⊢ area = (𝑠 ∈ dom area ↦ ∫ℝ(vol‘(𝑠 “ {𝑥})) d𝑥)
Theorem	areaf 26950	Area measurement is a function whose values are nonnegative reals. (Contributed by Mario Carneiro, 21-Jun-2015.)
⊢ area:dom area⟶(0[,)+∞)
Theorem	areacl 26951	The area of a measurable region is a real number. (Contributed by Mario Carneiro, 21-Jun-2015.)
⊢ (𝑆 ∈ dom area → (area‘𝑆) ∈ ℝ)
Theorem	areage0 26952	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 26953*	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 26954*	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 26955*	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 26956*	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 26957*	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 26958*	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 26959). (Contributed by Mario Carneiro, 1-Mar-2015.) Avoid ax-mulf 11116. (Revised by GG, 19-Apr-2025.)
⊢ 𝑆 = (0(ball‘(abs ∘ − ))(1 / ((abs‘𝐴) + 1)))    ⇒   ⊢ (𝐴 ∈ ℂ → (𝑘 ∈ ℝ+ ↦ ((1 + (𝐴 / 𝑘))↑𝑐𝑘)) ⇝𝑟 (exp‘𝐴))
Theorem	dfef2 26959*	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 26960*	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 26961	The inverse square root function converges to zero. (Contributed by Mario Carneiro, 18-May-2016.)
⊢ (𝑛 ∈ ℝ+ ↦ (1 / (√‘𝑛))) ⇝𝑟 0
Theorem	rlimcxp 26962*	Any power to a positive exponent of a converging sequence also converges. (Contributed by Mario Carneiro, 18-Sep-2014.)
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑛 ∈ 𝐴 ↦ 𝐵) ⇝𝑟 0)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝑛 ∈ 𝐴 ↦ (𝐵↑𝑐𝐶)) ⇝𝑟 0)
Theorem	o1cxp 26963*	An eventually bounded function taken to a nonnegative power is eventually bounded. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 0 ≤ (ℜ‘𝐶))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝑂(1))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ (𝐵↑𝑐𝐶)) ∈ 𝑂(1))
Theorem	cxp2limlem 26964*	A linear factor grows slower than any exponential with base greater than 1. (Contributed by Mario Carneiro, 15-Sep-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 1 < 𝐴) → (𝑛 ∈ ℝ+ ↦ (𝑛 / (𝐴↑𝑐𝑛))) ⇝𝑟 0)
Theorem	cxp2lim 26965*	Any power grows slower than any exponential with base greater than 1. (Contributed by Mario Carneiro, 18-Sep-2014.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → (𝑛 ∈ ℝ+ ↦ ((𝑛↑𝑐𝐴) / (𝐵↑𝑐𝑛))) ⇝𝑟 0)
Theorem	cxploglim 26966*	The logarithm grows slower than any positive power. (Contributed by Mario Carneiro, 18-Sep-2014.)
⊢ (𝐴 ∈ ℝ+ → (𝑛 ∈ ℝ+ ↦ ((log‘𝑛) / (𝑛↑𝑐𝐴))) ⇝𝑟 0)
Theorem	cxploglim2 26967*	Every power of the logarithm grows slower than any positive power. (Contributed by Mario Carneiro, 20-May-2016.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℝ+) → (𝑛 ∈ ℝ+ ↦ (((log‘𝑛)↑𝑐𝐴) / (𝑛↑𝑐𝐵))) ⇝𝑟 0)
Theorem	divsqrtsumlem 26968*	Lemma for divsqrsum 26970 and divsqrtsum2 26971. (Contributed by Mario Carneiro, 18-May-2016.)
⊢ 𝐹 = (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑛)) − (2 · (√‘𝑥))))    ⇒   ⊢ (𝐹:ℝ+⟶ℝ ∧ 𝐹 ∈ dom ⇝𝑟 ∧ ((𝐹 ⇝𝑟 𝐿 ∧ 𝐴 ∈ ℝ+) → (abs‘((𝐹‘𝐴) − 𝐿)) ≤ (1 / (√‘𝐴))))
Theorem	divsqrsumf 26969*	The function 𝐹 used in divsqrsum 26970 is a real function. (Contributed by Mario Carneiro, 12-May-2016.)
⊢ 𝐹 = (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(1 / (√‘𝑛)) − (2 · (√‘𝑥))))    ⇒   ⊢ 𝐹:ℝ+⟶ℝ
Theorem	divsqrsum 26970*	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 26971*	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 26972*	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 26973*	Closure of a 0-1 linear combination in a convex set. (Contributed by Mario Carneiro, 21-Jun-2015.)
⊢ (𝜑 → 𝐷 ⊆ ℝ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷)) → (𝑥[,]𝑦) ⊆ 𝐷)    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌)) ∈ 𝐷)
Theorem	scvxcvx 26974*	A strictly convex function is convex. (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ (𝜑 → 𝐷 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹:𝐷⟶ℝ)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐷 ∧ 𝑏 ∈ 𝐷)) → (𝑎[,]𝑏) ⊆ 𝐷)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))))    ⇒   ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑇 ∈ (0[,]1))) → (𝐹‘((𝑇 · 𝑋) + ((1 − 𝑇) · 𝑌))) ≤ ((𝑇 · (𝐹‘𝑋)) + ((1 − 𝑇) · (𝐹‘𝑌))))
Theorem	jensenlem1 26975*	Lemma for jensen 26977. (Contributed by Mario Carneiro, 4-Jun-2016.)
⊢ (𝜑 → 𝐷 ⊆ ℝ)    &   ⊢ (𝜑 → 𝐹:𝐷⟶ℝ)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐷 ∧ 𝑏 ∈ 𝐷)) → (𝑎[,]𝑏) ⊆ 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝑇:𝐴⟶(0[,)+∞))    &   ⊢ (𝜑 → 𝑋:𝐴⟶𝐷)    &   ⊢ (𝜑 → 0 < (ℂfld Σg 𝑇))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑡 ∈ (0[,]1))) → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ≤ ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦))))    &   ⊢ (𝜑 → ¬ 𝑧 ∈ 𝐵)    &   ⊢ (𝜑 → (𝐵 ∪ {𝑧}) ⊆ 𝐴)    &   ⊢ 𝑆 = (ℂfld Σg (𝑇 ↾ 𝐵))    &   ⊢ 𝐿 = (ℂfld Σg (𝑇 ↾ (𝐵 ∪ {𝑧})))    ⇒   ⊢ (𝜑 → 𝐿 = (𝑆 + (𝑇‘𝑧)))
Theorem	jensenlem2 26976*	Lemma for jensen 26977. (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 26977*	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 26978	Lemma for amgm 26979. (Contributed by Mario Carneiro, 21-Jun-2015.)
⊢ 𝑀 = (mulGrp‘ℂfld)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → 𝐹:𝐴⟶ℝ+)    ⇒   ⊢ (𝜑 → ((𝑀 Σg 𝐹)↑𝑐(1 / (♯‘𝐴))) ≤ ((ℂfld Σg 𝐹) / (♯‘𝐴)))
Theorem	amgm 26979	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 26980	The Euler-Mascheroni constant. (The label abbreviates Euler-Mascheroni.)
class γ
Definition	df-em 26981	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 26991. (Contributed by Mario Carneiro, 11-Jul-2014.)
⊢ γ = Σ𝑘 ∈ ℕ ((1 / 𝑘) − (log‘(1 + (1 / 𝑘))))
Theorem	logdifbnd 26982	Bound on the difference of logs. (Contributed by Mario Carneiro, 23-May-2016.)
⊢ (𝐴 ∈ ℝ+ → ((log‘(𝐴 + 1)) − (log‘𝐴)) ≤ (1 / 𝐴))
Theorem	logdiflbnd 26983	Lower bound on the difference of logs. (Contributed by Mario Carneiro, 3-Jul-2017.)
⊢ (𝐴 ∈ ℝ+ → (1 / (𝐴 + 1)) ≤ ((log‘(𝐴 + 1)) − (log‘𝐴)))
Theorem	emcllem1 26984*	Lemma for emcl 26991. 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 26985*	Lemma for emcl 26991. 𝐹 is increasing, and 𝐺 is decreasing. (Contributed by Mario Carneiro, 11-Jul-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘𝑛)))    &   ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (Σ𝑚 ∈ (1...𝑛)(1 / 𝑚) − (log‘(𝑛 + 1))))    ⇒   ⊢ (𝑁 ∈ ℕ → ((𝐹‘(𝑁 + 1)) ≤ (𝐹‘𝑁) ∧ (𝐺‘𝑁) ≤ (𝐺‘(𝑁 + 1))))
Theorem	emcllem3 26986*	Lemma for emcl 26991. 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 26987*	Lemma for emcl 26991. 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 26988*	Lemma for emcl 26991. The partial sums of the series 𝑇, which is used in Definition df-em 26981, 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 26989*	Lemma for emcl 26991. 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 26990*	Lemma for emcl 26991 and harmonicbnd 26992. 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 26991	Closure and bounds for the Euler-Mascheroni constant. (Contributed by Mario Carneiro, 11-Jul-2014.)
⊢ γ ∈ ((1 − (log‘2))[,]1)
Theorem	harmonicbnd 26992*	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 26993*	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 26994	The Euler-Mascheroni constant is a real number. (Contributed by Mario Carneiro, 11-Jul-2014.)
⊢ γ ∈ ℝ
Theorem	emgt0 26995	The Euler-Mascheroni constant is positive. (Contributed by Mario Carneiro, 11-Jul-2014.)
⊢ 0 < γ
Theorem	harmonicbnd3 26996*	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 26997*	A bound on the harmonic series, as compared to the natural logarithm. (Contributed by Mario Carneiro, 13-Apr-2016.)
⊢ (𝐴 ∈ ℝ+ → (log‘𝐴) ≤ Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚))
Theorem	harmonicubnd 26998*	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 26999*	The asymptotic behavior of Σ𝑚 ≤ 𝐴, 1 / 𝑚 = log𝐴 + γ + 𝑂(1 / 𝐴). (Contributed by Mario Carneiro, 14-May-2016.)
⊢ (𝐴 ∈ ℝ+ → (abs‘(Σ𝑚 ∈ (1...(⌊‘𝐴))(1 / 𝑚) − ((log‘𝐴) + γ))) ≤ (1 / 𝐴))
Theorem	fsumharmonic 27000*	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))))