Theorem zmulcld 12701

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

Syntax hints:   → wi 4   ∈ wcel 2108  (class class class)co 7403   · cmul 11132  ℤcz 12586

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727  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 theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  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 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-fv 6538  df-riota 7360  df-ov 7406  df-oprab 7407  df-mpo 7408  df-om 7860  df-2nd 7987  df-frecs 8278  df-wrecs 8309  df-recs 8383  df-rdg 8422  df-er 8717  df-en 8958  df-dom 8959  df-sdom 8960  df-pnf 11269  df-mnf 11270  df-ltxr 11272  df-sub 11466  df-neg 11467  df-nn 12239  df-n0 12500  df-z 12587

This theorem is referenced by:  2tnp1ge0ge0  13844  flhalf  13845  quoremz  13870  intfracq  13874  zmodcl  13906  modmul1  13940  sqoddm1div8  14259  eirrlem  16220  modmulconst  16305  dvds2ln  16306  dvdsexp2im  16344  dvdsmod  16346  3dvds  16348  even2n  16359  mod2eq1n2dvds  16364  2tp1odd  16369  ltoddhalfle  16378  m1expo  16392  m1exp1  16393  modremain  16425  flodddiv4  16432  bits0e  16446  bits0o  16447  bitsp1e  16449  bitsp1o  16450  bitsmod  16453  bitscmp  16455  bitsinv1lem  16458  bitsuz  16491  bitsshft  16492  smumullem  16509  smumul  16510  gcdmultipled  16551  bezoutlem3  16558  bezoutlem4  16559  mulgcd  16565  dvdsmulgcd  16573  bezoutr  16585  lcmgcdlem  16623  mulgcddvds  16672  rpmulgcd2  16673  coprmprod  16678  divgcdcoprm0  16682  cncongr1  16684  cncongr2  16685  exprmfct  16721  prmdvdsbc  16743  hashdvds  16792  eulerthlem1  16798  eulerthlem2  16799  prmdiv  16802  prmdiveq  16803  pcpremul  16861  pcqmul  16871  pcaddlem  16906  prmpwdvds  16922  4sqlem5  16960  4sqlem10  16965  4sqlem14  16976  mulgass  19092  mulgmodid  19094  odmod  19525  odmulgid  19533  odbezout  19537  gexdvds  19563  odadd1  19827  odadd2  19828  torsubg  19833  ablfacrp  20047  pgpfac1lem2  20056  pgpfac1lem3a  20057  pgpfac1lem3  20058  ablsimpgfindlem1  20088  pzriprnglem6  21445  pzriprnglem8  21447  pzriprnglem12  21451  znunit  21522  znrrg  21524  dyaddisjlem  25546  elqaalem3  26279  aalioulem1  26290  aaliou3lem2  26301  aaliou3lem8  26303  mpodvdsmulf1o  27154  dvdsmulf1o  27156  lgsdirprm  27292  lgsdir  27293  lgsdilem2  27294  lgsdi  27295  gausslemma2dlem1a  27326  gausslemma2dlem5a  27331  gausslemma2dlem5  27332  gausslemma2dlem6  27333  gausslemma2dlem7  27334  gausslemma2d  27335  lgseisenlem1  27336  lgseisenlem2  27337  lgseisenlem3  27338  lgseisenlem4  27339  lgsquadlem1  27341  lgsquad2lem1  27345  lgsquad3  27348  2lgslem1a1  27350  2lgslem1a2  27351  2lgslem1b  27353  2lgslem3b1  27362  2lgslem3c1  27363  2lgsoddprmlem2  27370  2sqlem3  27381  2sqlem4  27382  2sqblem  27392  2sqmod  27397  ex-ind-dvds  30388  elrgspnlem2  33184  zringfrac  33515  cos9thpiminplylem2  33763  qqhghm  33965  qqhrhm  33966  breprexplemc  34610  circlemeth  34618  knoppndvlem2  36477  lcmineqlem6  41993  lcmineqlem14  42001  lcmineqlem18  42005  lcmineqlem21  42008  lcmineqlem22  42009  aks4d1p8d2  42044  aks4d1p8  42046  aks4d1p9  42047  primrootscoprmpow  42058  posbezout  42059  primrootscoprbij  42061  primrootspoweq0  42065  aks6d1c3  42082  aks6d1c4  42083  2np3bcnp1  42103  aks6d1c6lem3  42131  aks6d1c6lem4  42132  aks6d1c6lem5  42136  pellexlem5  42803  pellexlem6  42804  pell1234qrmulcl  42825  congmul  42938  jm2.18  42959  jm2.19lem1  42960  jm2.19lem2  42961  jm2.19lem3  42962  jm2.19lem4  42963  jm2.22  42966  jm2.23  42967  jm2.20nn  42968  jm2.25  42970  jm2.15nn0  42974  jm2.16nn0  42975  jm2.27c  42978  jm3.1lem3  42990  jm3.1  42991  expdiophlem1  42992  inductionexd  44126  sumnnodd  45607  wallispilem4  46045  stirlinglem3  46053  stirlinglem7  46057  stirlinglem10  46060  stirlinglem11  46061  dirkertrigeqlem1  46075  dirkertrigeqlem3  46077  dirkertrigeq  46078  dirkercncflem2  46081  fourierswlem  46207  fouriersw  46208  etransclem3  46214  etransclem7  46218  etransclem10  46221  etransclem25  46236  etransclem26  46237  etransclem27  46238  etransclem28  46239  etransclem35  46246  etransclem37  46248  etransclem44  46255  etransclem45  46256  minusmodnep2tmod  47330  fmtnoprmfac2lem1  47528  fmtno4prmfac  47534  2pwp1prm  47551  mod42tp1mod8  47564  lighneallem4b  47571  lighneallem4  47572  m2even  47616  fppr2odd  47693  gpg3nbgrvtxlem  48017  gpg3kgrtriexlem3  48035  gpg3kgrtriexlem6  48038  2zlidl  48163  dignn0fr  48529  dignn0flhalflem1  48543