Theorem zmulcld 12633

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

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7361   · cmul 11037  ℤcz 12518

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 2709  ax-sep 5232  ax-nul 5242  ax-pow 5303  ax-pr 5371  ax-un 7683  ax-resscn 11089  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-addrcl 11093  ax-mulcl 11094  ax-mulrcl 11095  ax-mulcom 11096  ax-addass 11097  ax-mulass 11098  ax-distr 11099  ax-i2m1 11100  ax-1ne0 11101  ax-1rid 11102  ax-rnegex 11103  ax-rrecex 11104  ax-cnre 11105  ax-pre-lttri 11106  ax-pre-lttrn 11107  ax-pre-ltadd 11108

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6260  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-riota 7318  df-ov 7364  df-oprab 7365  df-mpo 7366  df-om 7812  df-2nd 7937  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11175  df-mnf 11176  df-ltxr 11178  df-sub 11373  df-neg 11374  df-nn 12169  df-n0 12432  df-z 12519

This theorem is referenced by:  2tnp1ge0ge0  13782  flhalf  13783  quoremz  13808  intfracq  13812  zmodcl  13844  modmul1  13880  sqoddm1div8  14199  eirrlem  16165  modmulconst  16251  dvds2ln  16252  dvdsexp2im  16290  dvdsmod  16292  3dvds  16294  even2n  16305  mod2eq1n2dvds  16310  2tp1odd  16315  ltoddhalfle  16324  m1expo  16338  m1exp1  16339  modremain  16371  flodddiv4  16378  bits0e  16392  bits0o  16393  bitsp1e  16395  bitsp1o  16396  bitsmod  16399  bitscmp  16401  bitsinv1lem  16404  bitsuz  16437  bitsshft  16438  smumullem  16455  smumul  16456  gcdmultipled  16497  bezoutlem3  16504  bezoutlem4  16505  mulgcd  16511  dvdsmulgcd  16519  bezoutr  16531  lcmgcdlem  16569  mulgcddvds  16618  rpmulgcd2  16619  coprmprod  16624  divgcdcoprm0  16628  cncongr1  16630  cncongr2  16631  exprmfct  16668  prmdvdsbc  16690  hashdvds  16739  eulerthlem1  16745  eulerthlem2  16746  prmdiv  16749  prmdiveq  16750  pcpremul  16808  pcqmul  16818  pcaddlem  16853  prmpwdvds  16869  4sqlem5  16907  4sqlem10  16912  4sqlem14  16923  mulgass  19081  mulgmodid  19083  odmod  19515  odmulgid  19523  odbezout  19527  gexdvds  19553  odadd1  19817  odadd2  19818  torsubg  19823  ablfacrp  20037  pgpfac1lem2  20046  pgpfac1lem3a  20047  pgpfac1lem3  20048  ablsimpgfindlem1  20078  pzriprnglem6  21479  pzriprnglem8  21481  pzriprnglem12  21485  znunit  21556  znrrg  21558  dyaddisjlem  25575  elqaalem3  26301  aalioulem1  26312  aaliou3lem2  26323  aaliou3lem8  26325  mpodvdsmulf1o  27174  dvdsmulf1o  27176  lgsdirprm  27311  lgsdir  27312  lgsdilem2  27313  lgsdi  27314  gausslemma2dlem1a  27345  gausslemma2dlem5a  27350  gausslemma2dlem5  27351  gausslemma2dlem6  27352  gausslemma2dlem7  27353  gausslemma2d  27354  lgseisenlem1  27355  lgseisenlem2  27356  lgseisenlem3  27357  lgseisenlem4  27358  lgsquadlem1  27360  lgsquad2lem1  27364  lgsquad3  27367  2lgslem1a1  27369  2lgslem1a2  27370  2lgslem1b  27372  2lgslem3b1  27381  2lgslem3c1  27382  2lgsoddprmlem2  27389  2sqlem3  27400  2sqlem4  27401  2sqblem  27411  2sqmod  27416  ex-ind-dvds  30549  elrgspnlem2  33322  zringfrac  33632  cos9thpiminplylem2  33946  qqhghm  34151  qqhrhm  34152  breprexplemc  34795  circlemeth  34803  knoppndvlem2  36792  lcmineqlem6  42490  lcmineqlem14  42498  lcmineqlem18  42502  lcmineqlem21  42505  lcmineqlem22  42506  aks4d1p8d2  42541  aks4d1p8  42543  aks4d1p9  42544  primrootscoprmpow  42555  posbezout  42556  primrootscoprbij  42558  primrootspoweq0  42562  aks6d1c3  42579  aks6d1c4  42580  2np3bcnp1  42600  aks6d1c6lem3  42628  aks6d1c6lem4  42629  aks6d1c6lem5  42633  pellexlem5  43282  pellexlem6  43283  pell1234qrmulcl  43304  congmul  43416  jm2.18  43437  jm2.19lem1  43438  jm2.19lem2  43439  jm2.19lem3  43440  jm2.19lem4  43441  jm2.22  43444  jm2.23  43445  jm2.20nn  43446  jm2.25  43448  jm2.15nn0  43452  jm2.16nn0  43453  jm2.27c  43456  jm3.1lem3  43468  jm3.1  43469  expdiophlem1  43470  inductionexd  44603  sumnnodd  46081  wallispilem4  46517  stirlinglem3  46525  stirlinglem7  46529  stirlinglem10  46532  stirlinglem11  46533  dirkertrigeqlem1  46547  dirkertrigeqlem3  46549  dirkertrigeq  46550  dirkercncflem2  46553  fourierswlem  46679  fouriersw  46680  etransclem3  46686  etransclem7  46690  etransclem10  46693  etransclem25  46708  etransclem26  46709  etransclem27  46710  etransclem28  46711  etransclem35  46718  etransclem37  46720  etransclem44  46727  etransclem45  46728  minusmodnep2tmod  47822  modmkpkne  47830  modmknepk  47831  fmtnoprmfac2lem1  48044  fmtno4prmfac  48050  2pwp1prm  48067  mod42tp1mod8  48080  lighneallem4b  48087  lighneallem4  48088  nprmdvdsfacm1lem4  48101  ppivalnnprm  48103  m2even  48145  fppr2odd  48222  gpg3kgrtriexlem3  48576  gpg3kgrtriexlem6  48579  2zlidl  48731  dignn0fr  49092  dignn0flhalflem1  49106