Theorem nn0fz0

Description: A nonnegative integer is always part of the finite set of sequential nonnegative integers with this integer as upper bound. (Contributed by Scott Fenton, 21-Mar-2018)

	Ref	Expression
Assertion	nn0fz0	⊢ ( 𝑁 ∈ ℕ0 ↔ 𝑁 ∈ ( 0 ... 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℕ0 )
2		nn0re	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
3	2	leidd	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ≤ 𝑁 )
4		fznn0	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 ∈ ( 0 ... 𝑁 ) ↔ ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≤ 𝑁 ) ) )
5	1 3 4	mpbir2and	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ( 0 ... 𝑁 ) )
6		elfz3nn0	⊢ ( 𝑁 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ℕ0 )
7	5 6	impbii	⊢ ( 𝑁 ∈ ℕ0 ↔ 𝑁 ∈ ( 0 ... 𝑁 ) )