MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-em Structured version   Visualization version   GIF version

Definition df-em 24436
Description: Define the Euler-Mascheroni constant, γ = 0.577... . This is the limit of the series Σ𝑘 ∈ (1...𝑚)(1 / 𝑘) − (log‘𝑚), with a proof that the limit exists in emcl 24446. (Contributed by Mario Carneiro, 11-Jul-2014.)
Assertion
Ref Expression
df-em γ = Σ𝑘 ∈ ℕ ((1 / 𝑘) − (log‘(1 + (1 / 𝑘))))

Detailed syntax breakdown of Definition df-em
StepHypRef Expression
1 cem 24435 . 2 class γ
2 cn 10867 . . 3 class
3 c1 9793 . . . . 5 class 1
4 vk . . . . . 6 setvar 𝑘
54cv 1473 . . . . 5 class 𝑘
6 cdiv 10533 . . . . 5 class /
73, 5, 6co 6527 . . . 4 class (1 / 𝑘)
8 caddc 9795 . . . . . 6 class +
93, 7, 8co 6527 . . . . 5 class (1 + (1 / 𝑘))
10 clog 24022 . . . . 5 class log
119, 10cfv 5790 . . . 4 class (log‘(1 + (1 / 𝑘)))
12 cmin 10117 . . . 4 class
137, 11, 12co 6527 . . 3 class ((1 / 𝑘) − (log‘(1 + (1 / 𝑘))))
142, 13, 4csu 14210 . 2 class Σ𝑘 ∈ ℕ ((1 / 𝑘) − (log‘(1 + (1 / 𝑘))))
151, 14wceq 1474 1 wff γ = Σ𝑘 ∈ ℕ ((1 / 𝑘) − (log‘(1 + (1 / 𝑘))))
Colors of variables: wff setvar class
This definition is referenced by:  emcllem6  24444
  Copyright terms: Public domain W3C validator