Theorem peano2zm 12559

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

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7358  1c1 11028   − cmin 11366  ℤcz 12513

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5300  ax-pr 5368  ax-un 7680  ax-resscn 11084  ax-1cn 11085  ax-icn 11086  ax-addcl 11087  ax-addrcl 11088  ax-mulcl 11089  ax-mulrcl 11090  ax-mulcom 11091  ax-addass 11092  ax-mulass 11093  ax-distr 11094  ax-i2m1 11095  ax-1ne0 11096  ax-1rid 11097  ax-rnegex 11098  ax-rrecex 11099  ax-cnre 11100  ax-pre-lttri 11101  ax-pre-lttrn 11102  ax-pre-ltadd 11103  ax-pre-mulgt0 11104

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5517  df-eprel 5522  df-po 5530  df-so 5531  df-fr 5575  df-we 5577  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-pred 6257  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-riota 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7809  df-2nd 7934  df-frecs 8222  df-wrecs 8253  df-recs 8302  df-rdg 8340  df-er 8634  df-en 8885  df-dom 8886  df-sdom 8887  df-pnf 11170  df-mnf 11171  df-xr 11172  df-ltxr 11173  df-le 11174  df-sub 11368  df-neg 11369  df-nn 12164  df-n0 12427  df-z 12514

This theorem is referenced by:  zlem1lt  12568  zltlem1  12569  zextlt  12592  zeo  12604  eluzp1m1  12803  uzm1  12811  zbtwnre  12885  fz01en  13495  fzsuc2  13525  elfzm11  13538  uzdisj  13540  preduz  13593  predfz  13596  elfzo  13604  fzon  13624  fzoss2  13631  fzossrbm1  13632  fzosplitsnm1  13684  ubmelm1fzo  13707  elfzom1b  13710  fzosplitprm1  13722  fzoshftral  13731  sermono  13985  seqf1olem1  13992  seqf1olem2  13993  bcm1k  14266  bcn2  14270  bcp1m1  14271  bcpasc  14272  bccl  14273  hashbclem  14403  seqcoll  14415  revccat  14717  revrev  14718  absrdbnd  15293  fsumm1  15702  binomlem  15783  isumsplit  15794  climcndslem1  15803  arisum2  15815  pwdif  15822  pwm1geoser  15823  mertenslem1  15838  fprodser  15903  fprodm1  15921  risefacval2  15964  fallfacval2  15965  fallfacval3  15966  fallfacfwd  15990  binomfallfaclem2  15994  3dvds  16289  oddm1even  16301  oddp1even  16302  mod2eq1n2dvds  16305  zob  16317  nno  16340  pwp1fsum  16349  isprm3  16641  ncoprmlnprm  16687  hashdvds  16734  pockthlem  16865  4sqlem11  16915  vdwapun  16934  vdwnnlem2  16956  chnccat  18581  efgsp1  19701  efgsres  19702  srgbinomlem4  20199  srgbinomlem  20200  znunit  21551  dvexp3  25954  dvfsumlem1  26004  degltlem1  26049  atantayl2  26919  wilthlem1  27049  basellem5  27066  mersenne  27209  perfectlem1  27211  lgslem1  27279  lgsval2lem  27289  lgseisenlem1  27357  lgseisenlem2  27358  lgseisenlem3  27359  lgsquadlem1  27362  lgsquadlem3  27364  lgsquad2lem1  27366  lgsquad3  27369  2sqlem8  27408  2sqblem  27413  dchrisumlem1  27471  logdivbnd  27538  pntrsumbnd2  27549  ostth2lem3  27617  axlowdim  29049  pthdlem1  29854  pthdlem2  29856  wwlksm1edg  29969  clwwlkccatlem  30079  clwlkclwwlklem2fv1  30085  clwlkclwwlklem2a4  30087  clwlkclwwlklem2a  30088  clwlkclwwlklem2  30090  clwlkclwwlk  30092  clwwisshclwwslem  30104  clwwlkf  30137  wwlksubclwwlk  30148  numclwwlk5  30478  numclwwlk7  30481  frgrreggt1  30483  0nn0m1nnn0  35316  erdszelem7  35400  elfzm12  35878  fz0n  35934  fwddifnp1  36368  knoppndvlem2  36786  ltflcei  37940  poimirlem1  37953  poimirlem2  37954  poimirlem6  37958  poimirlem7  37959  poimirlem8  37960  poimirlem9  37961  poimirlem15  37967  poimirlem16  37968  poimirlem17  37969  poimirlem18  37970  poimirlem19  37971  poimirlem20  37972  poimirlem24  37976  poimirlem27  37979  poimirlem31  37983  poimirlem32  37984  mettrifi  38089  rmxluc  43379  rmyluc  43380  jm2.24  43406  jm2.18  43431  jm2.22  43438  jm2.23  43439  jm2.26lem3  43444  jm2.15nn0  43446  jm2.16nn0  43447  jm2.27a  43448  jm2.27c  43450  jm3.1lem3  43462  hashnzfz  44762  monoords  45745  fzisoeu  45748  dvnmul  46386  stoweidlem11  46454  dirkercncflem1  46546  fourierdlem48  46597  fourierdlem49  46598  fourierdlem65  46614  fourierdlem79  46628  chnsubseq  47323  zm1nn  47747  flmrecm1  47788  m1modmmod  47809  difmodm1lt  47810  muldvdsfacgt  47831  iccpartipre  47878  sfprmdvdsmersenne  48063  lighneallem4a  48068  proththd  48074  dfodd6  48110  evenm1odd  48112  oddm1eveni  48115  onego  48119  m1expoddALTV  48121  dfodd4  48132  oddflALTV  48136  oddm1evenALTV  48148  nnoALTV  48168  perfectALTVlem1  48194  altgsumbcALT  48826  pw2m1lepw2m1  48993  zofldiv2  49004  logbpw2m1  49040  nnolog2flm1  49063  dignn0flhalflem1  49088