Theorem uz0

Description: The upper integers function applied to a non-integer, is the empty set. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Assertion	uz0	⊢ ( ¬ 𝑀 ∈ ℤ → ( ℤ≥ ‘ 𝑀 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		dmuz	⊢ dom ℤ≥ = ℤ
2	1	eqcomi	⊢ ℤ = dom ℤ≥
3	2	eleq2i	⊢ ( 𝑀 ∈ ℤ ↔ 𝑀 ∈ dom ℤ≥ )
4	3	notbii	⊢ ( ¬ 𝑀 ∈ ℤ ↔ ¬ 𝑀 ∈ dom ℤ≥ )
5	4	biimpi	⊢ ( ¬ 𝑀 ∈ ℤ → ¬ 𝑀 ∈ dom ℤ≥ )
6		ndmfv	⊢ ( ¬ 𝑀 ∈ dom ℤ≥ → ( ℤ≥ ‘ 𝑀 ) = ∅ )
7	5 6	syl	⊢ ( ¬ 𝑀 ∈ ℤ → ( ℤ≥ ‘ 𝑀 ) = ∅ )