Metamath Proof Explorer

Theorem elfzom1elfzo

Description: Membership in a half-open range of nonnegative integers. (Contributed by Alexander van der Vekens, 18-Jun-2018)

Ref Expression
Assertion elfzom1elfzo ⊢ N ∈ ℤ ∧ I ∈ 0 ..^ N − 1 → I ∈ 0 ..^ N

Proof

Step Hyp Ref Expression
1 fzossrbm1 ⊢ N ∈ ℤ → 0 ..^ N − 1 ⊆ 0 ..^ N
2 1 sselda ⊢ N ∈ ℤ ∧ I ∈ 0 ..^ N − 1 → I ∈ 0 ..^ N