Theorem zmulcld 12724

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  (class class class)co 7419   · cmul 11122  ℤcz 12608

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742  ax-resscn 11174  ax-1cn 11175  ax-icn 11176  ax-addcl 11177  ax-addrcl 11178  ax-mulcl 11179  ax-mulrcl 11180  ax-mulcom 11181  ax-addass 11182  ax-mulass 11183  ax-distr 11184  ax-i2m1 11185  ax-1ne0 11186  ax-1rid 11187  ax-rnegex 11188  ax-rrecex 11189  ax-cnre 11190  ax-pre-lttri 11191  ax-pre-lttrn 11192  ax-pre-ltadd 11193

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 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7376  df-ov 7422  df-oprab 7423  df-mpo 7424  df-om 7869  df-2nd 7993  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-er 8700  df-en 8950  df-dom 8951  df-sdom 8952  df-pnf 11262  df-mnf 11263  df-ltxr 11265  df-sub 11460  df-neg 11461  df-nn 12251  df-n0 12522  df-z 12609

This theorem is used by:  2tnp1ge0ge0  13882  flhalf  13883  quoremz  13908  intfracq  13912  zmodcl  13944  modmul1  13980  sqoddm1div8  14299  eirrlem  16284  modmulconst  16370  dvds2ln  16371  dvdsexp2im  16409  dvdsmod  16411  3dvds  16413  even2n  16424  mod2eq1n2dvds  16429  2tp1odd  16434  ltoddhalfle  16443  m1expo  16457  m1exp1  16458  modremain  16490  flodddiv4  16497  bits0e  16511  bits0o  16512  bitsp1e  16514  bitsp1o  16515  bitsmod  16518  bitscmp  16520  bitsinv1lem  16523  bitsuz  16556  bitsshft  16557  smumullem  16574  smumul  16575  gcdmultipled  16616  bezoutlem3  16623  bezoutlem4  16624  mulgcd  16630  dvdsmulgcd  16638  bezoutr  16650  lcmgcdlem  16688  mulgcddvds  16737  rpmulgcd2  16738  coprmprod  16743  divgcdcoprm0  16747  cncongr1  16749  cncongr2  16750  exprmfct  16787  prmdvdsbc  16809  hashdvds  16858  eulerthlem1  16864  eulerthlem2  16865  prmdiv  16868  prmdiveq  16869  pcpremul  16927  pcqmul  16937  pcaddlem  16972  prmpwdvds  16988  4sqlem5  17026  4sqlem10  17031  4sqlem14  17042  mulgass  19223  mulgmodid  19225  odmod  19662  odmulgid  19670  odbezout  19674  gexdvds  19700  odadd1  19964  odadd2  19965  torsubg  19970  ablfacrp  20184  pgpfac1lem2  20193  pgpfac1lem3a  20194  pgpfac1lem3  20195  ablsimpgfindlem1  20225  pzriprnglem6  21688  pzriprnglem8  21690  pzriprnglem12  21694  znunit  21765  znrrg  21767  dyaddisjlem  25807  elqaalem3  26535  aalioulem1  26548  aaliou3lem2  26559  aaliou3lem8  26561  mpodvdsmulf1o  27411  dvdsmulf1o  27413  lgsdirprm  27548  lgsdir  27549  lgsdilem2  27550  lgsdi  27551  gausslemma2dlem1a  27582  gausslemma2dlem5a  27587  gausslemma2dlem5  27588  gausslemma2dlem6  27589  gausslemma2dlem7  27590  gausslemma2d  27591  lgseisenlem1  27592  lgseisenlem2  27593  lgseisenlem3  27594  lgseisenlem4  27595  lgsquadlem1  27597  lgsquad2lem1  27601  lgsquad3  27604  2lgslem1a1  27606  2lgslem1a2  27607  2lgslem1b  27609  2lgslem3b1  27618  2lgslem3c1  27619  2lgsoddprmlem2  27626  2sqlem3  27637  2sqlem4  27638  2sqblem  27648  2sqmod  27653  ex-ind-dvds  30885  elrgspnlem2  33629  zringfrac  33910  cos9thpiminplylem2  34239  qqhghm  34444  qqhrhm  34445  breprexplemc  35086  circlemeth  35094  knoppndvlem2  37161  lcmineqlem6  42861  lcmineqlem14  42869  lcmineqlem18  42873  lcmineqlem21  42876  lcmineqlem22  42877  aks4d1p8d2  42912  aks4d1p8  42914  aks4d1p9  42915  primrootscoprmpow  42926  posbezout  42927  primrootscoprbij  42929  primrootspoweq0  42933  aks6d1c3  42950  aks6d1c4  42951  2np3bcnp1  42971  aks6d1c6lem3  42999  aks6d1c6lem4  43000  aks6d1c6lem5  43004  pellexlem5  43620  pellexlem6  43621  pell1234qrmulcl  43642  congmul  43754  jm2.18  43775  jm2.19lem1  43776  jm2.19lem2  43777  jm2.19lem3  43778  jm2.19lem4  43779  jm2.22  43782  jm2.23  43783  jm2.20nn  43784  jm2.25  43786  jm2.15nn0  43790  jm2.16nn0  43791  jm2.27c  43794  jm3.1lem3  43806  jm3.1  43807  expdiophlem1  43808  inductionexd  44941  sumnnodd  46406  wallispilem4  46842  stirlinglem3  46850  stirlinglem7  46854  stirlinglem10  46857  stirlinglem11  46858  dirkertrigeqlem1  46872  dirkertrigeqlem3  46874  dirkertrigeq  46875  dirkercncflem2  46878  fourierswlem  47004  fouriersw  47005  etransclem3  47011  etransclem7  47015  etransclem10  47018  etransclem25  47033  etransclem26  47034  etransclem27  47035  etransclem28  47036  etransclem35  47043  etransclem37  47045  etransclem44  47052  etransclem45  47053  minusmodnep2tmod  48156  modmkpkne  48164  modmknepk  48165  fmtnoprmfac2lem1  48378  fmtno4prmfac  48384  2pwp1prm  48401  mod42tp1mod8  48414  lighneallem4b  48421  lighneallem4  48422  nprmdvdsfacm1lem4  48435  ppivalnnprm  48437  m2even  48479  fppr2odd  48556  gpg3kgrtriexlem3  48910  gpg3kgrtriexlem6  48913  2zlidl  49064  dignn0fr  49440  dignn0flhalflem1  49454