Definition df-em

Description: Define the Euler-Mascheroni constant, gamma = 0.57721.... 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	|- gamma = sum_ k e. NN ( ( 1 / k ) - ( log ` ( 1 + ( 1 / k ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cem	|- gamma
1		vk	|- k
2		cn	|- NN
3		c1	|- 1
4		cdiv	|- /
5	1	cv	|- k
6	3 5 4	co	|- ( 1 / k )
7		cmin	|- -
8		clog	|- log
9		caddc	|- +
10	3 6 9	co	|- ( 1 + ( 1 / k ) )
11	10 8	cfv	|- ( log ` ( 1 + ( 1 / k ) ) )
12	6 11 7	co	|- ( ( 1 / k ) - ( log ` ( 1 + ( 1 / k ) ) ) )
13	2 12 1	csu	|- sum_ k e. NN ( ( 1 / k ) - ( log ` ( 1 + ( 1 / k ) ) ) )
14	0 13	wceq	|- gamma = sum_ k e. NN ( ( 1 / k ) - ( log ` ( 1 + ( 1 / k ) ) ) )