Theorem nnmulcld 12267

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

Hypotheses

Ref	Expression
nnge1d.1	⊢ (𝜑 → 𝐴 ∈ ℕ)
nnmulcld.2	⊢ (𝜑 → 𝐵 ∈ ℕ)

Assertion

Ref	Expression
nnmulcld	⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℕ)

Proof of Theorem nnmulcld

Step	Hyp	Ref	Expression
1		nnge1d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ)
2		nnmulcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℕ)
3		nnmulcl 12238	. 2 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 · 𝐵) ∈ ℕ)
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℕ)

Syntax hints:   → wi 4   ∈ wcel 2106  (class class class)co 7411   · cmul 11117  ℕcn 12214

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7727  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-addass 11177  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rrecex 11184  ax-cnre 11185

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7414  df-om 7858  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-nn 12215

This theorem is referenced by:  bcm1k  14277  bcp1n  14278  permnn  14288  trireciplem  15810  efaddlem  16038  eftlub  16054  eirrlem  16149  modmulconst  16233  isprm5  16646  crth  16713  phimullem  16714  pcqmul  16788  pcaddlem  16823  pcbc  16835  oddprmdvds  16838  pockthlem  16840  pockthg  16841  vdwlem3  16918  vdwlem6  16921  vdwlem9  16924  torsubg  19724  ablfacrp  19938  dgrcolem1  25794  aalioulem5  25856  aaliou3lem2  25863  log2cnv  26456  log2tlbnd  26457  log2ublem2  26459  log2ub  26461  lgamgulmlem4  26543  wilthlem2  26580  ftalem7  26590  basellem5  26596  mumul  26692  fsumfldivdiaglem  26700  dvdsmulf1o  26705  sgmmul  26711  chtublem  26721  bcmono  26787  bposlem3  26796  bposlem5  26798  gausslemma2dlem1a  26875  lgsquadlem2  26891  lgsquadlem3  26892  lgsquad2lem2  26895  2sqlem6  26933  2sqmod  26946  rplogsumlem1  26994  rplogsumlem2  26995  dchrisum0fmul  27016  vmalogdivsum2  27048  pntrsumbnd2  27077  pntpbnd1  27096  pntpbnd2  27097  ostth2lem2  27144  oddpwdc  33422  eulerpartlemgh  33446  subfaclim  34248  bcprod  34777  faclim2  34787  nnproddivdvdsd  40952  lcmineqlem14  40993  lcmineqlem15  40994  lcmineqlem16  40995  lcmineqlem19  40998  lcmineqlem20  40999  lcmineqlem22  41001  aks4d1p3  41029  aks6d1c2p1  41042  aks6d1c2p2  41043  nnadddir  41266  flt4lem5  41474  flt4lem5e  41480  flt4lem5f  41481  jm2.27c  41828  relexpmulnn  42542  mccllem  44392  limsup10exlem  44567  wallispilem5  44864  wallispi2lem1  44866  wallispi2  44868  stirlinglem3  44871  stirlinglem8  44876  stirlinglem15  44883  dirkertrigeqlem3  44895  hoicvrrex  45351  deccarry  46098  fmtnoprmfac2  46314  sfprmdvdsmersenne  46350  lighneallem3  46354  proththdlem  46360  fppr2odd  46478  blennnt2  47353