Database
BASIC REAL AND COMPLEX FUNCTIONS
Basic trigonometry
Euler-Mascheroni constant
df-em
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 ) - ( log m ) ,
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 ) ) ) )