Theorem peano2zm 12293

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 12280	. 2 ⊢ 1 ∈ ℤ
2		zsubcl 12292	. 2 ⊢ ((𝑁 ∈ ℤ ∧ 1 ∈ ℤ) → (𝑁 − 1) ∈ ℤ)
3	1, 2	mpan2 687	1 ⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2108  (class class class)co 7255  1c1 10803   − cmin 11135  ℤcz 12249

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-i2m1 10870  ax-1ne0 10871  ax-1rid 10872  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877  ax-pre-ltadd 10878  ax-pre-mulgt0 10879

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260  df-om 7688  df-2nd 7805  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-pnf 10942  df-mnf 10943  df-xr 10944  df-ltxr 10945  df-le 10946  df-sub 11137  df-neg 11138  df-nn 11904  df-n0 12164  df-z 12250

This theorem is referenced by:  zlem1lt  12302  zltlem1  12303  zextlt  12324  zeo  12336  eluzp1m1  12537  uzm1  12545  zbtwnre  12615  fz01en  13213  fzsuc2  13243  elfzm11  13256  uzdisj  13258  preduz  13307  predfz  13310  elfzo  13318  fzon  13336  fzoss2  13343  fzossrbm1  13344  fzosplitsnm1  13390  ubmelm1fzo  13411  elfzom1b  13414  fzosplitprm1  13425  fzoshftral  13432  sermono  13683  seqf1olem1  13690  seqf1olem2  13691  bcm1k  13957  bcn2  13961  bcp1m1  13962  bcpasc  13963  bccl  13964  hashbclem  14092  seqcoll  14106  revccat  14407  revrev  14408  absrdbnd  14981  fsumm1  15391  binomlem  15469  isumsplit  15480  climcndslem1  15489  arisum2  15501  pwdif  15508  pwm1geoser  15509  mertenslem1  15524  fprodser  15587  fprodm1  15605  risefacval2  15648  fallfacval2  15649  fallfacval3  15650  fallfacfwd  15674  binomfallfaclem2  15678  3dvds  15968  oddm1even  15980  oddp1even  15981  mod2eq1n2dvds  15984  zob  15996  nno  16019  pwp1fsum  16028  isprm3  16316  ncoprmlnprm  16360  hashdvds  16404  pockthlem  16534  4sqlem11  16584  vdwapun  16603  vdwnnlem2  16625  efgsp1  19258  efgsres  19259  srgbinomlem4  19694  srgbinomlem  19695  znunit  20683  dvexp3  25047  dvfsumlem1  25095  degltlem1  25142  atantayl2  25993  wilthlem1  26122  basellem5  26139  mersenne  26280  perfectlem1  26282  lgslem1  26350  lgsval2lem  26360  lgseisenlem1  26428  lgseisenlem2  26429  lgseisenlem3  26430  lgsquadlem1  26433  lgsquadlem3  26435  lgsquad2lem1  26437  lgsquad3  26440  2sqlem8  26479  2sqblem  26484  dchrisumlem1  26542  logdivbnd  26609  pntrsumbnd2  26620  ostth2lem3  26688  axlowdim  27232  pthdlem1  28035  pthdlem2  28037  wwlksm1edg  28147  clwwlkccatlem  28254  clwlkclwwlklem2fv1  28260  clwlkclwwlklem2a4  28262  clwlkclwwlklem2a  28263  clwlkclwwlklem2  28265  clwlkclwwlk  28267  clwwisshclwwslem  28279  clwwlkf  28312  wwlksubclwwlk  28323  numclwwlk5  28653  numclwwlk7  28656  frgrreggt1  28658  0nn0m1nnn0  32971  erdszelem7  33059  elfzm12  33533  fz0n  33602  fwddifnp1  34394  knoppndvlem2  34620  ltflcei  35692  poimirlem1  35705  poimirlem2  35706  poimirlem6  35710  poimirlem7  35711  poimirlem8  35712  poimirlem9  35713  poimirlem15  35719  poimirlem16  35720  poimirlem17  35721  poimirlem18  35722  poimirlem19  35723  poimirlem20  35724  poimirlem24  35728  poimirlem27  35731  poimirlem31  35735  poimirlem32  35736  mettrifi  35842  rmxluc  40674  rmyluc  40675  jm2.24  40701  jm2.18  40726  jm2.22  40733  jm2.23  40734  jm2.26lem3  40739  jm2.15nn0  40741  jm2.16nn0  40742  jm2.27a  40743  jm2.27c  40745  jm3.1lem3  40757  hashnzfz  41827  monoords  42726  fzisoeu  42729  dvnmul  43374  stoweidlem11  43442  dirkercncflem1  43534  fourierdlem48  43585  fourierdlem49  43586  fourierdlem65  43602  fourierdlem79  43616  zm1nn  44682  iccpartipre  44761  sfprmdvdsmersenne  44943  lighneallem4a  44948  proththd  44954  dfodd6  44977  evenm1odd  44979  oddm1eveni  44982  onego  44986  m1expoddALTV  44988  dfodd4  44999  oddflALTV  45003  oddm1evenALTV  45015  nnoALTV  45035  perfectALTVlem1  45061  altgsumbcALT  45577  pw2m1lepw2m1  45749  m1modmmod  45755  difmodm1lt  45756  zofldiv2  45765  logbpw2m1  45801  nnolog2flm1  45824  dignn0flhalflem1  45849