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  35962  elfzm12  36440  fz0n  36496  fwddifnp1  36930  knoppndvlem2  37379  ltflcei  38532  poimirlem1  38540  poimirlem2  38541  poimirlem6  38545  poimirlem7  38546  poimirlem8  38547  poimirlem9  38548  poimirlem15  38554  poimirlem16  38555  poimirlem17  38556  poimirlem18  38557  poimirlem19  38558  poimirlem20  38559  poimirlem24  38563  poimirlem27  38566  poimirlem31  38570  poimirlem32  38571  mettrifi  38692  rmxluc  43943  rmyluc  43944  jm2.24  43970  jm2.18  43995  jm2.22  44002  jm2.23  44003  jm2.26lem3  44008  jm2.15nn0  44010  jm2.16nn0  44011  jm2.27a  44012  jm2.27c  44014  jm3.1lem3  44026  hashnzfz  45304  monoords  46313  fzisoeu  46316  dvnmul  46953  stoweidlem11  47021  dirkercncflem1  47113  fourierdlem48  47164  fourierdlem49  47165  fourierdlem65  47181  fourierdlem79  47195  chnsubseq  47890  zm1nn  48372  flmrecm1  48413  m1modmmod  48434  difmodm1lt  48435  muldvdsfacgt  48456  iccpartipre  48503  sfprmdvdsmersenne  48688  lighneallem4a  48693  proththd  48699  dfodd6  48735  evenm1odd  48737  oddm1eveni  48740  onego  48744  m1expoddALTV  48746  dfodd4  48757  oddflALTV  48761  oddm1evenALTV  48773  nnoALTV  48793  perfectALTVlem1  48819  altgsumbcALT  49465  pw2m1lepw2m1  49632  zofldiv2  49643  logbpw2m1  49679  nnolog2flm1  49702  dignn0flhalflem1  49727