This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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