Theorem peano2zm 12739

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  (class class class)co 7420  1c1 11201   − cmin 11541  ℤcz 12693

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-mulcom 11264  ax-addass 11265  ax-mulass 11266  ax-distr 11267  ax-i2m1 11268  ax-1ne0 11269  ax-1rid 11270  ax-rnegex 11271  ax-rrecex 11272  ax-cnre 11273  ax-pre-lttri 11274  ax-pre-lttrn 11275  ax-pre-ltadd 11276  ax-pre-mulgt0 11277

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-om 7878  df-2nd 8002  df-frecs 8299  df-wrecs 8330  df-recs 8379  df-rdg 8418  df-er 8717  df-en 8974  df-dom 8975  df-sdom 8976  df-pnf 11345  df-mnf 11346  df-xr 11347  df-ltxr 11348  df-le 11349  df-sub 11543  df-neg 11544  df-nn 12336  df-n0 12607  df-z 12694

This theorem is used by:  zlem1lt  12748  zltlem1  12749  0nn0m1nnn0  12753  zextlt  12773  zeo  12785  eluzp1m1  12991  uzm1  12999  zbtwnre  13073  fz01en  13686  fzsuc2  13716  elfzm11  13729  uzdisj  13731  preduz  13784  predfz  13787  elfzo  13795  fzon  13815  fzoss2  13822  fzossrbm1  13823  fzosplitsnm1  13875  ubmelm1fzo  13898  elfzom1b  13901  fzosplitprm1  13913  fzoshftral  13922  sermono  14177  seqf1olem1  14184  seqf1olem2  14185  bcm1k  14459  bcn2  14463  bcp1m1  14464  bcpasc  14465  bccl  14466  hashbclem  14597  seqcoll  14609  revccat  14915  revrev  14916  absrdbnd  15509  fsumm1  15917  binomlem  15998  isumsplit  16009  climcndslem1  16018  arisum2  16030  pwdif  16037  pwm1geoser  16038  mertenslem1  16053  fprodser  16116  fprodm1  16134  risefacval2  16177  fallfacval2  16178  fallfacval3  16179  fallfacfwd  16202  binomfallfaclem2  16206  3dvds  16501  oddm1even  16513  oddp1even  16514  mod2eq1n2dvds  16517  zob  16529  nno  16552  pwp1fsum  16561  isprm3  16858  ncoprmlnprm  16904  hashdvds  16952  pockthlem  17083  4sqlem11  17133  vdwapun  17152  vdwnnlem2  17174  chnccat  18800  efgsp1  19951  efgsres  19952  srgbinomlem4  20455  srgbinomlem  20456  znunit  21869  dvexp3  26298  dvfsumlem1  26346  degltlem1  26390  atantayl2  27266  wilthlem1  27395  basellem5  27412  mersenne  27554  perfectlem1  27556  lgslem1  27624  lgsval2lem  27634  lgseisenlem1  27702  lgseisenlem2  27703  lgseisenlem3  27704  lgsquadlem1  27707  lgsquadlem3  27709  lgsquad2lem1  27711  lgsquad3  27714  2sqlem8  27753  2sqblem  27758  dchrisumlem1  27816  logdivbnd  27883  pntrsumbnd2  27894  ostth2lem3  27962  axlowdim  29539  pthdlem1  30352  pthdlem2  30354  wwlksm1edg  30470  clwwlkccatlem  30580  clwlkclwwlklem2fv1  30586  clwlkclwwlklem2a4  30588  clwlkclwwlklem2a  30589  clwlkclwwlklem2  30591  clwlkclwwlk  30593  clwwisshclwwslem  30605  clwwlkf  30638  wwlksubclwwlk  30649  numclwwlk5  30989  numclwwlk7  30992  frgrreggt1  30994  erdszelem7  36004  elfzm12  36482  fz0n  36538  fwddifnp1  36972  knoppndvlem2  37421  ltflcei  38574  poimirlem1  38582  poimirlem2  38583  poimirlem6  38587  poimirlem7  38588  poimirlem8  38589  poimirlem9  38590  poimirlem15  38596  poimirlem16  38597  poimirlem17  38598  poimirlem18  38599  poimirlem19  38600  poimirlem20  38601  poimirlem24  38605  poimirlem27  38608  poimirlem31  38612  poimirlem32  38613  mettrifi  38734  rmxluc  43985  rmyluc  43986  jm2.24  44012  jm2.18  44037  jm2.22  44044  jm2.23  44045  jm2.26lem3  44050  jm2.15nn0  44052  jm2.16nn0  44053  jm2.27a  44054  jm2.27c  44056  jm3.1lem3  44068  hashnzfz  45346  monoords  46355  fzisoeu  46358  dvnmul  46995  stoweidlem11  47063  dirkercncflem1  47155  fourierdlem48  47206  fourierdlem49  47207  fourierdlem65  47223  fourierdlem79  47237  chnsubseq  47932  zm1nn  48414  flmrecm1  48455  m1modmmod  48476  difmodm1lt  48477  muldvdsfacgt  48498  iccpartipre  48545  sfprmdvdsmersenne  48730  lighneallem4a  48735  proththd  48741  dfodd6  48777  evenm1odd  48779  oddm1eveni  48782  onego  48786  m1expoddALTV  48788  dfodd4  48799  oddflALTV  48803  oddm1evenALTV  48815  nnoALTV  48835  perfectALTVlem1  48861  altgsumbcALT  49507  pw2m1lepw2m1  49674  zofldiv2  49685  logbpw2m1  49721  nnolog2flm1  49744  dignn0flhalflem1  49769