Definition df-em 23520

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

Assertion

Ref	Expression
df-em	|- gamma = sum_ k e. NN ( ( 1 / k ) - ( log ` ( 1 + ( 1 / k ) ) ) )

Detailed syntax breakdown of Definition df-em

Step	Hyp	Ref	Expression
1		cem 23519	. 2 class gamma
2		cn 10531	. . 3 class NN
3		c1 9482	. . . . 5 class 1
4		vk	. . . . . 6 setvar k
5	4	cv 1397	. . . . 5 class k
6		cdiv 10202	. . . . 5 class /
7	3, 5, 6	co 6270	. . . 4 class ( 1 / k )
8		caddc 9484	. . . . . 6 class +
9	3, 7, 8	co 6270	. . . . 5 class ( 1 + ( 1 / k ) )
10		clog 23108	. . . . 5 class log
11	9, 10	cfv 5570	. . . 4 class ( log ` ( 1 + ( 1 / k ) ) )
12		cmin 9796	. . . 4 class -
13	7, 11, 12	co 6270	. . 3 class ( ( 1 / k ) - ( log ` ( 1 + ( 1 / k ) ) ) )
14	2, 13, 4	csu 13590	. 2 class sum_ k e. NN ( ( 1 / k ) - ( log ` ( 1 + ( 1 / k ) ) ) )
15	1, 14	wceq 1398	1 wff gamma = sum_ k e. NN ( ( 1 / k ) - ( log ` ( 1 + ( 1 / k ) ) ) )

This definition is referenced by:  emcllem6  23528