Theorem peano2zm 12639

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

Syntax hints:   → wi 4   ∈ wcel 2149  (class class class)co 7413  1c1 11103   − cmin 11443  ℤcz 12593

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5273  ax-pow 5339  ax-pr 5407  ax-un 7735  ax-resscn 11159  ax-1cn 11160  ax-icn 11161  ax-addcl 11162  ax-addrcl 11163  ax-mulcl 11164  ax-mulrcl 11165  ax-mulcom 11166  ax-addass 11167  ax-mulass 11168  ax-distr 11169  ax-i2m1 11170  ax-1ne0 11171  ax-1rid 11172  ax-rnegex 11173  ax-rrecex 11174  ax-cnre 11175  ax-pre-lttri 11176  ax-pre-lttrn 11177  ax-pre-ltadd 11178  ax-pre-mulgt0 11179

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-iun 4962  df-br 5114  df-opab 5178  df-mpt 5197  df-tr 5223  df-id 5559  df-eprel 5564  df-po 5572  df-so 5573  df-fr 5617  df-we 5619  df-xp 5670  df-rel 5671  df-cnv 5672  df-co 5673  df-dm 5674  df-rn 5675  df-res 5676  df-ima 5677  df-pred 6305  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6495  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547  df-riota 7370  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7865  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-er 8696  df-en 8946  df-dom 8947  df-sdom 8948  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11445  df-neg 11446  df-nn 12236  df-n0 12507  df-z 12594

This theorem is referenced by:  zlem1lt  12648  zltlem1  12649  zextlt  12672  zeo  12684  eluzp1m1  12890  uzm1  12898  zbtwnre  12972  fz01en  13582  fzsuc2  13612  elfzm11  13625  uzdisj  13627  preduz  13680  predfz  13683  elfzo  13691  fzon  13711  fzoss2  13718  fzossrbm1  13719  fzosplitsnm1  13771  ubmelm1fzo  13794  elfzom1b  13797  fzosplitprm1  13809  fzoshftral  13818  sermono  14072  seqf1olem1  14079  seqf1olem2  14080  bcm1k  14353  bcn2  14357  bcp1m1  14358  bcpasc  14359  bccl  14360  hashbclem  14491  seqcoll  14503  revccat  14805  revrev  14806  absrdbnd  15395  fsumm1  15804  binomlem  15885  isumsplit  15896  climcndslem1  15905  arisum2  15917  pwdif  15924  pwm1geoser  15925  mertenslem1  15940  fprodser  16005  fprodm1  16023  risefacval2  16066  fallfacval2  16067  fallfacval3  16068  fallfacfwd  16092  binomfallfaclem2  16096  3dvds  16391  oddm1even  16403  oddp1even  16404  mod2eq1n2dvds  16407  zob  16419  nno  16442  pwp1fsum  16451  isprm3  16743  ncoprmlnprm  16789  hashdvds  16836  pockthlem  16967  4sqlem11  17017  vdwapun  17036  vdwnnlem2  17058  chnccat  18684  efgsp1  19809  efgsres  19810  srgbinomlem4  20313  srgbinomlem  20314  znunit  21684  dvexp3  26108  dvfsumlem1  26156  degltlem1  26200  atantayl2  27071  wilthlem1  27200  basellem5  27217  mersenne  27359  perfectlem1  27361  lgslem1  27429  lgsval2lem  27439  lgseisenlem1  27507  lgseisenlem2  27508  lgseisenlem3  27509  lgsquadlem1  27512  lgsquadlem3  27514  lgsquad2lem1  27516  lgsquad3  27519  2sqlem8  27558  2sqblem  27563  dchrisumlem1  27621  logdivbnd  27688  pntrsumbnd2  27699  ostth2lem3  27767  axlowdim  29254  pthdlem1  30058  pthdlem2  30060  wwlksm1edg  30173  clwwlkccatlem  30283  clwlkclwwlklem2fv1  30289  clwlkclwwlklem2a4  30291  clwlkclwwlklem2a  30292  clwlkclwwlklem2  30294  clwlkclwwlk  30296  clwwisshclwwslem  30308  clwwlkf  30341  wwlksubclwwlk  30352  numclwwlk5  30682  numclwwlk7  30685  frgrreggt1  30687  0nn0m1nnn0  35539  erdszelem7  35624  elfzm12  36102  fz0n  36158  fwddifnp1  36592  knoppndvlem2  37027  ltflcei  38184  poimirlem1  38197  poimirlem2  38198  poimirlem6  38202  poimirlem7  38203  poimirlem8  38204  poimirlem9  38205  poimirlem15  38211  poimirlem16  38212  poimirlem17  38213  poimirlem18  38214  poimirlem19  38215  poimirlem20  38216  poimirlem24  38220  poimirlem27  38223  poimirlem31  38227  poimirlem32  38228  mettrifi  38333  rmxluc  43592  rmyluc  43593  jm2.24  43619  jm2.18  43644  jm2.22  43651  jm2.23  43652  jm2.26lem3  43657  jm2.15nn0  43659  jm2.16nn0  43660  jm2.27a  43661  jm2.27c  43663  jm3.1lem3  43675  hashnzfz  44959  monoords  45945  fzisoeu  45948  dvnmul  46586  stoweidlem11  46654  dirkercncflem1  46746  fourierdlem48  46797  fourierdlem49  46798  fourierdlem65  46814  fourierdlem79  46828  chnsubseq  47525  zm1nn  47965  flmrecm1  48006  m1modmmod  48027  difmodm1lt  48028  muldvdsfacgt  48049  iccpartipre  48096  sfprmdvdsmersenne  48281  lighneallem4a  48286  proththd  48292  dfodd6  48328  evenm1odd  48330  oddm1eveni  48333  onego  48337  m1expoddALTV  48339  dfodd4  48350  oddflALTV  48354  oddm1evenALTV  48366  nnoALTV  48386  perfectALTVlem1  48412  altgsumbcALT  49055  pw2m1lepw2m1  49222  zofldiv2  49233  logbpw2m1  49269  nnolog2flm1  49292  dignn0flhalflem1  49317