MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nnmulcld Structured version   Unicode version

Theorem nnmulcld 10388
Description: Closure of multiplication of positive integers. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
nnge1d.1  |-  ( ph  ->  A  e.  NN )
nnmulcld.2  |-  ( ph  ->  B  e.  NN )
Assertion
Ref Expression
nnmulcld  |-  ( ph  ->  ( A  x.  B
)  e.  NN )

Proof of Theorem nnmulcld
StepHypRef Expression
1 nnge1d.1 . 2  |-  ( ph  ->  A  e.  NN )
2 nnmulcld.2 . 2  |-  ( ph  ->  B  e.  NN )
3 nnmulcl 10364 . 2  |-  ( ( A  e.  NN  /\  B  e.  NN )  ->  ( A  x.  B
)  e.  NN )
41, 2, 3syl2anc 661 1  |-  ( ph  ->  ( A  x.  B
)  e.  NN )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756  (class class class)co 6110    x. cmul 9306   NNcn 10341
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4432  ax-nul 4440  ax-pow 4489  ax-pr 4550  ax-un 6391  ax-resscn 9358  ax-1cn 9359  ax-icn 9360  ax-addcl 9361  ax-addrcl 9362  ax-mulcl 9363  ax-mulrcl 9364  ax-mulcom 9365  ax-addass 9366  ax-mulass 9367  ax-distr 9368  ax-i2m1 9369  ax-1ne0 9370  ax-1rid 9371  ax-rrecex 9373  ax-cnre 9374
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2739  df-rex 2740  df-reu 2741  df-rab 2743  df-v 2993  df-sbc 3206  df-csb 3308  df-dif 3350  df-un 3352  df-in 3354  df-ss 3361  df-pss 3363  df-nul 3657  df-if 3811  df-pw 3881  df-sn 3897  df-pr 3899  df-tp 3901  df-op 3903  df-uni 4111  df-iun 4192  df-br 4312  df-opab 4370  df-mpt 4371  df-tr 4405  df-eprel 4651  df-id 4655  df-po 4660  df-so 4661  df-fr 4698  df-we 4700  df-ord 4741  df-on 4742  df-lim 4743  df-suc 4744  df-xp 4865  df-rel 4866  df-cnv 4867  df-co 4868  df-dm 4869  df-rn 4870  df-res 4871  df-ima 4872  df-iota 5400  df-fun 5439  df-fn 5440  df-f 5441  df-f1 5442  df-fo 5443  df-f1o 5444  df-fv 5445  df-ov 6113  df-om 6496  df-recs 6851  df-rdg 6885  df-nn 10342
This theorem is referenced by:  bcm1k  12110  bcp1n  12111  permnn  12121  trireciplem  13343  efaddlem  13397  eftlub  13412  eirrlem  13505  isprm5  13817  crt  13872  phimullem  13873  pcqmul  13939  pcaddlem  13969  pcbc  13981  pockthlem  13985  pockthg  13986  vdwlem3  14063  vdwlem6  14066  vdwlem9  14069  torsubg  16355  ablfacrp  16586  dgrcolem1  21759  aalioulem5  21821  aaliou3lem2  21828  log2cnv  22358  log2tlbnd  22359  log2ublem2  22361  log2ub  22363  wilthlem2  22426  ftalem7  22435  basellem5  22441  mumul  22538  fsumfldivdiaglem  22548  dvdsmulf1o  22553  sgmmul  22559  chtublem  22569  bcmono  22635  bposlem3  22644  bposlem5  22646  lgsquadlem2  22713  lgsquadlem3  22714  lgsquad2lem2  22717  2sqlem6  22727  rplogsumlem1  22752  rplogsumlem2  22753  dchrisum0fmul  22774  vmalogdivsum2  22806  pntrsumbnd2  22835  pntpbnd1  22854  pntpbnd2  22855  ostth2lem2  22902  oddpwdc  26756  eulerpartlemgh  26780  lgamgulmlem4  27037  subfaclim  27095  faclim2  27573  jm2.27c  29379  wallispilem5  29887  wallispi2lem1  29889  wallispi2  29891  stirlinglem3  29894  stirlinglem8  29899  stirlinglem15  29906
  Copyright terms: Public domain W3C validator