Theorem emre

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

	Ref	Expression
Assertion	emre	$$⊢\gamma \in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		1re	$$⊢1\in ℝ$$
2		2rp	$$⊢2\in {ℝ}^{+}$$
3		relogcl	$$⊢2\in {ℝ}^{+}\to \log 2\in ℝ$$
4	2 3	ax-mp	$$⊢\log 2\in ℝ$$
5	1 4	resubcli	$$⊢1-\log 2\in ℝ$$
6		iccssre	$$⊢\left(1-\log 2\in ℝ\wedge 1\in ℝ\right)\to \left[1-\log 2,1\right]\subseteq ℝ$$
7	5 1 6	mp2an	$$⊢\left[1-\log 2,1\right]\subseteq ℝ$$
8		emcl	$$⊢\gamma \in \left[1-\log 2,1\right]$$
9	7 8	sselii	$$⊢\gamma \in ℝ$$