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

Theorem zmulcld 10971
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 10908 . 2  |-  ( ( A  e.  ZZ  /\  B  e.  ZZ )  ->  ( A  x.  B
)  e.  ZZ )
41, 2, 3syl2anc 659 1  |-  ( ph  ->  ( A  x.  B
)  e.  ZZ )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1823  (class class class)co 6270    x. cmul 9486   ZZcz 10860
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565  ax-resscn 9538  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-addrcl 9542  ax-mulcl 9543  ax-mulrcl 9544  ax-mulcom 9545  ax-addass 9546  ax-mulass 9547  ax-distr 9548  ax-i2m1 9549  ax-1ne0 9550  ax-1rid 9551  ax-rnegex 9552  ax-rrecex 9553  ax-cnre 9554  ax-pre-lttri 9555  ax-pre-lttrn 9556  ax-pre-ltadd 9557
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-nel 2652  df-ral 2809  df-rex 2810  df-reu 2811  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-tp 4021  df-op 4023  df-uni 4236  df-iun 4317  df-br 4440  df-opab 4498  df-mpt 4499  df-tr 4533  df-eprel 4780  df-id 4784  df-po 4789  df-so 4790  df-fr 4827  df-we 4829  df-ord 4870  df-on 4871  df-lim 4872  df-suc 4873  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578  df-riota 6232  df-ov 6273  df-oprab 6274  df-mpt2 6275  df-om 6674  df-recs 7034  df-rdg 7068  df-er 7303  df-en 7510  df-dom 7511  df-sdom 7512  df-pnf 9619  df-mnf 9620  df-ltxr 9622  df-sub 9798  df-neg 9799  df-nn 10532  df-n0 10792  df-z 10861
This theorem is referenced by:  flhalf  11944  quoremz  11964  intfracq  11968  zmodcl  11997  modmul1  12022  eirrlem  14019  dvds2ln  14098  dvdsmod  14127  3dvds  14134  bits0e  14163  bits0o  14164  bitsp1e  14166  bitsp1o  14167  bitsmod  14170  bitscmp  14172  bitsinv1lem  14175  bitsuz  14208  bitsshft  14209  smumullem  14226  smumul  14227  bezoutlem3  14262  bezoutlem4  14263  mulgcd  14268  dvdsmulgcd  14276  mulgcddvds  14329  rpmulgcd2  14330  exprmfct  14335  hashdvds  14389  eulerthlem1  14395  eulerthlem2  14396  prmdiv  14399  prmdiveq  14400  pcpremul  14451  pcqmul  14461  pcaddlem  14491  prmpwdvds  14506  4sqlem5  14544  4sqlem10  14549  4sqlem14  14560  mulgass  16371  odmod  16769  odmulgid  16775  odbezout  16779  gexdvds  16803  odadd1  17053  odadd2  17054  torsubg  17059  ablfacrp  17312  pgpfac1lem2  17321  pgpfac1lem3a  17322  pgpfac1lem3  17323  znunit  18775  znrrg  18777  dyaddisjlem  22170  elqaalem3  22883  aalioulem1  22894  aaliou3lem2  22905  aaliou3lem8  22907  dvdsmulf1o  23668  lgsdirprm  23802  lgsdir  23803  lgsdilem2  23804  lgsdi  23805  lgseisenlem1  23822  lgseisenlem2  23823  lgseisenlem3  23824  lgseisenlem4  23825  lgsquadlem1  23827  lgsquad2lem1  23831  lgsquad3  23834  2sqlem3  23839  2sqlem4  23840  2sqblem  23850  ex-ind-dvds  25372  gxmodid  25479  2sqmod  27870  qqhghm  28203  qqhrhm  28204  dvdspw  29416  pellexlem5  31008  pellexlem6  31009  pell1234qrmulcl  31030  congmul  31144  bezoutr  31162  jm2.18  31169  jm2.19lem1  31170  jm2.19lem2  31171  jm2.19lem3  31172  jm2.19lem4  31173  jm2.22  31176  jm2.23  31177  jm2.20nn  31178  jm2.25  31180  jm2.15nn0  31184  jm2.16nn0  31185  jm2.27c  31188  jm3.1lem3  31200  jm3.1  31201  expdiophlem1  31202  lcmgcdlem  31453  sumnnodd  31875  wallispilem4  32089  stirlinglem3  32097  stirlinglem7  32101  stirlinglem10  32104  stirlinglem11  32105  dirkertrigeqlem1  32119  dirkertrigeqlem3  32121  dirkertrigeq  32122  dirkercncflem2  32125  fourierswlem  32252  fouriersw  32253  etransclem3  32259  etransclem7  32263  etransclem10  32266  etransclem25  32281  etransclem26  32282  etransclem27  32283  etransclem28  32284  etransclem35  32291  etransclem37  32293  etransclem44  32300  etransclem45  32301  mod2eq1n2dvds  32534  2zlidl  32994  dignn0fr  33476  dignn0flhalflem1  33490  inductionexd  38419
  Copyright terms: Public domain W3C validator