Theorem zmulcld 12630

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

Syntax hints:   → wi 4   ∈ wcel 2119  (class class class)co 7356   · cmul 11034  ℤcz 12515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-er 8633  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11172  df-mnf 11173  df-ltxr 11175  df-sub 11370  df-neg 11371  df-nn 12166  df-n0 12429  df-z 12516

This theorem is referenced by:  2tnp1ge0ge0  13779  flhalf  13780  quoremz  13805  intfracq  13809  zmodcl  13841  modmul1  13877  sqoddm1div8  14196  eirrlem  16162  modmulconst  16248  dvds2ln  16249  dvdsexp2im  16287  dvdsmod  16289  3dvds  16291  even2n  16302  mod2eq1n2dvds  16307  2tp1odd  16312  ltoddhalfle  16321  m1expo  16335  m1exp1  16336  modremain  16368  flodddiv4  16375  bits0e  16389  bits0o  16390  bitsp1e  16392  bitsp1o  16393  bitsmod  16396  bitscmp  16398  bitsinv1lem  16401  bitsuz  16434  bitsshft  16435  smumullem  16452  smumul  16453  gcdmultipled  16494  bezoutlem3  16501  bezoutlem4  16502  mulgcd  16508  dvdsmulgcd  16516  bezoutr  16528  lcmgcdlem  16566  mulgcddvds  16615  rpmulgcd2  16616  coprmprod  16621  divgcdcoprm0  16625  cncongr1  16627  cncongr2  16628  exprmfct  16665  prmdvdsbc  16687  hashdvds  16736  eulerthlem1  16742  eulerthlem2  16743  prmdiv  16746  prmdiveq  16747  pcpremul  16805  pcqmul  16815  pcaddlem  16850  prmpwdvds  16866  4sqlem5  16904  4sqlem10  16909  4sqlem14  16920  mulgass  19078  mulgmodid  19080  odmod  19512  odmulgid  19520  odbezout  19524  gexdvds  19550  odadd1  19814  odadd2  19815  torsubg  19820  ablfacrp  20034  pgpfac1lem2  20043  pgpfac1lem3a  20044  pgpfac1lem3  20045  ablsimpgfindlem1  20075  pzriprnglem6  21461  pzriprnglem8  21463  pzriprnglem12  21467  znunit  21538  znrrg  21540  dyaddisjlem  25580  elqaalem3  26305  aalioulem1  26316  aaliou3lem2  26327  aaliou3lem8  26329  mpodvdsmulf1o  27175  dvdsmulf1o  27177  lgsdirprm  27312  lgsdir  27313  lgsdilem2  27314  lgsdi  27315  gausslemma2dlem1a  27346  gausslemma2dlem5a  27351  gausslemma2dlem5  27352  gausslemma2dlem6  27353  gausslemma2dlem7  27354  gausslemma2d  27355  lgseisenlem1  27356  lgseisenlem2  27357  lgseisenlem3  27358  lgseisenlem4  27359  lgsquadlem1  27361  lgsquad2lem1  27365  lgsquad3  27368  2lgslem1a1  27370  2lgslem1a2  27371  2lgslem1b  27373  2lgslem3b1  27382  2lgslem3c1  27383  2lgsoddprmlem2  27390  2sqlem3  27401  2sqlem4  27402  2sqblem  27412  2sqmod  27417  ex-ind-dvds  30549  elrgspnlem2  33324  zringfrac  33637  cos9thpiminplylem2  33967  qqhghm  34172  qqhrhm  34173  breprexplemc  34816  circlemeth  34824  knoppndvlem2  36819  lcmineqlem6  42519  lcmineqlem14  42527  lcmineqlem18  42531  lcmineqlem21  42534  lcmineqlem22  42535  aks4d1p8d2  42570  aks4d1p8  42572  aks4d1p9  42573  primrootscoprmpow  42584  posbezout  42585  primrootscoprbij  42587  primrootspoweq0  42591  aks6d1c3  42608  aks6d1c4  42609  2np3bcnp1  42629  aks6d1c6lem3  42657  aks6d1c6lem4  42658  aks6d1c6lem5  42662  pellexlem5  43278  pellexlem6  43279  pell1234qrmulcl  43300  congmul  43412  jm2.18  43433  jm2.19lem1  43434  jm2.19lem2  43435  jm2.19lem3  43436  jm2.19lem4  43437  jm2.22  43440  jm2.23  43441  jm2.20nn  43442  jm2.25  43444  jm2.15nn0  43448  jm2.16nn0  43449  jm2.27c  43452  jm3.1lem3  43464  jm3.1  43465  expdiophlem1  43466  inductionexd  44599  sumnnodd  46075  wallispilem4  46511  stirlinglem3  46519  stirlinglem7  46523  stirlinglem10  46526  stirlinglem11  46527  dirkertrigeqlem1  46541  dirkertrigeqlem3  46543  dirkertrigeq  46544  dirkercncflem2  46547  fourierswlem  46673  fouriersw  46674  etransclem3  46680  etransclem7  46684  etransclem10  46687  etransclem25  46702  etransclem26  46703  etransclem27  46704  etransclem28  46705  etransclem35  46712  etransclem37  46714  etransclem44  46721  etransclem45  46722  minusmodnep2tmod  47822  modmkpkne  47830  modmknepk  47831  fmtnoprmfac2lem1  48044  fmtno4prmfac  48050  2pwp1prm  48067  mod42tp1mod8  48080  lighneallem4b  48087  lighneallem4  48088  nprmdvdsfacm1lem4  48101  ppivalnnprm  48103  m2even  48145  fppr2odd  48222  gpg3kgrtriexlem3  48576  gpg3kgrtriexlem6  48579  2zlidl  48731  dignn0fr  49092  dignn0flhalflem1  49106