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

Theorem peano2zm 12013
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 12000 . 2 1 ∈ ℤ
2 zsubcl 12012 . 2 ((𝑁 ∈ ℤ ∧ 1 ∈ ℤ) → (𝑁 − 1) ∈ ℤ)
31, 2mpan2 690 1 (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2114  (class class class)co 7140  1c1 10527  cmin 10859  cz 11969
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-sep 5179  ax-nul 5186  ax-pow 5243  ax-pr 5307  ax-un 7446  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ne 3012  df-nel 3116  df-ral 3135  df-rex 3136  df-reu 3137  df-rab 3139  df-v 3471  df-sbc 3748  df-csb 3856  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4266  df-if 4440  df-pw 4513  df-sn 4540  df-pr 4542  df-tp 4544  df-op 4546  df-uni 4814  df-iun 4896  df-br 5043  df-opab 5105  df-mpt 5123  df-tr 5149  df-id 5437  df-eprel 5442  df-po 5451  df-so 5452  df-fr 5491  df-we 5493  df-xp 5538  df-rel 5539  df-cnv 5540  df-co 5541  df-dm 5542  df-rn 5543  df-res 5544  df-ima 5545  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6293  df-fun 6336  df-fn 6337  df-f 6338  df-f1 6339  df-fo 6340  df-f1o 6341  df-fv 6342  df-riota 7098  df-ov 7143  df-oprab 7144  df-mpo 7145  df-om 7566  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-er 8276  df-en 8497  df-dom 8498  df-sdom 8499  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-nn 11626  df-n0 11886  df-z 11970
This theorem is referenced by:  zlem1lt  12022  zltlem1  12023  zextlt  12044  zeo  12056  eluzp1m1  12256  uzm1  12264  zbtwnre  12334  fz01en  12930  fzsuc2  12960  elfzm11  12973  uzdisj  12975  preduz  13024  predfz  13027  elfzo  13035  fzon  13053  fzoss2  13060  fzossrbm1  13061  fzosplitsnm1  13107  ubmelm1fzo  13128  elfzom1b  13131  fzosplitprm1  13142  fzoshftral  13149  sermono  13398  seqf1olem1  13405  seqf1olem2  13406  bcm1k  13671  bcn2  13675  bcp1m1  13676  bcpasc  13677  bccl  13678  hashbclem  13806  seqcoll  13818  revccat  14119  revrev  14120  absrdbnd  14692  fsumm1  15097  binomlem  15175  isumsplit  15186  climcndslem1  15195  arisum2  15207  pwdif  15214  pwm1geoser  15215  mertenslem1  15231  fprodser  15294  fprodm1  15312  risefacval2  15355  fallfacval2  15356  fallfacval3  15357  fallfacfwd  15381  binomfallfaclem2  15385  3dvds  15671  oddm1even  15683  oddp1even  15684  mod2eq1n2dvds  15687  zob  15699  nno  15722  pwp1fsum  15731  isprm3  16016  ncoprmlnprm  16057  hashdvds  16101  pockthlem  16230  4sqlem11  16280  vdwapun  16299  vdwnnlem2  16321  efgsp1  18854  efgsres  18855  srgbinomlem4  19284  srgbinomlem  19285  znunit  20253  dvexp3  24579  dvfsumlem1  24627  degltlem1  24671  atantayl2  25522  wilthlem1  25651  basellem5  25668  mersenne  25809  perfectlem1  25811  lgslem1  25879  lgsval2lem  25889  lgseisenlem1  25957  lgseisenlem2  25958  lgseisenlem3  25959  lgsquadlem1  25962  lgsquadlem3  25964  lgsquad2lem1  25966  lgsquad3  25969  2sqlem8  26008  2sqblem  26013  dchrisumlem1  26071  logdivbnd  26138  pntrsumbnd2  26149  ostth2lem3  26217  axlowdim  26753  pthdlem1  27553  pthdlem2  27555  wwlksm1edg  27665  clwwlkccatlem  27772  clwlkclwwlklem2fv1  27778  clwlkclwwlklem2a4  27780  clwlkclwwlklem2a  27781  clwlkclwwlklem2  27783  clwlkclwwlk  27785  clwwisshclwwslem  27797  clwwlkf  27830  wwlksubclwwlk  27841  numclwwlk5  28171  numclwwlk7  28174  frgrreggt1  28176  0nn0m1nnn0  32425  erdszelem7  32518  elfzm12  32992  fz0n  33036  fwddifnp1  33700  knoppndvlem2  33926  ltflcei  35007  poimirlem1  35020  poimirlem2  35021  poimirlem6  35025  poimirlem7  35026  poimirlem8  35027  poimirlem9  35028  poimirlem15  35034  poimirlem16  35035  poimirlem17  35036  poimirlem18  35037  poimirlem19  35038  poimirlem20  35039  poimirlem24  35043  poimirlem27  35046  poimirlem31  35050  poimirlem32  35051  mettrifi  35157  rmxluc  39811  rmyluc  39812  jm2.24  39838  jm2.18  39863  jm2.22  39870  jm2.23  39871  jm2.26lem3  39876  jm2.15nn0  39878  jm2.16nn0  39879  jm2.27a  39880  jm2.27c  39882  jm3.1lem3  39894  hashnzfz  40962  monoords  41872  fzisoeu  41875  dvnmul  42528  stoweidlem11  42596  dirkercncflem1  42688  fourierdlem48  42739  fourierdlem49  42740  fourierdlem65  42756  fourierdlem79  42770  zm1nn  43802  iccpartipre  43881  sfprmdvdsmersenne  44064  lighneallem4a  44069  proththd  44075  dfodd6  44098  evenm1odd  44100  oddm1eveni  44103  onego  44107  m1expoddALTV  44109  dfodd4  44120  oddflALTV  44124  oddm1evenALTV  44136  nnoALTV  44156  perfectALTVlem1  44182  altgsumbcALT  44698  pw2m1lepw2m1  44872  m1modmmod  44878  difmodm1lt  44879  zofldiv2  44888  logbpw2m1  44924  nnolog2flm1  44947  dignn0flhalflem1  44972
  Copyright terms: Public domain W3C validator