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 \in ℕ ⟼ \sum_{m = 1}^{n} (\frac{1}{m}) - \log n)$
		emcl.2	$⊢ G = (n \in ℕ ⟼ \sum_{m = 1}^{n} (\frac{1}{m}) - \log (n + 1))$
	Assertion	emcllem1	$⊢ (F : ℕ ⟶ ℝ \land G : ℕ ⟶ ℝ)$

Proof

Step	Hyp	Ref	Expression
1		emcl.1	$⊢ F = (n \in ℕ ⟼ \sum_{m = 1}^{n} (\frac{1}{m}) - \log n)$
2		emcl.2	$⊢ G = (n \in ℕ ⟼ \sum_{m = 1}^{n} (\frac{1}{m}) - \log (n + 1))$
3		fzfid	$⊢ n \in ℕ \to (1 \dots n) \in Fin$
4		elfznn	$⊢ m \in (1 \dots n) \to m \in ℕ$
5	4	adantl	$⊢ (n \in ℕ \land m \in (1 \dots n)) \to m \in ℕ$
6	5	nnrecred	$⊢ (n \in ℕ \land m \in (1 \dots n)) \to \frac{1}{m} \in ℝ$
7	3 6	fsumrecl	$⊢ n \in ℕ \to \sum_{m = 1}^{n} (\frac{1}{m}) \in ℝ$
8		nnrp	$⊢ n \in ℕ \to n \in ℝ^{+}$
9	8	relogcld	$⊢ n \in ℕ \to \log n \in ℝ$
10	7 9	resubcld	$⊢ n \in ℕ \to \sum_{m = 1}^{n} (\frac{1}{m}) - \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 \log (n + 1) \in ℝ$
15	7 14	resubcld	$⊢ n \in ℕ \to \sum_{m = 1}^{n} (\frac{1}{m}) - \log (n + 1) \in ℝ$
16	2 15	fmpti	$⊢ G : ℕ ⟶ ℝ$
17	11 16	pm3.2i	$⊢ (F : ℕ ⟶ ℝ \land G : ℕ ⟶ ℝ)$