Theorem peano2zm 12605

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

Syntax hints:   → wi 4   ∈ wcel 2107  (class class class)co 7409  1c1 11111   − cmin 11444  ℤcz 12558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-er 8703  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-nn 12213  df-n0 12473  df-z 12559

This theorem is referenced by:  zlem1lt  12614  zltlem1  12615  zextlt  12636  zeo  12648  eluzp1m1  12848  uzm1  12860  zbtwnre  12930  fz01en  13529  fzsuc2  13559  elfzm11  13572  uzdisj  13574  preduz  13623  predfz  13626  elfzo  13634  fzon  13653  fzoss2  13660  fzossrbm1  13661  fzosplitsnm1  13707  ubmelm1fzo  13728  elfzom1b  13731  fzosplitprm1  13742  fzoshftral  13749  sermono  14000  seqf1olem1  14007  seqf1olem2  14008  bcm1k  14275  bcn2  14279  bcp1m1  14280  bcpasc  14281  bccl  14282  hashbclem  14411  seqcoll  14425  revccat  14716  revrev  14717  absrdbnd  15288  fsumm1  15697  binomlem  15775  isumsplit  15786  climcndslem1  15795  arisum2  15807  pwdif  15814  pwm1geoser  15815  mertenslem1  15830  fprodser  15893  fprodm1  15911  risefacval2  15954  fallfacval2  15955  fallfacval3  15956  fallfacfwd  15980  binomfallfaclem2  15984  3dvds  16274  oddm1even  16286  oddp1even  16287  mod2eq1n2dvds  16290  zob  16302  nno  16325  pwp1fsum  16334  isprm3  16620  ncoprmlnprm  16664  hashdvds  16708  pockthlem  16838  4sqlem11  16888  vdwapun  16907  vdwnnlem2  16929  efgsp1  19605  efgsres  19606  srgbinomlem4  20052  srgbinomlem  20053  znunit  21119  dvexp3  25495  dvfsumlem1  25543  degltlem1  25590  atantayl2  26443  wilthlem1  26572  basellem5  26589  mersenne  26730  perfectlem1  26732  lgslem1  26800  lgsval2lem  26810  lgseisenlem1  26878  lgseisenlem2  26879  lgseisenlem3  26880  lgsquadlem1  26883  lgsquadlem3  26885  lgsquad2lem1  26887  lgsquad3  26890  2sqlem8  26929  2sqblem  26934  dchrisumlem1  26992  logdivbnd  27059  pntrsumbnd2  27070  ostth2lem3  27138  axlowdim  28219  pthdlem1  29023  pthdlem2  29025  wwlksm1edg  29135  clwwlkccatlem  29242  clwlkclwwlklem2fv1  29248  clwlkclwwlklem2a4  29250  clwlkclwwlklem2a  29251  clwlkclwwlklem2  29253  clwlkclwwlk  29255  clwwisshclwwslem  29267  clwwlkf  29300  wwlksubclwwlk  29311  numclwwlk5  29641  numclwwlk7  29644  frgrreggt1  29646  0nn0m1nnn0  34102  erdszelem7  34188  elfzm12  34660  fz0n  34700  fwddifnp1  35137  knoppndvlem2  35389  ltflcei  36476  poimirlem1  36489  poimirlem2  36490  poimirlem6  36494  poimirlem7  36495  poimirlem8  36496  poimirlem9  36497  poimirlem15  36503  poimirlem16  36504  poimirlem17  36505  poimirlem18  36506  poimirlem19  36507  poimirlem20  36508  poimirlem24  36512  poimirlem27  36515  poimirlem31  36519  poimirlem32  36520  mettrifi  36625  rmxluc  41675  rmyluc  41676  jm2.24  41702  jm2.18  41727  jm2.22  41734  jm2.23  41735  jm2.26lem3  41740  jm2.15nn0  41742  jm2.16nn0  41743  jm2.27a  41744  jm2.27c  41746  jm3.1lem3  41758  hashnzfz  43079  monoords  44007  fzisoeu  44010  dvnmul  44659  stoweidlem11  44727  dirkercncflem1  44819  fourierdlem48  44870  fourierdlem49  44871  fourierdlem65  44887  fourierdlem79  44901  zm1nn  46010  iccpartipre  46089  sfprmdvdsmersenne  46271  lighneallem4a  46276  proththd  46282  dfodd6  46305  evenm1odd  46307  oddm1eveni  46310  onego  46314  m1expoddALTV  46316  dfodd4  46327  oddflALTV  46331  oddm1evenALTV  46343  nnoALTV  46363  perfectALTVlem1  46389  altgsumbcALT  47029  pw2m1lepw2m1  47201  m1modmmod  47207  difmodm1lt  47208  zofldiv2  47217  logbpw2m1  47253  nnolog2flm1  47276  dignn0flhalflem1  47301