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

Definition df-em 20287
Description: Define the Euler-Macheroni 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 20296. (Contributed by Mario Carneiro, 11-Jul-2014.)
Assertion
Ref Expression
df-em  |-  gamma  =  sum_ k  e.  NN  (
( 1  /  k
)  -  ( log `  ( 1  +  ( 1  /  k ) ) ) )

Detailed syntax breakdown of Definition df-em
StepHypRef Expression
1 cem 20286 . 2  class  gamma
2 cn 9746 . . 3  class  NN
3 c1 8738 . . . . 5  class  1
4 vk . . . . . 6  set  k
54cv 1622 . . . . 5  class  k
6 cdiv 9423 . . . . 5  class  /
73, 5, 6co 5858 . . . 4  class  ( 1  /  k )
8 caddc 8740 . . . . . 6  class  +
93, 7, 8co 5858 . . . . 5  class  ( 1  +  ( 1  / 
k ) )
10 clog 19912 . . . . 5  class  log
119, 10cfv 5255 . . . 4  class  ( log `  ( 1  +  ( 1  /  k ) ) )
12 cmin 9037 . . . 4  class  -
137, 11, 12co 5858 . . 3  class  ( ( 1  /  k )  -  ( log `  (
1  +  ( 1  /  k ) ) ) )
142, 13, 4csu 12158 . 2  class  sum_ k  e.  NN  ( ( 1  /  k )  -  ( log `  ( 1  +  ( 1  / 
k ) ) ) )
151, 14wceq 1623 1  wff  gamma  =  sum_ k  e.  NN  (
( 1  /  k
)  -  ( log `  ( 1  +  ( 1  /  k ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  emcllem6  20294
  Copyright terms: Public domain W3C validator