Theorem fznnfl

Description: Finite set of sequential integers starting at 1 and ending at a real number. (Contributed by Mario Carneiro, 3-May-2016)

	Ref	Expression
Assertion	fznnfl	⊢ ( 𝑁 ∈ ℝ → ( 𝐾 ∈ ( 1 ... ( ⌊ ‘ 𝑁 ) ) ↔ ( 𝐾 ∈ ℕ ∧ 𝐾 ≤ 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		flcl	⊢ ( 𝑁 ∈ ℝ → ( ⌊ ‘ 𝑁 ) ∈ ℤ )
2		fznn	⊢ ( ( ⌊ ‘ 𝑁 ) ∈ ℤ → ( 𝐾 ∈ ( 1 ... ( ⌊ ‘ 𝑁 ) ) ↔ ( 𝐾 ∈ ℕ ∧ 𝐾 ≤ ( ⌊ ‘ 𝑁 ) ) ) )
3	1 2	syl	⊢ ( 𝑁 ∈ ℝ → ( 𝐾 ∈ ( 1 ... ( ⌊ ‘ 𝑁 ) ) ↔ ( 𝐾 ∈ ℕ ∧ 𝐾 ≤ ( ⌊ ‘ 𝑁 ) ) ) )
4		nnz	⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ℤ )
5		flge	⊢ ( ( 𝑁 ∈ ℝ ∧ 𝐾 ∈ ℤ ) → ( 𝐾 ≤ 𝑁 ↔ 𝐾 ≤ ( ⌊ ‘ 𝑁 ) ) )
6	4 5	sylan2	⊢ ( ( 𝑁 ∈ ℝ ∧ 𝐾 ∈ ℕ ) → ( 𝐾 ≤ 𝑁 ↔ 𝐾 ≤ ( ⌊ ‘ 𝑁 ) ) )
7	6	pm5.32da	⊢ ( 𝑁 ∈ ℝ → ( ( 𝐾 ∈ ℕ ∧ 𝐾 ≤ 𝑁 ) ↔ ( 𝐾 ∈ ℕ ∧ 𝐾 ≤ ( ⌊ ‘ 𝑁 ) ) ) )
8	3 7	bitr4d	⊢ ( 𝑁 ∈ ℝ → ( 𝐾 ∈ ( 1 ... ( ⌊ ‘ 𝑁 ) ) ↔ ( 𝐾 ∈ ℕ ∧ 𝐾 ≤ 𝑁 ) ) )