Theorem eluzelre

Description: A member of an upper set of integers is a real. (Contributed by Mario Carneiro, 31-Aug-2013)

	Ref	Expression
Assertion	eluzelre	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		eluzelz	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℤ )
2	1	zred	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℝ )