Theorem emgt0

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

	Ref	Expression
Assertion	emgt0	⊢ 0 < γ

Proof

Step	Hyp	Ref	Expression
1		log2le1	⊢ ( log ‘ 2 ) < 1
2		2rp	⊢ 2 ∈ ℝ+
3		relogcl	⊢ ( 2 ∈ ℝ+ → ( log ‘ 2 ) ∈ ℝ )
4	2 3	ax-mp	⊢ ( log ‘ 2 ) ∈ ℝ
5		1re	⊢ 1 ∈ ℝ
6	4 5	posdifi	⊢ ( ( log ‘ 2 ) < 1 ↔ 0 < ( 1 − ( log ‘ 2 ) ) )
7	1 6	mpbi	⊢ 0 < ( 1 − ( log ‘ 2 ) )
8		emcl	⊢ γ ∈ ( ( 1 − ( log ‘ 2 ) ) [,] 1 )
9	5 4	resubcli	⊢ ( 1 − ( log ‘ 2 ) ) ∈ ℝ
10	9 5	elicc2i	⊢ ( γ ∈ ( ( 1 − ( log ‘ 2 ) ) [,] 1 ) ↔ ( γ ∈ ℝ ∧ ( 1 − ( log ‘ 2 ) ) ≤ γ ∧ γ ≤ 1 ) )
11	10	simp2bi	⊢ ( γ ∈ ( ( 1 − ( log ‘ 2 ) ) [,] 1 ) → ( 1 − ( log ‘ 2 ) ) ≤ γ )
12	8 11	ax-mp	⊢ ( 1 − ( log ‘ 2 ) ) ≤ γ
13		0re	⊢ 0 ∈ ℝ
14		emre	⊢ γ ∈ ℝ
15	13 9 14	ltletri	⊢ ( ( 0 < ( 1 − ( log ‘ 2 ) ) ∧ ( 1 − ( log ‘ 2 ) ) ≤ γ ) → 0 < γ )
16	7 12 15	mp2an	⊢ 0 < γ