This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database BASIC REAL AND COMPLEX FUNCTIONS Basic trigonometry Euler-Mascheroni constant df-em
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 ) - ( log m ) ,
with a proof that the limit exists in emcl . (Contributed by Mario
Carneiro , 11-Jul-2014)
Ref
Expression
Assertion
df-em ⊢ γ = Σ 𝑘 ∈ ℕ ( ( 1 / 𝑘 ) − ( log ‘ ( 1 + ( 1 / 𝑘 ) ) ) )
Detailed syntax breakdown
Step
Hyp
Ref
Expression
0
cem ⊢ γ
1
vk ⊢ 𝑘
2
cn ⊢ ℕ
3
c1 ⊢ 1
4
cdiv ⊢ /
5
1
cv ⊢ 𝑘
6
3 5 4
co ⊢ ( 1 / 𝑘 )
7
cmin ⊢ −
8
clog ⊢ log
9
caddc ⊢ +
10
3 6 9
co ⊢ ( 1 + ( 1 / 𝑘 ) )
11
10 8
cfv ⊢ ( log ‘ ( 1 + ( 1 / 𝑘 ) ) )
12
6 11 7
co ⊢ ( ( 1 / 𝑘 ) − ( log ‘ ( 1 + ( 1 / 𝑘 ) ) ) )
13
2 12 1
csu ⊢ Σ 𝑘 ∈ ℕ ( ( 1 / 𝑘 ) − ( log ‘ ( 1 + ( 1 / 𝑘 ) ) ) )
14
0 13
wceq ⊢ γ = Σ 𝑘 ∈ ℕ ( ( 1 / 𝑘 ) − ( log ‘ ( 1 + ( 1 / 𝑘 ) ) ) )