Metamath Proof Explorer
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 |