Theorem nn0mulcli

Description: Closure of multiplication of nonnegative integers, inference form. (Contributed by Raph Levien, 10-Dec-2002)

	Ref	Expression
Hypotheses	nn0addcli.1	⊢ 𝑀 ∈ ℕ0
	nn0addcli.2	⊢ 𝑁 ∈ ℕ0
Assertion	nn0mulcli	⊢ ( 𝑀 · 𝑁 ) ∈ ℕ0

Proof

Step	Hyp	Ref	Expression
1		nn0addcli.1	⊢ 𝑀 ∈ ℕ0
2		nn0addcli.2	⊢ 𝑁 ∈ ℕ0
3		nn0mulcl	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 · 𝑁 ) ∈ ℕ0 )
4	1 2 3	mp2an	⊢ ( 𝑀 · 𝑁 ) ∈ ℕ0