MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  zaddcld Structured version   Visualization version   GIF version

Theorem zaddcld 11599
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
StepHypRef Expression
1 zred.1 . 2 (𝜑𝐴 ∈ ℤ)
2 zaddcld.1 . 2 (𝜑𝐵 ∈ ℤ)
3 zaddcl 11530 . 2 ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 + 𝐵) ∈ ℤ)
41, 2, 3syl2anc 696 1 (𝜑 → (𝐴 + 𝐵) ∈ ℤ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2103  (class class class)co 6765   + caddc 10052  cz 11490
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-8 2105  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-sep 4889  ax-nul 4897  ax-pow 4948  ax-pr 5011  ax-un 7066  ax-resscn 10106  ax-1cn 10107  ax-icn 10108  ax-addcl 10109  ax-addrcl 10110  ax-mulcl 10111  ax-mulrcl 10112  ax-mulcom 10113  ax-addass 10114  ax-mulass 10115  ax-distr 10116  ax-i2m1 10117  ax-1ne0 10118  ax-1rid 10119  ax-rnegex 10120  ax-rrecex 10121  ax-cnre 10122  ax-pre-lttri 10123  ax-pre-lttrn 10124  ax-pre-ltadd 10125  ax-pre-mulgt0 10126
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ne 2897  df-nel 3000  df-ral 3019  df-rex 3020  df-reu 3021  df-rab 3023  df-v 3306  df-sbc 3542  df-csb 3640  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-pss 3696  df-nul 4024  df-if 4195  df-pw 4268  df-sn 4286  df-pr 4288  df-tp 4290  df-op 4292  df-uni 4545  df-iun 4630  df-br 4761  df-opab 4821  df-mpt 4838  df-tr 4861  df-id 5128  df-eprel 5133  df-po 5139  df-so 5140  df-fr 5177  df-we 5179  df-xp 5224  df-rel 5225  df-cnv 5226  df-co 5227  df-dm 5228  df-rn 5229  df-res 5230  df-ima 5231  df-pred 5793  df-ord 5839  df-on 5840  df-lim 5841  df-suc 5842  df-iota 5964  df-fun 6003  df-fn 6004  df-f 6005  df-f1 6006  df-fo 6007  df-f1o 6008  df-fv 6009  df-riota 6726  df-ov 6768  df-oprab 6769  df-mpt2 6770  df-om 7183  df-wrecs 7527  df-recs 7588  df-rdg 7626  df-er 7862  df-en 8073  df-dom 8074  df-sdom 8075  df-pnf 10189  df-mnf 10190  df-xr 10191  df-ltxr 10192  df-le 10193  df-sub 10381  df-neg 10382  df-nn 11134  df-n0 11406  df-z 11491
This theorem is referenced by:  zadd2cl  11603  qaddcl  11918  elincfzoext  12641  eluzgtdifelfzo  12645  fladdz  12741  seqshft2  12942  expaddzlem  13018  sqoddm1div8  13143  ccatass  13481  lswccatn0lsw  13484  cshf1  13677  2cshw  13680  2cshwcshw  13692  fsumrev2  14634  isumshft  14691  divcnvshft  14707  dvds2ln  15137  sadadd3  15306  sadaddlem  15311  sadadd  15312  bezoutlem4  15382  lcmgcdlem  15442  divgcdcoprm0  15502  hashdvds  15603  pythagtriplem4  15647  pythagtriplem11  15653  pcaddlem  15715  gzmulcl  15765  4sqlem8  15772  4sqlem10  15774  4sqlem11  15782  4sqlem14  15785  4sqlem16  15787  prmgaplem7  15884  prmgaplem8  15885  gsumccat  17500  mulgdir  17695  mndodconglem  18081  chfacfscmulfsupp  20787  chfacfpmmulfsupp  20791  ulmshftlem  24263  ulmshft  24264  dchrptlem2  25110  lgsqrlem2  25192  lgsquad2lem1  25229  2lgsoddprmlem2  25254  2sqlem4  25266  2sqlem8  25271  crctcshwlkn0lem5  26838  numclwlk2lem2f  27459  numclwlk2lem2fOLD  27466  ex-ind-dvds  27550  2sqmod  29878  archirngz  29973  archiabllem2c  29979  qqhghm  30262  qqhrhm  30263  fsum2dsub  30915  breprexplemc  30940  divcnvlin  31846  caushft  33789  pell1234qrmulcl  37838  jm2.18  37974  jm2.19lem3  37977  jm2.19lem4  37978  jm2.25  37985  inductionexd  38872  fzisoeu  39930  uzubioo  40214  wallispilem4  40705  etransclem44  40915  gbowgt5  42077  mogoldbb  42100  nnsum4primesevenALTV  42116  2zlidl  42361
  Copyright terms: Public domain W3C validator