Description: The floor of a number greater than or equal to 1 is a positive integer. (Contributed by NM, 26-Apr-2005)
Ref | Expression | ||
---|---|---|---|
Assertion | flge1nn | ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ⌊ ‘ 𝐴 ) ∈ ℕ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | flcl | ⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℤ ) | |
2 | 1 | adantr | ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ⌊ ‘ 𝐴 ) ∈ ℤ ) |
3 | 1z | ⊢ 1 ∈ ℤ | |
4 | flge | ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ∈ ℤ ) → ( 1 ≤ 𝐴 ↔ 1 ≤ ( ⌊ ‘ 𝐴 ) ) ) | |
5 | 3 4 | mpan2 | ⊢ ( 𝐴 ∈ ℝ → ( 1 ≤ 𝐴 ↔ 1 ≤ ( ⌊ ‘ 𝐴 ) ) ) |
6 | 5 | biimpa | ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 1 ≤ ( ⌊ ‘ 𝐴 ) ) |
7 | elnnz1 | ⊢ ( ( ⌊ ‘ 𝐴 ) ∈ ℕ ↔ ( ( ⌊ ‘ 𝐴 ) ∈ ℤ ∧ 1 ≤ ( ⌊ ‘ 𝐴 ) ) ) | |
8 | 2 6 7 | sylanbrc | ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ⌊ ‘ 𝐴 ) ∈ ℕ ) |