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	$$⊢\left(A\in ℝ\wedge 1\le A\right)\to ⌊A⌋\in \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		flcl	$$⊢A\in ℝ\to ⌊A⌋\in \mathbb{Z}$$
2	1	adantr	$$⊢\left(A\in ℝ\wedge 1\le A\right)\to ⌊A⌋\in \mathbb{Z}$$
3		1z	$$⊢1\in \mathbb{Z}$$
4		flge	$$⊢\left(A\in ℝ\wedge 1\in \mathbb{Z}\right)\to \left(1\le A\leftrightarrow 1\le ⌊A⌋\right)$$
5	3 4	mpan2	$$⊢A\in ℝ\to \left(1\le A\leftrightarrow 1\le ⌊A⌋\right)$$
6	5	biimpa	$$⊢\left(A\in ℝ\wedge 1\le A\right)\to 1\le ⌊A⌋$$
7		elnnz1	$$⊢⌊A⌋\in \mathbb{N}\leftrightarrow \left(⌊A⌋\in \mathbb{Z}\wedge 1\le ⌊A⌋\right)$$
8	2 6 7	sylanbrc	$$⊢\left(A\in ℝ\wedge 1\le A\right)\to ⌊A⌋\in \mathbb{N}$$