Theorem peano2zm 12532

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

Syntax hints:   → wi 4   ∈ wcel 2113  (class class class)co 7356  1c1 11025   − cmin 11362  ℤcz 12486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pow 5308  ax-pr 5375  ax-un 7678  ax-resscn 11081  ax-1cn 11082  ax-icn 11083  ax-addcl 11084  ax-addrcl 11085  ax-mulcl 11086  ax-mulrcl 11087  ax-mulcom 11088  ax-addass 11089  ax-mulass 11090  ax-distr 11091  ax-i2m1 11092  ax-1ne0 11093  ax-1rid 11094  ax-rnegex 11095  ax-rrecex 11096  ax-cnre 11097  ax-pre-lttri 11098  ax-pre-lttrn 11099  ax-pre-ltadd 11100  ax-pre-mulgt0 11101

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3059  df-reu 3349  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-iun 4946  df-br 5097  df-opab 5159  df-mpt 5178  df-tr 5204  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 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-er 8633  df-en 8882  df-dom 8883  df-sdom 8884  df-pnf 11166  df-mnf 11167  df-xr 11168  df-ltxr 11169  df-le 11170  df-sub 11364  df-neg 11365  df-nn 12144  df-n0 12400  df-z 12487

This theorem is referenced by:  zlem1lt  12541  zltlem1  12542  zextlt  12564  zeo  12576  eluzp1m1  12775  uzm1  12783  zbtwnre  12857  fz01en  13466  fzsuc2  13496  elfzm11  13509  uzdisj  13511  preduz  13564  predfz  13567  elfzo  13575  fzon  13594  fzoss2  13601  fzossrbm1  13602  fzosplitsnm1  13654  ubmelm1fzo  13677  elfzom1b  13680  fzosplitprm1  13692  fzoshftral  13701  sermono  13955  seqf1olem1  13962  seqf1olem2  13963  bcm1k  14236  bcn2  14240  bcp1m1  14241  bcpasc  14242  bccl  14243  hashbclem  14373  seqcoll  14385  revccat  14687  revrev  14688  absrdbnd  15263  fsumm1  15672  binomlem  15750  isumsplit  15761  climcndslem1  15770  arisum2  15782  pwdif  15789  pwm1geoser  15790  mertenslem1  15805  fprodser  15870  fprodm1  15888  risefacval2  15931  fallfacval2  15932  fallfacval3  15933  fallfacfwd  15957  binomfallfaclem2  15961  3dvds  16256  oddm1even  16268  oddp1even  16269  mod2eq1n2dvds  16272  zob  16284  nno  16307  pwp1fsum  16316  isprm3  16608  ncoprmlnprm  16653  hashdvds  16700  pockthlem  16831  4sqlem11  16881  vdwapun  16900  vdwnnlem2  16922  chnccat  18547  efgsp1  19664  efgsres  19665  srgbinomlem4  20162  srgbinomlem  20163  znunit  21516  dvexp3  25936  dvfsumlem1  25986  degltlem1  26031  atantayl2  26902  wilthlem1  27032  basellem5  27049  mersenne  27192  perfectlem1  27194  lgslem1  27262  lgsval2lem  27272  lgseisenlem1  27340  lgseisenlem2  27341  lgseisenlem3  27342  lgsquadlem1  27345  lgsquadlem3  27347  lgsquad2lem1  27349  lgsquad3  27352  2sqlem8  27391  2sqblem  27396  dchrisumlem1  27454  logdivbnd  27521  pntrsumbnd2  27532  ostth2lem3  27600  axlowdim  28983  pthdlem1  29788  pthdlem2  29790  wwlksm1edg  29903  clwwlkccatlem  30013  clwlkclwwlklem2fv1  30019  clwlkclwwlklem2a4  30021  clwlkclwwlklem2a  30022  clwlkclwwlklem2  30024  clwlkclwwlk  30026  clwwisshclwwslem  30038  clwwlkf  30071  wwlksubclwwlk  30082  numclwwlk5  30412  numclwwlk7  30415  frgrreggt1  30417  0nn0m1nnn0  35256  erdszelem7  35340  elfzm12  35818  fz0n  35874  fwddifnp1  36308  knoppndvlem2  36656  ltflcei  37748  poimirlem1  37761  poimirlem2  37762  poimirlem6  37766  poimirlem7  37767  poimirlem8  37768  poimirlem9  37769  poimirlem15  37775  poimirlem16  37776  poimirlem17  37777  poimirlem18  37778  poimirlem19  37779  poimirlem20  37780  poimirlem24  37784  poimirlem27  37787  poimirlem31  37791  poimirlem32  37792  mettrifi  37897  rmxluc  43120  rmyluc  43121  jm2.24  43147  jm2.18  43172  jm2.22  43179  jm2.23  43180  jm2.26lem3  43185  jm2.15nn0  43187  jm2.16nn0  43188  jm2.27a  43189  jm2.27c  43191  jm3.1lem3  43203  hashnzfz  44503  monoords  45487  fzisoeu  45490  dvnmul  46129  stoweidlem11  46197  dirkercncflem1  46289  fourierdlem48  46340  fourierdlem49  46341  fourierdlem65  46357  fourierdlem79  46371  chnsubseq  47066  zm1nn  47490  m1modmmod  47546  difmodm1lt  47547  iccpartipre  47609  sfprmdvdsmersenne  47791  lighneallem4a  47796  proththd  47802  dfodd6  47825  evenm1odd  47827  oddm1eveni  47830  onego  47834  m1expoddALTV  47836  dfodd4  47847  oddflALTV  47851  oddm1evenALTV  47863  nnoALTV  47883  perfectALTVlem1  47909  altgsumbcALT  48541  pw2m1lepw2m1  48708  zofldiv2  48719  logbpw2m1  48755  nnolog2flm1  48778  dignn0flhalflem1  48803