MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  zsubcl Unicode version

Theorem zsubcl 10551
Description: Closure of subtraction of integers. (Contributed by NM, 11-May-2004.)
Assertion
Ref Expression
zsubcl

Proof of Theorem zsubcl
StepHypRef Expression
1 zcn 10515 . . 3
2 zcn 10515 . . 3
3 negsub 9532 . . 3
41, 2, 3syl2an 465 . 2
5 znegcl 10544 . . 3
6 zaddcl 10549 . . 3
75, 6sylan2 462 . 2
84, 7eqeltrrd 2564 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  /\wa 360  =wceq 1670  e.wcel 1732  (class class class)co 6103   cc 9159   caddc 9164   cmin 9472  -ucneg 9473   cz 10510
This theorem is referenced by:  peano2zm  10552  zrevaddcl  10554  znnsub  10555  znn0sub  10556  zneo  10588  uzindOLD  10600  zsubcld  10616  eluzsubi  10752  fzen  11323  uzsubsubfz  11327  fz0fzdiffz0  11345  fzrev  11371  fzrev2  11372  fzm1  11392  fzrevral2  11397  fzshftral  11399  fzonfzoufzol  11477  elfzomelpfzo  11478  zmodcl  11576  fzen2  11640  facndiv  11913  bccmpl  11934  bcval5  11943  bcpasc  11946  hashfz  12035  ccatsymb  12128  swrdlend  12172  swrd0  12174  swrdspsleq  12189  swrdccatin12lem1  12222  swrdccatin12lem2a  12223  swrdccatin12lem2b  12224  swrdccatin12lem2  12227  swrdccat  12231  repswswrd  12269  cshwsublen  12280  2cshwid  12295  3cshw  12299  cshweqdif2  12300  seqshft  12421  isercoll2  12993  moddvds  13389  dvds2sub  13412  dvdssub2  13417  dvdssubr  13421  fzocongeq  13434  odd2np1  13439  3dvds  13443  divalglem0  13444  divalglem4  13447  divalglem9  13452  divalgb  13455  divalgmod  13457  ndvdsadd  13459  nn0seqcvgd  13592  eulerthlem2  13704  prmdiv  13707  prmdiveq  13708  omoe  13726  omeo  13728  pythagtriplem4  13733  pythagtriplem8  13737  mod2xnegi  13947  cshwshashlem2  13970  mndodcongi  15790  odcong  15796  odf1  15807  odf1o1  15815  efgredleme  15984  plyeq0lem  21144  aaliou3lem1  21274  aaliou3lem2  21275  efif1olem2  21465  wilthlem2  21873  basellem2  21885  dchrptlem1  22069  bposlem6  22094  lgsquadlem1  22159  ballotlemfelz  26023  zfallfaccl  26676  binomrisefac  26697  bpolydiflem  27439  irrapxlem1  28311  jm2.24nn  28450  congtr  28456  congadd  28457  congmul  28458  congabseq  28465  acongeq  28474  jm2.26a  28497  jm2.15nn0  28500  jm2.27c  28504  jm3.1  28517  lesubnn0  29360  2elfz2melfz  29381  elfzlble  29387  elfzelfzlble  29388  subsubelfzo0  29389  clwlkisclwwlklem2fv2  29626  erclwwlksym0  29659  difelfzle  29668  difelfznle  29669  cshwlemma1  29670
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1570  ax-4 1581  ax-5 1644  ax-6 1685  ax-7 1705  ax-8 1734  ax-9 1736  ax-10 1751  ax-11 1756  ax-12 1768  ax-13 1955  ax-ext 2470  ax-sep 4439  ax-nul 4447  ax-pow 4493  ax-pr 4554  ax-un 6382  ax-resscn 9218  ax-1cn 9219  ax-icn 9220  ax-addcl 9221  ax-addrcl 9222  ax-mulcl 9223  ax-mulrcl 9224  ax-mulcom 9225  ax-addass 9226  ax-mulass 9227  ax-distr 9228  ax-i2m1 9229  ax-1ne0 9230  ax-1rid 9231  ax-rnegex 9232  ax-rrecex 9233  ax-cnre 9234  ax-pre-lttri 9235  ax-pre-lttrn 9236  ax-pre-ltadd 9237  ax-pre-mulgt0 9238
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1338  df-ex 1566  df-nf 1569  df-sb 1677  df-eu 2317  df-mo 2318  df-clab 2476  df-cleq 2482  df-clel 2485  df-nfc 2614  df-ne 2654  df-nel 2655  df-ral 2764  df-rex 2765  df-reu 2766  df-rab 2768  df-v 3017  df-sbc 3225  df-csb 3326  df-dif 3368  df-un 3370  df-in 3372  df-ss 3379  df-pss 3381  df-nul 3674  df-if 3826  df-pw 3895  df-sn 3915  df-pr 3916  df-tp 3917  df-op 3918  df-uni 4118  df-iun 4199  df-br 4319  df-opab 4377  df-mpt 4378  df-tr 4412  df-eprel 4653  df-id 4657  df-po 4662  df-so 4663  df-fr 4700  df-we 4702  df-ord 4743  df-on 4744  df-lim 4745  df-suc 4746  df-xp 4868  df-rel 4869  df-cnv 4870  df-co 4871  df-dm 4872  df-rn 4873  df-res 4874  df-ima 4875  df-iota 5401  df-fun 5440  df-fn 5441  df-f 5442  df-f1 5443  df-fo 5444  df-f1o 5445  df-fv 5446  df-riota 6062  df-ov 6106  df-oprab 6107  df-mpt2 6108  df-om 6487  df-recs 6795  df-rdg 6830  df-er 7067  df-en 7274  df-dom 7275  df-sdom 7276  df-pnf 9299  df-mnf 9300  df-xr 9301  df-ltxr 9302  df-le 9303  df-sub 9474  df-neg 9475  df-nn 10189  df-n0 10446  df-z 10511
  Copyright terms: Public domain W3C validator