Theorem nnmulcld 11691

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

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7156   · cmul 10542  ℕcn 11638

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-addrcl 10598  ax-mulcl 10599  ax-mulrcl 10600  ax-addass 10602  ax-distr 10604  ax-i2m1 10605  ax-1ne0 10606  ax-1rid 10607  ax-rrecex 10609  ax-cnre 10610

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-tr 5173  df-id 5460  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-we 5516  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-pred 6148  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-ov 7159  df-om 7581  df-wrecs 7947  df-recs 8008  df-rdg 8046  df-nn 11639

This theorem is referenced by:  bcm1k  13676  bcp1n  13677  permnn  13687  trireciplem  15217  efaddlem  15446  eftlub  15462  eirrlem  15557  modmulconst  15641  isprm5  16051  crth  16115  phimullem  16116  pcqmul  16190  pcaddlem  16224  pcbc  16236  oddprmdvds  16239  pockthlem  16241  pockthg  16242  vdwlem3  16319  vdwlem6  16322  vdwlem9  16325  torsubg  18974  ablfacrp  19188  dgrcolem1  24863  aalioulem5  24925  aaliou3lem2  24932  log2cnv  25522  log2tlbnd  25523  log2ublem2  25525  log2ub  25527  lgamgulmlem4  25609  wilthlem2  25646  ftalem7  25656  basellem5  25662  mumul  25758  fsumfldivdiaglem  25766  dvdsmulf1o  25771  sgmmul  25777  chtublem  25787  bcmono  25853  bposlem3  25862  bposlem5  25864  gausslemma2dlem1a  25941  lgsquadlem2  25957  lgsquadlem3  25958  lgsquad2lem2  25961  2sqlem6  25999  2sqmod  26012  rplogsumlem1  26060  rplogsumlem2  26061  dchrisum0fmul  26082  vmalogdivsum2  26114  pntrsumbnd2  26143  pntpbnd1  26162  pntpbnd2  26163  ostth2lem2  26210  oddpwdc  31612  eulerpartlemgh  31636  subfaclim  32435  bcprod  32970  faclim2  32980  nnadddir  39212  jm2.27c  39653  relexpmulnn  40103  mccllem  41927  limsup10exlem  42102  wallispilem5  42403  wallispi2lem1  42405  wallispi2  42407  stirlinglem3  42410  stirlinglem8  42415  stirlinglem15  42422  dirkertrigeqlem3  42434  hoicvrrex  42887  deccarry  43560  fmtnoprmfac2  43778  sfprmdvdsmersenne  43817  lighneallem3  43821  proththdlem  43827  fppr2odd  43945  blennnt2  44698