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 ⊢ N ∈ ℝ → K ∈ 1 … N ↔ K ∈ ℕ ∧ K ≤ N

Proof

Step Hyp Ref Expression
1 flcl ⊢ N ∈ ℝ → N ∈ ℤ
2 fznn ⊢ N ∈ ℤ → K ∈ 1 … N ↔ K ∈ ℕ ∧ K ≤ N
3 1 2 syl ⊢ N ∈ ℝ → K ∈ 1 … N ↔ K ∈ ℕ ∧ K ≤ N
4 nnz ⊢ K ∈ ℕ → K ∈ ℤ
5 flge ⊢ N ∈ ℝ ∧ K ∈ ℤ → K ≤ N ↔ K ≤ N
6 4 5 sylan2 ⊢ N ∈ ℝ ∧ K ∈ ℕ → K ≤ N ↔ K ≤ N
7 6 pm5.32da ⊢ N ∈ ℝ → K ∈ ℕ ∧ K ≤ N ↔ K ∈ ℕ ∧ K ≤ N
8 3 7 bitr4d ⊢ N ∈ ℝ → K ∈ 1 … N ↔ K ∈ ℕ ∧ K ≤ N