Theorem nnmulcld 12170

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 12141	. 2 ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 · 𝐵) ∈ ℕ)
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℕ)

Syntax hints:   → wi 4   ∈ wcel 2110  (class class class)co 7341   · cmul 11003  ℕcn 12117

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-10 2143  ax-11 2159  ax-12 2179  ax-ext 2702  ax-sep 5232  ax-nul 5242  ax-pr 5368  ax-un 7663  ax-1cn 11056  ax-icn 11057  ax-addcl 11058  ax-addrcl 11059  ax-mulcl 11060  ax-mulrcl 11061  ax-addass 11063  ax-distr 11065  ax-i2m1 11066  ax-1ne0 11067  ax-1rid 11068  ax-rrecex 11070  ax-cnre 11071

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-reu 3345  df-rab 3394  df-v 3436  df-sbc 3740  df-csb 3849  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-pss 3920  df-nul 4282  df-if 4474  df-pw 4550  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4858  df-iun 4941  df-br 5090  df-opab 5152  df-mpt 5171  df-tr 5197  df-id 5509  df-eprel 5514  df-po 5522  df-so 5523  df-fr 5567  df-we 5569  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-pred 6244  df-ord 6305  df-on 6306  df-lim 6307  df-suc 6308  df-iota 6433  df-fun 6479  df-fn 6480  df-f 6481  df-f1 6482  df-fo 6483  df-f1o 6484  df-fv 6485  df-ov 7344  df-om 7792  df-2nd 7917  df-frecs 8206  df-wrecs 8237  df-recs 8286  df-rdg 8324  df-nn 12118

This theorem is referenced by:  bcm1k  14214  bcp1n  14215  permnn  14225  trireciplem  15761  efaddlem  15992  eftlub  16010  eirrlem  16105  modmulconst  16191  isprm5  16610  crth  16681  phimullem  16682  pcqmul  16757  pcaddlem  16792  pcbc  16804  oddprmdvds  16807  pockthlem  16809  pockthg  16810  vdwlem3  16887  vdwlem6  16890  vdwlem9  16893  torsubg  19759  ablfacrp  19973  dgrcolem1  26199  aalioulem5  26264  aaliou3lem2  26271  log2cnv  26874  log2tlbnd  26875  log2ublem2  26877  log2ub  26879  lgamgulmlem4  26962  wilthlem2  26999  ftalem7  27009  basellem5  27015  mumul  27111  fsumfldivdiaglem  27119  mpodvdsmulf1o  27124  dvdsmulf1o  27126  sgmmul  27132  chtublem  27142  bcmono  27208  bposlem3  27217  bposlem5  27219  gausslemma2dlem1a  27296  lgsquadlem2  27312  lgsquadlem3  27313  lgsquad2lem2  27316  2sqlem6  27354  2sqmod  27367  rplogsumlem1  27415  rplogsumlem2  27416  dchrisum0fmul  27437  vmalogdivsum2  27469  pntrsumbnd2  27498  pntpbnd1  27517  pntpbnd2  27518  ostth2lem2  27565  zringfrac  33509  fldext2rspun  33685  oddpwdc  34357  eulerpartlemgh  34381  subfaclim  35200  bcprod  35750  faclim2  35760  nnproddivdvdsd  42012  lcmineqlem14  42054  lcmineqlem15  42055  lcmineqlem16  42056  lcmineqlem19  42059  lcmineqlem20  42060  lcmineqlem22  42062  aks4d1p3  42090  aks6d1c1p5  42124  aks6d1c1  42128  aks6d1c2p1  42130  aks6d1c2p2  42131  nnadddir  42282  flt4lem5  42662  flt4lem5e  42668  flt4lem5f  42669  jm2.27c  43019  relexpmulnn  43721  mccllem  45616  limsup10exlem  45789  wallispilem5  46086  wallispi2lem1  46088  wallispi2  46090  stirlinglem3  46093  stirlinglem8  46098  stirlinglem15  46105  dirkertrigeqlem3  46117  hoicvrrex  46573  deccarry  47321  fmtnoprmfac2  47577  sfprmdvdsmersenne  47613  lighneallem3  47617  proththdlem  47623  fppr2odd  47741  gpg3kgrtriexlem2  48094  gpg3kgrtriexlem5  48097  gpg3kgrtriexlem6  48098  gpg3kgrtriex  48099  blennnt2  48600