Theorem nnmulcld 12312

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

Syntax hints:   → wi 4   ∈ wcel 2098  (class class class)co 7423   · cmul 11159  ℕcn 12259

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5303  ax-nul 5310  ax-pr 5432  ax-un 7745  ax-1cn 11212  ax-icn 11213  ax-addcl 11214  ax-addrcl 11215  ax-mulcl 11216  ax-mulrcl 11217  ax-addass 11219  ax-distr 11221  ax-i2m1 11222  ax-1ne0 11223  ax-1rid 11224  ax-rrecex 11226  ax-cnre 11227

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-ral 3051  df-rex 3060  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3966  df-nul 4325  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5579  df-eprel 5585  df-po 5593  df-so 5594  df-fr 5636  df-we 5638  df-xp 5687  df-rel 5688  df-cnv 5689  df-co 5690  df-dm 5691  df-rn 5692  df-res 5693  df-ima 5694  df-pred 6311  df-ord 6378  df-on 6379  df-lim 6380  df-suc 6381  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-ov 7426  df-om 7876  df-2nd 8003  df-frecs 8295  df-wrecs 8326  df-recs 8400  df-rdg 8439  df-nn 12260

This theorem is referenced by:  bcm1k  14327  bcp1n  14328  permnn  14338  trireciplem  15861  efaddlem  16090  eftlub  16106  eirrlem  16201  modmulconst  16285  isprm5  16703  crth  16775  phimullem  16776  pcqmul  16850  pcaddlem  16885  pcbc  16897  oddprmdvds  16900  pockthlem  16902  pockthg  16903  vdwlem3  16980  vdwlem6  16983  vdwlem9  16986  torsubg  19847  ablfacrp  20061  dgrcolem1  26293  aalioulem5  26356  aaliou3lem2  26363  log2cnv  26964  log2tlbnd  26965  log2ublem2  26967  log2ub  26969  lgamgulmlem4  27052  wilthlem2  27089  ftalem7  27099  basellem5  27105  mumul  27201  fsumfldivdiaglem  27209  mpodvdsmulf1o  27214  dvdsmulf1o  27216  sgmmul  27222  chtublem  27232  bcmono  27298  bposlem3  27307  bposlem5  27309  gausslemma2dlem1a  27386  lgsquadlem2  27402  lgsquadlem3  27403  lgsquad2lem2  27406  2sqlem6  27444  2sqmod  27457  rplogsumlem1  27505  rplogsumlem2  27506  dchrisum0fmul  27527  vmalogdivsum2  27559  pntrsumbnd2  27588  pntpbnd1  27607  pntpbnd2  27608  ostth2lem2  27655  zringfrac  33406  oddpwdc  34144  eulerpartlemgh  34168  subfaclim  34968  bcprod  35508  faclim2  35518  nnproddivdvdsd  41647  lcmineqlem14  41689  lcmineqlem15  41690  lcmineqlem16  41691  lcmineqlem19  41694  lcmineqlem20  41695  lcmineqlem22  41697  aks4d1p3  41725  aks6d1c1p5  41758  aks6d1c1  41762  aks6d1c2p1  41764  aks6d1c2p2  41765  nnadddir  42026  flt4lem5  42241  flt4lem5e  42247  flt4lem5f  42248  jm2.27c  42602  relexpmulnn  43313  mccllem  45155  limsup10exlem  45330  wallispilem5  45627  wallispi2lem1  45629  wallispi2  45631  stirlinglem3  45634  stirlinglem8  45639  stirlinglem15  45646  dirkertrigeqlem3  45658  hoicvrrex  46114  deccarry  46861  fmtnoprmfac2  47076  sfprmdvdsmersenne  47112  lighneallem3  47116  proththdlem  47122  fppr2odd  47240  blennnt2  47914