Theorem zaddcld 12820

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  (class class class)co 7430   + caddc 11216  ℤcz 12706

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7761  ax-resscn 11270  ax-1cn 11271  ax-icn 11272  ax-addcl 11273  ax-addrcl 11274  ax-mulcl 11275  ax-mulrcl 11276  ax-mulcom 11277  ax-addass 11278  ax-mulass 11279  ax-distr 11280  ax-i2m1 11281  ax-1ne0 11282  ax-1rid 11283  ax-rnegex 11284  ax-rrecex 11285  ax-cnre 11286  ax-pre-lttri 11287  ax-pre-lttrn 11288  ax-pre-ltadd 11289  ax-pre-mulgt0 11290

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6311  df-ord 6372  df-on 6373  df-lim 6374  df-suc 6375  df-iota 6501  df-fun 6549  df-fn 6550  df-f 6551  df-f1 6552  df-fo 6553  df-f1o 6554  df-fv 6555  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7888  df-2nd 8012  df-frecs 8313  df-wrecs 8344  df-recs 8393  df-rdg 8432  df-er 8731  df-en 8988  df-dom 8989  df-sdom 8990  df-pnf 11358  df-mnf 11359  df-xr 11360  df-ltxr 11361  df-le 11362  df-sub 11556  df-neg 11557  df-nn 12349  df-n0 12620  df-z 12707

This theorem is used by:  zadd2cl  12824  qaddcl  13106  elincfzoext  13871  eluzgtdifelfzo  13875  fladdz  13978  seqshft2  14184  expaddzlem  14261  sqoddm1div8  14400  ccatass  14747  cshf1  14975  2cshw  14978  2cshwcshw  14990  fsumrev2  15963  isumshft  16023  divcnvshft  16039  addmulmodb  16450  dvds2ln  16474  sadadd3  16646  sadaddlem  16651  sadadd  16652  bezoutlem4  16730  lcmgcdlem  16796  divgcdcoprm0  16855  hashdvds  16967  pythagtriplem4  17012  pythagtriplem11  17018  pcaddlem  17081  gzmulcl  17131  4sqlem8  17138  4sqlem10  17140  4sqlem11  17148  4sqlem14  17151  4sqlem16  17153  prmgaplem7  17250  prmgaplem8  17251  chnccat  18815  gsumsgrpccat  19051  mulgdir  19331  mndodconglem  19770  pzriprnglem10  21811  pzriprng1ALT  21817  chfacfscmulfsupp  23192  chfacfpmmulfsupp  23196  ulmshftlem  26731  ulmshft  26732  dchrptlem2  27607  lgsqrlem2  27689  lgsquad2lem1  27726  2lgsoddprmlem2  27751  2sqlem4  27763  2sqlem8  27768  2sqmod  27778  flt4lem3  27993  crctcshwlkn0lem5  30418  numclwlk2lem2f  30993  ex-ind-dvds  31077  cshwrnid  33578  archirngz  33806  archiabllem2c  33812  zringfrac  34142  qqhghm  34676  qqhrhm  34677  fsum2dsub  35292  breprexplemc  35317  divcnvlin  36628  caushft  38838  lcmineqlem22  43243  posbezout  43293  2np3bcnp1  43337  sticksstones7  43345  sticksstones10  43348  aks6d1c6isolem1  43367  aks6d1c6isolem2  43368  bcle2d  43372  aks6d1c7lem1  43373  sumcubes  43513  pell1234qrmulcl  44005  jm2.18  44138  jm2.19lem3  44141  jm2.19lem4  44142  jm2.25  44149  inductionexd  45298  fzisoeu  46458  uzubioo  46719  wallispilem4  47220  etransclem44  47430  evenwodadd  48053  submodaddmod  48559  zplusmodne  48561  gbowgt5  49002  mogoldbb  49025  nnsum4primesevenALTV  49041  gpgiedgdmellem  49286  gpgvtx1  49294  pgnbgreunbgrlem2lem1  49354  pgnbgreunbgrlem2lem3  49356  2zlidl  49479