Theorem flge0nn0

Description: The floor of a number greater than or equal to 0 is a nonnegative integer. (Contributed by NM, 26-Apr-2005)

	Ref	Expression
Assertion	flge0nn0	$$⊢\left(A\in ℝ\wedge 0\le A\right)\to ⌊A⌋\in {\mathbb{N}}_0$$

Proof

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