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

Metamath Proof Explorer

Theorem nnmulge

Description: Multiplying by a positive integer M yields greater than or equal nonnegative integers. (Contributed by Thierry Arnoux, 13-Dec-2021)

Ref Expression
Assertion nnmulge ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ≤ ( 𝑀 · 𝑁 ) )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 )
2 1 nn0cnd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℂ )
3 2 mullidd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 1 · 𝑁 ) = 𝑁 )
4 1red ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → 1 ∈ ℝ )
5 nnre ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℝ )
6 5 adantr ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → 𝑀 ∈ ℝ )
7 1 nn0red ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℝ )
8 1 nn0ge0d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → 0 ≤ 𝑁 )
9 nnge1 ⊢ ( 𝑀 ∈ ℕ → 1 ≤ 𝑀 )
10 9 adantr ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → 1 ≤ 𝑀 )
11 4 6 7 8 10 lemul1ad ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 1 · 𝑁 ) ≤ ( 𝑀 · 𝑁 ) )
12 3 11 eqbrtrrd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ≤ ( 𝑀 · 𝑁 ) )