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	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℝ ) → ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) ≤ ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		reflcl	⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℝ )
2	1	adantl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℝ ) → ( ⌊ ‘ 𝐴 ) ∈ ℝ )
3		simpr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℝ ) → 𝐴 ∈ ℝ )
4		simpl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℝ ) → 𝑁 ∈ ℕ0 )
5	4	nn0red	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℝ ) → 𝑁 ∈ ℝ )
6	4	nn0ge0d	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℝ ) → 0 ≤ 𝑁 )
7		flle	⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ≤ 𝐴 )
8	7	adantl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℝ ) → ( ⌊ ‘ 𝐴 ) ≤ 𝐴 )
9	2 3 5 6 8	lemul2ad	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℝ ) → ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) ≤ ( 𝑁 · 𝐴 ) )
10	5 3	remulcld	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℝ ) → ( 𝑁 · 𝐴 ) ∈ ℝ )
11		nn0z	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
12		flcl	⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℤ )
13		zmulcl	⊢ ( ( 𝑁 ∈ ℤ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℤ ) → ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) ∈ ℤ )
14	11 12 13	syl2an	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℝ ) → ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) ∈ ℤ )
15		flge	⊢ ( ( ( 𝑁 · 𝐴 ) ∈ ℝ ∧ ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) ∈ ℤ ) → ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) ≤ ( 𝑁 · 𝐴 ) ↔ ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) ≤ ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) ) )
16	10 14 15	syl2anc	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℝ ) → ( ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) ≤ ( 𝑁 · 𝐴 ) ↔ ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) ≤ ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) ) )
17	9 16	mpbid	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℝ ) → ( 𝑁 · ( ⌊ ‘ 𝐴 ) ) ≤ ( ⌊ ‘ ( 𝑁 · 𝐴 ) ) )