Theorem peano2zm 12640

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7410  1c1 11135   − cmin 11471  ℤcz 12593

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734  ax-resscn 11191  ax-1cn 11192  ax-icn 11193  ax-addcl 11194  ax-addrcl 11195  ax-mulcl 11196  ax-mulrcl 11197  ax-mulcom 11198  ax-addass 11199  ax-mulass 11200  ax-distr 11201  ax-i2m1 11202  ax-1ne0 11203  ax-1rid 11204  ax-rnegex 11205  ax-rrecex 11206  ax-cnre 11207  ax-pre-lttri 11208  ax-pre-lttrn 11209  ax-pre-ltadd 11210  ax-pre-mulgt0 11211

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-iun 4974  df-br 5125  df-opab 5187  df-mpt 5207  df-tr 5235  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6295  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-om 7867  df-2nd 7994  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-rdg 8429  df-er 8724  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11276  df-mnf 11277  df-xr 11278  df-ltxr 11279  df-le 11280  df-sub 11473  df-neg 11474  df-nn 12246  df-n0 12507  df-z 12594

This theorem is referenced by:  zlem1lt  12649  zltlem1  12650  zextlt  12672  zeo  12684  eluzp1m1  12883  uzm1  12895  zbtwnre  12967  fz01en  13574  fzsuc2  13604  elfzm11  13617  uzdisj  13619  preduz  13672  predfz  13675  elfzo  13683  fzon  13702  fzoss2  13709  fzossrbm1  13710  fzosplitsnm1  13761  ubmelm1fzo  13784  elfzom1b  13787  fzosplitprm1  13798  fzoshftral  13805  sermono  14057  seqf1olem1  14064  seqf1olem2  14065  bcm1k  14338  bcn2  14342  bcp1m1  14343  bcpasc  14344  bccl  14345  hashbclem  14475  seqcoll  14487  revccat  14789  revrev  14790  absrdbnd  15365  fsumm1  15772  binomlem  15850  isumsplit  15861  climcndslem1  15870  arisum2  15882  pwdif  15889  pwm1geoser  15890  mertenslem1  15905  fprodser  15970  fprodm1  15988  risefacval2  16031  fallfacval2  16032  fallfacval3  16033  fallfacfwd  16057  binomfallfaclem2  16061  3dvds  16355  oddm1even  16367  oddp1even  16368  mod2eq1n2dvds  16371  zob  16383  nno  16406  pwp1fsum  16415  isprm3  16707  ncoprmlnprm  16752  hashdvds  16799  pockthlem  16930  4sqlem11  16980  vdwapun  16999  vdwnnlem2  17021  efgsp1  19723  efgsres  19724  srgbinomlem4  20194  srgbinomlem  20195  znunit  21529  dvexp3  25939  dvfsumlem1  25989  degltlem1  26034  atantayl2  26905  wilthlem1  27035  basellem5  27052  mersenne  27195  perfectlem1  27197  lgslem1  27265  lgsval2lem  27275  lgseisenlem1  27343  lgseisenlem2  27344  lgseisenlem3  27345  lgsquadlem1  27348  lgsquadlem3  27350  lgsquad2lem1  27352  lgsquad3  27355  2sqlem8  27394  2sqblem  27399  dchrisumlem1  27457  logdivbnd  27524  pntrsumbnd2  27535  ostth2lem3  27603  axlowdim  28945  pthdlem1  29753  pthdlem2  29755  wwlksm1edg  29868  clwwlkccatlem  29975  clwlkclwwlklem2fv1  29981  clwlkclwwlklem2a4  29983  clwlkclwwlklem2a  29984  clwlkclwwlklem2  29986  clwlkclwwlk  29988  clwwisshclwwslem  30000  clwwlkf  30033  wwlksubclwwlk  30044  numclwwlk5  30374  numclwwlk7  30377  frgrreggt1  30379  0nn0m1nnn0  35140  erdszelem7  35224  elfzm12  35702  fz0n  35753  fwddifnp1  36188  knoppndvlem2  36536  ltflcei  37637  poimirlem1  37650  poimirlem2  37651  poimirlem6  37655  poimirlem7  37656  poimirlem8  37657  poimirlem9  37658  poimirlem15  37664  poimirlem16  37665  poimirlem17  37666  poimirlem18  37667  poimirlem19  37668  poimirlem20  37669  poimirlem24  37673  poimirlem27  37676  poimirlem31  37680  poimirlem32  37681  mettrifi  37786  rmxluc  42935  rmyluc  42936  jm2.24  42962  jm2.18  42987  jm2.22  42994  jm2.23  42995  jm2.26lem3  43000  jm2.15nn0  43002  jm2.16nn0  43003  jm2.27a  43004  jm2.27c  43006  jm3.1lem3  43018  hashnzfz  44319  monoords  45306  fzisoeu  45309  dvnmul  45952  stoweidlem11  46020  dirkercncflem1  46112  fourierdlem48  46163  fourierdlem49  46164  fourierdlem65  46180  fourierdlem79  46194  zm1nn  47311  iccpartipre  47415  sfprmdvdsmersenne  47597  lighneallem4a  47602  proththd  47608  dfodd6  47631  evenm1odd  47633  oddm1eveni  47636  onego  47640  m1expoddALTV  47642  dfodd4  47653  oddflALTV  47657  oddm1evenALTV  47669  nnoALTV  47689  perfectALTVlem1  47715  altgsumbcALT  48308  pw2m1lepw2m1  48476  m1modmmod  48481  difmodm1lt  48482  zofldiv2  48491  logbpw2m1  48527  nnolog2flm1  48550  dignn0flhalflem1  48575