Theorem flmulnn0

Description: Move a nonnegative integer in and out of a floor. (Contributed by NM, 2-Jan-2009) (Proof shortened by Fan Zheng, 7-Jun-2016)

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

Proof

Step	Hyp	Ref	Expression
1		reflcl	$$⊢A\in ℝ\to ⌊A⌋\in ℝ$$
2	1	adantl	$$⊢\left(N\in {\mathbb{N}}_0\wedge A\in ℝ\right)\to ⌊A⌋\in ℝ$$
3		simpr	$$⊢\left(N\in {\mathbb{N}}_0\wedge A\in ℝ\right)\to A\in ℝ$$
4		simpl	$$⊢\left(N\in {\mathbb{N}}_0\wedge A\in ℝ\right)\to N\in {\mathbb{N}}_0$$
5	4	nn0red	$$⊢\left(N\in {\mathbb{N}}_0\wedge A\in ℝ\right)\to N\in ℝ$$
6	4	nn0ge0d	$$⊢\left(N\in {\mathbb{N}}_0\wedge A\in ℝ\right)\to 0\le N$$
7		flle	$$⊢A\in ℝ\to ⌊A⌋\le A$$
8	7	adantl	$$⊢\left(N\in {\mathbb{N}}_0\wedge A\in ℝ\right)\to ⌊A⌋\le A$$
9	2 3 5 6 8	lemul2ad	$$⊢\left(N\in {\mathbb{N}}_0\wedge A\in ℝ\right)\to N⌊A⌋\le NA$$
10	5 3	remulcld	$$⊢\left(N\in {\mathbb{N}}_0\wedge A\in ℝ\right)\to NA\in ℝ$$
11		nn0z	$$⊢N\in {\mathbb{N}}_0\to N\in \mathbb{Z}$$
12		flcl	$$⊢A\in ℝ\to ⌊A⌋\in \mathbb{Z}$$
13		zmulcl	$$⊢\left(N\in \mathbb{Z}\wedge ⌊A⌋\in \mathbb{Z}\right)\to N⌊A⌋\in \mathbb{Z}$$
14	11 12 13	syl2an	$$⊢\left(N\in {\mathbb{N}}_0\wedge A\in ℝ\right)\to N⌊A⌋\in \mathbb{Z}$$
15		flge	$$⊢\left(NA\in ℝ\wedge N⌊A⌋\in \mathbb{Z}\right)\to \left(N⌊A⌋\le NA\leftrightarrow N⌊A⌋\le ⌊NA⌋\right)$$
16	10 14 15	syl2anc	$$⊢\left(N\in {\mathbb{N}}_0\wedge A\in ℝ\right)\to \left(N⌊A⌋\le NA\leftrightarrow N⌊A⌋\le ⌊NA⌋\right)$$
17	9 16	mpbid	$$⊢\left(N\in {\mathbb{N}}_0\wedge A\in ℝ\right)\to N⌊A⌋\le ⌊NA⌋$$