Metamath Proof Explorer

Theorem fzossrbm1

Description: Subset of a half-open range. (Contributed by Alexander van der Vekens, 1-Nov-2017)

Ref Expression
Assertion fzossrbm1 ⊢ N ∈ ℤ → 0 ..^ N − 1 ⊆ 0 ..^ N

Proof

Step Hyp Ref Expression
1 peano2zm ⊢ N ∈ ℤ → N − 1 ∈ ℤ
2 id ⊢ N ∈ ℤ → N ∈ ℤ
3 zre ⊢ N ∈ ℤ → N ∈ ℝ
4 3 lem1d ⊢ N ∈ ℤ → N − 1 ≤ N
5 eluz2 ⊢ N ∈ ℤ ≥ N − 1 ↔ N − 1 ∈ ℤ ∧ N ∈ ℤ ∧ N − 1 ≤ N
6 1 2 4 5 syl3anbrc ⊢ N ∈ ℤ → N ∈ ℤ ≥ N − 1
7 fzoss2 ⊢ N ∈ ℤ ≥ N − 1 → 0 ..^ N − 1 ⊆ 0 ..^ N
8 6 7 syl ⊢ N ∈ ℤ → 0 ..^ N − 1 ⊆ 0 ..^ N