This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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