emgt0

Description: The Euler-Mascheroni constant is positive. (Contributed by Mario Carneiro, 11-Jul-2014)

		Ref	Expression
	Assertion	emgt0	$⊢ 0 < γ$

Step	Hyp	Ref	Expression
1		log2le1	$⊢ \log 2 < 1$
2		2rp	$⊢ 2 \in ℝ^{+}$
3		relogcl	$⊢ 2 \in ℝ^{+} \to \log 2 \in ℝ$
4	2 3	ax-mp	$⊢ \log 2 \in ℝ$
5		1re	$⊢ 1 \in ℝ$
6	4 5	posdifi	$⊢ \log 2 < 1 \leftrightarrow 0 < 1 - \log 2$
7	1 6	mpbi	$⊢ 0 < 1 - \log 2$
8		emcl	$⊢ γ \in [1 - \log 2, 1]$
9	5 4	resubcli	$⊢ 1 - \log 2 \in ℝ$
10	9 5	elicc2i	$⊢ γ \in [1 - \log 2, 1] \leftrightarrow (γ \in ℝ \land 1 - \log 2 \leq γ \land γ \leq 1)$
11	10	simp2bi	$⊢ γ \in [1 - \log 2, 1] \to 1 - \log 2 \leq γ$
12	8 11	ax-mp	$⊢ 1 - \log 2 \leq γ$
13		0re	$⊢ 0 \in ℝ$
14		emre	$⊢ γ \in ℝ$
15	13 9 14	ltletri	$⊢ (0 < 1 - \log 2 \land 1 - \log 2 \leq γ) \to 0 < γ$
16	7 12 15	mp2an	$⊢ 0 < γ$

Metamath Proof Explorer