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