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

Theorem zsubcl 10905
Description: Closure of subtraction of integers. (Contributed by NM, 11-May-2004.)
Assertion
Ref Expression
zsubcl  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( M  -  N
)  e.  ZZ )

Proof of Theorem zsubcl
StepHypRef Expression
1 zcn 10869 . . 3  |-  ( M  e.  ZZ  ->  M  e.  CC )
2 zcn 10869 . . 3  |-  ( N  e.  ZZ  ->  N  e.  CC )
3 negsub 9867 . . 3  |-  ( ( M  e.  CC  /\  N  e.  CC )  ->  ( M  +  -u N )  =  ( M  -  N ) )
41, 2, 3syl2an 477 . 2  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( M  +  -u N )  =  ( M  -  N ) )
5 znegcl 10898 . . 3  |-  ( N  e.  ZZ  ->  -u N  e.  ZZ )
6 zaddcl 10903 . . 3  |-  ( ( M  e.  ZZ  /\  -u N  e.  ZZ )  ->  ( M  +  -u N )  e.  ZZ )
75, 6sylan2 474 . 2  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( M  +  -u N )  e.  ZZ )
84, 7eqeltrrd 2556 1  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( M  -  N
)  e.  ZZ )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1379    e. wcel 1767  (class class class)co 6284   CCcc 9490    + caddc 9495    - cmin 9805   -ucneg 9806   ZZcz 10864
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6576  ax-resscn 9549  ax-1cn 9550  ax-icn 9551  ax-addcl 9552  ax-addrcl 9553  ax-mulcl 9554  ax-mulrcl 9555  ax-mulcom 9556  ax-addass 9557  ax-mulass 9558  ax-distr 9559  ax-i2m1 9560  ax-1ne0 9561  ax-1rid 9562  ax-rnegex 9563  ax-rrecex 9564  ax-cnre 9565  ax-pre-lttri 9566  ax-pre-lttrn 9567  ax-pre-ltadd 9568  ax-pre-mulgt0 9569
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2819  df-rex 2820  df-reu 2821  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5551  df-fun 5590  df-fn 5591  df-f 5592  df-f1 5593  df-fo 5594  df-f1o 5595  df-fv 5596  df-riota 6245  df-ov 6287  df-oprab 6288  df-mpt2 6289  df-om 6685  df-recs 7042  df-rdg 7076  df-er 7311  df-en 7517  df-dom 7518  df-sdom 7519  df-pnf 9630  df-mnf 9631  df-xr 9632  df-ltxr 9633  df-le 9634  df-sub 9807  df-neg 9808  df-nn 10537  df-n0 10796  df-z 10865
This theorem is referenced by:  peano2zm  10906  zrevaddcl  10908  znnsub  10909  znn0sub  10910  zneo  10943  uzindOLD  10955  zsubcld  10971  eluzsubi  11109  fzen  11703  uzsubsubfz  11707  fzrev  11742  fzrev2  11743  fzm1  11758  fzrevral2  11763  fzshftral  11765  fz0fzdiffz0  11781  difelfzle  11785  difelfznle  11786  fzonfzoufzol  11881  elfzomelpfzo  11882  zmodcl  11983  fzen2  12047  facndiv  12334  bccmpl  12355  bcval5  12364  bcpasc  12367  hashfz  12450  ccatsymb  12565  swrdlend  12619  swrd0  12621  swrdspsleq  12636  swrdccatin12lem1  12672  swrdccatin12lem2a  12673  swrdccatin12lem2b  12674  swrdccatin12lem2  12677  swrdccat  12681  repswswrd  12719  cshwsublen  12730  2cshwid  12745  3cshw  12749  cshweqdif2  12750  2cshwcshw  12756  cshwcshid  12758  seqshft  12881  isercoll2  13454  moddvds  13854  dvds2sub  13877  dvdssub2  13882  dvdssubr  13886  fzocongeq  13899  odd2np1  13905  3dvds  13909  divalglem0  13910  divalglem4  13913  divalglem9  13918  divalgb  13921  divalgmod  13923  ndvdsadd  13925  nn0seqcvgd  14058  eulerthlem2  14171  prmdiv  14174  prmdiveq  14175  omoe  14195  omeo  14197  pythagtriplem4  14202  pythagtriplem8  14206  mod2xnegi  14416  cshwshashlem2  14439  mndodcongi  16373  odcong  16379  odf1  16390  odf1o1  16398  efgredleme  16567  srgbinomlem4  16996  plyeq0lem  22370  aaliou3lem1  22500  aaliou3lem2  22501  efif1olem2  22691  wilthlem2  23099  basellem2  23111  dchrptlem1  23295  bposlem6  23320  lgsquadlem1  23385  clwlkisclwwlklem2fv2  24487  ballotlemfelz  28097  zfallfaccl  28748  binomrisefac  28769  bpolydiflem  29421  irrapxlem1  30390  jm2.24nn  30529  congtr  30535  congadd  30536  congmul  30537  congabseq  30544  acongeq  30553  jm2.26a  30574  jm2.15nn0  30577  jm2.27c  30581  jm3.1  30594  lesubnn0  31821  2elfz2melfz  31829  elfzlble  31831  elfzelfzlble  31832  subsubelfzo0  31833  altgsumbc  32037  altgsumbcALT  32038  zlmodzxzsub  32045
  Copyright terms: Public domain W3C validator