Theorem peano2zm 12518

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7349  1c1 11010   − cmin 11347  ℤcz 12471

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 2701  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-i2m1 11077  ax-1ne0 11078  ax-1rid 11079  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084  ax-pre-ltadd 11085  ax-pre-mulgt0 11086

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5174  df-tr 5200  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6249  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-riota 7306  df-ov 7352  df-oprab 7353  df-mpo 7354  df-om 7800  df-2nd 7925  df-frecs 8214  df-wrecs 8245  df-recs 8294  df-rdg 8332  df-er 8625  df-en 8873  df-dom 8874  df-sdom 8875  df-pnf 11151  df-mnf 11152  df-xr 11153  df-ltxr 11154  df-le 11155  df-sub 11349  df-neg 11350  df-nn 12129  df-n0 12385  df-z 12472

This theorem is referenced by:  zlem1lt  12527  zltlem1  12528  zextlt  12550  zeo  12562  eluzp1m1  12761  uzm1  12773  zbtwnre  12847  fz01en  13455  fzsuc2  13485  elfzm11  13498  uzdisj  13500  preduz  13553  predfz  13556  elfzo  13564  fzon  13583  fzoss2  13590  fzossrbm1  13591  fzosplitsnm1  13643  ubmelm1fzo  13666  elfzom1b  13669  fzosplitprm1  13680  fzoshftral  13687  sermono  13941  seqf1olem1  13948  seqf1olem2  13949  bcm1k  14222  bcn2  14226  bcp1m1  14227  bcpasc  14228  bccl  14229  hashbclem  14359  seqcoll  14371  revccat  14672  revrev  14673  absrdbnd  15249  fsumm1  15658  binomlem  15736  isumsplit  15747  climcndslem1  15756  arisum2  15768  pwdif  15775  pwm1geoser  15776  mertenslem1  15791  fprodser  15856  fprodm1  15874  risefacval2  15917  fallfacval2  15918  fallfacval3  15919  fallfacfwd  15943  binomfallfaclem2  15947  3dvds  16242  oddm1even  16254  oddp1even  16255  mod2eq1n2dvds  16258  zob  16270  nno  16293  pwp1fsum  16302  isprm3  16594  ncoprmlnprm  16639  hashdvds  16686  pockthlem  16817  4sqlem11  16867  vdwapun  16886  vdwnnlem2  16908  efgsp1  19616  efgsres  19617  srgbinomlem4  20114  srgbinomlem  20115  znunit  21470  dvexp3  25880  dvfsumlem1  25930  degltlem1  25975  atantayl2  26846  wilthlem1  26976  basellem5  26993  mersenne  27136  perfectlem1  27138  lgslem1  27206  lgsval2lem  27216  lgseisenlem1  27284  lgseisenlem2  27285  lgseisenlem3  27286  lgsquadlem1  27289  lgsquadlem3  27291  lgsquad2lem1  27293  lgsquad3  27296  2sqlem8  27335  2sqblem  27340  dchrisumlem1  27398  logdivbnd  27465  pntrsumbnd2  27476  ostth2lem3  27544  axlowdim  28906  pthdlem1  29711  pthdlem2  29713  wwlksm1edg  29826  clwwlkccatlem  29933  clwlkclwwlklem2fv1  29939  clwlkclwwlklem2a4  29941  clwlkclwwlklem2a  29942  clwlkclwwlklem2  29944  clwlkclwwlk  29946  clwwisshclwwslem  29958  clwwlkf  29991  wwlksubclwwlk  30002  numclwwlk5  30332  numclwwlk7  30335  frgrreggt1  30337  0nn0m1nnn0  35096  erdszelem7  35180  elfzm12  35658  fz0n  35714  fwddifnp1  36149  knoppndvlem2  36497  ltflcei  37598  poimirlem1  37611  poimirlem2  37612  poimirlem6  37616  poimirlem7  37617  poimirlem8  37618  poimirlem9  37619  poimirlem15  37625  poimirlem16  37626  poimirlem17  37627  poimirlem18  37628  poimirlem19  37629  poimirlem20  37630  poimirlem24  37634  poimirlem27  37637  poimirlem31  37641  poimirlem32  37642  mettrifi  37747  rmxluc  42919  rmyluc  42920  jm2.24  42946  jm2.18  42971  jm2.22  42978  jm2.23  42979  jm2.26lem3  42984  jm2.15nn0  42986  jm2.16nn0  42987  jm2.27a  42988  jm2.27c  42990  jm3.1lem3  43002  hashnzfz  44303  monoords  45289  fzisoeu  45292  dvnmul  45934  stoweidlem11  46002  dirkercncflem1  46094  fourierdlem48  46145  fourierdlem49  46146  fourierdlem65  46162  fourierdlem79  46176  zm1nn  47296  m1modmmod  47352  difmodm1lt  47353  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  48347  pw2m1lepw2m1  48515  zofldiv2  48526  logbpw2m1  48562  nnolog2flm1  48585  dignn0flhalflem1  48610