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

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

Proof of Theorem zsubcl
StepHypRef Expression
1 zcn 10458 . . 3
2 zcn 10458 . . 3
3 negsub 9475 . . 3
41, 2, 3syl2an 465 . 2
5 znegcl 10487 . . 3
6 zaddcl 10492 . . 3
75, 6sylan2 462 . 2
84, 7eqeltrrd 2556 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  /\wa 360  =wceq 1662  e.wcel 1724  (class class class)co 6067   cc 9102   caddc 9107   cmin 9415  -ucneg 9416   cz 10453
This theorem is referenced by:  peano2zm  10495  zrevaddcl  10497  znnsub  10498  znn0sub  10499  zneo  10531  uzindOLD  10543  zsubcld  10559  eluzsubi  10695  fzen  11266  uzsubsubfz  11270  fz0fzdiffz0  11288  fzrev  11314  fzrev2  11315  fzm1  11335  fzrevral2  11340  fzshftral  11342  fzonfzoufzol  11420  elfzomelpfzo  11421  zmodcl  11519  fzen2  11583  facndiv  11856  bccmpl  11877  bcval5  11886  bcpasc  11889  hashfz  11975  ccatsymb  12068  swrdlend  12112  swrd0  12114  swrdspsleq  12129  swrdccatin12lem1  12161  swrdccatin12lem2a  12162  swrdccatin12lem2b  12163  swrdccatin12lem2  12166  swrdccat  12170  repswswrd  12208  cshwsublen  12219  2cshwid  12234  3cshw  12238  cshweqdif2  12239  seqshft  12360  isercoll2  12932  moddvds  13328  dvds2sub  13351  dvdssub2  13356  dvdssubr  13360  fzocongeq  13373  odd2np1  13378  3dvds  13382  divalglem0  13383  divalglem4  13386  divalglem9  13391  divalgb  13394  divalgmod  13396  ndvdsadd  13398  nn0seqcvgd  13531  eulerthlem2  13643  prmdiv  13646  prmdiveq  13647  omoe  13665  omeo  13667  pythagtriplem4  13672  pythagtriplem8  13676  mod2xnegi  13886  cshwshashlem2  13909  mndodcongi  15684  odcong  15690  odf1  15701  odf1o1  15709  efgredleme  15878  plyeq0lem  20633  aaliou3lem1  20763  aaliou3lem2  20764  efif1olem2  20954  wilthlem2  21361  basellem2  21373  dchrptlem1  21557  bposlem6  21582  lgsquadlem1  21647  ballotlemfelz  25514  zfallfaccl  26167  binomrisefac  26188  bpolydiflem  26930  irrapxlem1  27814  jm2.24nn  27953  congtr  27959  congadd  27960  congmul  27961  congabseq  27968  acongeq  27977  jm2.26a  28000  jm2.15nn0  28003  jm2.27c  28007  jm3.1  28020  lesubnn0  29038  2elfz2melfz  29059  elfzlble  29065  elfzelfzlble  29066  subsubelfzo0  29067  clwlkisclwwlklem2fv2  29304  erclwwlksym0  29337  difelfzle  29346  difelfznle  29347  cshwlemma1  29348
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1562  ax-4 1573  ax-5 1636  ax-6 1677  ax-7 1697  ax-8 1726  ax-9 1728  ax-10 1743  ax-11 1748  ax-12 1760  ax-13 1947  ax-ext 2462  ax-sep 4423  ax-nul 4431  ax-pow 4477  ax-pr 4538  ax-un 6338  ax-resscn 9161  ax-1cn 9162  ax-icn 9163  ax-addcl 9164  ax-addrcl 9165  ax-mulcl 9166  ax-mulrcl 9167  ax-mulcom 9168  ax-addass 9169  ax-mulass 9170  ax-distr 9171  ax-i2m1 9172  ax-1ne0 9173  ax-1rid 9174  ax-rnegex 9175  ax-rrecex 9176  ax-cnre 9177  ax-pre-lttri 9178  ax-pre-lttrn 9179  ax-pre-ltadd 9180  ax-pre-mulgt0 9181
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1337  df-ex 1558  df-nf 1561  df-sb 1669  df-eu 2309  df-mo 2310  df-clab 2468  df-cleq 2474  df-clel 2477  df-nfc 2606  df-ne 2646  df-nel 2647  df-ral 2756  df-rex 2757  df-reu 2758  df-rab 2760  df-v 3008  df-sbc 3213  df-csb 3314  df-dif 3356  df-un 3358  df-in 3360  df-ss 3367  df-pss 3369  df-nul 3661  df-if 3813  df-pw 3880  df-sn 3900  df-pr 3901  df-tp 3902  df-op 3903  df-uni 4102  df-iun 4183  df-br 4303  df-opab 4361  df-mpt 4362  df-tr 4396  df-eprel 4635  df-id 4639  df-po 4644  df-so 4645  df-fr 4682  df-we 4684  df-ord 4725  df-on 4726  df-lim 4727  df-suc 4728  df-xp 4850  df-rel 4851  df-cnv 4852  df-co 4853  df-dm 4854  df-rn 4855  df-res 4856  df-ima 4857  df-iota 5380  df-fun 5419  df-fn 5420  df-f 5421  df-f1 5422  df-fo 5423  df-f1o 5424  df-fv 5425  df-riota 6026  df-ov 6070  df-oprab 6071  df-mpt2 6072  df-om 6442  df-recs 6745  df-rdg 6780  df-er 7017  df-en 7222  df-dom 7223  df-sdom 7224  df-pnf 9242  df-mnf 9243  df-xr 9244  df-ltxr 9245  df-le 9246  df-sub 9417  df-neg 9418  df-nn 10132  df-n0 10389  df-z 10454
  Copyright terms: Public domain W3C validator