Definition df-em 25570

Description: Define the Euler-Mascheroni constant, γ = 0.577.... This is the limit of the series Σ𝑘 ∈ (1...𝑚)(1 / 𝑘) − (log‘𝑚), with a proof that the limit exists in emcl 25580. (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 25569	. 2 class γ
2		cn 11638	. . 3 class ℕ
3		c1 10538	. . . . 5 class 1
4		vk	. . . . . 6 setvar 𝑘
5	4	cv 1536	. . . . 5 class 𝑘
6		cdiv 11297	. . . . 5 class /
7	3, 5, 6	co 7156	. . . 4 class (1 / 𝑘)
8		caddc 10540	. . . . . 6 class +
9	3, 7, 8	co 7156	. . . . 5 class (1 + (1 / 𝑘))
10		clog 25138	. . . . 5 class log
11	9, 10	cfv 6355	. . . 4 class (log‘(1 + (1 / 𝑘)))
12		cmin 10870	. . . 4 class −
13	7, 11, 12	co 7156	. . 3 class ((1 / 𝑘) − (log‘(1 + (1 / 𝑘))))
14	2, 13, 4	csu 15042	. 2 class Σ𝑘 ∈ ℕ ((1 / 𝑘) − (log‘(1 + (1 / 𝑘))))
15	1, 14	wceq 1537	1 wff γ = Σ𝑘 ∈ ℕ ((1 / 𝑘) − (log‘(1 + (1 / 𝑘))))

This definition is referenced by:  emcllem6  25578