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	$$⊢\left(M\in \mathbb{N}\wedge N\in {\mathbb{N}}_0\right)\to N\le \mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$

Proof

Step	Hyp	Ref	Expression
1		simpr	$$⊢\left(M\in \mathbb{N}\wedge N\in {\mathbb{N}}_0\right)\to N\in {\mathbb{N}}_0$$
2	1	nn0cnd	$$⊢\left(M\in \mathbb{N}\wedge N\in {\mathbb{N}}_0\right)\to N\in ℂ$$
3	2	mulid2d	$$⊢\left(M\in \mathbb{N}\wedge N\in {\mathbb{N}}_0\right)\to 1\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=N$$
4		1red	$$⊢\left(M\in \mathbb{N}\wedge N\in {\mathbb{N}}_0\right)\to 1\in ℝ$$
5		nnre	$$⊢M\in \mathbb{N}\to M\in ℝ$$
6	5	adantr	$$⊢\left(M\in \mathbb{N}\wedge N\in {\mathbb{N}}_0\right)\to M\in ℝ$$
7	1	nn0red	$$⊢\left(M\in \mathbb{N}\wedge N\in {\mathbb{N}}_0\right)\to N\in ℝ$$
8	1	nn0ge0d	$$⊢\left(M\in \mathbb{N}\wedge N\in {\mathbb{N}}_0\right)\to 0\le N$$
9		nnge1	$$⊢M\in \mathbb{N}\to 1\le M$$
10	9	adantr	$$⊢\left(M\in \mathbb{N}\wedge N\in {\mathbb{N}}_0\right)\to 1\le M$$
11	4 6 7 8 10	lemul1ad	$$⊢\left(M\in \mathbb{N}\wedge N\in {\mathbb{N}}_0\right)\to 1\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\le \mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
12	3 11	eqbrtrrd	$$⊢\left(M\in \mathbb{N}\wedge N\in {\mathbb{N}}_0\right)\to N\le \mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$