Theorem emgt0

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

	Ref	Expression
Assertion	emgt0	$$⊢0<\gamma$$

Proof

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	$$⊢\gamma \in \left[1-\log 2,1\right]$$
9	5 4	resubcli	$$⊢1-\log 2\in ℝ$$
10	9 5	elicc2i	$$⊢\gamma \in \left[1-\log 2,1\right]\leftrightarrow \left(\gamma \in ℝ\wedge 1-\log 2\le \gamma \wedge \gamma \le 1\right)$$
11	10	simp2bi	$$⊢\gamma \in \left[1-\log 2,1\right]\to 1-\log 2\le \gamma$$
12	8 11	ax-mp	$$⊢1-\log 2\le \gamma$$
13		0re	$$⊢0\in ℝ$$
14		emre	$$⊢\gamma \in ℝ$$
15	13 9 14	ltletri	$$⊢\left(0<1-\log 2\wedge 1-\log 2\le \gamma \right)\to 0<\gamma$$
16	7 12 15	mp2an	$$⊢0<\gamma$$