Theorem nnmulcld 12320

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

Syntax hints:   → wi 4   ∈ wcel 2107  (class class class)co 7432   · cmul 11161  ℕcn 12267

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pr 5431  ax-un 7756  ax-1cn 11214  ax-icn 11215  ax-addcl 11216  ax-addrcl 11217  ax-mulcl 11218  ax-mulrcl 11219  ax-addass 11221  ax-distr 11223  ax-i2m1 11224  ax-1ne0 11225  ax-1rid 11226  ax-rrecex 11228  ax-cnre 11229

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-iun 4992  df-br 5143  df-opab 5205  df-mpt 5225  df-tr 5259  df-id 5577  df-eprel 5583  df-po 5591  df-so 5592  df-fr 5636  df-we 5638  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-pred 6320  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-ov 7435  df-om 7889  df-2nd 8016  df-frecs 8307  df-wrecs 8338  df-recs 8412  df-rdg 8451  df-nn 12268

This theorem is referenced by:  bcm1k  14355  bcp1n  14356  permnn  14366  trireciplem  15899  efaddlem  16130  eftlub  16146  eirrlem  16241  modmulconst  16326  isprm5  16745  crth  16816  phimullem  16817  pcqmul  16892  pcaddlem  16927  pcbc  16939  oddprmdvds  16942  pockthlem  16944  pockthg  16945  vdwlem3  17022  vdwlem6  17025  vdwlem9  17028  torsubg  19873  ablfacrp  20087  dgrcolem1  26314  aalioulem5  26379  aaliou3lem2  26386  log2cnv  26988  log2tlbnd  26989  log2ublem2  26991  log2ub  26993  lgamgulmlem4  27076  wilthlem2  27113  ftalem7  27123  basellem5  27129  mumul  27225  fsumfldivdiaglem  27233  mpodvdsmulf1o  27238  dvdsmulf1o  27240  sgmmul  27246  chtublem  27256  bcmono  27322  bposlem3  27331  bposlem5  27333  gausslemma2dlem1a  27410  lgsquadlem2  27426  lgsquadlem3  27427  lgsquad2lem2  27430  2sqlem6  27468  2sqmod  27481  rplogsumlem1  27529  rplogsumlem2  27530  dchrisum0fmul  27551  vmalogdivsum2  27583  pntrsumbnd2  27612  pntpbnd1  27631  pntpbnd2  27632  ostth2lem2  27679  zringfrac  33583  fldext2rspun  33733  oddpwdc  34357  eulerpartlemgh  34381  subfaclim  35194  bcprod  35739  faclim2  35749  nnproddivdvdsd  42002  lcmineqlem14  42044  lcmineqlem15  42045  lcmineqlem16  42046  lcmineqlem19  42049  lcmineqlem20  42050  lcmineqlem22  42052  aks4d1p3  42080  aks6d1c1p5  42114  aks6d1c1  42118  aks6d1c2p1  42120  aks6d1c2p2  42121  nnadddir  42310  flt4lem5  42665  flt4lem5e  42671  flt4lem5f  42672  jm2.27c  43024  relexpmulnn  43727  mccllem  45617  limsup10exlem  45792  wallispilem5  46089  wallispi2lem1  46091  wallispi2  46093  stirlinglem3  46096  stirlinglem8  46101  stirlinglem15  46108  dirkertrigeqlem3  46120  hoicvrrex  46576  deccarry  47328  fmtnoprmfac2  47559  sfprmdvdsmersenne  47595  lighneallem3  47599  proththdlem  47605  fppr2odd  47723  gpg3kgrtriexlem2  48045  gpg3kgrtriexlem5  48048  gpg3kgrtriexlem6  48049  gpg3kgrtriex  48050  blennnt2  48515