Metamath Proof Explorer

Theorem emcl

Description: Closure and bounds for the Euler-Mascheroni constant. (Contributed by Mario Carneiro, 11-Jul-2014)

Ref Expression
Assertion emcl ${⊢}\gamma \in \left[1-\mathrm{log}2,1\right]$

Proof

Step Hyp Ref Expression
1 eqid ${⊢}\left({n}\in ℕ⟼\sum _{{m}=1}^{{n}}\left(\frac{1}{{m}}\right)-\mathrm{log}{n}\right)=\left({n}\in ℕ⟼\sum _{{m}=1}^{{n}}\left(\frac{1}{{m}}\right)-\mathrm{log}{n}\right)$
2 eqid ${⊢}\left({n}\in ℕ⟼\sum _{{m}=1}^{{n}}\left(\frac{1}{{m}}\right)-\mathrm{log}\left({n}+1\right)\right)=\left({n}\in ℕ⟼\sum _{{m}=1}^{{n}}\left(\frac{1}{{m}}\right)-\mathrm{log}\left({n}+1\right)\right)$
3 eqid ${⊢}\left({n}\in ℕ⟼\mathrm{log}\left(1+\left(\frac{1}{{n}}\right)\right)\right)=\left({n}\in ℕ⟼\mathrm{log}\left(1+\left(\frac{1}{{n}}\right)\right)\right)$
4 oveq2 ${⊢}{k}={n}\to \frac{1}{{k}}=\frac{1}{{n}}$
5 4 oveq2d ${⊢}{k}={n}\to 1+\left(\frac{1}{{k}}\right)=1+\left(\frac{1}{{n}}\right)$
6 5 fveq2d ${⊢}{k}={n}\to \mathrm{log}\left(1+\left(\frac{1}{{k}}\right)\right)=\mathrm{log}\left(1+\left(\frac{1}{{n}}\right)\right)$
7 4 6 oveq12d ${⊢}{k}={n}\to \left(\frac{1}{{k}}\right)-\mathrm{log}\left(1+\left(\frac{1}{{k}}\right)\right)=\left(\frac{1}{{n}}\right)-\mathrm{log}\left(1+\left(\frac{1}{{n}}\right)\right)$
8 7 cbvmptv ${⊢}\left({k}\in ℕ⟼\left(\frac{1}{{k}}\right)-\mathrm{log}\left(1+\left(\frac{1}{{k}}\right)\right)\right)=\left({n}\in ℕ⟼\left(\frac{1}{{n}}\right)-\mathrm{log}\left(1+\left(\frac{1}{{n}}\right)\right)\right)$
9 1 2 3 8 emcllem7 ${⊢}\left(\gamma \in \left[1-\mathrm{log}2,1\right]\wedge \left({n}\in ℕ⟼\sum _{{m}=1}^{{n}}\left(\frac{1}{{m}}\right)-\mathrm{log}{n}\right):ℕ⟶\left[\gamma ,1\right]\wedge \left({n}\in ℕ⟼\sum _{{m}=1}^{{n}}\left(\frac{1}{{m}}\right)-\mathrm{log}\left({n}+1\right)\right):ℕ⟶\left[1-\mathrm{log}2,\gamma \right]\right)$
10 9 simp1i ${⊢}\gamma \in \left[1-\mathrm{log}2,1\right]$