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 ) ) )