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)
|- gamma = sum_ k e. NN ( ( 1 / k ) - ( log ` ( 1 + ( 1 / k ) ) ) )
|- gamma
|- k
|- NN
|- 1
|- /
|- ( 1 / k )
|- -
|- log
|- +
|- ( 1 + ( 1 / k ) )
|- ( log ` ( 1 + ( 1 / k ) ) )
|- ( ( 1 / k ) - ( log ` ( 1 + ( 1 / k ) ) ) )
|- sum_ k e. NN ( ( 1 / k ) - ( log ` ( 1 + ( 1 / k ) ) ) )