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

Theorem zmulcld 12081
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 12019 . 2 ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 · 𝐵) ∈ ℤ)
41, 2, 3syl2anc 584 1 (𝜑 → (𝐴 · 𝐵) ∈ ℤ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  (class class class)co 7145   · cmul 10530  cz 11969
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-i2m1 10593  ax-1ne0 10594  ax-1rid 10595  ax-rnegex 10596  ax-rrecex 10597  ax-cnre 10598  ax-pre-lttri 10599  ax-pre-lttrn 10600  ax-pre-ltadd 10601
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7570  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-er 8278  df-en 8498  df-dom 8499  df-sdom 8500  df-pnf 10665  df-mnf 10666  df-ltxr 10668  df-sub 10860  df-neg 10861  df-nn 11627  df-n0 11886  df-z 11970
This theorem is referenced by:  2tnp1ge0ge0  13187  flhalf  13188  quoremz  13211  intfracq  13215  zmodcl  13247  modmul1  13280  sqoddm1div8  13592  eirrlem  15545  modmulconst  15629  dvds2ln  15630  dvdsmod  15666  3dvds  15668  even2n  15679  mod2eq1n2dvds  15684  2tp1odd  15689  ltoddhalfle  15698  m1expo  15714  m1exp1  15715  modremain  15747  flodddiv4  15752  bits0e  15766  bits0o  15767  bitsp1e  15769  bitsp1o  15770  bitsmod  15773  bitscmp  15775  bitsinv1lem  15778  bitsuz  15811  bitsshft  15812  smumullem  15829  smumul  15830  gcdmultipled  15870  bezoutlem3  15877  bezoutlem4  15878  mulgcd  15884  dvdsmulgcd  15893  bezoutr  15900  lcmgcdlem  15938  mulgcddvds  15987  rpmulgcd2  15988  coprmprod  15993  divgcdcoprm0  15997  cncongr1  15999  cncongr2  16000  exprmfct  16036  hashdvds  16100  eulerthlem1  16106  eulerthlem2  16107  prmdiv  16110  prmdiveq  16111  pcpremul  16168  pcqmul  16178  pcaddlem  16212  prmpwdvds  16228  4sqlem5  16266  4sqlem10  16271  4sqlem14  16282  mulgass  18202  mulgmodid  18204  odmod  18603  odmulgid  18610  odbezout  18614  gexdvds  18638  odadd1  18897  odadd2  18898  torsubg  18903  ablfacrp  19117  pgpfac1lem2  19126  pgpfac1lem3a  19127  pgpfac1lem3  19128  ablsimpgfindlem1  19158  znunit  20638  znrrg  20640  dyaddisjlem  24123  elqaalem3  24837  aalioulem1  24848  aaliou3lem2  24859  aaliou3lem8  24861  dvdsmulf1o  25698  lgsdirprm  25834  lgsdir  25835  lgsdilem2  25836  lgsdi  25837  gausslemma2dlem1a  25868  gausslemma2dlem5a  25873  gausslemma2dlem5  25874  gausslemma2dlem6  25875  gausslemma2dlem7  25876  gausslemma2d  25877  lgseisenlem1  25878  lgseisenlem2  25879  lgseisenlem3  25880  lgseisenlem4  25881  lgsquadlem1  25883  lgsquad2lem1  25887  lgsquad3  25890  2lgslem1a1  25892  2lgslem1a2  25893  2lgslem1b  25895  2lgslem3b1  25904  2lgslem3c1  25905  2lgsoddprmlem2  25912  2sqlem3  25923  2sqlem4  25924  2sqblem  25934  2sqmod  25939  ex-ind-dvds  28167  prmdvdsbc  30458  qqhghm  31128  qqhrhm  31129  breprexplemc  31802  circlemeth  31810  dvdspw  32879  knoppndvlem2  33749  pellexlem5  39308  pellexlem6  39309  pell1234qrmulcl  39330  congmul  39442  jm2.18  39463  jm2.19lem1  39464  jm2.19lem2  39465  jm2.19lem3  39466  jm2.19lem4  39467  jm2.22  39470  jm2.23  39471  jm2.20nn  39472  jm2.25  39474  jm2.15nn0  39478  jm2.16nn0  39479  jm2.27c  39482  jm3.1lem3  39494  jm3.1  39495  expdiophlem1  39496  inductionexd  40383  sumnnodd  41787  wallispilem4  42230  stirlinglem3  42238  stirlinglem7  42242  stirlinglem10  42245  stirlinglem11  42246  dirkertrigeqlem1  42260  dirkertrigeqlem3  42262  dirkertrigeq  42263  dirkercncflem2  42266  fourierswlem  42392  fouriersw  42393  etransclem3  42399  etransclem7  42403  etransclem10  42406  etransclem25  42421  etransclem26  42422  etransclem27  42423  etransclem28  42424  etransclem35  42431  etransclem37  42433  etransclem44  42440  etransclem45  42441  fmtnoprmfac2lem1  43605  fmtno4prmfac  43611  2pwp1prm  43628  mod42tp1mod8  43644  lighneallem4b  43651  lighneallem4  43652  m2even  43696  fppr2odd  43773  2zlidl  44133  dignn0fr  44589  dignn0flhalflem1  44603
  Copyright terms: Public domain W3C validator