MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nnmulcld Structured version   Visualization version   GIF version

Theorem nnmulcld 11678
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
StepHypRef Expression
1 nnge1d.1 . 2 (𝜑𝐴 ∈ ℕ)
2 nnmulcld.2 . 2 (𝜑𝐵 ∈ ℕ)
3 nnmulcl 11649 . 2 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 · 𝐵) ∈ ℕ)
41, 2, 3syl2anc 587 1 (𝜑 → (𝐴 · 𝐵) ∈ ℕ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2114  (class class class)co 7140   · cmul 10531  cn 11625
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-sep 5179  ax-nul 5186  ax-pow 5243  ax-pr 5307  ax-un 7446  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-addass 10591  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rrecex 10598  ax-cnre 10599
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ne 3012  df-ral 3135  df-rex 3136  df-reu 3137  df-rab 3139  df-v 3471  df-sbc 3748  df-csb 3856  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4266  df-if 4440  df-pw 4513  df-sn 4540  df-pr 4542  df-tp 4544  df-op 4546  df-uni 4814  df-iun 4896  df-br 5043  df-opab 5105  df-mpt 5123  df-tr 5149  df-id 5437  df-eprel 5442  df-po 5451  df-so 5452  df-fr 5491  df-we 5493  df-xp 5538  df-rel 5539  df-cnv 5540  df-co 5541  df-dm 5542  df-rn 5543  df-res 5544  df-ima 5545  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6293  df-fun 6336  df-fn 6337  df-f 6338  df-f1 6339  df-fo 6340  df-f1o 6341  df-fv 6342  df-ov 7143  df-om 7566  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-nn 11626
This theorem is referenced by:  bcm1k  13671  bcp1n  13672  permnn  13682  trireciplem  15208  efaddlem  15437  eftlub  15453  eirrlem  15548  modmulconst  15632  isprm5  16040  crth  16104  phimullem  16105  pcqmul  16179  pcaddlem  16213  pcbc  16225  oddprmdvds  16228  pockthlem  16230  pockthg  16231  vdwlem3  16308  vdwlem6  16311  vdwlem9  16314  torsubg  18965  ablfacrp  19179  dgrcolem1  24868  aalioulem5  24930  aaliou3lem2  24937  log2cnv  25528  log2tlbnd  25529  log2ublem2  25531  log2ub  25533  lgamgulmlem4  25615  wilthlem2  25652  ftalem7  25662  basellem5  25668  mumul  25764  fsumfldivdiaglem  25772  dvdsmulf1o  25777  sgmmul  25783  chtublem  25793  bcmono  25859  bposlem3  25868  bposlem5  25870  gausslemma2dlem1a  25947  lgsquadlem2  25963  lgsquadlem3  25964  lgsquad2lem2  25967  2sqlem6  26005  2sqmod  26018  rplogsumlem1  26066  rplogsumlem2  26067  dchrisum0fmul  26088  vmalogdivsum2  26120  pntrsumbnd2  26149  pntpbnd1  26168  pntpbnd2  26169  ostth2lem2  26216  oddpwdc  31686  eulerpartlemgh  31710  subfaclim  32509  bcprod  33044  faclim2  33054  nnproddivdvdsd  39250  lcmineqlem14  39291  lcmineqlem15  39292  lcmineqlem16  39293  lcmineqlem19  39296  lcmineqlem20  39297  lcmineqlem22  39299  nnadddir  39415  jm2.27c  39878  relexpmulnn  40340  mccllem  42178  limsup10exlem  42353  wallispilem5  42650  wallispi2lem1  42652  wallispi2  42654  stirlinglem3  42657  stirlinglem8  42662  stirlinglem15  42669  dirkertrigeqlem3  42681  hoicvrrex  43134  deccarry  43807  fmtnoprmfac2  44023  sfprmdvdsmersenne  44060  lighneallem3  44064  proththdlem  44070  fppr2odd  44188  blennnt2  44942
  Copyright terms: Public domain W3C validator