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

Definition df-em 20303
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 20312. (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 20302 . 2  class  gamma
2 cn 9762 . . 3  class  NN
3 c1 8754 . . . . 5  class  1
4 vk . . . . . 6  set  k
54cv 1631 . . . . 5  class  k
6 cdiv 9439 . . . . 5  class  /
73, 5, 6co 5874 . . . 4  class  ( 1  /  k )
8 caddc 8756 . . . . . 6  class  +
93, 7, 8co 5874 . . . . 5  class  ( 1  +  ( 1  / 
k ) )
10 clog 19928 . . . . 5  class  log
119, 10cfv 5271 . . . 4  class  ( log `  ( 1  +  ( 1  /  k ) ) )
12 cmin 9053 . . . 4  class  -
137, 11, 12co 5874 . . 3  class  ( ( 1  /  k )  -  ( log `  (
1  +  ( 1  /  k ) ) ) )
142, 13, 4csu 12174 . 2  class  sum_ k  e.  NN  ( ( 1  /  k )  -  ( log `  ( 1  +  ( 1  / 
k ) ) ) )
151, 14wceq 1632 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  20310
  Copyright terms: Public domain W3C validator