This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑁 ∈ ℕ0 → ( 0 ..^ 𝑁 ) ⊆ ( 0 ..^ ( 𝑁 + 1 ) ) )

Proof

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