This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝐹 : ℕ ⟶ ℝ ∧ 𝐺 : ℕ ⟶ ℝ )