Theorem zmulcld 12728

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

Syntax hints:   → wi 4   ∈ wcel 2108  (class class class)co 7431   · cmul 11160  ℤcz 12613

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-pnf 11297  df-mnf 11298  df-ltxr 11300  df-sub 11494  df-neg 11495  df-nn 12267  df-n0 12527  df-z 12614

This theorem is referenced by:  2tnp1ge0ge0  13869  flhalf  13870  quoremz  13895  intfracq  13899  zmodcl  13931  modmul1  13965  sqoddm1div8  14282  eirrlem  16240  modmulconst  16325  dvds2ln  16326  dvdsexp2im  16364  dvdsmod  16366  3dvds  16368  even2n  16379  mod2eq1n2dvds  16384  2tp1odd  16389  ltoddhalfle  16398  m1expo  16412  m1exp1  16413  modremain  16445  flodddiv4  16452  bits0e  16466  bits0o  16467  bitsp1e  16469  bitsp1o  16470  bitsmod  16473  bitscmp  16475  bitsinv1lem  16478  bitsuz  16511  bitsshft  16512  smumullem  16529  smumul  16530  gcdmultipled  16571  bezoutlem3  16578  bezoutlem4  16579  mulgcd  16585  dvdsmulgcd  16593  bezoutr  16605  lcmgcdlem  16643  mulgcddvds  16692  rpmulgcd2  16693  coprmprod  16698  divgcdcoprm0  16702  cncongr1  16704  cncongr2  16705  exprmfct  16741  prmdvdsbc  16763  hashdvds  16812  eulerthlem1  16818  eulerthlem2  16819  prmdiv  16822  prmdiveq  16823  pcpremul  16881  pcqmul  16891  pcaddlem  16926  prmpwdvds  16942  4sqlem5  16980  4sqlem10  16985  4sqlem14  16996  mulgass  19129  mulgmodid  19131  odmod  19564  odmulgid  19572  odbezout  19576  gexdvds  19602  odadd1  19866  odadd2  19867  torsubg  19872  ablfacrp  20086  pgpfac1lem2  20095  pgpfac1lem3a  20096  pgpfac1lem3  20097  ablsimpgfindlem1  20127  pzriprnglem6  21497  pzriprnglem8  21499  pzriprnglem12  21503  znunit  21582  znrrg  21584  dyaddisjlem  25630  elqaalem3  26363  aalioulem1  26374  aaliou3lem2  26385  aaliou3lem8  26387  mpodvdsmulf1o  27237  dvdsmulf1o  27239  lgsdirprm  27375  lgsdir  27376  lgsdilem2  27377  lgsdi  27378  gausslemma2dlem1a  27409  gausslemma2dlem5a  27414  gausslemma2dlem5  27415  gausslemma2dlem6  27416  gausslemma2dlem7  27417  gausslemma2d  27418  lgseisenlem1  27419  lgseisenlem2  27420  lgseisenlem3  27421  lgseisenlem4  27422  lgsquadlem1  27424  lgsquad2lem1  27428  lgsquad3  27431  2lgslem1a1  27433  2lgslem1a2  27434  2lgslem1b  27436  2lgslem3b1  27445  2lgslem3c1  27446  2lgsoddprmlem2  27453  2sqlem3  27464  2sqlem4  27465  2sqblem  27475  2sqmod  27480  ex-ind-dvds  30480  elrgspnlem2  33247  zringfrac  33582  qqhghm  33989  qqhrhm  33990  breprexplemc  34647  circlemeth  34655  knoppndvlem2  36514  lcmineqlem6  42035  lcmineqlem14  42043  lcmineqlem18  42047  lcmineqlem21  42050  lcmineqlem22  42051  aks4d1p8d2  42086  aks4d1p8  42088  aks4d1p9  42089  primrootscoprmpow  42100  posbezout  42101  primrootscoprbij  42103  primrootspoweq0  42107  aks6d1c3  42124  aks6d1c4  42125  2np3bcnp1  42145  aks6d1c6lem3  42173  aks6d1c6lem4  42174  aks6d1c6lem5  42178  pellexlem5  42844  pellexlem6  42845  pell1234qrmulcl  42866  congmul  42979  jm2.18  43000  jm2.19lem1  43001  jm2.19lem2  43002  jm2.19lem3  43003  jm2.19lem4  43004  jm2.22  43007  jm2.23  43008  jm2.20nn  43009  jm2.25  43011  jm2.15nn0  43015  jm2.16nn0  43016  jm2.27c  43019  jm3.1lem3  43031  jm3.1  43032  expdiophlem1  43033  inductionexd  44168  sumnnodd  45645  wallispilem4  46083  stirlinglem3  46091  stirlinglem7  46095  stirlinglem10  46098  stirlinglem11  46099  dirkertrigeqlem1  46113  dirkertrigeqlem3  46115  dirkertrigeq  46116  dirkercncflem2  46119  fourierswlem  46245  fouriersw  46246  etransclem3  46252  etransclem7  46256  etransclem10  46259  etransclem25  46274  etransclem26  46275  etransclem27  46276  etransclem28  46277  etransclem35  46284  etransclem37  46286  etransclem44  46293  etransclem45  46294  minusmodnep2tmod  47355  fmtnoprmfac2lem1  47553  fmtno4prmfac  47559  2pwp1prm  47576  mod42tp1mod8  47589  lighneallem4b  47596  lighneallem4  47597  m2even  47641  fppr2odd  47718  gpg3nbgrvtxlem  48023  gpg3kgrtriexlem3  48041  gpg3kgrtriexlem6  48044  2zlidl  48156  dignn0fr  48522  dignn0flhalflem1  48536