Theorem nnmulcld 9120

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

Step	Hyp	Ref	Expression
1		nnge1d.1	. 2 |- ( ph -> A e. NN )
2		nnmulcld.2	. 2 |- ( ph -> B e. NN )
3		nnmulcl 9092	. 2 |- ( ( A e. NN /\ B e. NN ) -> ( A x. B ) e. NN )
4	1, 2, 3	syl2anc 411	1 |- ( ph -> ( A x. B ) e. NN )

Syntax hints:   -> wi 4   e. wcel 2178  (class class class)co 5967   x. cmul 7965   NNcn 9071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189  ax-sep 4178  ax-cnex 8051  ax-resscn 8052  ax-1cn 8053  ax-1re 8054  ax-icn 8055  ax-addcl 8056  ax-addrcl 8057  ax-mulcl 8058  ax-mulcom 8061  ax-addass 8062  ax-mulass 8063  ax-distr 8064  ax-1rid 8067  ax-cnre 8071

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-ral 2491  df-rex 2492  df-rab 2495  df-v 2778  df-un 3178  df-in 3180  df-ss 3187  df-sn 3649  df-pr 3650  df-op 3652  df-uni 3865  df-int 3900  df-br 4060  df-iota 5251  df-fv 5298  df-ov 5970  df-inn 9072

This theorem is referenced by:  qbtwnre  10436  bcval  10931  bcm1k  10942  bcp1n  10943  permnn  10953  cvg1nlemcxze  11408  cvg1nlemf  11409  cvg1nlemcau  11410  cvg1nlemres  11411  trireciplem  11926  efaddlem  12100  eftlub  12116  eirraplem  12203  modmulconst  12249  lcmval  12500  oddpwdclemxy  12606  oddpwdclemdc  12610  sqpweven  12612  2sqpwodd  12613  crth  12661  phimullem  12662  modprm0  12692  pcqmul  12741  pcaddlem  12777  pcbc  12789  oddprmdvds  12792  pockthlem  12794  pockthg  12795  4sqlem13m  12841  4sqlem14  12842  4sqlem17  12845  4sqlem18  12846  evenennn  12879  mpodvdsmulf1o  15577  fsumdvdsmul  15578  sgmmul  15583  gausslemma2dlem1a  15650  lgseisenlem2  15663  lgseisenlem4  15665  lgsquadlemsfi  15667  lgsquadlem2  15670  lgsquadlem3  15671  lgsquad2lem2  15674  2sqlem6  15712