This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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