Metamath Proof Explorer


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 < γ