Definition df-em 27037

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 27047. (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 27036	. 2 class γ
2		cn 12267	. . 3 class ℕ
3		c1 11157	. . . . 5 class 1
4		vk	. . . . . 6 setvar 𝑘
5	4	cv 1538	. . . . 5 class 𝑘
6		cdiv 11921	. . . . 5 class /
7	3, 5, 6	co 7432	. . . 4 class (1 / 𝑘)
8		caddc 11159	. . . . . 6 class +
9	3, 7, 8	co 7432	. . . . 5 class (1 + (1 / 𝑘))
10		clog 26597	. . . . 5 class log
11	9, 10	cfv 6560	. . . 4 class (log‘(1 + (1 / 𝑘)))
12		cmin 11493	. . . 4 class −
13	7, 11, 12	co 7432	. . 3 class ((1 / 𝑘) − (log‘(1 + (1 / 𝑘))))
14	2, 13, 4	csu 15723	. 2 class Σ𝑘 ∈ ℕ ((1 / 𝑘) − (log‘(1 + (1 / 𝑘))))
15	1, 14	wceq 1539	1 wff γ = Σ𝑘 ∈ ℕ ((1 / 𝑘) − (log‘(1 + (1 / 𝑘))))

This definition is referenced by:  emcllem6  27045