Theorem zmulcld 12441

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

Syntax hints:   → wi 4   ∈ wcel 2107  (class class class)co 7284   · cmul 10885  ℤcz 12328

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597  ax-resscn 10937  ax-1cn 10938  ax-icn 10939  ax-addcl 10940  ax-addrcl 10941  ax-mulcl 10942  ax-mulrcl 10943  ax-mulcom 10944  ax-addass 10945  ax-mulass 10946  ax-distr 10947  ax-i2m1 10948  ax-1ne0 10949  ax-1rid 10950  ax-rnegex 10951  ax-rrecex 10952  ax-cnre 10953  ax-pre-lttri 10954  ax-pre-lttrn 10955  ax-pre-ltadd 10956

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3070  df-rex 3071  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-iun 4927  df-br 5076  df-opab 5138  df-mpt 5159  df-tr 5193  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6206  df-ord 6273  df-on 6274  df-lim 6275  df-suc 6276  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-riota 7241  df-ov 7287  df-oprab 7288  df-mpo 7289  df-om 7722  df-2nd 7841  df-frecs 8106  df-wrecs 8137  df-recs 8211  df-rdg 8250  df-er 8507  df-en 8743  df-dom 8744  df-sdom 8745  df-pnf 11020  df-mnf 11021  df-ltxr 11023  df-sub 11216  df-neg 11217  df-nn 11983  df-n0 12243  df-z 12329

This theorem is referenced by:  2tnp1ge0ge0  13558  flhalf  13559  quoremz  13584  intfracq  13588  zmodcl  13620  modmul1  13653  sqoddm1div8  13967  eirrlem  15922  modmulconst  16006  dvds2ln  16007  dvdsexp2im  16045  dvdsmod  16047  3dvds  16049  even2n  16060  mod2eq1n2dvds  16065  2tp1odd  16070  ltoddhalfle  16079  m1expo  16093  m1exp1  16094  modremain  16126  flodddiv4  16131  bits0e  16145  bits0o  16146  bitsp1e  16148  bitsp1o  16149  bitsmod  16152  bitscmp  16154  bitsinv1lem  16157  bitsuz  16190  bitsshft  16191  smumullem  16208  smumul  16209  gcdmultipled  16251  bezoutlem3  16258  bezoutlem4  16259  mulgcd  16265  dvdsmulgcd  16274  bezoutr  16282  lcmgcdlem  16320  mulgcddvds  16369  rpmulgcd2  16370  coprmprod  16375  divgcdcoprm0  16379  cncongr1  16381  cncongr2  16382  exprmfct  16418  hashdvds  16485  eulerthlem1  16491  eulerthlem2  16492  prmdiv  16495  prmdiveq  16496  pcpremul  16553  pcqmul  16563  pcaddlem  16598  prmpwdvds  16614  4sqlem5  16652  4sqlem10  16657  4sqlem14  16668  mulgass  18749  mulgmodid  18751  odmod  19163  odmulgid  19170  odbezout  19174  gexdvds  19198  odadd1  19458  odadd2  19459  torsubg  19464  ablfacrp  19678  pgpfac1lem2  19687  pgpfac1lem3a  19688  pgpfac1lem3  19689  ablsimpgfindlem1  19719  znunit  20780  znrrg  20782  dyaddisjlem  24768  elqaalem3  25490  aalioulem1  25501  aaliou3lem2  25512  aaliou3lem8  25514  dvdsmulf1o  26352  lgsdirprm  26488  lgsdir  26489  lgsdilem2  26490  lgsdi  26491  gausslemma2dlem1a  26522  gausslemma2dlem5a  26527  gausslemma2dlem5  26528  gausslemma2dlem6  26529  gausslemma2dlem7  26530  gausslemma2d  26531  lgseisenlem1  26532  lgseisenlem2  26533  lgseisenlem3  26534  lgseisenlem4  26535  lgsquadlem1  26537  lgsquad2lem1  26541  lgsquad3  26544  2lgslem1a1  26546  2lgslem1a2  26547  2lgslem1b  26549  2lgslem3b1  26558  2lgslem3c1  26559  2lgsoddprmlem2  26566  2sqlem3  26577  2sqlem4  26578  2sqblem  26588  2sqmod  26593  ex-ind-dvds  28834  prmdvdsbc  31139  qqhghm  31947  qqhrhm  31948  breprexplemc  32621  circlemeth  32629  knoppndvlem2  34702  lcmineqlem6  40049  lcmineqlem14  40057  lcmineqlem18  40061  lcmineqlem21  40064  lcmineqlem22  40065  aks4d1p8d2  40100  aks4d1p8  40102  aks4d1p9  40103  2np3bcnp1  40107  pellexlem5  40662  pellexlem6  40663  pell1234qrmulcl  40684  congmul  40796  jm2.18  40817  jm2.19lem1  40818  jm2.19lem2  40819  jm2.19lem3  40820  jm2.19lem4  40821  jm2.22  40824  jm2.23  40825  jm2.20nn  40826  jm2.25  40828  jm2.15nn0  40832  jm2.16nn0  40833  jm2.27c  40836  jm3.1lem3  40848  jm3.1  40849  expdiophlem1  40850  inductionexd  41772  sumnnodd  43178  wallispilem4  43616  stirlinglem3  43624  stirlinglem7  43628  stirlinglem10  43631  stirlinglem11  43632  dirkertrigeqlem1  43646  dirkertrigeqlem3  43648  dirkertrigeq  43649  dirkercncflem2  43652  fourierswlem  43778  fouriersw  43779  etransclem3  43785  etransclem7  43789  etransclem10  43792  etransclem25  43807  etransclem26  43808  etransclem27  43809  etransclem28  43810  etransclem35  43817  etransclem37  43819  etransclem44  43826  etransclem45  43827  fmtnoprmfac2lem1  45029  fmtno4prmfac  45035  2pwp1prm  45052  mod42tp1mod8  45065  lighneallem4b  45072  lighneallem4  45073  m2even  45117  fppr2odd  45194  2zlidl  45503  dignn0fr  45958  dignn0flhalflem1  45972