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 = n ∈ ℕ ⟼ ∑ m = 1 n 1 m − log ⁡ n
emcl.2 ⊢ G = n ∈ ℕ ⟼ ∑ m = 1 n 1 m − log ⁡ n + 1
Assertion emcllem1 ⊢ F : ℕ ⟶ ℝ ∧ G : ℕ ⟶ ℝ

Proof

Step Hyp Ref Expression
1 emcl.1 ⊢ F = n ∈ ℕ ⟼ ∑ m = 1 n 1 m − log ⁡ n
2 emcl.2 ⊢ G = n ∈ ℕ ⟼ ∑ m = 1 n 1 m − log ⁡ n + 1
3 fzfid ⊢ n ∈ ℕ → 1 … n ∈ Fin
4 elfznn ⊢ m ∈ 1 … n → m ∈ ℕ
5 4 adantl ⊢ n ∈ ℕ ∧ m ∈ 1 … n → m ∈ ℕ
6 5 nnrecred ⊢ n ∈ ℕ ∧ m ∈ 1 … n → 1 m ∈ ℝ
7 3 6 fsumrecl ⊢ n ∈ ℕ → ∑ m = 1 n 1 m ∈ ℝ
8 nnrp ⊢ n ∈ ℕ → n ∈ ℝ +
9 8 relogcld ⊢ n ∈ ℕ → log ⁡ n ∈ ℝ
10 7 9 resubcld ⊢ n ∈ ℕ → ∑ m = 1 n 1 m − log ⁡ n ∈ ℝ
11 1 10 fmpti ⊢ F : ℕ ⟶ ℝ
12 peano2nn ⊢ n ∈ ℕ → n + 1 ∈ ℕ
13 12 nnrpd ⊢ n ∈ ℕ → n + 1 ∈ ℝ +
14 13 relogcld ⊢ n ∈ ℕ → log ⁡ n + 1 ∈ ℝ
15 7 14 resubcld ⊢ n ∈ ℕ → ∑ m = 1 n 1 m − log ⁡ n + 1 ∈ ℝ
16 2 15 fmpti ⊢ G : ℕ ⟶ ℝ
17 11 16 pm3.2i ⊢ F : ℕ ⟶ ℝ ∧ G : ℕ ⟶ ℝ