Theorem elfzom1elfzo

Description: Membership in a half-open range of nonnegative integers. (Contributed by Alexander van der Vekens, 18-Jun-2018)

	Ref	Expression
Assertion	elfzom1elfzo	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → 𝐼 ∈ ( 0 ..^ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		fzossrbm1	⊢ ( 𝑁 ∈ ℤ → ( 0 ..^ ( 𝑁 − 1 ) ) ⊆ ( 0 ..^ 𝑁 ) )
2	1	sselda	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐼 ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) → 𝐼 ∈ ( 0 ..^ 𝑁 ) )