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