Metamath Proof Explorer


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