This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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