emcl

Description: Closure and bounds for the Euler-Mascheroni constant. (Contributed by Mario Carneiro, 11-Jul-2014)

		Ref	Expression
	Assertion	emcl	$⊢ γ \in [1 - \log 2, 1]$

Step	Hyp	Ref	Expression
1		eqid	$⊢ (n \in ℕ ⟼ \sum_{m = 1}^{n} (\frac{1}{m}) - \log n) = (n \in ℕ ⟼ \sum_{m = 1}^{n} (\frac{1}{m}) - \log n)$
2		eqid	$⊢ (n \in ℕ ⟼ \sum_{m = 1}^{n} (\frac{1}{m}) - \log (n + 1)) = (n \in ℕ ⟼ \sum_{m = 1}^{n} (\frac{1}{m}) - \log (n + 1))$
3		eqid	$⊢ (n \in ℕ ⟼ \log (1 + (\frac{1}{n}))) = (n \in ℕ ⟼ \log (1 + (\frac{1}{n})))$
4		oveq2	$⊢ k = n \to \frac{1}{k} = \frac{1}{n}$
5	4	oveq2d	$⊢ k = n \to 1 + (\frac{1}{k}) = 1 + (\frac{1}{n})$
6	5	fveq2d	$⊢ k = n \to \log (1 + (\frac{1}{k})) = \log (1 + (\frac{1}{n}))$
7	4 6	oveq12d	$⊢ k = n \to (\frac{1}{k}) - \log (1 + (\frac{1}{k})) = (\frac{1}{n}) - \log (1 + (\frac{1}{n}))$
8	7	cbvmptv	$⊢ (k \in ℕ ⟼ (\frac{1}{k}) - \log (1 + (\frac{1}{k}))) = (n \in ℕ ⟼ (\frac{1}{n}) - \log (1 + (\frac{1}{n})))$
9	1 2 3 8	emcllem7	$⊢ (γ \in [1 - \log 2, 1] \land (n \in ℕ ⟼ \sum_{m = 1}^{n} (\frac{1}{m}) - \log n) : ℕ ⟶ [γ, 1] \land (n \in ℕ ⟼ \sum_{m = 1}^{n} (\frac{1}{m}) - \log (n + 1)) : ℕ ⟶ [1 - \log 2, γ])$
10	9	simp1i	$⊢ γ \in [1 - \log 2, 1]$

Metamath Proof Explorer