Metamath Proof Explorer


Theorem flge1nn

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 ≤ 𝐴 ) → ( ⌊ ‘ 𝐴 ) ∈ ℕ )

Proof

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 ≤ 𝐴 ) → ( ⌊ ‘ 𝐴 ) ∈ ℕ )