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 ∈ ℝ+ → ( log ‘ 2 ) ∈ ℝ )
4	2 3	ax-mp	⊢ ( log ‘ 2 ) ∈ ℝ
5	1 4	resubcli	⊢ ( 1 − ( log ‘ 2 ) ) ∈ ℝ
6		iccssre	⊢ ( ( ( 1 − ( log ‘ 2 ) ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 1 − ( log ‘ 2 ) ) [,] 1 ) ⊆ ℝ )
7	5 1 6	mp2an	⊢ ( ( 1 − ( log ‘ 2 ) ) [,] 1 ) ⊆ ℝ
8		emcl	⊢ γ ∈ ( ( 1 − ( log ‘ 2 ) ) [,] 1 )
9	7 8	sselii	⊢ γ ∈ ℝ