Theorem peano2zm 12616

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

Syntax hints:   → wi 4   ∈ wcel 2144  (class class class)co 7398  1c1 11076   − cmin 11416  ℤcz 12570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2214  ax-ext 2736  ax-sep 5248  ax-nul 5258  ax-pow 5324  ax-pr 5392  ax-un 7720  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151  ax-pre-mulgt0 11152

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-nf 1806  df-sb 2093  df-mo 2568  df-eu 2598  df-clab 2743  df-cleq 2756  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3064  df-ral 3079  df-rex 3089  df-reu 3370  df-rab 3417  df-v 3458  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5544  df-eprel 5549  df-po 5557  df-so 5558  df-fr 5602  df-we 5604  df-xp 5655  df-rel 5656  df-cnv 5657  df-co 5658  df-dm 5659  df-rn 5660  df-res 5661  df-ima 5662  df-pred 6290  df-ord 6351  df-on 6352  df-lim 6353  df-suc 6354  df-iota 6479  df-fun 6525  df-fn 6526  df-f 6527  df-f1 6528  df-fo 6529  df-f1o 6530  df-fv 6531  df-riota 7355  df-ov 7401  df-oprab 7402  df-mpo 7403  df-om 7849  df-2nd 7973  df-frecs 8264  df-wrecs 8295  df-recs 8344  df-rdg 8383  df-er 8680  df-en 8930  df-dom 8931  df-sdom 8932  df-pnf 11220  df-mnf 11221  df-xr 11222  df-ltxr 11223  df-le 11224  df-sub 11418  df-neg 11419  df-nn 12213  df-n0 12484  df-z 12571

This theorem is referenced by:  zlem1lt  12625  zltlem1  12626  zextlt  12649  zeo  12661  eluzp1m1  12867  uzm1  12875  zbtwnre  12949  fz01en  13559  fzsuc2  13589  elfzm11  13602  uzdisj  13604  preduz  13657  predfz  13660  elfzo  13668  fzon  13688  fzoss2  13695  fzossrbm1  13696  fzosplitsnm1  13748  ubmelm1fzo  13771  elfzom1b  13774  fzosplitprm1  13786  fzoshftral  13795  sermono  14049  seqf1olem1  14056  seqf1olem2  14057  bcm1k  14330  bcn2  14334  bcp1m1  14335  bcpasc  14336  bccl  14337  hashbclem  14467  seqcoll  14479  revccat  14781  revrev  14782  absrdbnd  15371  fsumm1  15780  binomlem  15861  isumsplit  15872  climcndslem1  15881  arisum2  15893  pwdif  15900  pwm1geoser  15901  mertenslem1  15916  fprodser  15981  fprodm1  15999  risefacval2  16042  fallfacval2  16043  fallfacval3  16044  fallfacfwd  16068  binomfallfaclem2  16072  3dvds  16367  oddm1even  16379  oddp1even  16380  mod2eq1n2dvds  16383  zob  16395  nno  16418  pwp1fsum  16427  isprm3  16719  ncoprmlnprm  16765  hashdvds  16812  pockthlem  16943  4sqlem11  16993  vdwapun  17012  vdwnnlem2  17034  chnccat  18660  efgsp1  19779  efgsres  19780  srgbinomlem4  20281  srgbinomlem  20282  znunit  21617  dvexp3  26042  dvfsumlem1  26090  degltlem1  26134  atantayl2  27005  wilthlem1  27134  basellem5  27151  mersenne  27293  perfectlem1  27295  lgslem1  27363  lgsval2lem  27373  lgseisenlem1  27441  lgseisenlem2  27442  lgseisenlem3  27443  lgsquadlem1  27446  lgsquadlem3  27448  lgsquad2lem1  27450  lgsquad3  27453  2sqlem8  27492  2sqblem  27497  dchrisumlem1  27555  logdivbnd  27622  pntrsumbnd2  27633  ostth2lem3  27701  axlowdim  29164  pthdlem1  29968  pthdlem2  29970  wwlksm1edg  30083  clwwlkccatlem  30193  clwlkclwwlklem2fv1  30199  clwlkclwwlklem2a4  30201  clwlkclwwlklem2a  30202  clwlkclwwlklem2  30204  clwlkclwwlk  30206  clwwisshclwwslem  30218  clwwlkf  30251  wwlksubclwwlk  30262  numclwwlk5  30592  numclwwlk7  30595  frgrreggt1  30597  0nn0m1nnn0  35467  erdszelem7  35552  elfzm12  36030  fz0n  36086  fwddifnp1  36520  knoppndvlem2  36956  ltflcei  38112  poimirlem1  38125  poimirlem2  38126  poimirlem6  38130  poimirlem7  38131  poimirlem8  38132  poimirlem9  38133  poimirlem15  38139  poimirlem16  38140  poimirlem17  38141  poimirlem18  38142  poimirlem19  38143  poimirlem20  38144  poimirlem24  38148  poimirlem27  38151  poimirlem31  38155  poimirlem32  38156  mettrifi  38261  rmxluc  43518  rmyluc  43519  jm2.24  43545  jm2.18  43570  jm2.22  43577  jm2.23  43578  jm2.26lem3  43583  jm2.15nn0  43585  jm2.16nn0  43586  jm2.27a  43587  jm2.27c  43589  jm3.1lem3  43601  hashnzfz  44901  monoords  45881  fzisoeu  45884  dvnmul  46522  stoweidlem11  46590  dirkercncflem1  46682  fourierdlem48  46733  fourierdlem49  46734  fourierdlem65  46750  fourierdlem79  46764  chnsubseq  47461  zm1nn  47901  flmrecm1  47942  m1modmmod  47963  difmodm1lt  47964  muldvdsfacgt  47985  iccpartipre  48032  sfprmdvdsmersenne  48217  lighneallem4a  48222  proththd  48228  dfodd6  48264  evenm1odd  48266  oddm1eveni  48269  onego  48273  m1expoddALTV  48275  dfodd4  48286  oddflALTV  48290  oddm1evenALTV  48302  nnoALTV  48322  perfectALTVlem1  48348  altgsumbcALT  48980  pw2m1lepw2m1  49147  zofldiv2  49158  logbpw2m1  49194  nnolog2flm1  49217  dignn0flhalflem1  49242