Theorem zmulcld 12586

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7349   · cmul 11014  ℤcz 12471

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 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-i2m1 11077  ax-1ne0 11078  ax-1rid 11079  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084  ax-pre-ltadd 11085

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 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5174  df-tr 5200  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6249  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-riota 7306  df-ov 7352  df-oprab 7353  df-mpo 7354  df-om 7800  df-2nd 7925  df-frecs 8214  df-wrecs 8245  df-recs 8294  df-rdg 8332  df-er 8625  df-en 8873  df-dom 8874  df-sdom 8875  df-pnf 11151  df-mnf 11152  df-ltxr 11154  df-sub 11349  df-neg 11350  df-nn 12129  df-n0 12385  df-z 12472

This theorem is referenced by:  2tnp1ge0ge0  13733  flhalf  13734  quoremz  13759  intfracq  13763  zmodcl  13795  modmul1  13831  sqoddm1div8  14150  eirrlem  16113  modmulconst  16199  dvds2ln  16200  dvdsexp2im  16238  dvdsmod  16240  3dvds  16242  even2n  16253  mod2eq1n2dvds  16258  2tp1odd  16263  ltoddhalfle  16272  m1expo  16286  m1exp1  16287  modremain  16319  flodddiv4  16326  bits0e  16340  bits0o  16341  bitsp1e  16343  bitsp1o  16344  bitsmod  16347  bitscmp  16349  bitsinv1lem  16352  bitsuz  16385  bitsshft  16386  smumullem  16403  smumul  16404  gcdmultipled  16445  bezoutlem3  16452  bezoutlem4  16453  mulgcd  16459  dvdsmulgcd  16467  bezoutr  16479  lcmgcdlem  16517  mulgcddvds  16566  rpmulgcd2  16567  coprmprod  16572  divgcdcoprm0  16576  cncongr1  16578  cncongr2  16579  exprmfct  16615  prmdvdsbc  16637  hashdvds  16686  eulerthlem1  16692  eulerthlem2  16693  prmdiv  16696  prmdiveq  16697  pcpremul  16755  pcqmul  16765  pcaddlem  16800  prmpwdvds  16816  4sqlem5  16854  4sqlem10  16859  4sqlem14  16870  mulgass  18990  mulgmodid  18992  odmod  19425  odmulgid  19433  odbezout  19437  gexdvds  19463  odadd1  19727  odadd2  19728  torsubg  19733  ablfacrp  19947  pgpfac1lem2  19956  pgpfac1lem3a  19957  pgpfac1lem3  19958  ablsimpgfindlem1  19988  pzriprnglem6  21393  pzriprnglem8  21395  pzriprnglem12  21399  znunit  21470  znrrg  21472  dyaddisjlem  25494  elqaalem3  26227  aalioulem1  26238  aaliou3lem2  26249  aaliou3lem8  26251  mpodvdsmulf1o  27102  dvdsmulf1o  27104  lgsdirprm  27240  lgsdir  27241  lgsdilem2  27242  lgsdi  27243  gausslemma2dlem1a  27274  gausslemma2dlem5a  27279  gausslemma2dlem5  27280  gausslemma2dlem6  27281  gausslemma2dlem7  27282  gausslemma2d  27283  lgseisenlem1  27284  lgseisenlem2  27285  lgseisenlem3  27286  lgseisenlem4  27287  lgsquadlem1  27289  lgsquad2lem1  27293  lgsquad3  27296  2lgslem1a1  27298  2lgslem1a2  27299  2lgslem1b  27301  2lgslem3b1  27310  2lgslem3c1  27311  2lgsoddprmlem2  27318  2sqlem3  27329  2sqlem4  27330  2sqblem  27340  2sqmod  27345  ex-ind-dvds  30405  elrgspnlem2  33184  zringfrac  33492  cos9thpiminplylem2  33756  qqhghm  33961  qqhrhm  33962  breprexplemc  34606  circlemeth  34614  knoppndvlem2  36497  lcmineqlem6  42017  lcmineqlem14  42025  lcmineqlem18  42029  lcmineqlem21  42032  lcmineqlem22  42033  aks4d1p8d2  42068  aks4d1p8  42070  aks4d1p9  42071  primrootscoprmpow  42082  posbezout  42083  primrootscoprbij  42085  primrootspoweq0  42089  aks6d1c3  42106  aks6d1c4  42107  2np3bcnp1  42127  aks6d1c6lem3  42155  aks6d1c6lem4  42156  aks6d1c6lem5  42160  pellexlem5  42816  pellexlem6  42817  pell1234qrmulcl  42838  congmul  42950  jm2.18  42971  jm2.19lem1  42972  jm2.19lem2  42973  jm2.19lem3  42974  jm2.19lem4  42975  jm2.22  42978  jm2.23  42979  jm2.20nn  42980  jm2.25  42982  jm2.15nn0  42986  jm2.16nn0  42987  jm2.27c  42990  jm3.1lem3  43002  jm3.1  43003  expdiophlem1  43004  inductionexd  44138  sumnnodd  45621  wallispilem4  46059  stirlinglem3  46067  stirlinglem7  46071  stirlinglem10  46074  stirlinglem11  46075  dirkertrigeqlem1  46089  dirkertrigeqlem3  46091  dirkertrigeq  46092  dirkercncflem2  46095  fourierswlem  46221  fouriersw  46222  etransclem3  46228  etransclem7  46232  etransclem10  46235  etransclem25  46250  etransclem26  46251  etransclem27  46252  etransclem28  46253  etransclem35  46260  etransclem37  46262  etransclem44  46269  etransclem45  46270  minusmodnep2tmod  47347  modmkpkne  47355  modmknepk  47356  fmtnoprmfac2lem1  47560  fmtno4prmfac  47566  2pwp1prm  47583  mod42tp1mod8  47596  lighneallem4b  47603  lighneallem4  47604  m2even  47648  fppr2odd  47725  gpg3kgrtriexlem3  48079  gpg3kgrtriexlem6  48082  2zlidl  48234  dignn0fr  48596  dignn0flhalflem1  48610