Theorem zmulcld 12710

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

Syntax hints:   → wi 4   ∈ wcel 2098  (class class class)co 7426   · cmul 11151  ℤcz 12596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-resscn 11203  ax-1cn 11204  ax-icn 11205  ax-addcl 11206  ax-addrcl 11207  ax-mulcl 11208  ax-mulrcl 11209  ax-mulcom 11210  ax-addass 11211  ax-mulass 11212  ax-distr 11213  ax-i2m1 11214  ax-1ne0 11215  ax-1rid 11216  ax-rnegex 11217  ax-rrecex 11218  ax-cnre 11219  ax-pre-lttri 11220  ax-pre-lttrn 11221  ax-pre-ltadd 11222

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6310  df-ord 6377  df-on 6378  df-lim 6379  df-suc 6380  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-riota 7382  df-ov 7429  df-oprab 7430  df-mpo 7431  df-om 7877  df-2nd 8000  df-frecs 8293  df-wrecs 8324  df-recs 8398  df-rdg 8437  df-er 8731  df-en 8971  df-dom 8972  df-sdom 8973  df-pnf 11288  df-mnf 11289  df-ltxr 11291  df-sub 11484  df-neg 11485  df-nn 12251  df-n0 12511  df-z 12597

This theorem is referenced by:  2tnp1ge0ge0  13834  flhalf  13835  quoremz  13860  intfracq  13864  zmodcl  13896  modmul1  13929  sqoddm1div8  14245  eirrlem  16188  modmulconst  16272  dvds2ln  16273  dvdsexp2im  16311  dvdsmod  16313  3dvds  16315  even2n  16326  mod2eq1n2dvds  16331  2tp1odd  16336  ltoddhalfle  16345  m1expo  16359  m1exp1  16360  modremain  16392  flodddiv4  16397  bits0e  16411  bits0o  16412  bitsp1e  16414  bitsp1o  16415  bitsmod  16418  bitscmp  16420  bitsinv1lem  16423  bitsuz  16456  bitsshft  16457  smumullem  16474  smumul  16475  gcdmultipled  16517  bezoutlem3  16524  bezoutlem4  16525  mulgcd  16531  dvdsmulgcd  16538  bezoutr  16546  lcmgcdlem  16584  mulgcddvds  16633  rpmulgcd2  16634  coprmprod  16639  divgcdcoprm0  16643  cncongr1  16645  cncongr2  16646  exprmfct  16682  prmdvdsbc  16705  hashdvds  16751  eulerthlem1  16757  eulerthlem2  16758  prmdiv  16761  prmdiveq  16762  pcpremul  16819  pcqmul  16829  pcaddlem  16864  prmpwdvds  16880  4sqlem5  16918  4sqlem10  16923  4sqlem14  16934  mulgass  19073  mulgmodid  19075  odmod  19508  odmulgid  19516  odbezout  19520  gexdvds  19546  odadd1  19810  odadd2  19811  torsubg  19816  ablfacrp  20030  pgpfac1lem2  20039  pgpfac1lem3a  20040  pgpfac1lem3  20041  ablsimpgfindlem1  20071  pzriprnglem6  21419  pzriprnglem8  21421  pzriprnglem12  21425  znunit  21504  znrrg  21506  dyaddisjlem  25544  elqaalem3  26276  aalioulem1  26287  aaliou3lem2  26298  aaliou3lem8  26300  mpodvdsmulf1o  27146  dvdsmulf1o  27148  lgsdirprm  27284  lgsdir  27285  lgsdilem2  27286  lgsdi  27287  gausslemma2dlem1a  27318  gausslemma2dlem5a  27323  gausslemma2dlem5  27324  gausslemma2dlem6  27325  gausslemma2dlem7  27326  gausslemma2d  27327  lgseisenlem1  27328  lgseisenlem2  27329  lgseisenlem3  27330  lgseisenlem4  27331  lgsquadlem1  27333  lgsquad2lem1  27337  lgsquad3  27340  2lgslem1a1  27342  2lgslem1a2  27343  2lgslem1b  27345  2lgslem3b1  27354  2lgslem3c1  27355  2lgsoddprmlem2  27362  2sqlem3  27373  2sqlem4  27374  2sqblem  27384  2sqmod  27389  ex-ind-dvds  30291  zringfrac  33277  qqhghm  33622  qqhrhm  33623  breprexplemc  34297  circlemeth  34305  knoppndvlem2  36021  lcmineqlem6  41537  lcmineqlem14  41545  lcmineqlem18  41549  lcmineqlem21  41552  lcmineqlem22  41553  aks4d1p8d2  41588  aks4d1p8  41590  aks4d1p9  41591  primrootscoprmpow  41602  posbezout  41603  primrootscoprbij  41605  primrootspoweq0  41609  aks6d1c3  41626  aks6d1c4  41627  2np3bcnp1  41648  aks6d1c6lem3  41676  aks6d1c6lem4  41677  aks6d1c6lem5  41681  pellexlem5  42284  pellexlem6  42285  pell1234qrmulcl  42306  congmul  42419  jm2.18  42440  jm2.19lem1  42441  jm2.19lem2  42442  jm2.19lem3  42443  jm2.19lem4  42444  jm2.22  42447  jm2.23  42448  jm2.20nn  42449  jm2.25  42451  jm2.15nn0  42455  jm2.16nn0  42456  jm2.27c  42459  jm3.1lem3  42471  jm3.1  42472  expdiophlem1  42473  inductionexd  43616  sumnnodd  45047  wallispilem4  45485  stirlinglem3  45493  stirlinglem7  45497  stirlinglem10  45500  stirlinglem11  45501  dirkertrigeqlem1  45515  dirkertrigeqlem3  45517  dirkertrigeq  45518  dirkercncflem2  45521  fourierswlem  45647  fouriersw  45648  etransclem3  45654  etransclem7  45658  etransclem10  45661  etransclem25  45676  etransclem26  45677  etransclem27  45678  etransclem28  45679  etransclem35  45686  etransclem37  45688  etransclem44  45695  etransclem45  45696  fmtnoprmfac2lem1  46935  fmtno4prmfac  46941  2pwp1prm  46958  mod42tp1mod8  46971  lighneallem4b  46978  lighneallem4  46979  m2even  47023  fppr2odd  47100  2zlidl  47380  dignn0fr  47752  dignn0flhalflem1  47766