Theorem zaddcld 12708

Description: Closure of addition of integers. (Contributed by Mario Carneiro, 28-May-2016.)

Hypotheses

Ref	Expression
zred.1	⊢ (𝜑 → 𝐴 ∈ ℤ)
zaddcld.1	⊢ (𝜑 → 𝐵 ∈ ℤ)

Assertion

Ref	Expression
zaddcld	⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℤ)

Proof of Theorem zaddcld

Step	Hyp	Ref	Expression
1		zred.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℤ)
2		zaddcld.1	. 2 ⊢ (𝜑 → 𝐵 ∈ ℤ)
3		zaddcl 12640	. 2 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 + 𝐵) ∈ ℤ)
4	1, 2, 3	syl2anc 582	1 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2098  (class class class)co 7426   + caddc 11149  ℤ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  ax-pre-mulgt0 11223

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-xr 11290  df-ltxr 11291  df-le 11292  df-sub 11484  df-neg 11485  df-nn 12251  df-n0 12511  df-z 12597

This theorem is referenced by:  zadd2cl  12712  qaddcl  12987  elincfzoext  13730  eluzgtdifelfzo  13734  fladdz  13830  seqshft2  14033  expaddzlem  14110  sqoddm1div8  14245  ccatass  14578  cshf1  14800  2cshw  14803  2cshwcshw  14816  fsumrev2  15768  isumshft  15825  divcnvshft  15841  dvds2ln  16273  sadadd3  16443  sadaddlem  16448  sadadd  16449  bezoutlem4  16525  lcmgcdlem  16584  divgcdcoprm0  16643  hashdvds  16751  pythagtriplem4  16795  pythagtriplem11  16801  pcaddlem  16864  gzmulcl  16914  4sqlem8  16921  4sqlem10  16923  4sqlem11  16931  4sqlem14  16934  4sqlem16  16936  prmgaplem7  17033  prmgaplem8  17034  gsumsgrpccat  18799  mulgdir  19068  mndodconglem  19503  pzriprnglem10  21423  pzriprng1ALT  21429  chfacfscmulfsupp  22781  chfacfpmmulfsupp  22785  ulmshftlem  26345  ulmshft  26346  dchrptlem2  27218  lgsqrlem2  27300  lgsquad2lem1  27337  2lgsoddprmlem2  27362  2sqlem4  27374  2sqlem8  27379  2sqmod  27389  crctcshwlkn0lem5  29645  numclwlk2lem2f  30207  ex-ind-dvds  30291  cshwrnid  32703  archirngz  32918  archiabllem2c  32924  zringfrac  33277  qqhghm  33622  qqhrhm  33623  fsum2dsub  34272  breprexplemc  34297  divcnvlin  35360  caushft  37267  lcmineqlem22  41553  posbezout  41603  2np3bcnp1  41648  sticksstones7  41656  sticksstones10  41659  aks6d1c6isolem1  41678  aks6d1c6isolem2  41679  bcle2d  41683  aks6d1c7lem1  41684  metakunt19  41707  metakunt21  41709  metakunt22  41710  metakunt25  41713  metakunt27  41715  metakunt29  41717  metakunt30  41718  metakunt32  41720  metakunt33  41721  prodsplit  41724  sumcubes  41904  flt4lem3  42103  pell1234qrmulcl  42306  jm2.18  42440  jm2.19lem3  42443  jm2.19lem4  42444  jm2.25  42451  inductionexd  43616  fzisoeu  44711  uzubioo  44981  wallispilem4  45485  etransclem44  45695  gbowgt5  47131  mogoldbb  47154  nnsum4primesevenALTV  47170  2zlidl  47380