Theorem 0nelfz1

Description: 0 is not an element of a finite interval of integers starting at 1. (Contributed by AV, 27-Aug-2020)

	Ref	Expression
Assertion	0nelfz1	⊢ 0 ∉ ( 1 ... 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		0lt1	⊢ 0 < 1
2		0re	⊢ 0 ∈ ℝ
3		1re	⊢ 1 ∈ ℝ
4	2 3	ltnlei	⊢ ( 0 < 1 ↔ ¬ 1 ≤ 0 )
5	1 4	mpbi	⊢ ¬ 1 ≤ 0
6	5	intnanr	⊢ ¬ ( 1 ≤ 0 ∧ 0 ≤ 𝑁 )
7	6	intnan	⊢ ¬ ( ( 1 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 0 ∈ ℤ ) ∧ ( 1 ≤ 0 ∧ 0 ≤ 𝑁 ) )
8		df-nel	⊢ ( 0 ∉ ( 1 ... 𝑁 ) ↔ ¬ 0 ∈ ( 1 ... 𝑁 ) )
9		elfz2	⊢ ( 0 ∈ ( 1 ... 𝑁 ) ↔ ( ( 1 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 0 ∈ ℤ ) ∧ ( 1 ≤ 0 ∧ 0 ≤ 𝑁 ) ) )
10	8 9	xchbinx	⊢ ( 0 ∉ ( 1 ... 𝑁 ) ↔ ¬ ( ( 1 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 0 ∈ ℤ ) ∧ ( 1 ≤ 0 ∧ 0 ≤ 𝑁 ) ) )
11	7 10	mpbir	⊢ 0 ∉ ( 1 ... 𝑁 )