Metamath Proof Explorer


Theorem emre

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

Ref Expression
Assertion emre γ

Proof

Step Hyp Ref Expression
1 1re 1
2 2rp 2+
3 relogcl 2+log2
4 2 3 ax-mp log2
5 1 4 resubcli 1log2
6 iccssre 1log211log21
7 5 1 6 mp2an 1log21
8 emcl γ1log21
9 7 8 sselii γ