Theorem peano2zm 12363

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

Syntax hints:   → wi 4   ∈ wcel 2106  (class class class)co 7275  1c1 10872   − cmin 11205  ℤcz 12319

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-mulcom 10935  ax-addass 10936  ax-mulass 10937  ax-distr 10938  ax-i2m1 10939  ax-1ne0 10940  ax-1rid 10941  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944  ax-pre-lttri 10945  ax-pre-lttrn 10946  ax-pre-ltadd 10947  ax-pre-mulgt0 10948

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-riota 7232  df-ov 7278  df-oprab 7279  df-mpo 7280  df-om 7713  df-2nd 7832  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-er 8498  df-en 8734  df-dom 8735  df-sdom 8736  df-pnf 11011  df-mnf 11012  df-xr 11013  df-ltxr 11014  df-le 11015  df-sub 11207  df-neg 11208  df-nn 11974  df-n0 12234  df-z 12320

This theorem is referenced by:  zlem1lt  12372  zltlem1  12373  zextlt  12394  zeo  12406  eluzp1m1  12608  uzm1  12616  zbtwnre  12686  fz01en  13284  fzsuc2  13314  elfzm11  13327  uzdisj  13329  preduz  13378  predfz  13381  elfzo  13389  fzon  13408  fzoss2  13415  fzossrbm1  13416  fzosplitsnm1  13462  ubmelm1fzo  13483  elfzom1b  13486  fzosplitprm1  13497  fzoshftral  13504  sermono  13755  seqf1olem1  13762  seqf1olem2  13763  bcm1k  14029  bcn2  14033  bcp1m1  14034  bcpasc  14035  bccl  14036  hashbclem  14164  seqcoll  14178  revccat  14479  revrev  14480  absrdbnd  15053  fsumm1  15463  binomlem  15541  isumsplit  15552  climcndslem1  15561  arisum2  15573  pwdif  15580  pwm1geoser  15581  mertenslem1  15596  fprodser  15659  fprodm1  15677  risefacval2  15720  fallfacval2  15721  fallfacval3  15722  fallfacfwd  15746  binomfallfaclem2  15750  3dvds  16040  oddm1even  16052  oddp1even  16053  mod2eq1n2dvds  16056  zob  16068  nno  16091  pwp1fsum  16100  isprm3  16388  ncoprmlnprm  16432  hashdvds  16476  pockthlem  16606  4sqlem11  16656  vdwapun  16675  vdwnnlem2  16697  efgsp1  19343  efgsres  19344  srgbinomlem4  19779  srgbinomlem  19780  znunit  20771  dvexp3  25142  dvfsumlem1  25190  degltlem1  25237  atantayl2  26088  wilthlem1  26217  basellem5  26234  mersenne  26375  perfectlem1  26377  lgslem1  26445  lgsval2lem  26455  lgseisenlem1  26523  lgseisenlem2  26524  lgseisenlem3  26525  lgsquadlem1  26528  lgsquadlem3  26530  lgsquad2lem1  26532  lgsquad3  26535  2sqlem8  26574  2sqblem  26579  dchrisumlem1  26637  logdivbnd  26704  pntrsumbnd2  26715  ostth2lem3  26783  axlowdim  27329  pthdlem1  28134  pthdlem2  28136  wwlksm1edg  28246  clwwlkccatlem  28353  clwlkclwwlklem2fv1  28359  clwlkclwwlklem2a4  28361  clwlkclwwlklem2a  28362  clwlkclwwlklem2  28364  clwlkclwwlk  28366  clwwisshclwwslem  28378  clwwlkf  28411  wwlksubclwwlk  28422  numclwwlk5  28752  numclwwlk7  28755  frgrreggt1  28757  0nn0m1nnn0  33071  erdszelem7  33159  elfzm12  33633  fz0n  33696  fwddifnp1  34467  knoppndvlem2  34693  ltflcei  35765  poimirlem1  35778  poimirlem2  35779  poimirlem6  35783  poimirlem7  35784  poimirlem8  35785  poimirlem9  35786  poimirlem15  35792  poimirlem16  35793  poimirlem17  35794  poimirlem18  35795  poimirlem19  35796  poimirlem20  35797  poimirlem24  35801  poimirlem27  35804  poimirlem31  35808  poimirlem32  35809  mettrifi  35915  rmxluc  40758  rmyluc  40759  jm2.24  40785  jm2.18  40810  jm2.22  40817  jm2.23  40818  jm2.26lem3  40823  jm2.15nn0  40825  jm2.16nn0  40826  jm2.27a  40827  jm2.27c  40829  jm3.1lem3  40841  hashnzfz  41938  monoords  42836  fzisoeu  42839  dvnmul  43484  stoweidlem11  43552  dirkercncflem1  43644  fourierdlem48  43695  fourierdlem49  43696  fourierdlem65  43712  fourierdlem79  43726  zm1nn  44794  iccpartipre  44873  sfprmdvdsmersenne  45055  lighneallem4a  45060  proththd  45066  dfodd6  45089  evenm1odd  45091  oddm1eveni  45094  onego  45098  m1expoddALTV  45100  dfodd4  45111  oddflALTV  45115  oddm1evenALTV  45127  nnoALTV  45147  perfectALTVlem1  45173  altgsumbcALT  45689  pw2m1lepw2m1  45861  m1modmmod  45867  difmodm1lt  45868  zofldiv2  45877  logbpw2m1  45913  nnolog2flm1  45936  dignn0flhalflem1  45961