# 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 𝐹 = ( 𝑛 ∈ ℕ ↦ ( Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) − ( log ‘ 𝑛 ) ) )
emcl.2 𝐺 = ( 𝑛 ∈ ℕ ↦ ( Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑛 + 1 ) ) ) )
Assertion emcllem1 ( 𝐹 : ℕ ⟶ ℝ ∧ 𝐺 : ℕ ⟶ ℝ )

### Proof

Step Hyp Ref Expression
1 emcl.1 𝐹 = ( 𝑛 ∈ ℕ ↦ ( Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) − ( log ‘ 𝑛 ) ) )
2 emcl.2 𝐺 = ( 𝑛 ∈ ℕ ↦ ( Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑛 + 1 ) ) ) )
3 fzfid ( 𝑛 ∈ ℕ → ( 1 ... 𝑛 ) ∈ Fin )
4 elfznn ( 𝑚 ∈ ( 1 ... 𝑛 ) → 𝑚 ∈ ℕ )
5 4 adantl ( ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ( 1 ... 𝑛 ) ) → 𝑚 ∈ ℕ )
6 5 nnrecred ( ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ( 1 ... 𝑛 ) ) → ( 1 / 𝑚 ) ∈ ℝ )
7 3 6 fsumrecl ( 𝑛 ∈ ℕ → Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) ∈ ℝ )
8 nnrp ( 𝑛 ∈ ℕ → 𝑛 ∈ ℝ+ )
9 8 relogcld ( 𝑛 ∈ ℕ → ( log ‘ 𝑛 ) ∈ ℝ )
10 7 9 resubcld ( 𝑛 ∈ ℕ → ( Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) − ( log ‘ 𝑛 ) ) ∈ ℝ )
11 1 10 fmpti 𝐹 : ℕ ⟶ ℝ
12 peano2nn ( 𝑛 ∈ ℕ → ( 𝑛 + 1 ) ∈ ℕ )
13 12 nnrpd ( 𝑛 ∈ ℕ → ( 𝑛 + 1 ) ∈ ℝ+ )
14 13 relogcld ( 𝑛 ∈ ℕ → ( log ‘ ( 𝑛 + 1 ) ) ∈ ℝ )
15 7 14 resubcld ( 𝑛 ∈ ℕ → ( Σ 𝑚 ∈ ( 1 ... 𝑛 ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑛 + 1 ) ) ) ∈ ℝ )
16 2 15 fmpti 𝐺 : ℕ ⟶ ℝ
17 11 16 pm3.2i ( 𝐹 : ℕ ⟶ ℝ ∧ 𝐺 : ℕ ⟶ ℝ )