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