Theorem peano2zm 12643

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

Syntax hints:   → wi 4   ∈ wcel 2098  (class class class)co 7426  1c1 11147   − cmin 11482  ℤcz 12596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-resscn 11203  ax-1cn 11204  ax-icn 11205  ax-addcl 11206  ax-addrcl 11207  ax-mulcl 11208  ax-mulrcl 11209  ax-mulcom 11210  ax-addass 11211  ax-mulass 11212  ax-distr 11213  ax-i2m1 11214  ax-1ne0 11215  ax-1rid 11216  ax-rnegex 11217  ax-rrecex 11218  ax-cnre 11219  ax-pre-lttri 11220  ax-pre-lttrn 11221  ax-pre-ltadd 11222  ax-pre-mulgt0 11223

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6310  df-ord 6377  df-on 6378  df-lim 6379  df-suc 6380  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-riota 7382  df-ov 7429  df-oprab 7430  df-mpo 7431  df-om 7877  df-2nd 8000  df-frecs 8293  df-wrecs 8324  df-recs 8398  df-rdg 8437  df-er 8731  df-en 8971  df-dom 8972  df-sdom 8973  df-pnf 11288  df-mnf 11289  df-xr 11290  df-ltxr 11291  df-le 11292  df-sub 11484  df-neg 11485  df-nn 12251  df-n0 12511  df-z 12597

This theorem is referenced by:  zlem1lt  12652  zltlem1  12653  zextlt  12674  zeo  12686  eluzp1m1  12886  uzm1  12898  zbtwnre  12968  fz01en  13569  fzsuc2  13599  elfzm11  13612  uzdisj  13614  preduz  13663  predfz  13666  elfzo  13674  fzon  13693  fzoss2  13700  fzossrbm1  13701  fzosplitsnm1  13747  ubmelm1fzo  13768  elfzom1b  13771  fzosplitprm1  13782  fzoshftral  13789  sermono  14039  seqf1olem1  14046  seqf1olem2  14047  bcm1k  14314  bcn2  14318  bcp1m1  14319  bcpasc  14320  bccl  14321  hashbclem  14451  seqcoll  14465  revccat  14756  revrev  14757  absrdbnd  15328  fsumm1  15737  binomlem  15815  isumsplit  15826  climcndslem1  15835  arisum2  15847  pwdif  15854  pwm1geoser  15855  mertenslem1  15870  fprodser  15933  fprodm1  15951  risefacval2  15994  fallfacval2  15995  fallfacval3  15996  fallfacfwd  16020  binomfallfaclem2  16024  3dvds  16315  oddm1even  16327  oddp1even  16328  mod2eq1n2dvds  16331  zob  16343  nno  16366  pwp1fsum  16375  isprm3  16661  ncoprmlnprm  16707  hashdvds  16751  pockthlem  16881  4sqlem11  16931  vdwapun  16950  vdwnnlem2  16972  efgsp1  19699  efgsres  19700  srgbinomlem4  20176  srgbinomlem  20177  znunit  21504  dvexp3  25930  dvfsumlem1  25980  degltlem1  26028  atantayl2  26890  wilthlem1  27020  basellem5  27037  mersenne  27180  perfectlem1  27182  lgslem1  27250  lgsval2lem  27260  lgseisenlem1  27328  lgseisenlem2  27329  lgseisenlem3  27330  lgsquadlem1  27333  lgsquadlem3  27335  lgsquad2lem1  27337  lgsquad3  27340  2sqlem8  27379  2sqblem  27384  dchrisumlem1  27442  logdivbnd  27509  pntrsumbnd2  27520  ostth2lem3  27588  axlowdim  28792  pthdlem1  29600  pthdlem2  29602  wwlksm1edg  29712  clwwlkccatlem  29819  clwlkclwwlklem2fv1  29825  clwlkclwwlklem2a4  29827  clwlkclwwlklem2a  29828  clwlkclwwlklem2  29830  clwlkclwwlk  29832  clwwisshclwwslem  29844  clwwlkf  29877  wwlksubclwwlk  29888  numclwwlk5  30218  numclwwlk7  30221  frgrreggt1  30223  0nn0m1nnn0  34755  erdszelem7  34840  elfzm12  35312  fz0n  35358  fwddifnp1  35794  knoppndvlem2  36021  ltflcei  37114  poimirlem1  37127  poimirlem2  37128  poimirlem6  37132  poimirlem7  37133  poimirlem8  37134  poimirlem9  37135  poimirlem15  37141  poimirlem16  37142  poimirlem17  37143  poimirlem18  37144  poimirlem19  37145  poimirlem20  37146  poimirlem24  37150  poimirlem27  37153  poimirlem31  37157  poimirlem32  37158  mettrifi  37263  rmxluc  42388  rmyluc  42389  jm2.24  42415  jm2.18  42440  jm2.22  42447  jm2.23  42448  jm2.26lem3  42453  jm2.15nn0  42455  jm2.16nn0  42456  jm2.27a  42457  jm2.27c  42459  jm3.1lem3  42471  hashnzfz  43788  monoords  44708  fzisoeu  44711  dvnmul  45360  stoweidlem11  45428  dirkercncflem1  45520  fourierdlem48  45571  fourierdlem49  45572  fourierdlem65  45588  fourierdlem79  45602  zm1nn  46711  iccpartipre  46790  sfprmdvdsmersenne  46972  lighneallem4a  46977  proththd  46983  dfodd6  47006  evenm1odd  47008  oddm1eveni  47011  onego  47015  m1expoddALTV  47017  dfodd4  47028  oddflALTV  47032  oddm1evenALTV  47044  nnoALTV  47064  perfectALTVlem1  47090  altgsumbcALT  47495  pw2m1lepw2m1  47666  m1modmmod  47672  difmodm1lt  47673  zofldiv2  47682  logbpw2m1  47718  nnolog2flm1  47741  dignn0flhalflem1  47766