Definition of the Euler--Mascheroni constant

[benjub]

The comment for the definition of the Euler--Mascheroni constant (https://us.metamath.org/mpeuni/df-em.html) gives the standard definition, but the formal definition actually uses a characterization, namely, it is currently

$a |- gamma = sum_ k e. NN ( ( 1 / k ) - ( log ` ( 1 + ( 1 / k ) ) ) ) $.

(maybe in order to avoid a dummy variable). However, the standard definition is

$a |- gamma = ( ~~> ` ( n e. NN |-> ( sum_ m e. ( 1 ... n ) ( 1 / m ) - ( log ` n ) ) ) ) $.

This should be our definition too, and the current definition should be a theorem. (Or if there is a strong preference for using the current definition because it has no dummy variables, then at least the standard definition should be added to the database as a theorem.)

That theorem is easy at a non-formalized level (convergence and telescoping sum), and the formalization is actually already contained (among stronger results) in some proofs of that section. See where https://us.metamath.org/mpeuni/emcllem5.html uses telfsum2. So it may just be a matter of refactoring some existing proofs.