Theorem uzid

Description: Membership of the least member in an upper set of integers. (Contributed by NM, 2-Sep-2005)

	Ref	Expression
Assertion	uzid	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		zre	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
2	1	leidd	⊢ ( 𝑀 ∈ ℤ → 𝑀 ≤ 𝑀 )
3	2	ancli	⊢ ( 𝑀 ∈ ℤ → ( 𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝑀 ) )
4		eluz1	⊢ ( 𝑀 ∈ ℤ → ( 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝑀 ) ) )
5	3 4	mpbird	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )