Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-em | Structured version Visualization version GIF version |
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 25909. (Contributed by Mario Carneiro, 11-Jul-2014.) |
Ref | Expression |
---|---|
df-em | ⊢ γ = Σ𝑘 ∈ ℕ ((1 / 𝑘) − (log‘(1 + (1 / 𝑘)))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cem 25898 | . 2 class γ | |
2 | cn 11854 | . . 3 class ℕ | |
3 | c1 10754 | . . . . 5 class 1 | |
4 | vk | . . . . . 6 setvar 𝑘 | |
5 | 4 | cv 1542 | . . . . 5 class 𝑘 |
6 | cdiv 11513 | . . . . 5 class / | |
7 | 3, 5, 6 | co 7231 | . . . 4 class (1 / 𝑘) |
8 | caddc 10756 | . . . . . 6 class + | |
9 | 3, 7, 8 | co 7231 | . . . . 5 class (1 + (1 / 𝑘)) |
10 | clog 25467 | . . . . 5 class log | |
11 | 9, 10 | cfv 6397 | . . . 4 class (log‘(1 + (1 / 𝑘))) |
12 | cmin 11086 | . . . 4 class − | |
13 | 7, 11, 12 | co 7231 | . . 3 class ((1 / 𝑘) − (log‘(1 + (1 / 𝑘)))) |
14 | 2, 13, 4 | csu 15273 | . 2 class Σ𝑘 ∈ ℕ ((1 / 𝑘) − (log‘(1 + (1 / 𝑘)))) |
15 | 1, 14 | wceq 1543 | 1 wff γ = Σ𝑘 ∈ ℕ ((1 / 𝑘) − (log‘(1 + (1 / 𝑘)))) |
Colors of variables: wff setvar class |
This definition is referenced by: emcllem6 25907 |
Copyright terms: Public domain | W3C validator |