Theorem zmulcld 12734

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  (class class class)co 7414   · cmul 11132  ℤcz 12618

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7737  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7371  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7864  df-2nd 7988  df-frecs 8281  df-wrecs 8312  df-recs 8361  df-rdg 8400  df-er 8699  df-en 8956  df-dom 8957  df-sdom 8958  df-pnf 11272  df-mnf 11273  df-ltxr 11275  df-sub 11470  df-neg 11471  df-nn 12261  df-n0 12532  df-z 12619

This theorem is used by:  2tnp1ge0ge0  13893  flhalf  13894  quoremz  13919  intfracq  13923  zmodcl  13955  modmul1  13991  sqoddm1div8  14310  eirrlem  16295  modmulconst  16381  dvds2ln  16382  dvdsexp2im  16420  dvdsmod  16422  3dvds  16424  even2n  16435  mod2eq1n2dvds  16440  2tp1odd  16445  ltoddhalfle  16454  m1expo  16468  m1exp1  16469  modremain  16501  flodddiv4  16508  bits0e  16522  bits0o  16523  bitsp1e  16525  bitsp1o  16526  bitsmod  16529  bitscmp  16531  bitsinv1lem  16534  bitsuz  16567  bitsshft  16568  smumullem  16585  smumul  16586  gcdmultipled  16627  bezoutlem3  16634  bezoutlem4  16635  mulgcd  16641  dvdsmulgcd  16649  bezoutr  16661  lcmgcdlem  16699  mulgcddvds  16748  rpmulgcd2  16749  coprmprod  16754  divgcdcoprm0  16758  cncongr1  16760  cncongr2  16761  exprmfct  16798  prmdvdsbc  16820  hashdvds  16869  eulerthlem1  16875  eulerthlem2  16876  prmdiv  16879  prmdiveq  16880  pcpremul  16938  pcqmul  16948  pcaddlem  16983  prmpwdvds  16999  4sqlem5  17037  4sqlem10  17042  4sqlem14  17053  mulgass  19237  mulgmodid  19239  odmod  19676  odmulgid  19684  odbezout  19688  gexdvds  19714  odadd1  19978  odadd2  19979  torsubg  19984  ablfacrp  20198  pgpfac1lem2  20207  pgpfac1lem3a  20208  pgpfac1lem3  20209  ablsimpgfindlem1  20239  pzriprnglem6  21702  pzriprnglem8  21704  pzriprnglem12  21708  znunit  21779  znrrg  21781  dyaddisjlem  25826  elqaalem3  26556  aalioulem1  26571  aaliou3lem2  26582  aaliou3lem8  26584  mpodvdsmulf1o  27433  dvdsmulf1o  27435  lgsdirprm  27570  lgsdir  27571  lgsdilem2  27572  lgsdi  27573  gausslemma2dlem1a  27604  gausslemma2dlem5a  27609  gausslemma2dlem5  27610  gausslemma2dlem6  27611  gausslemma2dlem7  27612  gausslemma2d  27613  lgseisenlem1  27614  lgseisenlem2  27615  lgseisenlem3  27616  lgseisenlem4  27617  lgsquadlem1  27619  lgsquad2lem1  27623  lgsquad3  27626  2lgslem1a1  27628  2lgslem1a2  27629  2lgslem1b  27631  2lgslem3b1  27640  2lgslem3c1  27641  2lgsoddprmlem2  27648  2sqlem3  27659  2sqlem4  27660  2sqblem  27670  2sqmod  27675  ex-ind-dvds  30944  elrgspnlem2  33686  zringfrac  33967  cos9thpiminplylem2  34296  qqhghm  34501  qqhrhm  34502  breprexplemc  35143  circlemeth  35151  knoppndvlem2  37213  lcmineqlem6  42903  lcmineqlem14  42911  lcmineqlem18  42915  lcmineqlem21  42918  lcmineqlem22  42919  aks4d1p8d2  42954  aks4d1p8  42956  aks4d1p9  42957  primrootscoprmpow  42968  posbezout  42969  primrootscoprbij  42971  primrootspoweq0  42975  aks6d1c3  42992  aks6d1c4  42993  2np3bcnp1  43013  aks6d1c6lem3  43041  aks6d1c6lem4  43042  aks6d1c6lem5  43046  pellexlem5  43677  pellexlem6  43678  pell1234qrmulcl  43699  congmul  43811  jm2.18  43832  jm2.19lem1  43833  jm2.19lem2  43834  jm2.19lem3  43835  jm2.19lem4  43836  jm2.22  43839  jm2.23  43840  jm2.20nn  43841  jm2.25  43843  jm2.15nn0  43847  jm2.16nn0  43848  jm2.27c  43851  jm3.1lem3  43863  jm3.1  43864  expdiophlem1  43865  inductionexd  44998  sumnnodd  46463  wallispilem4  46899  stirlinglem3  46907  stirlinglem7  46911  stirlinglem10  46914  stirlinglem11  46915  dirkertrigeqlem1  46929  dirkertrigeqlem3  46931  dirkertrigeq  46932  dirkercncflem2  46935  fourierswlem  47061  fouriersw  47062  etransclem3  47068  etransclem7  47072  etransclem10  47075  etransclem25  47090  etransclem26  47091  etransclem27  47092  etransclem28  47093  etransclem35  47100  etransclem37  47102  etransclem44  47109  etransclem45  47110  minusmodnep2tmod  48250  modmkpkne  48258  modmknepk  48259  fmtnoprmfac2lem1  48472  fmtno4prmfac  48478  2pwp1prm  48495  mod42tp1mod8  48508  lighneallem4b  48515  lighneallem4  48516  nprmdvdsfacm1lem4  48529  ppivalnnprm  48531  m2even  48573  fppr2odd  48650  gpg3kgrtriexlem3  49004  gpg3kgrtriexlem6  49007  2zlidl  49158  dignn0fr  49534  dignn0flhalflem1  49548