Theorem zmulcld 12668

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

Syntax hints:   → wi 4   ∈ wcel 2106  (class class class)co 7405   · cmul 11111  ℤcz 12554

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7852  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-pnf 11246  df-mnf 11247  df-ltxr 11249  df-sub 11442  df-neg 11443  df-nn 12209  df-n0 12469  df-z 12555

This theorem is referenced by:  2tnp1ge0ge0  13790  flhalf  13791  quoremz  13816  intfracq  13820  zmodcl  13852  modmul1  13885  sqoddm1div8  14202  eirrlem  16143  modmulconst  16227  dvds2ln  16228  dvdsexp2im  16266  dvdsmod  16268  3dvds  16270  even2n  16281  mod2eq1n2dvds  16286  2tp1odd  16291  ltoddhalfle  16300  m1expo  16314  m1exp1  16315  modremain  16347  flodddiv4  16352  bits0e  16366  bits0o  16367  bitsp1e  16369  bitsp1o  16370  bitsmod  16373  bitscmp  16375  bitsinv1lem  16378  bitsuz  16411  bitsshft  16412  smumullem  16429  smumul  16430  gcdmultipled  16472  bezoutlem3  16479  bezoutlem4  16480  mulgcd  16486  dvdsmulgcd  16493  bezoutr  16501  lcmgcdlem  16539  mulgcddvds  16588  rpmulgcd2  16589  coprmprod  16594  divgcdcoprm0  16598  cncongr1  16600  cncongr2  16601  exprmfct  16637  hashdvds  16704  eulerthlem1  16710  eulerthlem2  16711  prmdiv  16714  prmdiveq  16715  pcpremul  16772  pcqmul  16782  pcaddlem  16817  prmpwdvds  16833  4sqlem5  16871  4sqlem10  16876  4sqlem14  16887  mulgass  18985  mulgmodid  18987  odmod  19408  odmulgid  19416  odbezout  19420  gexdvds  19446  odadd1  19710  odadd2  19711  torsubg  19716  ablfacrp  19930  pgpfac1lem2  19939  pgpfac1lem3a  19940  pgpfac1lem3  19941  ablsimpgfindlem1  19971  znunit  21110  znrrg  21112  dyaddisjlem  25103  elqaalem3  25825  aalioulem1  25836  aaliou3lem2  25847  aaliou3lem8  25849  dvdsmulf1o  26687  lgsdirprm  26823  lgsdir  26824  lgsdilem2  26825  lgsdi  26826  gausslemma2dlem1a  26857  gausslemma2dlem5a  26862  gausslemma2dlem5  26863  gausslemma2dlem6  26864  gausslemma2dlem7  26865  gausslemma2d  26866  lgseisenlem1  26867  lgseisenlem2  26868  lgseisenlem3  26869  lgseisenlem4  26870  lgsquadlem1  26872  lgsquad2lem1  26876  lgsquad3  26879  2lgslem1a1  26881  2lgslem1a2  26882  2lgslem1b  26884  2lgslem3b1  26893  2lgslem3c1  26894  2lgsoddprmlem2  26901  2sqlem3  26912  2sqlem4  26913  2sqblem  26923  2sqmod  26928  ex-ind-dvds  29703  prmdvdsbc  32009  qqhghm  32956  qqhrhm  32957  breprexplemc  33632  circlemeth  33640  knoppndvlem2  35377  lcmineqlem6  40887  lcmineqlem14  40895  lcmineqlem18  40899  lcmineqlem21  40902  lcmineqlem22  40903  aks4d1p8d2  40938  aks4d1p8  40940  aks4d1p9  40941  2np3bcnp1  40948  pellexlem5  41556  pellexlem6  41557  pell1234qrmulcl  41578  congmul  41691  jm2.18  41712  jm2.19lem1  41713  jm2.19lem2  41714  jm2.19lem3  41715  jm2.19lem4  41716  jm2.22  41719  jm2.23  41720  jm2.20nn  41721  jm2.25  41723  jm2.15nn0  41727  jm2.16nn0  41728  jm2.27c  41731  jm3.1lem3  41743  jm3.1  41744  expdiophlem1  41745  inductionexd  42891  sumnnodd  44332  wallispilem4  44770  stirlinglem3  44778  stirlinglem7  44782  stirlinglem10  44785  stirlinglem11  44786  dirkertrigeqlem1  44800  dirkertrigeqlem3  44802  dirkertrigeq  44803  dirkercncflem2  44806  fourierswlem  44932  fouriersw  44933  etransclem3  44939  etransclem7  44943  etransclem10  44946  etransclem25  44961  etransclem26  44962  etransclem27  44963  etransclem28  44964  etransclem35  44971  etransclem37  44973  etransclem44  44980  etransclem45  44981  fmtnoprmfac2lem1  46220  fmtno4prmfac  46226  2pwp1prm  46243  mod42tp1mod8  46256  lighneallem4b  46263  lighneallem4  46264  m2even  46308  fppr2odd  46385  2zlidl  46785  dignn0fr  47240  dignn0flhalflem1  47254