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 ) → 𝑁 ≤ ( 𝑀 · 𝑁 ) )