Theorem zmulcld 12819

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  (class class class)co 7427   · cmul 11215  ℤcz 12703

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-sep 5251  ax-nul 5262  ax-pow 5330  ax-pr 5394  ax-un 7758  ax-resscn 11267  ax-1cn 11268  ax-icn 11269  ax-addcl 11270  ax-addrcl 11271  ax-mulcl 11272  ax-mulrcl 11273  ax-mulcom 11274  ax-addass 11275  ax-mulass 11276  ax-distr 11277  ax-i2m1 11278  ax-1ne0 11279  ax-1rid 11280  ax-rnegex 11281  ax-rrecex 11282  ax-cnre 11283  ax-pre-lttri 11284  ax-pre-lttrn 11285  ax-pre-ltadd 11286

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3369  df-rab 3416  df-v 3455  df-sbc 3742  df-csb 3851  df-ss 3900  df-pss 4016  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-pw 4561  df-sn 4588  df-pr 4590  df-op 4838  df-uni 4870  df-iun 4955  df-br 5106  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5549  df-eprel 5554  df-po 5562  df-so 5563  df-fr 5607  df-we 5609  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6310  df-ord 6371  df-on 6372  df-lim 6373  df-suc 6374  df-iota 6500  df-fun 6548  df-fn 6549  df-f 6550  df-f1 6551  df-fo 6552  df-f1o 6553  df-fv 6554  df-riota 7384  df-ov 7430  df-oprab 7431  df-mpo 7432  df-om 7885  df-2nd 8009  df-frecs 8310  df-wrecs 8341  df-recs 8390  df-rdg 8429  df-er 8728  df-en 8985  df-dom 8986  df-sdom 8987  df-pnf 11355  df-mnf 11356  df-ltxr 11358  df-sub 11553  df-neg 11554  df-nn 12346  df-n0 12617  df-z 12704

This theorem is used by:  2tnp1ge0ge0  13979  flhalf  13980  quoremz  14005  intfracq  14009  zmodcl  14041  modmul1  14077  sqoddm1div8  14397  eirrlem  16384  modmulconst  16470  dvds2ln  16471  dvdsexp2im  16509  dvdsmod  16511  3dvds  16513  even2n  16524  mod2eq1n2dvds  16529  2tp1odd  16534  ltoddhalfle  16543  m1expo  16557  m1exp1  16558  modremain  16590  flodddiv4  16597  bits0e  16611  bits0o  16612  bitsp1e  16614  bitsp1o  16615  bitsmod  16618  bitscmp  16620  bitsinv1lem  16623  bitsuz  16656  bitsshft  16657  smumullem  16674  smumul  16675  gcdmultipled  16719  bezoutlem3  16726  bezoutlem4  16727  mulgcd  16733  dvdsmulgcd  16742  bezoutr  16755  lcmgcdlem  16793  mulgcddvds  16842  rpmulgcd2  16843  coprmprod  16848  divgcdcoprm0  16852  cncongr1  16854  cncongr2  16855  exprmfct  16892  prmdvdsbc  16914  hashdvds  16964  eulerthlem1  16970  eulerthlem2  16971  prmdiv  16974  prmdiveq  16975  pcpremul  17033  pcqmul  17043  pcaddlem  17078  prmpwdvds  17094  4sqlem5  17132  4sqlem10  17137  4sqlem14  17148  mulgass  19333  mulgmodid  19335  odmod  19772  odmulgid  19780  odbezout  19784  gexdvds  19810  odadd1  20074  odadd2  20075  torsubg  20080  ablfacrp  20294  pgpfac1lem2  20303  pgpfac1lem3a  20304  pgpfac1lem3  20305  ablsimpgfindlem1  20335  pzriprnglem6  21804  pzriprnglem8  21806  pzriprnglem12  21810  znunit  21881  znrrg  21883  dyaddisjlem  25928  elqaalem3  26656  aalioulem1  26671  aaliou3lem2  26682  aaliou3lem8  26684  mpodvdsmulf1o  27533  dvdsmulf1o  27535  lgsdirprm  27670  lgsdir  27671  lgsdilem2  27672  lgsdi  27673  gausslemma2dlem1a  27704  gausslemma2dlem5a  27709  gausslemma2dlem5  27710  gausslemma2dlem6  27711  gausslemma2dlem7  27712  gausslemma2d  27713  lgseisenlem1  27714  lgseisenlem2  27715  lgseisenlem3  27716  lgseisenlem4  27717  lgsquadlem1  27719  lgsquad2lem1  27723  lgsquad3  27726  2lgslem1a1  27728  2lgslem1a2  27729  2lgslem1b  27731  2lgslem3b1  27740  2lgslem3c1  27741  2lgsoddprmlem2  27748  2sqlem3  27759  2sqlem4  27760  2sqblem  27770  2sqmod  27775  ex-ind-dvds  31074  elrgspnlem2  33857  zringfrac  34139  cos9thpiminplylem2  34468  qqhghm  34673  qqhrhm  34674  breprexplemc  35314  circlemeth  35322  knoppndvlem2  37506  lcmineqlem6  43224  lcmineqlem14  43232  lcmineqlem18  43236  lcmineqlem21  43239  lcmineqlem22  43240  aks4d1p8d2  43275  aks4d1p8  43277  aks4d1p9  43278  primrootscoprmpow  43289  posbezout  43290  primrootscoprbij  43292  primrootspoweq0  43296  aks6d1c3  43313  aks6d1c4  43314  2np3bcnp1  43334  aks6d1c6lem3  43362  aks6d1c6lem4  43363  aks6d1c6lem5  43367  pellexlem5  43980  pellexlem6  43981  pell1234qrmulcl  44002  congmul  44114  jm2.18  44135  jm2.19lem1  44136  jm2.19lem2  44137  jm2.19lem3  44138  jm2.19lem4  44139  jm2.22  44142  jm2.23  44143  jm2.20nn  44144  jm2.25  44146  jm2.15nn0  44150  jm2.16nn0  44151  jm2.27c  44154  jm3.1lem3  44166  jm3.1  44167  expdiophlem1  44168  inductionexd  45295  sumnnodd  46781  wallispilem4  47217  stirlinglem3  47225  stirlinglem7  47229  stirlinglem10  47232  stirlinglem11  47233  dirkertrigeqlem1  47247  dirkertrigeqlem3  47249  dirkertrigeq  47250  dirkercncflem2  47253  fourierswlem  47379  fouriersw  47380  etransclem3  47386  etransclem7  47390  etransclem10  47393  etransclem25  47408  etransclem26  47409  etransclem27  47410  etransclem28  47411  etransclem35  47418  etransclem37  47420  etransclem44  47427  etransclem45  47428  minusmodnep2tmod  48568  modmkpkne  48576  modmknepk  48577  fmtnoprmfac2lem1  48790  fmtno4prmfac  48796  2pwp1prm  48813  mod42tp1mod8  48826  lighneallem4b  48833  lighneallem4  48834  nprmdvdsfacm1lem4  48847  ppivalnnprm  48849  m2even  48891  fppr2odd  48968  gpg3kgrtriexlem3  49322  gpg3kgrtriexlem6  49325  2zlidl  49476  dignn0fr  49852  dignn0flhalflem1  49866