Theorem zmulcld 11840

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 11778	. 2 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 · 𝐵) ∈ ℤ)
4	1, 2, 3	syl2anc 579	1 ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2106  (class class class)co 6922   · cmul 10277  ℤcz 11728

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-8 2108  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-resscn 10329  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-addrcl 10333  ax-mulcl 10334  ax-mulrcl 10335  ax-mulcom 10336  ax-addass 10337  ax-mulass 10338  ax-distr 10339  ax-i2m1 10340  ax-1ne0 10341  ax-1rid 10342  ax-rnegex 10343  ax-rrecex 10344  ax-cnre 10345  ax-pre-lttri 10346  ax-pre-lttrn 10347  ax-pre-ltadd 10348

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2550  df-eu 2586  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-ne 2969  df-nel 3075  df-ral 3094  df-rex 3095  df-reu 3096  df-rab 3098  df-v 3399  df-sbc 3652  df-csb 3751  df-dif 3794  df-un 3796  df-in 3798  df-ss 3805  df-pss 3807  df-nul 4141  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4672  df-iun 4755  df-br 4887  df-opab 4949  df-mpt 4966  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-pred 5933  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-riota 6883  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-om 7344  df-wrecs 7689  df-recs 7751  df-rdg 7789  df-er 8026  df-en 8242  df-dom 8243  df-sdom 8244  df-pnf 10413  df-mnf 10414  df-ltxr 10416  df-sub 10608  df-neg 10609  df-nn 11375  df-n0 11643  df-z 11729

This theorem is referenced by:  2tnp1ge0ge0  12949  flhalf  12950  quoremz  12973  intfracq  12977  zmodcl  13009  modmul1  13042  sqoddm1div8  13349  eirrlem  15336  modmulconst  15420  dvds2ln  15421  dvdsmod  15457  3dvds  15459  even2n  15470  mod2eq1n2dvds  15475  2tp1odd  15480  ltoddhalfle  15489  m1expo  15505  m1exp1  15506  modremain  15538  flodddiv4  15543  bits0e  15557  bits0o  15558  bitsp1e  15560  bitsp1o  15561  bitsmod  15564  bitscmp  15566  bitsinv1lem  15569  bitsuz  15602  bitsshft  15603  smumullem  15620  smumul  15621  bezoutlem3  15664  bezoutlem4  15665  mulgcd  15671  dvdsmulgcd  15680  bezoutr  15687  lcmgcdlem  15725  mulgcddvds  15774  rpmulgcd2  15775  coprmprod  15780  divgcdcoprm0  15784  cncongr1  15786  cncongr2  15787  exprmfct  15820  hashdvds  15884  eulerthlem1  15890  eulerthlem2  15891  prmdiv  15894  prmdiveq  15895  pcpremul  15952  pcqmul  15962  pcaddlem  15996  prmpwdvds  16012  4sqlem5  16050  4sqlem10  16055  4sqlem14  16066  mulgass  17963  mulgmodid  17965  odmod  18349  odmulgid  18355  odbezout  18359  gexdvds  18383  odadd1  18637  odadd2  18638  torsubg  18643  ablfacrp  18852  pgpfac1lem2  18861  pgpfac1lem3a  18862  pgpfac1lem3  18863  znunit  20307  znrrg  20309  dyaddisjlem  23799  elqaalem3  24513  aalioulem1  24524  aaliou3lem2  24535  aaliou3lem8  24537  dvdsmulf1o  25372  lgsdirprm  25508  lgsdir  25509  lgsdilem2  25510  lgsdi  25511  gausslemma2dlem1a  25542  gausslemma2dlem5a  25547  gausslemma2dlem5  25548  gausslemma2dlem6  25549  gausslemma2dlem7  25550  gausslemma2d  25551  lgseisenlem1  25552  lgseisenlem2  25553  lgseisenlem3  25554  lgseisenlem4  25555  lgsquadlem1  25557  lgsquad2lem1  25561  lgsquad3  25564  2lgslem1a1  25566  2lgslem1a2  25567  2lgslem1b  25569  2lgslem3b1  25578  2lgslem3c1  25579  2lgsoddprmlem2  25586  2sqlem3  25597  2sqlem4  25598  2sqblem  25608  ex-ind-dvds  27907  2sqmod  30224  qqhghm  30644  qqhrhm  30645  breprexplemc  31326  circlemeth  31334  dvdspw  32244  knoppndvlem2  33100  pellexlem5  38349  pellexlem6  38350  pell1234qrmulcl  38371  congmul  38485  jm2.18  38506  jm2.19lem1  38507  jm2.19lem2  38508  jm2.19lem3  38509  jm2.19lem4  38510  jm2.22  38513  jm2.23  38514  jm2.20nn  38515  jm2.25  38517  jm2.15nn0  38521  jm2.16nn0  38522  jm2.27c  38525  jm3.1lem3  38537  jm3.1  38538  expdiophlem1  38539  inductionexd  39401  sumnnodd  40762  wallispilem4  41204  stirlinglem3  41212  stirlinglem7  41216  stirlinglem10  41219  stirlinglem11  41220  dirkertrigeqlem1  41234  dirkertrigeqlem3  41236  dirkertrigeq  41237  dirkercncflem2  41240  fourierswlem  41366  fouriersw  41367  etransclem3  41373  etransclem7  41377  etransclem10  41380  etransclem25  41395  etransclem26  41396  etransclem27  41397  etransclem28  41398  etransclem35  41405  etransclem37  41407  etransclem44  41414  etransclem45  41415  fmtnoprmfac2lem1  42491  fmtno4prmfac  42497  2pwp1prm  42516  mod42tp1mod8  42532  lighneallem4b  42539  lighneallem4  42540  2zlidl  42941  dignn0fr  43402  dignn0flhalflem1  43416