This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database REAL AND COMPLEX NUMBERS Order sets Finite intervals of nonnegative integers 0elfz
Description: 0 is an element of a finite set of sequential nonnegative integers with a
nonnegative integer as upper bound. (Contributed by AV , 6-Apr-2018)
Ref
Expression
Assertion
0elfz ⊢ ( 𝑁 ∈ ℕ0 → 0 ∈ ( 0 ... 𝑁 ) )
Proof
Step
Hyp
Ref
Expression
1
0nn0 ⊢ 0 ∈ ℕ0
2
1
a1i ⊢ ( 𝑁 ∈ ℕ0 → 0 ∈ ℕ0 )
3
id ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℕ0 )
4
nn0ge0 ⊢ ( 𝑁 ∈ ℕ0 → 0 ≤ 𝑁 )
5
elfz2nn0 ⊢ ( 0 ∈ ( 0 ... 𝑁 ) ↔ ( 0 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 0 ≤ 𝑁 ) )
6
2 3 4 5
syl3anbrc ⊢ ( 𝑁 ∈ ℕ0 → 0 ∈ ( 0 ... 𝑁 ) )