Metamath Proof Explorer

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 e. RR+
3 relogcl 
 |-  ( 2 e. RR+ -> ( log ` 2 ) e. RR )
4 2 3 ax-mp 
 |-  ( log ` 2 ) e. RR
5 1re 
 |-  1 e. RR
6 4 5 posdifi 
 |-  ( ( log ` 2 ) < 1 <-> 0 < ( 1 - ( log ` 2 ) ) )
7 1 6 mpbi 
 |-  0 < ( 1 - ( log ` 2 ) )
8 emcl 
 |-  gamma e. ( ( 1 - ( log ` 2 ) ) [,] 1 )
9 5 4 resubcli 
 |-  ( 1 - ( log ` 2 ) ) e. RR
10 9 5 elicc2i 
 |-  ( gamma e. ( ( 1 - ( log ` 2 ) ) [,] 1 ) <-> ( gamma e. RR /\ ( 1 - ( log ` 2 ) ) <_ gamma /\ gamma <_ 1 ) )
11 10 simp2bi 
 |-  ( gamma e. ( ( 1 - ( log ` 2 ) ) [,] 1 ) -> ( 1 - ( log ` 2 ) ) <_ gamma )
12 8 11 ax-mp 
 |-  ( 1 - ( log ` 2 ) ) <_ gamma
13 0re 
 |-  0 e. RR
14 emre 
 |-  gamma e. RR
15 13 9 14 ltletri 
 |-  ( ( 0 < ( 1 - ( log ` 2 ) ) /\ ( 1 - ( log ` 2 ) ) <_ gamma ) -> 0 < gamma )
16 7 12 15 mp2an 
 |-  0 < gamma