Metamath Proof Explorer


Theorem nn0mulcld

Description: Closure of multiplication of nonnegative integers, inference form. (Contributed by Mario Carneiro, 27-May-2016)

Ref Expression
Hypotheses nn0red.1 φ A 0
nn0addcld.2 φ B 0
Assertion nn0mulcld φ A B 0

Proof

Step Hyp Ref Expression
1 nn0red.1 φ A 0
2 nn0addcld.2 φ B 0
3 nn0mulcl A 0 B 0 A B 0
4 1 2 3 syl2anc φ A B 0