Theorem fzossrbm1

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

	Ref	Expression
Assertion	fzossrbm1	⊢ ( 𝑁 ∈ ℤ → ( 0 ..^ ( 𝑁 − 1 ) ) ⊆ ( 0 ..^ 𝑁 ) )

Proof

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