Metamath Proof Explorer


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 ... ( ⌊ ‘ 𝑁 ) ) ↔ ( 𝐾 ∈ ℕ ∧ 𝐾𝑁 ) ) )