# Metamath Proof Explorer

## Theorem emcllem1

Description: Lemma for emcl . The series F and G are sequences of real numbers that approach gamma from above and below, respectively. (Contributed by Mario Carneiro, 11-Jul-2014)

Ref Expression
Hypotheses emcl.1 ${⊢}{F}=\left({n}\in ℕ⟼\sum _{{m}=1}^{{n}}\left(\frac{1}{{m}}\right)-\mathrm{log}{n}\right)$
emcl.2 ${⊢}{G}=\left({n}\in ℕ⟼\sum _{{m}=1}^{{n}}\left(\frac{1}{{m}}\right)-\mathrm{log}\left({n}+1\right)\right)$
Assertion emcllem1 ${⊢}\left({F}:ℕ⟶ℝ\wedge {G}:ℕ⟶ℝ\right)$

### Proof

Step Hyp Ref Expression
1 emcl.1 ${⊢}{F}=\left({n}\in ℕ⟼\sum _{{m}=1}^{{n}}\left(\frac{1}{{m}}\right)-\mathrm{log}{n}\right)$
2 emcl.2 ${⊢}{G}=\left({n}\in ℕ⟼\sum _{{m}=1}^{{n}}\left(\frac{1}{{m}}\right)-\mathrm{log}\left({n}+1\right)\right)$
3 fzfid ${⊢}{n}\in ℕ\to \left(1\dots {n}\right)\in \mathrm{Fin}$
4 elfznn ${⊢}{m}\in \left(1\dots {n}\right)\to {m}\in ℕ$
5 4 adantl ${⊢}\left({n}\in ℕ\wedge {m}\in \left(1\dots {n}\right)\right)\to {m}\in ℕ$
6 5 nnrecred ${⊢}\left({n}\in ℕ\wedge {m}\in \left(1\dots {n}\right)\right)\to \frac{1}{{m}}\in ℝ$
7 3 6 fsumrecl ${⊢}{n}\in ℕ\to \sum _{{m}=1}^{{n}}\left(\frac{1}{{m}}\right)\in ℝ$
8 nnrp ${⊢}{n}\in ℕ\to {n}\in {ℝ}^{+}$
9 8 relogcld ${⊢}{n}\in ℕ\to \mathrm{log}{n}\in ℝ$
10 7 9 resubcld ${⊢}{n}\in ℕ\to \sum _{{m}=1}^{{n}}\left(\frac{1}{{m}}\right)-\mathrm{log}{n}\in ℝ$
11 1 10 fmpti ${⊢}{F}:ℕ⟶ℝ$
12 peano2nn ${⊢}{n}\in ℕ\to {n}+1\in ℕ$
13 12 nnrpd ${⊢}{n}\in ℕ\to {n}+1\in {ℝ}^{+}$
14 13 relogcld ${⊢}{n}\in ℕ\to \mathrm{log}\left({n}+1\right)\in ℝ$
15 7 14 resubcld ${⊢}{n}\in ℕ\to \sum _{{m}=1}^{{n}}\left(\frac{1}{{m}}\right)-\mathrm{log}\left({n}+1\right)\in ℝ$
16 2 15 fmpti ${⊢}{G}:ℕ⟶ℝ$
17 11 16 pm3.2i ${⊢}\left({F}:ℕ⟶ℝ\wedge {G}:ℕ⟶ℝ\right)$