Theorem peano2zm 12662

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  (class class class)co 7416  1c1 11126   − cmin 11466  ℤcz 12616

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7739  ax-resscn 11182  ax-1cn 11183  ax-icn 11184  ax-addcl 11185  ax-addrcl 11186  ax-mulcl 11187  ax-mulrcl 11188  ax-mulcom 11189  ax-addass 11190  ax-mulass 11191  ax-distr 11192  ax-i2m1 11193  ax-1ne0 11194  ax-1rid 11195  ax-rnegex 11196  ax-rrecex 11197  ax-cnre 11198  ax-pre-lttri 11199  ax-pre-lttrn 11200  ax-pre-ltadd 11201  ax-pre-mulgt0 11202

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7373  df-ov 7419  df-oprab 7420  df-mpo 7421  df-om 7866  df-2nd 7990  df-frecs 8283  df-wrecs 8314  df-recs 8363  df-rdg 8402  df-er 8699  df-en 8956  df-dom 8957  df-sdom 8958  df-pnf 11270  df-mnf 11271  df-xr 11272  df-ltxr 11273  df-le 11274  df-sub 11468  df-neg 11469  df-nn 12259  df-n0 12530  df-z 12617

This theorem is used by:  zlem1lt  12671  zltlem1  12672  0nn0m1nnn0  12676  zextlt  12696  zeo  12708  eluzp1m1  12914  uzm1  12922  zbtwnre  12996  fz01en  13607  fzsuc2  13637  elfzm11  13650  uzdisj  13652  preduz  13705  predfz  13708  elfzo  13716  fzon  13736  fzoss2  13743  fzossrbm1  13744  fzosplitsnm1  13796  ubmelm1fzo  13819  elfzom1b  13822  fzosplitprm1  13834  fzoshftral  13843  sermono  14098  seqf1olem1  14105  seqf1olem2  14106  bcm1k  14379  bcn2  14383  bcp1m1  14384  bcpasc  14385  bccl  14386  hashbclem  14517  seqcoll  14529  revccat  14835  revrev  14836  absrdbnd  15429  fsumm1  15837  binomlem  15918  isumsplit  15929  climcndslem1  15938  arisum2  15950  pwdif  15957  pwm1geoser  15958  mertenslem1  15973  fprodser  16038  fprodm1  16056  risefacval2  16099  fallfacval2  16100  fallfacval3  16101  fallfacfwd  16124  binomfallfaclem2  16128  3dvds  16423  oddm1even  16435  oddp1even  16436  mod2eq1n2dvds  16439  zob  16451  nno  16474  pwp1fsum  16483  isprm3  16775  ncoprmlnprm  16821  hashdvds  16868  pockthlem  16999  4sqlem11  17049  vdwapun  17068  vdwnnlem2  17090  chnccat  18716  efgsp1  19863  efgsres  19864  srgbinomlem4  20367  srgbinomlem  20368  znunit  21775  dvexp3  26205  dvfsumlem1  26253  degltlem1  26297  atantayl2  27171  wilthlem1  27300  basellem5  27317  mersenne  27459  perfectlem1  27461  lgslem1  27529  lgsval2lem  27539  lgseisenlem1  27607  lgseisenlem2  27608  lgseisenlem3  27609  lgsquadlem1  27612  lgsquadlem3  27614  lgsquad2lem1  27616  lgsquad3  27619  2sqlem8  27658  2sqblem  27663  dchrisumlem1  27721  logdivbnd  27788  pntrsumbnd2  27799  ostth2lem3  27867  axlowdim  29402  pthdlem1  30215  pthdlem2  30217  wwlksm1edg  30333  clwwlkccatlem  30443  clwlkclwwlklem2fv1  30449  clwlkclwwlklem2a4  30451  clwlkclwwlklem2a  30452  clwlkclwwlklem2  30454  clwlkclwwlk  30456  clwwisshclwwslem  30468  clwwlkf  30501  wwlksubclwwlk  30512  numclwwlk5  30852  numclwwlk7  30855  frgrreggt1  30857  erdszelem7  35761  elfzm12  36239  fz0n  36295  fwddifnp1  36730  knoppndvlem2  37195  ltflcei  38347  poimirlem1  38355  poimirlem2  38356  poimirlem6  38360  poimirlem7  38361  poimirlem8  38362  poimirlem9  38363  poimirlem15  38369  poimirlem16  38370  poimirlem17  38371  poimirlem18  38372  poimirlem19  38373  poimirlem20  38374  poimirlem24  38378  poimirlem27  38381  poimirlem31  38385  poimirlem32  38386  mettrifi  38492  rmxluc  43762  rmyluc  43763  jm2.24  43789  jm2.18  43814  jm2.22  43821  jm2.23  43822  jm2.26lem3  43827  jm2.15nn0  43829  jm2.16nn0  43830  jm2.27a  43831  jm2.27c  43833  jm3.1lem3  43845  hashnzfz  45129  monoords  46115  fzisoeu  46118  dvnmul  46756  stoweidlem11  46824  dirkercncflem1  46916  fourierdlem48  46967  fourierdlem49  46968  fourierdlem65  46984  fourierdlem79  46998  chnsubseq  47693  zm1nn  48175  flmrecm1  48216  m1modmmod  48237  difmodm1lt  48238  muldvdsfacgt  48259  iccpartipre  48306  sfprmdvdsmersenne  48491  lighneallem4a  48496  proththd  48502  dfodd6  48538  evenm1odd  48540  oddm1eveni  48543  onego  48547  m1expoddALTV  48549  dfodd4  48560  oddflALTV  48564  oddm1evenALTV  48576  nnoALTV  48596  perfectALTVlem1  48622  altgsumbcALT  49268  pw2m1lepw2m1  49435  zofldiv2  49446  logbpw2m1  49482  nnolog2flm1  49505  dignn0flhalflem1  49530