Theorem nnmulcld 12198

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

Syntax hints:   → wi 4   ∈ wcel 2113  (class class class)co 7358   · cmul 11031  ℕcn 12145

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-un 7680  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-addass 11091  ax-distr 11093  ax-i2m1 11094  ax-1ne0 11095  ax-1rid 11096  ax-rrecex 11098  ax-cnre 11099

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 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7361  df-om 7809  df-2nd 7934  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-nn 12146

This theorem is referenced by:  bcm1k  14238  bcp1n  14239  permnn  14249  trireciplem  15785  efaddlem  16016  eftlub  16034  eirrlem  16129  modmulconst  16215  isprm5  16634  crth  16705  phimullem  16706  pcqmul  16781  pcaddlem  16816  pcbc  16828  oddprmdvds  16831  pockthlem  16833  pockthg  16834  vdwlem3  16911  vdwlem6  16914  vdwlem9  16917  torsubg  19783  ablfacrp  19997  dgrcolem1  26235  aalioulem5  26300  aaliou3lem2  26307  log2cnv  26910  log2tlbnd  26911  log2ublem2  26913  log2ub  26915  lgamgulmlem4  26998  wilthlem2  27035  ftalem7  27045  basellem5  27051  mumul  27147  fsumfldivdiaglem  27155  mpodvdsmulf1o  27160  dvdsmulf1o  27162  sgmmul  27168  chtublem  27178  bcmono  27244  bposlem3  27253  bposlem5  27255  gausslemma2dlem1a  27332  lgsquadlem2  27348  lgsquadlem3  27349  lgsquad2lem2  27352  2sqlem6  27390  2sqmod  27403  rplogsumlem1  27451  rplogsumlem2  27452  dchrisum0fmul  27473  vmalogdivsum2  27505  pntrsumbnd2  27534  pntpbnd1  27553  pntpbnd2  27554  ostth2lem2  27601  zringfrac  33635  fldext2rspun  33839  oddpwdc  34511  eulerpartlemgh  34535  subfaclim  35382  bcprod  35932  faclim2  35942  nnproddivdvdsd  42254  lcmineqlem14  42296  lcmineqlem15  42297  lcmineqlem16  42298  lcmineqlem19  42301  lcmineqlem20  42302  lcmineqlem22  42304  aks4d1p3  42332  aks6d1c1p5  42366  aks6d1c1  42370  aks6d1c2p1  42372  aks6d1c2p2  42373  nnadddir  42525  flt4lem5  42893  flt4lem5e  42899  flt4lem5f  42900  jm2.27c  43249  relexpmulnn  43950  mccllem  45843  limsup10exlem  46016  wallispilem5  46313  wallispi2lem1  46315  wallispi2  46317  stirlinglem3  46320  stirlinglem8  46325  stirlinglem15  46332  dirkertrigeqlem3  46344  hoicvrrex  46800  deccarry  47557  fmtnoprmfac2  47813  sfprmdvdsmersenne  47849  lighneallem3  47853  proththdlem  47859  fppr2odd  47977  gpg3kgrtriexlem2  48330  gpg3kgrtriexlem5  48333  gpg3kgrtriexlem6  48334  gpg3kgrtriex  48335  blennnt2  48835