Theorem uzn0d

Description: The upper integers are all nonempty. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	uzn0d.1	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	uzn0d.2	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
Assertion	uzn0d	⊢ ( 𝜑 → 𝑍 ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		uzn0d.1	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2		uzn0d.2	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3	1 2	uzidd2	⊢ ( 𝜑 → 𝑀 ∈ 𝑍 )
4	3	ne0d	⊢ ( 𝜑 → 𝑍 ≠ ∅ )