Theorem zmulcld 12644

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7387   · cmul 11073  ℤcz 12529

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-mulcom 11132  ax-addass 11133  ax-mulass 11134  ax-distr 11135  ax-i2m1 11136  ax-1ne0 11137  ax-1rid 11138  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141  ax-pre-lttri 11142  ax-pre-lttrn 11143  ax-pre-ltadd 11144

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-riota 7344  df-ov 7390  df-oprab 7391  df-mpo 7392  df-om 7843  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-er 8671  df-en 8919  df-dom 8920  df-sdom 8921  df-pnf 11210  df-mnf 11211  df-ltxr 11213  df-sub 11407  df-neg 11408  df-nn 12187  df-n0 12443  df-z 12530

This theorem is referenced by:  2tnp1ge0ge0  13791  flhalf  13792  quoremz  13817  intfracq  13821  zmodcl  13853  modmul1  13889  sqoddm1div8  14208  eirrlem  16172  modmulconst  16258  dvds2ln  16259  dvdsexp2im  16297  dvdsmod  16299  3dvds  16301  even2n  16312  mod2eq1n2dvds  16317  2tp1odd  16322  ltoddhalfle  16331  m1expo  16345  m1exp1  16346  modremain  16378  flodddiv4  16385  bits0e  16399  bits0o  16400  bitsp1e  16402  bitsp1o  16403  bitsmod  16406  bitscmp  16408  bitsinv1lem  16411  bitsuz  16444  bitsshft  16445  smumullem  16462  smumul  16463  gcdmultipled  16504  bezoutlem3  16511  bezoutlem4  16512  mulgcd  16518  dvdsmulgcd  16526  bezoutr  16538  lcmgcdlem  16576  mulgcddvds  16625  rpmulgcd2  16626  coprmprod  16631  divgcdcoprm0  16635  cncongr1  16637  cncongr2  16638  exprmfct  16674  prmdvdsbc  16696  hashdvds  16745  eulerthlem1  16751  eulerthlem2  16752  prmdiv  16755  prmdiveq  16756  pcpremul  16814  pcqmul  16824  pcaddlem  16859  prmpwdvds  16875  4sqlem5  16913  4sqlem10  16918  4sqlem14  16929  mulgass  19043  mulgmodid  19045  odmod  19476  odmulgid  19484  odbezout  19488  gexdvds  19514  odadd1  19778  odadd2  19779  torsubg  19784  ablfacrp  19998  pgpfac1lem2  20007  pgpfac1lem3a  20008  pgpfac1lem3  20009  ablsimpgfindlem1  20039  pzriprnglem6  21396  pzriprnglem8  21398  pzriprnglem12  21402  znunit  21473  znrrg  21475  dyaddisjlem  25496  elqaalem3  26229  aalioulem1  26240  aaliou3lem2  26251  aaliou3lem8  26253  mpodvdsmulf1o  27104  dvdsmulf1o  27106  lgsdirprm  27242  lgsdir  27243  lgsdilem2  27244  lgsdi  27245  gausslemma2dlem1a  27276  gausslemma2dlem5a  27281  gausslemma2dlem5  27282  gausslemma2dlem6  27283  gausslemma2dlem7  27284  gausslemma2d  27285  lgseisenlem1  27286  lgseisenlem2  27287  lgseisenlem3  27288  lgseisenlem4  27289  lgsquadlem1  27291  lgsquad2lem1  27295  lgsquad3  27298  2lgslem1a1  27300  2lgslem1a2  27301  2lgslem1b  27303  2lgslem3b1  27312  2lgslem3c1  27313  2lgsoddprmlem2  27320  2sqlem3  27331  2sqlem4  27332  2sqblem  27342  2sqmod  27347  ex-ind-dvds  30390  elrgspnlem2  33194  zringfrac  33525  cos9thpiminplylem2  33773  qqhghm  33978  qqhrhm  33979  breprexplemc  34623  circlemeth  34631  knoppndvlem2  36501  lcmineqlem6  42022  lcmineqlem14  42030  lcmineqlem18  42034  lcmineqlem21  42037  lcmineqlem22  42038  aks4d1p8d2  42073  aks4d1p8  42075  aks4d1p9  42076  primrootscoprmpow  42087  posbezout  42088  primrootscoprbij  42090  primrootspoweq0  42094  aks6d1c3  42111  aks6d1c4  42112  2np3bcnp1  42132  aks6d1c6lem3  42160  aks6d1c6lem4  42161  aks6d1c6lem5  42165  pellexlem5  42821  pellexlem6  42822  pell1234qrmulcl  42843  congmul  42956  jm2.18  42977  jm2.19lem1  42978  jm2.19lem2  42979  jm2.19lem3  42980  jm2.19lem4  42981  jm2.22  42984  jm2.23  42985  jm2.20nn  42986  jm2.25  42988  jm2.15nn0  42992  jm2.16nn0  42993  jm2.27c  42996  jm3.1lem3  43008  jm3.1  43009  expdiophlem1  43010  inductionexd  44144  sumnnodd  45628  wallispilem4  46066  stirlinglem3  46074  stirlinglem7  46078  stirlinglem10  46081  stirlinglem11  46082  dirkertrigeqlem1  46096  dirkertrigeqlem3  46098  dirkertrigeq  46099  dirkercncflem2  46102  fourierswlem  46228  fouriersw  46229  etransclem3  46235  etransclem7  46239  etransclem10  46242  etransclem25  46257  etransclem26  46258  etransclem27  46259  etransclem28  46260  etransclem35  46267  etransclem37  46269  etransclem44  46276  etransclem45  46277  minusmodnep2tmod  47354  modmkpkne  47362  modmknepk  47363  fmtnoprmfac2lem1  47567  fmtno4prmfac  47573  2pwp1prm  47590  mod42tp1mod8  47603  lighneallem4b  47610  lighneallem4  47611  m2even  47655  fppr2odd  47732  gpg3kgrtriexlem3  48076  gpg3kgrtriexlem6  48079  2zlidl  48228  dignn0fr  48590  dignn0flhalflem1  48604