Theorem peano2zm 11297

Description: "Reverse" second Peano postulate for integers. (Contributed by NM, 12-Sep-2005.)

Assertion

Ref	Expression
peano2zm	⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)

Proof of Theorem peano2zm

Step	Hyp	Ref	Expression
1		1z 11284	. 2 ⊢ 1 ∈ ℤ
2		zsubcl 11296	. 2 ⊢ ((𝑁 ∈ ℤ ∧ 1 ∈ ℤ) → (𝑁 − 1) ∈ ℤ)
3	1, 2	mpan2 703	1 ⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 1977  (class class class)co 6549  1c1 9816   − cmin 10145  ℤcz 11254

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-n0 11170  df-z 11255

This theorem is referenced by:  zlem1lt  11306  zltlem1  11307  zextlt  11327  zeo  11339  eluzp1m1  11587  uzm1  11594  zbtwnre  11662  fz01en  12240  fzsuc2  12268  elfzm11  12280  uzdisj  12282  preduz  12330  predfz  12333  elfzo  12341  fzon  12358  fzoss2  12365  fzossrbm1  12366  fzosplitsnm1  12409  ubmelm1fzo  12430  elfzom1b  12433  fzosplitprm1  12443  fzoshftral  12447  sermono  12695  seqf1olem1  12702  seqf1olem2  12703  bcm1k  12964  bcn2  12968  bcp1m1  12969  bcpasc  12970  bccl  12971  hashbclem  13093  seqcoll  13105  revccat  13366  revrev  13367  absrdbnd  13929  fsumm1  14324  binomlem  14400  isumsplit  14411  climcndslem1  14420  arisum2  14432  mertenslem1  14455  fprodser  14518  fprodm1  14536  risefacval2  14580  fallfacval2  14581  fallfacval3  14582  fallfacfwd  14606  binomfallfaclem2  14610  3dvds  14890  3dvdsOLD  14891  oddm1even  14905  oddp1even  14906  mod2eq1n2dvds  14909  zob  14921  nno  14936  pwp1fsum  14952  isprm3  15234  ncoprmlnprm  15274  hashdvds  15318  pockthlem  15447  4sqlem11  15497  vdwapun  15516  vdwap0  15518  vdwnnlem2  15538  efgsp1  17973  efgsres  17974  srgbinomlem4  18366  srgbinomlem  18367  znunit  19731  dvexp3  23545  dvfsumlem1  23593  degltlem1  23636  abelthlem6  23994  atantayl2  24465  wilthlem1  24594  basellem5  24611  mersenne  24752  perfectlem1  24754  lgslem1  24822  lgsval2lem  24832  lgseisenlem1  24900  lgseisenlem2  24901  lgseisenlem3  24902  lgsquadlem1  24905  lgsquadlem3  24907  lgsquad2lem1  24909  lgsquad3  24912  2sqlem8  24951  2sqblem  24956  dchrisumlem1  24978  logdivbnd  25045  pntrsumbnd2  25056  ostth2lem3  25124  axlowdim  25641  wwlkm1edg  26263  clwlkisclwwlklem2fv1  26310  clwlkisclwwlklem2a4  26312  clwlkisclwwlklem2a  26313  clwlkisclwwlklem1  26315  clwlkisclwwlk  26317  clwwlkf  26322  wwlksubclwwlk  26332  clwwisshclwwlem  26334  clwlkfclwwlk  26371  nbhashuvtx1  26442  extwwlkfablem2  26605  numclwwlk5  26639  numclwwlk7  26641  frgrareggt1  26643  erdszelem7  30433  elfzm12  30823  fz0n  30869  fwddifnp1  31442  knoppndvlem2  31674  ltflcei  32567  poimirlem1  32580  poimirlem2  32581  poimirlem6  32585  poimirlem7  32586  poimirlem8  32587  poimirlem9  32588  poimirlem15  32594  poimirlem16  32595  poimirlem17  32596  poimirlem18  32597  poimirlem19  32598  poimirlem20  32599  poimirlem24  32603  poimirlem27  32606  poimirlem31  32610  poimirlem32  32611  mettrifi  32723  rmxluc  36519  rmyluc  36520  jm2.24  36548  jm2.18  36573  jm2.22  36580  jm2.23  36581  jm2.26lem3  36586  jm2.15nn0  36588  jm2.16nn0  36589  jm2.27a  36590  jm2.27c  36592  jm3.1lem3  36604  hashnzfz  37541  monoords  38452  fzisoeu  38455  dvnmul  38833  stoweidlem11  38904  dirkercncflem1  38996  fourierdlem48  39047  fourierdlem49  39048  fourierdlem65  39064  fourierdlem79  39078  iccpartipre  39959  pwdif  40039  pwm1geoserALT  40040  sfprmdvdsmersenne  40058  lighneallem4a  40063  proththd  40069  dfodd6  40088  evenm1odd  40090  oddm1eveni  40093  onego  40097  m1expoddALTV  40099  dfodd4  40109  oddflALTV  40113  oddm1evenALTV  40124  nnoALTV  40144  perfectALTVlem1  40164  zm1nn  40348  pthdlem1  40972  pthdlem2  40974  wwlksm1edg  41078  clwlkclwwlklem2fv1  41204  clwlkclwwlklem2a4  41206  clwlkclwwlklem2a  41207  clwlkclwwlklem2  41209  clwlkclwwlk  41211  clwwlksf  41222  wwlksubclwwlks  41232  clwwisshclwwslem  41234  clwlksfclwwlk  41269  av-extwwlkfablem2  41510  av-numclwwlk5  41542  av-numclwwlk7  41545  av-frgrareggt1  41547  altgsumbcALT  41924  pw2m1lepw2m1  42104  m1modmmod  42110  difmodm1lt  42111  zofldiv2  42119  logbpw2m1  42159  nnolog2flm1  42182  dignn0flhalflem1  42207