Theorem uzn0bi

Description: The upper integers function needs to be applied to an integer, in order to return a nonempty set. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Assertion	uzn0bi	⊢ ( ( ℤ≥ ‘ 𝑀 ) ≠ ∅ ↔ 𝑀 ∈ ℤ )

Proof

Step	Hyp	Ref	Expression
1		uz0	⊢ ( ¬ 𝑀 ∈ ℤ → ( ℤ≥ ‘ 𝑀 ) = ∅ )
2	1	adantl	⊢ ( ( ( ℤ≥ ‘ 𝑀 ) ≠ ∅ ∧ ¬ 𝑀 ∈ ℤ ) → ( ℤ≥ ‘ 𝑀 ) = ∅ )
3		neneq	⊢ ( ( ℤ≥ ‘ 𝑀 ) ≠ ∅ → ¬ ( ℤ≥ ‘ 𝑀 ) = ∅ )
4	3	adantr	⊢ ( ( ( ℤ≥ ‘ 𝑀 ) ≠ ∅ ∧ ¬ 𝑀 ∈ ℤ ) → ¬ ( ℤ≥ ‘ 𝑀 ) = ∅ )
5	2 4	condan	⊢ ( ( ℤ≥ ‘ 𝑀 ) ≠ ∅ → 𝑀 ∈ ℤ )
6		id	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℤ )
7		eqid	⊢ ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝑀 )
8	6 7	uzn0d	⊢ ( 𝑀 ∈ ℤ → ( ℤ≥ ‘ 𝑀 ) ≠ ∅ )
9	5 8	impbii	⊢ ( ( ℤ≥ ‘ 𝑀 ) ≠ ∅ ↔ 𝑀 ∈ ℤ )