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	$⊢ (N \in ℕ_{0} \land A \in ℝ) \to N ⌊A⌋ \leq ⌊N A⌋$

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

Metamath Proof Explorer