Metamath Proof Explorer

Theorem fzossfzop1

Description: A half-open range of nonnegative integers is a subset of a half-open range of nonnegative integers with the upper bound increased by one. (Contributed by Alexander van der Vekens, 5-Aug-2018)

Ref Expression
Assertion fzossfzop1 ⊢ N ∈ ℕ 0 → 0 ..^ N ⊆ 0 ..^ N + 1

Proof

Step Hyp Ref Expression
1 nn0z ⊢ N ∈ ℕ 0 → N ∈ ℤ
2 id ⊢ N ∈ ℤ → N ∈ ℤ
3 peano2z ⊢ N ∈ ℤ → N + 1 ∈ ℤ
4 zre ⊢ N ∈ ℤ → N ∈ ℝ
5 4 lep1d ⊢ N ∈ ℤ → N ≤ N + 1
6 2 3 5 3jca ⊢ N ∈ ℤ → N ∈ ℤ ∧ N + 1 ∈ ℤ ∧ N ≤ N + 1
7 1 6 syl ⊢ N ∈ ℕ 0 → N ∈ ℤ ∧ N + 1 ∈ ℤ ∧ N ≤ N + 1
8 eluz2 ⊢ N + 1 ∈ ℤ ≥ N ↔ N ∈ ℤ ∧ N + 1 ∈ ℤ ∧ N ≤ N + 1
9 7 8 sylibr ⊢ N ∈ ℕ 0 → N + 1 ∈ ℤ ≥ N
10 fzoss2 ⊢ N + 1 ∈ ℤ ≥ N → 0 ..^ N ⊆ 0 ..^ N + 1
11 9 10 syl ⊢ N ∈ ℕ 0 → 0 ..^ N ⊆ 0 ..^ N + 1