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

Definition df-em 22271
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 22281. (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 22270 . 2  class  gamma
2 cn 10310 . . 3  class  NN
3 c1 9271 . . . . 5  class  1
4 vk . . . . . 6  setvar  k
54cv 1361 . . . . 5  class  k
6 cdiv 9981 . . . . 5  class  /
73, 5, 6co 6080 . . . 4  class  ( 1  /  k )
8 caddc 9273 . . . . . 6  class  +
93, 7, 8co 6080 . . . . 5  class  ( 1  +  ( 1  / 
k ) )
10 clog 21891 . . . . 5  class  log
119, 10cfv 5406 . . . 4  class  ( log `  ( 1  +  ( 1  /  k ) ) )
12 cmin 9583 . . . 4  class  -
137, 11, 12co 6080 . . 3  class  ( ( 1  /  k )  -  ( log `  (
1  +  ( 1  /  k ) ) ) )
142, 13, 4csu 13147 . 2  class  sum_ k  e.  NN  ( ( 1  /  k )  -  ( log `  ( 1  +  ( 1  / 
k ) ) ) )
151, 14wceq 1362 1  wff  gamma  =  sum_ k  e.  NN  (
( 1  /  k
)  -  ( log `  ( 1  +  ( 1  /  k ) ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  emcllem6  22279
  Copyright terms: Public domain W3C validator