Theorem zmulcld 12676

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

Step	Hyp	Ref	Expression
1		zred.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℤ)
2		zaddcld.1	. 2 ⊢ (𝜑 → 𝐵 ∈ ℤ)
3		zmulcl 12615	. 2 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 · 𝐵) ∈ ℤ)
4	1, 2, 3	syl2anc 582	1 ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2104  (class class class)co 7411   · cmul 11117  ℤcz 12562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-pnf 11254  df-mnf 11255  df-ltxr 11257  df-sub 11450  df-neg 11451  df-nn 12217  df-n0 12477  df-z 12563

This theorem is referenced by:  2tnp1ge0ge0  13798  flhalf  13799  quoremz  13824  intfracq  13828  zmodcl  13860  modmul1  13893  sqoddm1div8  14210  eirrlem  16151  modmulconst  16235  dvds2ln  16236  dvdsexp2im  16274  dvdsmod  16276  3dvds  16278  even2n  16289  mod2eq1n2dvds  16294  2tp1odd  16299  ltoddhalfle  16308  m1expo  16322  m1exp1  16323  modremain  16355  flodddiv4  16360  bits0e  16374  bits0o  16375  bitsp1e  16377  bitsp1o  16378  bitsmod  16381  bitscmp  16383  bitsinv1lem  16386  bitsuz  16419  bitsshft  16420  smumullem  16437  smumul  16438  gcdmultipled  16480  bezoutlem3  16487  bezoutlem4  16488  mulgcd  16494  dvdsmulgcd  16501  bezoutr  16509  lcmgcdlem  16547  mulgcddvds  16596  rpmulgcd2  16597  coprmprod  16602  divgcdcoprm0  16606  cncongr1  16608  cncongr2  16609  exprmfct  16645  hashdvds  16712  eulerthlem1  16718  eulerthlem2  16719  prmdiv  16722  prmdiveq  16723  pcpremul  16780  pcqmul  16790  pcaddlem  16825  prmpwdvds  16841  4sqlem5  16879  4sqlem10  16884  4sqlem14  16895  mulgass  19027  mulgmodid  19029  odmod  19455  odmulgid  19463  odbezout  19467  gexdvds  19493  odadd1  19757  odadd2  19758  torsubg  19763  ablfacrp  19977  pgpfac1lem2  19986  pgpfac1lem3a  19987  pgpfac1lem3  19988  ablsimpgfindlem1  20018  pzriprnglem6  21255  pzriprnglem8  21257  pzriprnglem12  21261  znunit  21338  znrrg  21340  dyaddisjlem  25344  elqaalem3  26070  aalioulem1  26081  aaliou3lem2  26092  aaliou3lem8  26094  dvdsmulf1o  26934  lgsdirprm  27070  lgsdir  27071  lgsdilem2  27072  lgsdi  27073  gausslemma2dlem1a  27104  gausslemma2dlem5a  27109  gausslemma2dlem5  27110  gausslemma2dlem6  27111  gausslemma2dlem7  27112  gausslemma2d  27113  lgseisenlem1  27114  lgseisenlem2  27115  lgseisenlem3  27116  lgseisenlem4  27117  lgsquadlem1  27119  lgsquad2lem1  27123  lgsquad3  27126  2lgslem1a1  27128  2lgslem1a2  27129  2lgslem1b  27131  2lgslem3b1  27140  2lgslem3c1  27141  2lgsoddprmlem2  27148  2sqlem3  27159  2sqlem4  27160  2sqblem  27170  2sqmod  27175  ex-ind-dvds  29981  prmdvdsbc  32289  qqhghm  33266  qqhrhm  33267  breprexplemc  33942  circlemeth  33950  knoppndvlem2  35692  lcmineqlem6  41205  lcmineqlem14  41213  lcmineqlem18  41217  lcmineqlem21  41220  lcmineqlem22  41221  aks4d1p8d2  41256  aks4d1p8  41258  aks4d1p9  41259  2np3bcnp1  41266  pellexlem5  41873  pellexlem6  41874  pell1234qrmulcl  41895  congmul  42008  jm2.18  42029  jm2.19lem1  42030  jm2.19lem2  42031  jm2.19lem3  42032  jm2.19lem4  42033  jm2.22  42036  jm2.23  42037  jm2.20nn  42038  jm2.25  42040  jm2.15nn0  42044  jm2.16nn0  42045  jm2.27c  42048  jm3.1lem3  42060  jm3.1  42061  expdiophlem1  42062  inductionexd  43208  sumnnodd  44644  wallispilem4  45082  stirlinglem3  45090  stirlinglem7  45094  stirlinglem10  45097  stirlinglem11  45098  dirkertrigeqlem1  45112  dirkertrigeqlem3  45114  dirkertrigeq  45115  dirkercncflem2  45118  fourierswlem  45244  fouriersw  45245  etransclem3  45251  etransclem7  45255  etransclem10  45258  etransclem25  45273  etransclem26  45274  etransclem27  45275  etransclem28  45276  etransclem35  45283  etransclem37  45285  etransclem44  45292  etransclem45  45293  fmtnoprmfac2lem1  46532  fmtno4prmfac  46538  2pwp1prm  46555  mod42tp1mod8  46568  lighneallem4b  46575  lighneallem4  46576  m2even  46620  fppr2odd  46697  2zlidl  46920  dignn0fr  47374  dignn0flhalflem1  47388