Definition df-em 26047

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 26057. (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 26046	. 2 class γ
2		cn 11903	. . 3 class ℕ
3		c1 10803	. . . . 5 class 1
4		vk	. . . . . 6 setvar 𝑘
5	4	cv 1538	. . . . 5 class 𝑘
6		cdiv 11562	. . . . 5 class /
7	3, 5, 6	co 7255	. . . 4 class (1 / 𝑘)
8		caddc 10805	. . . . . 6 class +
9	3, 7, 8	co 7255	. . . . 5 class (1 + (1 / 𝑘))
10		clog 25615	. . . . 5 class log
11	9, 10	cfv 6418	. . . 4 class (log‘(1 + (1 / 𝑘)))
12		cmin 11135	. . . 4 class −
13	7, 11, 12	co 7255	. . 3 class ((1 / 𝑘) − (log‘(1 + (1 / 𝑘))))
14	2, 13, 4	csu 15325	. 2 class Σ𝑘 ∈ ℕ ((1 / 𝑘) − (log‘(1 + (1 / 𝑘))))
15	1, 14	wceq 1539	1 wff γ = Σ𝑘 ∈ ℕ ((1 / 𝑘) − (log‘(1 + (1 / 𝑘))))

This definition is referenced by:  emcllem6  26055