Definition df-em 26497

Description: 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 26507. (Contributed by Mario Carneiro, 11-Jul-2014.)

Assertion

Ref	Expression
df-em	⊢ γ = Σ𝑘 ∈ ℕ ((1 / 𝑘) − (log‘(1 + (1 / 𝑘))))

Detailed syntax breakdown of Definition df-em

Step	Hyp	Ref	Expression
1		cem 26496	. 2 class γ
2		cn 12212	. . 3 class ℕ
3		c1 11111	. . . . 5 class 1
4		vk	. . . . . 6 setvar 𝑘
5	4	cv 1541	. . . . 5 class 𝑘
6		cdiv 11871	. . . . 5 class /
7	3, 5, 6	co 7409	. . . 4 class (1 / 𝑘)
8		caddc 11113	. . . . . 6 class +
9	3, 7, 8	co 7409	. . . . 5 class (1 + (1 / 𝑘))
10		clog 26063	. . . . 5 class log
11	9, 10	cfv 6544	. . . 4 class (log‘(1 + (1 / 𝑘)))
12		cmin 11444	. . . 4 class −
13	7, 11, 12	co 7409	. . 3 class ((1 / 𝑘) − (log‘(1 + (1 / 𝑘))))
14	2, 13, 4	csu 15632	. 2 class Σ𝑘 ∈ ℕ ((1 / 𝑘) − (log‘(1 + (1 / 𝑘))))
15	1, 14	wceq 1542	1 wff γ = Σ𝑘 ∈ ℕ ((1 / 𝑘) − (log‘(1 + (1 / 𝑘))))

This definition is referenced by:  emcllem6  26505