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	$⊢ (M \in ℕ \land N \in ℕ_{0}) \to N \leq M \cdot N$

Step	Hyp	Ref	Expression
1		simpr	$⊢ (M \in ℕ \land N \in ℕ_{0}) \to N \in ℕ_{0}$
2	1	nn0cnd	$⊢ (M \in ℕ \land N \in ℕ_{0}) \to N \in ℂ$
3	2	mullidd	$⊢ (M \in ℕ \land N \in ℕ_{0}) \to 1 \cdot N = N$
4		1red	$⊢ (M \in ℕ \land N \in ℕ_{0}) \to 1 \in ℝ$
5		nnre	$⊢ M \in ℕ \to M \in ℝ$
6	5	adantr	$⊢ (M \in ℕ \land N \in ℕ_{0}) \to M \in ℝ$
7	1	nn0red	$⊢ (M \in ℕ \land N \in ℕ_{0}) \to N \in ℝ$
8	1	nn0ge0d	$⊢ (M \in ℕ \land N \in ℕ_{0}) \to 0 \leq N$
9		nnge1	$⊢ M \in ℕ \to 1 \leq M$
10	9	adantr	$⊢ (M \in ℕ \land N \in ℕ_{0}) \to 1 \leq M$
11	4 6 7 8 10	lemul1ad	$⊢ (M \in ℕ \land N \in ℕ_{0}) \to 1 \cdot N \leq M \cdot N$
12	3 11	eqbrtrrd	$⊢ (M \in ℕ \land N \in ℕ_{0}) \to N \leq M \cdot N$

Metamath Proof Explorer