This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nnmulcli

Description: Closure of multiplication of positive integers. (Contributed by Mario Carneiro, 18-Feb-2014)

Ref Expression
Hypotheses nnmulcli.1 ⊢ A ∈ ℕ
nnmulcli.2 ⊢ B ∈ ℕ
Assertion nnmulcli ⊢ A ⁢ B ∈ ℕ

Proof

Step Hyp Ref Expression
1 nnmulcli.1 ⊢ A ∈ ℕ
2 nnmulcli.2 ⊢ B ∈ ℕ
3 nnmulcl ⊢ A ∈ ℕ ∧ B ∈ ℕ → A ⁢ B ∈ ℕ
4 1 2 3 mp2an ⊢ A ⁢ B ∈ ℕ