Theorem nn0mulcl

Description: Closure of multiplication of nonnegative integers. (Contributed by NM, 22-Jul-2004) (Proof shortened by Mario Carneiro, 17-Jul-2014)

	Ref	Expression
Assertion	nn0mulcl	$$⊢\left(M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to \mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in {\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		nnsscn	$$⊢\mathbb{N}\subseteq ℂ$$
2		id	$$⊢\mathbb{N}\subseteq ℂ\to \mathbb{N}\subseteq ℂ$$
3		df-n0	$$⊢{\mathbb{N}}_0=\mathbb{N}\cup \left\{0\right\}$$
4		nnmulcl	$$⊢\left(M\in \mathbb{N}\wedge N\in \mathbb{N}\right)\to \mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in \mathbb{N}$$
5	4	adantl	$$⊢\left(\mathbb{N}\subseteq ℂ\wedge \left(M\in \mathbb{N}\wedge N\in \mathbb{N}\right)\right)\to \mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in \mathbb{N}$$
6	2 3 5	un0mulcl	$$⊢\left(\mathbb{N}\subseteq ℂ\wedge \left(M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\right)\to \mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in {\mathbb{N}}_0$$
7	1 6	mpan	$$⊢\left(M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to \mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in {\mathbb{N}}_0$$