Definition df-em

Description: Define the Euler-Mascheroni constant, gamma = 0.577.... This is the limit of the series sum_ k e. ( 1 ... m ) ( 1 / k ) - ( logm ) , with a proof that the limit exists in emcl . (Contributed by Mario Carneiro, 11-Jul-2014)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cem	⊢ γ
1		vk	⊢ 𝑘
2		cn	⊢ ℕ
3		c1	⊢ 1
4		cdiv	⊢ /
5	1	cv	⊢ 𝑘
6	3 5 4	co	⊢ ( 1 / 𝑘 )
7		cmin	⊢ −
8		clog	⊢ log
9		caddc	⊢ +
10	3 6 9	co	⊢ ( 1 + ( 1 / 𝑘 ) )
11	10 8	cfv	⊢ ( log ‘ ( 1 + ( 1 / 𝑘 ) ) )
12	6 11 7	co	⊢ ( ( 1 / 𝑘 ) − ( log ‘ ( 1 + ( 1 / 𝑘 ) ) ) )
13	2 12 1	csu	⊢ Σ 𝑘 ∈ ℕ ( ( 1 / 𝑘 ) − ( log ‘ ( 1 + ( 1 / 𝑘 ) ) ) )
14	0 13	wceq	⊢ γ = Σ 𝑘 ∈ ℕ ( ( 1 / 𝑘 ) − ( log ‘ ( 1 + ( 1 / 𝑘 ) ) ) )