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