Theorem fzonn0p1

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

	Ref	Expression
Assertion	fzonn0p1	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℕ0 )
2		nn0p1nn	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ )
3		nn0re	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
4	3	ltp1d	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 < ( 𝑁 + 1 ) )
5		elfzo0	⊢ ( 𝑁 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) ↔ ( 𝑁 ∈ ℕ0 ∧ ( 𝑁 + 1 ) ∈ ℕ ∧ 𝑁 < ( 𝑁 + 1 ) ) )
6	1 2 4 5	syl3anbrc	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) )