Theorem emre

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

	Ref	Expression
Assertion	emre	|- gamma e. RR

Proof

Step	Hyp	Ref	Expression
1		1re	|- 1 e. RR
2		2rp	|- 2 e. RR+
3		relogcl	|- ( 2 e. RR+ -> ( log ` 2 ) e. RR )
4	2 3	ax-mp	|- ( log ` 2 ) e. RR
5	1 4	resubcli	|- ( 1 - ( log ` 2 ) ) e. RR
6		iccssre	|- ( ( ( 1 - ( log ` 2 ) ) e. RR /\ 1 e. RR ) -> ( ( 1 - ( log ` 2 ) ) [,] 1 ) C_ RR )
7	5 1 6	mp2an	|- ( ( 1 - ( log ` 2 ) ) [,] 1 ) C_ RR
8		emcl	|- gamma e. ( ( 1 - ( log ` 2 ) ) [,] 1 )
9	7 8	sselii	|- gamma e. RR