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

Theorem zmulcld 12614
Description: Closure of multiplication of integers. (Contributed by Mario Carneiro, 28-May-2016.)
Hypotheses
Ref Expression
zred.1 (๐œ‘ โ†’ ๐ด โˆˆ โ„ค)
zaddcld.1 (๐œ‘ โ†’ ๐ต โˆˆ โ„ค)
Assertion
Ref Expression
zmulcld (๐œ‘ โ†’ (๐ด ยท ๐ต) โˆˆ โ„ค)

Proof of Theorem zmulcld
StepHypRef Expression
1 zred.1 . 2 (๐œ‘ โ†’ ๐ด โˆˆ โ„ค)
2 zaddcld.1 . 2 (๐œ‘ โ†’ ๐ต โˆˆ โ„ค)
3 zmulcl 12553 . 2 ((๐ด โˆˆ โ„ค โˆง ๐ต โˆˆ โ„ค) โ†’ (๐ด ยท ๐ต) โˆˆ โ„ค)
41, 2, 3syl2anc 585 1 (๐œ‘ โ†’ (๐ด ยท ๐ต) โˆˆ โ„ค)
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โˆˆ wcel 2107  (class class class)co 7358   ยท cmul 11057  โ„คcz 12500
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-resscn 11109  ax-1cn 11110  ax-icn 11111  ax-addcl 11112  ax-addrcl 11113  ax-mulcl 11114  ax-mulrcl 11115  ax-mulcom 11116  ax-addass 11117  ax-mulass 11118  ax-distr 11119  ax-i2m1 11120  ax-1ne0 11121  ax-1rid 11122  ax-rnegex 11123  ax-rrecex 11124  ax-cnre 11125  ax-pre-lttri 11126  ax-pre-lttrn 11127  ax-pre-ltadd 11128
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-reu 3355  df-rab 3409  df-v 3448  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7804  df-2nd 7923  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-rdg 8357  df-er 8649  df-en 8885  df-dom 8886  df-sdom 8887  df-pnf 11192  df-mnf 11193  df-ltxr 11195  df-sub 11388  df-neg 11389  df-nn 12155  df-n0 12415  df-z 12501
This theorem is referenced by:  2tnp1ge0ge0  13735  flhalf  13736  quoremz  13761  intfracq  13765  zmodcl  13797  modmul1  13830  sqoddm1div8  14147  eirrlem  16087  modmulconst  16171  dvds2ln  16172  dvdsexp2im  16210  dvdsmod  16212  3dvds  16214  even2n  16225  mod2eq1n2dvds  16230  2tp1odd  16235  ltoddhalfle  16244  m1expo  16258  m1exp1  16259  modremain  16291  flodddiv4  16296  bits0e  16310  bits0o  16311  bitsp1e  16313  bitsp1o  16314  bitsmod  16317  bitscmp  16319  bitsinv1lem  16322  bitsuz  16355  bitsshft  16356  smumullem  16373  smumul  16374  gcdmultipled  16416  bezoutlem3  16423  bezoutlem4  16424  mulgcd  16430  dvdsmulgcd  16437  bezoutr  16445  lcmgcdlem  16483  mulgcddvds  16532  rpmulgcd2  16533  coprmprod  16538  divgcdcoprm0  16542  cncongr1  16544  cncongr2  16545  exprmfct  16581  hashdvds  16648  eulerthlem1  16654  eulerthlem2  16655  prmdiv  16658  prmdiveq  16659  pcpremul  16716  pcqmul  16726  pcaddlem  16761  prmpwdvds  16777  4sqlem5  16815  4sqlem10  16820  4sqlem14  16831  mulgass  18914  mulgmodid  18916  odmod  19329  odmulgid  19337  odbezout  19341  gexdvds  19367  odadd1  19627  odadd2  19628  torsubg  19633  ablfacrp  19846  pgpfac1lem2  19855  pgpfac1lem3a  19856  pgpfac1lem3  19857  ablsimpgfindlem1  19887  znunit  20973  znrrg  20975  dyaddisjlem  24962  elqaalem3  25684  aalioulem1  25695  aaliou3lem2  25706  aaliou3lem8  25708  dvdsmulf1o  26546  lgsdirprm  26682  lgsdir  26683  lgsdilem2  26684  lgsdi  26685  gausslemma2dlem1a  26716  gausslemma2dlem5a  26721  gausslemma2dlem5  26722  gausslemma2dlem6  26723  gausslemma2dlem7  26724  gausslemma2d  26725  lgseisenlem1  26726  lgseisenlem2  26727  lgseisenlem3  26728  lgseisenlem4  26729  lgsquadlem1  26731  lgsquad2lem1  26735  lgsquad3  26738  2lgslem1a1  26740  2lgslem1a2  26741  2lgslem1b  26743  2lgslem3b1  26752  2lgslem3c1  26753  2lgsoddprmlem2  26760  2sqlem3  26771  2sqlem4  26772  2sqblem  26782  2sqmod  26787  ex-ind-dvds  29408  prmdvdsbc  31715  qqhghm  32572  qqhrhm  32573  breprexplemc  33248  circlemeth  33256  knoppndvlem2  34979  lcmineqlem6  40494  lcmineqlem14  40502  lcmineqlem18  40506  lcmineqlem21  40509  lcmineqlem22  40510  aks4d1p8d2  40545  aks4d1p8  40547  aks4d1p9  40548  2np3bcnp1  40555  pellexlem5  41159  pellexlem6  41160  pell1234qrmulcl  41181  congmul  41294  jm2.18  41315  jm2.19lem1  41316  jm2.19lem2  41317  jm2.19lem3  41318  jm2.19lem4  41319  jm2.22  41322  jm2.23  41323  jm2.20nn  41324  jm2.25  41326  jm2.15nn0  41330  jm2.16nn0  41331  jm2.27c  41334  jm3.1lem3  41346  jm3.1  41347  expdiophlem1  41348  inductionexd  42434  sumnnodd  43878  wallispilem4  44316  stirlinglem3  44324  stirlinglem7  44328  stirlinglem10  44331  stirlinglem11  44332  dirkertrigeqlem1  44346  dirkertrigeqlem3  44348  dirkertrigeq  44349  dirkercncflem2  44352  fourierswlem  44478  fouriersw  44479  etransclem3  44485  etransclem7  44489  etransclem10  44492  etransclem25  44507  etransclem26  44508  etransclem27  44509  etransclem28  44510  etransclem35  44517  etransclem37  44519  etransclem44  44526  etransclem45  44527  fmtnoprmfac2lem1  45765  fmtno4prmfac  45771  2pwp1prm  45788  mod42tp1mod8  45801  lighneallem4b  45808  lighneallem4  45809  m2even  45853  fppr2odd  45930  2zlidl  46239  dignn0fr  46694  dignn0flhalflem1  46708
  Copyright terms: Public domain W3C validator