Theorem zmulcld 12443

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

Syntax hints:   → wi 4   ∈ wcel 2110  (class class class)co 7272   · cmul 10887  ℤcz 12330

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 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pow 5292  ax-pr 5356  ax-un 7583  ax-resscn 10939  ax-1cn 10940  ax-icn 10941  ax-addcl 10942  ax-addrcl 10943  ax-mulcl 10944  ax-mulrcl 10945  ax-mulcom 10946  ax-addass 10947  ax-mulass 10948  ax-distr 10949  ax-i2m1 10950  ax-1ne0 10951  ax-1rid 10952  ax-rnegex 10953  ax-rrecex 10954  ax-cnre 10955  ax-pre-lttri 10956  ax-pre-lttrn 10957  ax-pre-ltadd 10958

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ne 2946  df-nel 3052  df-ral 3071  df-rex 3072  df-reu 3073  df-rab 3075  df-v 3433  df-sbc 3721  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-iun 4932  df-br 5080  df-opab 5142  df-mpt 5163  df-tr 5197  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6201  df-ord 6268  df-on 6269  df-lim 6270  df-suc 6271  df-iota 6390  df-fun 6434  df-fn 6435  df-f 6436  df-f1 6437  df-fo 6438  df-f1o 6439  df-fv 6440  df-riota 7229  df-ov 7275  df-oprab 7276  df-mpo 7277  df-om 7708  df-2nd 7826  df-frecs 8089  df-wrecs 8120  df-recs 8194  df-rdg 8233  df-er 8490  df-en 8726  df-dom 8727  df-sdom 8728  df-pnf 11022  df-mnf 11023  df-ltxr 11025  df-sub 11218  df-neg 11219  df-nn 11985  df-n0 12245  df-z 12331

This theorem is referenced by:  2tnp1ge0ge0  13560  flhalf  13561  quoremz  13586  intfracq  13590  zmodcl  13622  modmul1  13655  sqoddm1div8  13969  eirrlem  15924  modmulconst  16008  dvds2ln  16009  dvdsexp2im  16047  dvdsmod  16049  3dvds  16051  even2n  16062  mod2eq1n2dvds  16067  2tp1odd  16072  ltoddhalfle  16081  m1expo  16095  m1exp1  16096  modremain  16128  flodddiv4  16133  bits0e  16147  bits0o  16148  bitsp1e  16150  bitsp1o  16151  bitsmod  16154  bitscmp  16156  bitsinv1lem  16159  bitsuz  16192  bitsshft  16193  smumullem  16210  smumul  16211  gcdmultipled  16253  bezoutlem3  16260  bezoutlem4  16261  mulgcd  16267  dvdsmulgcd  16276  bezoutr  16284  lcmgcdlem  16322  mulgcddvds  16371  rpmulgcd2  16372  coprmprod  16377  divgcdcoprm0  16381  cncongr1  16383  cncongr2  16384  exprmfct  16420  hashdvds  16487  eulerthlem1  16493  eulerthlem2  16494  prmdiv  16497  prmdiveq  16498  pcpremul  16555  pcqmul  16565  pcaddlem  16600  prmpwdvds  16616  4sqlem5  16654  4sqlem10  16659  4sqlem14  16670  mulgass  18751  mulgmodid  18753  odmod  19165  odmulgid  19172  odbezout  19176  gexdvds  19200  odadd1  19460  odadd2  19461  torsubg  19466  ablfacrp  19680  pgpfac1lem2  19689  pgpfac1lem3a  19690  pgpfac1lem3  19691  ablsimpgfindlem1  19721  znunit  20782  znrrg  20784  dyaddisjlem  24770  elqaalem3  25492  aalioulem1  25503  aaliou3lem2  25514  aaliou3lem8  25516  dvdsmulf1o  26354  lgsdirprm  26490  lgsdir  26491  lgsdilem2  26492  lgsdi  26493  gausslemma2dlem1a  26524  gausslemma2dlem5a  26529  gausslemma2dlem5  26530  gausslemma2dlem6  26531  gausslemma2dlem7  26532  gausslemma2d  26533  lgseisenlem1  26534  lgseisenlem2  26535  lgseisenlem3  26536  lgseisenlem4  26537  lgsquadlem1  26539  lgsquad2lem1  26543  lgsquad3  26546  2lgslem1a1  26548  2lgslem1a2  26549  2lgslem1b  26551  2lgslem3b1  26560  2lgslem3c1  26561  2lgsoddprmlem2  26568  2sqlem3  26579  2sqlem4  26580  2sqblem  26590  2sqmod  26595  ex-ind-dvds  28834  prmdvdsbc  31139  qqhghm  31947  qqhrhm  31948  breprexplemc  32621  circlemeth  32629  knoppndvlem2  34702  lcmineqlem6  40051  lcmineqlem14  40059  lcmineqlem18  40063  lcmineqlem21  40066  lcmineqlem22  40067  aks4d1p8d2  40102  aks4d1p8  40104  aks4d1p9  40105  2np3bcnp1  40109  pellexlem5  40664  pellexlem6  40665  pell1234qrmulcl  40686  congmul  40798  jm2.18  40819  jm2.19lem1  40820  jm2.19lem2  40821  jm2.19lem3  40822  jm2.19lem4  40823  jm2.22  40826  jm2.23  40827  jm2.20nn  40828  jm2.25  40830  jm2.15nn0  40834  jm2.16nn0  40835  jm2.27c  40838  jm3.1lem3  40850  jm3.1  40851  expdiophlem1  40852  inductionexd  41747  sumnnodd  43153  wallispilem4  43591  stirlinglem3  43599  stirlinglem7  43603  stirlinglem10  43606  stirlinglem11  43607  dirkertrigeqlem1  43621  dirkertrigeqlem3  43623  dirkertrigeq  43624  dirkercncflem2  43627  fourierswlem  43753  fouriersw  43754  etransclem3  43760  etransclem7  43764  etransclem10  43767  etransclem25  43782  etransclem26  43783  etransclem27  43784  etransclem28  43785  etransclem35  43792  etransclem37  43794  etransclem44  43801  etransclem45  43802  fmtnoprmfac2lem1  44997  fmtno4prmfac  45003  2pwp1prm  45020  mod42tp1mod8  45033  lighneallem4b  45040  lighneallem4  45041  m2even  45085  fppr2odd  45162  2zlidl  45471  dignn0fr  45926  dignn0flhalflem1  45940