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

Theorem zmulcld 11035
Description: Closure of multiplication of integers. (Contributed by Mario Carneiro, 28-May-2016.)
Hypotheses
Ref Expression
zred.1  |-  ( ph  ->  A  e.  ZZ )
zaddcld.1  |-  ( ph  ->  B  e.  ZZ )
Assertion
Ref Expression
zmulcld  |-  ( ph  ->  ( A  x.  B
)  e.  ZZ )

Proof of Theorem zmulcld
StepHypRef Expression
1 zred.1 . 2  |-  ( ph  ->  A  e.  ZZ )
2 zaddcld.1 . 2  |-  ( ph  ->  B  e.  ZZ )
3 zmulcl 10974 . 2  |-  ( ( A  e.  ZZ  /\  B  e.  ZZ )  ->  ( A  x.  B
)  e.  ZZ )
41, 2, 3syl2anc 671 1  |-  ( ph  ->  ( A  x.  B
)  e.  ZZ )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1890  (class class class)co 6275    x. cmul 9530   ZZcz 10926
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1672  ax-4 1685  ax-5 1761  ax-6 1808  ax-7 1854  ax-8 1892  ax-9 1899  ax-10 1918  ax-11 1923  ax-12 1936  ax-13 2091  ax-ext 2431  ax-sep 4496  ax-nul 4505  ax-pow 4553  ax-pr 4611  ax-un 6570  ax-resscn 9582  ax-1cn 9583  ax-icn 9584  ax-addcl 9585  ax-addrcl 9586  ax-mulcl 9587  ax-mulrcl 9588  ax-mulcom 9589  ax-addass 9590  ax-mulass 9591  ax-distr 9592  ax-i2m1 9593  ax-1ne0 9594  ax-1rid 9595  ax-rnegex 9596  ax-rrecex 9597  ax-cnre 9598  ax-pre-lttri 9599  ax-pre-lttrn 9600  ax-pre-ltadd 9601
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 987  df-3an 988  df-tru 1450  df-ex 1667  df-nf 1671  df-sb 1801  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2623  df-nel 2624  df-ral 2741  df-rex 2742  df-reu 2743  df-rab 2745  df-v 3014  df-sbc 3235  df-csb 3331  df-dif 3374  df-un 3376  df-in 3378  df-ss 3385  df-pss 3387  df-nul 3699  df-if 3849  df-pw 3920  df-sn 3936  df-pr 3938  df-tp 3940  df-op 3942  df-uni 4168  df-iun 4249  df-br 4374  df-opab 4433  df-mpt 4434  df-tr 4469  df-eprel 4722  df-id 4726  df-po 4732  df-so 4733  df-fr 4770  df-we 4772  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824  df-pred 5358  df-ord 5404  df-on 5405  df-lim 5406  df-suc 5407  df-iota 5524  df-fun 5562  df-fn 5563  df-f 5564  df-f1 5565  df-fo 5566  df-f1o 5567  df-fv 5568  df-riota 6237  df-ov 6278  df-oprab 6279  df-mpt2 6280  df-om 6680  df-wrecs 7014  df-recs 7076  df-rdg 7114  df-er 7349  df-en 7556  df-dom 7557  df-sdom 7558  df-pnf 9663  df-mnf 9664  df-ltxr 9666  df-sub 9848  df-neg 9849  df-nn 10598  df-n0 10859  df-z 10927
This theorem is referenced by:  flhalf  12055  quoremz  12075  intfracq  12079  zmodcl  12109  modmul1  12136  eirrlem  14266  dvds2ln  14343  dvdsmod  14372  3dvds  14379  bits0e  14412  bits0o  14413  bitsp1e  14415  bitsp1o  14416  bitsmod  14420  bitscmp  14422  bitsinv1lem  14425  bitsuz  14458  bitsshft  14459  smumullem  14476  smumul  14477  bezoutlem3OLD  14515  bezoutlem4OLD  14516  bezoutlem3  14518  bezoutlem4  14519  mulgcd  14524  dvdsmulgcd  14532  lcmgcdlem  14581  exprmfct  14658  mulgcddvds  14671  rpmulgcd2  14672  coprmprod  14688  hashdvds  14733  eulerthlem1  14739  eulerthlem2  14740  prmdiv  14743  prmdiveq  14744  pcpremul  14803  pcqmul  14813  pcaddlem  14843  prmpwdvds  14858  4sqlem5  14896  4sqlem10  14901  4sqlem14OLD  14912  4sqlem14  14918  mulgass  16798  odmod  17205  odmulgid  17215  odbezout  17219  gexdvds  17245  odadd1  17496  odadd2  17497  torsubg  17502  ablfacrp  17709  pgpfac1lem2  17718  pgpfac1lem3a  17719  pgpfac1lem3  17720  znunit  19144  znrrg  19146  dyaddisjlem  22564  elqaalem3  23285  elqaalem3OLD  23288  aalioulem1  23299  aaliou3lem2  23310  aaliou3lem8  23312  dvdsmulf1o  24134  lgsdirprm  24268  lgsdir  24269  lgsdilem2  24270  lgsdi  24271  lgseisenlem1  24288  lgseisenlem2  24289  lgseisenlem3  24290  lgseisenlem4  24291  lgsquadlem1  24293  lgsquad2lem1  24297  lgsquad3  24300  2sqlem3  24305  2sqlem4  24306  2sqblem  24316  ex-ind-dvds  25910  gxmodid  26018  2sqmod  28416  qqhghm  28798  qqhrhm  28799  dvdspw  30391  pellexlem5  35678  pellexlem6  35679  pell1234qrmulcl  35702  congmul  35818  bezoutr  35836  jm2.18  35844  jm2.19lem1  35845  jm2.19lem2  35846  jm2.19lem3  35847  jm2.19lem4  35848  jm2.22  35851  jm2.23  35852  jm2.20nn  35853  jm2.25  35855  jm2.15nn0  35859  jm2.16nn0  35860  jm2.27c  35863  jm3.1lem3  35875  jm3.1  35876  expdiophlem1  35877  inductionexd  36594  sumnnodd  37751  wallispilem4  37986  stirlinglem3  37994  stirlinglem7  37998  stirlinglem10  38001  stirlinglem11  38002  dirkertrigeqlem1  38016  dirkertrigeqlem3  38018  dirkertrigeq  38019  dirkercncflem2  38022  fourierswlem  38150  fouriersw  38151  etransclem3  38158  etransclem7  38162  etransclem10  38165  etransclem25  38180  etransclem26  38181  etransclem27  38182  etransclem28  38183  etransclem35  38190  etransclem37  38192  etransclem44  38199  etransclem45  38200  mod2eq1n2dvds  38815  2zlidl  40258  dignn0fr  40736  dignn0flhalflem1  40750
  Copyright terms: Public domain W3C validator