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

Theorem peano2zm 11458
Description: "Reverse" second Peano postulate for integers. (Contributed by NM, 12-Sep-2005.)
Assertion
Ref Expression
peano2zm (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)

Proof of Theorem peano2zm
StepHypRef Expression
1 1z 11445 . 2 1 ∈ ℤ
2 zsubcl 11457 . 2 ((𝑁 ∈ ℤ ∧ 1 ∈ ℤ) → (𝑁 − 1) ∈ ℤ)
31, 2mpan2 707 1 (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030  (class class class)co 6690  1c1 9975  cmin 10304  cz 11415
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059  df-n0 11331  df-z 11416
This theorem is referenced by:  zlem1lt  11467  zltlem1  11468  zextlt  11489  zeo  11501  eluzp1m1  11749  uzm1  11756  zbtwnre  11824  fz01en  12407  fzsuc2  12436  elfzm11  12449  uzdisj  12451  preduz  12500  predfz  12503  elfzo  12511  fzon  12528  fzoss2  12535  fzossrbm1  12536  fzosplitsnm1  12582  ubmelm1fzo  12604  elfzom1b  12607  fzosplitprm1  12618  fzoshftral  12625  sermono  12873  seqf1olem1  12880  seqf1olem2  12881  bcm1k  13142  bcn2  13146  bcp1m1  13147  bcpasc  13148  bccl  13149  hashbclem  13274  seqcoll  13286  revccat  13561  revrev  13562  absrdbnd  14125  fsumm1  14524  binomlem  14605  isumsplit  14616  climcndslem1  14625  arisum2  14637  mertenslem1  14660  fprodser  14723  fprodm1  14741  risefacval2  14785  fallfacval2  14786  fallfacval3  14787  fallfacfwd  14811  binomfallfaclem2  14815  3dvds  15099  3dvdsOLD  15100  oddm1even  15114  oddp1even  15115  mod2eq1n2dvds  15118  zob  15130  nno  15145  pwp1fsum  15161  isprm3  15443  ncoprmlnprm  15483  hashdvds  15527  pockthlem  15656  4sqlem11  15706  vdwapun  15725  vdwap0  15727  vdwnnlem2  15747  efgsp1  18196  efgsres  18197  srgbinomlem4  18589  srgbinomlem  18590  znunit  19960  dvexp3  23786  dvfsumlem1  23834  degltlem1  23877  abelthlem6  24235  atantayl2  24710  wilthlem1  24839  basellem5  24856  mersenne  24997  perfectlem1  24999  lgslem1  25067  lgsval2lem  25077  lgseisenlem1  25145  lgseisenlem2  25146  lgseisenlem3  25147  lgsquadlem1  25150  lgsquadlem3  25152  lgsquad2lem1  25154  lgsquad3  25157  2sqlem8  25196  2sqblem  25201  dchrisumlem1  25223  logdivbnd  25290  pntrsumbnd2  25301  ostth2lem3  25369  axlowdim  25886  pthdlem1  26718  pthdlem2  26720  wwlksm1edg  26835  clwlkclwwlklem2fv1  26961  clwlkclwwlklem2a4  26963  clwlkclwwlklem2a  26964  clwlkclwwlklem2  26966  clwlkclwwlk  26968  clwwisshclwwslem  26971  clwwlkf  27010  wwlksubclwwlk  27023  clwlksfclwwlk  27049  extwwlkfablem  27326  clwwlkccatlem  27331  numclwwlk5  27375  numclwwlk7  27378  frgrreggt1  27380  erdszelem7  31305  elfzm12  31695  fz0n  31742  fwddifnp1  32397  knoppndvlem2  32629  ltflcei  33527  poimirlem1  33540  poimirlem2  33541  poimirlem6  33545  poimirlem7  33546  poimirlem8  33547  poimirlem9  33548  poimirlem15  33554  poimirlem16  33555  poimirlem17  33556  poimirlem18  33557  poimirlem19  33558  poimirlem20  33559  poimirlem24  33563  poimirlem27  33566  poimirlem31  33570  poimirlem32  33571  mettrifi  33683  rmxluc  37818  rmyluc  37819  jm2.24  37847  jm2.18  37872  jm2.22  37879  jm2.23  37880  jm2.26lem3  37885  jm2.15nn0  37887  jm2.16nn0  37888  jm2.27a  37889  jm2.27c  37891  jm3.1lem3  37903  hashnzfz  38836  monoords  39825  fzisoeu  39828  dvnmul  40476  stoweidlem11  40546  dirkercncflem1  40638  fourierdlem48  40689  fourierdlem49  40690  fourierdlem65  40706  fourierdlem79  40720  zm1nn  41641  iccpartipre  41682  pwdif  41826  pwm1geoserALT  41827  sfprmdvdsmersenne  41845  lighneallem4a  41850  proththd  41856  dfodd6  41875  evenm1odd  41877  oddm1eveni  41880  onego  41884  m1expoddALTV  41886  dfodd4  41896  oddflALTV  41900  oddm1evenALTV  41911  nnoALTV  41931  perfectALTVlem1  41955  altgsumbcALT  42456  pw2m1lepw2m1  42635  m1modmmod  42641  difmodm1lt  42642  zofldiv2  42650  logbpw2m1  42686  nnolog2flm1  42709  dignn0flhalflem1  42734
  Copyright terms: Public domain W3C validator