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	$$⊢\gamma =\sum _{k\in \mathbb{N}}\left(\left(\frac{1}{k}\right)-\log \left(1+\left(\frac{1}{k}\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cem	$$class\gamma$$
1		vk	$$setvark$$
2		cn	$$class\mathbb{N}$$
3		c1	$$class1$$
4		cdiv	$$class÷$$
5	1	cv	$$setvark$$
6	3 5 4	co	$$class\left(\frac{1}{k}\right)$$
7		cmin	$$class-$$
8		clog	$$classlog$$
9		caddc	$$class+$$
10	3 6 9	co	$$class\left(1+\left(\frac{1}{k}\right)\right)$$
11	10 8	cfv	$$class\log \left(1+\left(\frac{1}{k}\right)\right)$$
12	6 11 7	co	$$class\left(\left(\frac{1}{k}\right)-\log \left(1+\left(\frac{1}{k}\right)\right)\right)$$
13	2 12 1	csu	$$class\sum _{k\in \mathbb{N}}\left(\left(\frac{1}{k}\right)-\log \left(1+\left(\frac{1}{k}\right)\right)\right)$$
14	0 13	wceq	$$wff\gamma =\sum _{k\in \mathbb{N}}\left(\left(\frac{1}{k}\right)-\log \left(1+\left(\frac{1}{k}\right)\right)\right)$$