Theorem fz1n

Description: A 1-based finite set of sequential integers is empty iff it ends at index 0 . (Contributed by Paul Chapman, 22-Jun-2011)

	Ref	Expression
Assertion	fz1n	⊢ ( 𝑁 ∈ ℕ0 → ( ( 1 ... 𝑁 ) = ∅ ↔ 𝑁 = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		1z	⊢ 1 ∈ ℤ
2		nn0z	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
3		fzn	⊢ ( ( 1 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 < 1 ↔ ( 1 ... 𝑁 ) = ∅ ) )
4	1 2 3	sylancr	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 < 1 ↔ ( 1 ... 𝑁 ) = ∅ ) )
5		nn0lt10b	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 < 1 ↔ 𝑁 = 0 ) )
6	4 5	bitr3d	⊢ ( 𝑁 ∈ ℕ0 → ( ( 1 ... 𝑁 ) = ∅ ↔ 𝑁 = 0 ) )