Metamath Proof Explorer


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 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 ) ) ) )