Theorem zmulcld 12639

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

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7367   · cmul 11043  ℤcz 12524

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3062  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-riota 7324  df-ov 7370  df-oprab 7371  df-mpo 7372  df-om 7818  df-2nd 7943  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-er 8643  df-en 8894  df-dom 8895  df-sdom 8896  df-pnf 11181  df-mnf 11182  df-ltxr 11184  df-sub 11379  df-neg 11380  df-nn 12175  df-n0 12438  df-z 12525

This theorem is referenced by:  2tnp1ge0ge0  13788  flhalf  13789  quoremz  13814  intfracq  13818  zmodcl  13850  modmul1  13886  sqoddm1div8  14205  eirrlem  16171  modmulconst  16257  dvds2ln  16258  dvdsexp2im  16296  dvdsmod  16298  3dvds  16300  even2n  16311  mod2eq1n2dvds  16316  2tp1odd  16321  ltoddhalfle  16330  m1expo  16344  m1exp1  16345  modremain  16377  flodddiv4  16384  bits0e  16398  bits0o  16399  bitsp1e  16401  bitsp1o  16402  bitsmod  16405  bitscmp  16407  bitsinv1lem  16410  bitsuz  16443  bitsshft  16444  smumullem  16461  smumul  16462  gcdmultipled  16503  bezoutlem3  16510  bezoutlem4  16511  mulgcd  16517  dvdsmulgcd  16525  bezoutr  16537  lcmgcdlem  16575  mulgcddvds  16624  rpmulgcd2  16625  coprmprod  16630  divgcdcoprm0  16634  cncongr1  16636  cncongr2  16637  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  19087  mulgmodid  19089  odmod  19521  odmulgid  19529  odbezout  19533  gexdvds  19559  odadd1  19823  odadd2  19824  torsubg  19829  ablfacrp  20043  pgpfac1lem2  20052  pgpfac1lem3a  20053  pgpfac1lem3  20054  ablsimpgfindlem1  20084  pzriprnglem6  21466  pzriprnglem8  21468  pzriprnglem12  21472  znunit  21543  znrrg  21545  dyaddisjlem  25562  elqaalem3  26287  aalioulem1  26298  aaliou3lem2  26309  aaliou3lem8  26311  mpodvdsmulf1o  27157  dvdsmulf1o  27159  lgsdirprm  27294  lgsdir  27295  lgsdilem2  27296  lgsdi  27297  gausslemma2dlem1a  27328  gausslemma2dlem5a  27333  gausslemma2dlem5  27334  gausslemma2dlem6  27335  gausslemma2dlem7  27336  gausslemma2d  27337  lgseisenlem1  27338  lgseisenlem2  27339  lgseisenlem3  27340  lgseisenlem4  27341  lgsquadlem1  27343  lgsquad2lem1  27347  lgsquad3  27350  2lgslem1a1  27352  2lgslem1a2  27353  2lgslem1b  27355  2lgslem3b1  27364  2lgslem3c1  27365  2lgsoddprmlem2  27372  2sqlem3  27383  2sqlem4  27384  2sqblem  27394  2sqmod  27399  ex-ind-dvds  30531  elrgspnlem2  33304  zringfrac  33614  cos9thpiminplylem2  33927  qqhghm  34132  qqhrhm  34133  breprexplemc  34776  circlemeth  34784  knoppndvlem2  36773  lcmineqlem6  42473  lcmineqlem14  42481  lcmineqlem18  42485  lcmineqlem21  42488  lcmineqlem22  42489  aks4d1p8d2  42524  aks4d1p8  42526  aks4d1p9  42527  primrootscoprmpow  42538  posbezout  42539  primrootscoprbij  42541  primrootspoweq0  42545  aks6d1c3  42562  aks6d1c4  42563  2np3bcnp1  42583  aks6d1c6lem3  42611  aks6d1c6lem4  42612  aks6d1c6lem5  42616  pellexlem5  43261  pellexlem6  43262  pell1234qrmulcl  43283  congmul  43395  jm2.18  43416  jm2.19lem1  43417  jm2.19lem2  43418  jm2.19lem3  43419  jm2.19lem4  43420  jm2.22  43423  jm2.23  43424  jm2.20nn  43425  jm2.25  43427  jm2.15nn0  43431  jm2.16nn0  43432  jm2.27c  43435  jm3.1lem3  43447  jm3.1  43448  expdiophlem1  43449  inductionexd  44582  sumnnodd  46060  wallispilem4  46496  stirlinglem3  46504  stirlinglem7  46508  stirlinglem10  46511  stirlinglem11  46512  dirkertrigeqlem1  46526  dirkertrigeqlem3  46528  dirkertrigeq  46529  dirkercncflem2  46532  fourierswlem  46658  fouriersw  46659  etransclem3  46665  etransclem7  46669  etransclem10  46672  etransclem25  46687  etransclem26  46688  etransclem27  46689  etransclem28  46690  etransclem35  46697  etransclem37  46699  etransclem44  46706  etransclem45  46707  minusmodnep2tmod  47807  modmkpkne  47815  modmknepk  47816  fmtnoprmfac2lem1  48029  fmtno4prmfac  48035  2pwp1prm  48052  mod42tp1mod8  48065  lighneallem4b  48072  lighneallem4  48073  nprmdvdsfacm1lem4  48086  ppivalnnprm  48088  m2even  48130  fppr2odd  48207  gpg3kgrtriexlem3  48561  gpg3kgrtriexlem6  48564  2zlidl  48716  dignn0fr  49077  dignn0flhalflem1  49091