Theorem peano2zm 9309

Description: "Reverse" second Peano postulate for integers. (Contributed by NM, 12-Sep-2005.)

Assertion

Ref	Expression
peano2zm	|- ( N e. ZZ -> ( N - 1 ) e. ZZ )

Proof of Theorem peano2zm

Step	Hyp	Ref	Expression
1		zcn 9276	. . . 4 |- ( N e. ZZ -> N e. CC )
2		1cnd 7991	. . . 4 |- ( N e. ZZ -> 1 e. CC )
3	1, 2	negsubdid 8301	. . 3 |- ( N e. ZZ -> -u ( N - 1 ) = ( -u N + 1 ) )
4		znegcl 9302	. . . 4 |- ( N e. ZZ -> -u N e. ZZ )
5		peano2z 9307	. . . 4 |- ( -u N e. ZZ -> ( -u N + 1 ) e. ZZ )
6	4, 5	syl 14	. . 3 |- ( N e. ZZ -> ( -u N + 1 ) e. ZZ )
7	3, 6	eqeltrd 2266	. 2 |- ( N e. ZZ -> -u ( N - 1 ) e. ZZ )
8	1, 2	subcld 8286	. . 3 |- ( N e. ZZ -> ( N - 1 ) e. CC )
9		znegclb 9304	. . 3 |- ( ( N - 1 ) e. CC -> ( ( N - 1 ) e. ZZ <-> -u ( N - 1 ) e. ZZ ) )
10	8, 9	syl 14	. 2 |- ( N e. ZZ -> ( ( N - 1 ) e. ZZ <-> -u ( N - 1 ) e. ZZ ) )
11	7, 10	mpbird 167	1 |- ( N e. ZZ -> ( N - 1 ) e. ZZ )

Syntax hints:   -> wi 4   <-> wb 105   e. wcel 2160  (class class class)co 5891   CCcc 7827   1c1 7830   + caddc 7832   - cmin 8146   -ucneg 8147   ZZcz 9271

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-sep 4136  ax-pow 4189  ax-pr 4224  ax-un 4448  ax-setind 4551  ax-cnex 7920  ax-resscn 7921  ax-1cn 7922  ax-1re 7923  ax-icn 7924  ax-addcl 7925  ax-addrcl 7926  ax-mulcl 7927  ax-addcom 7929  ax-addass 7931  ax-distr 7933  ax-i2m1 7934  ax-0lt1 7935  ax-0id 7937  ax-rnegex 7938  ax-cnre 7940  ax-pre-ltirr 7941  ax-pre-ltwlin 7942  ax-pre-lttrn 7943  ax-pre-ltadd 7945

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ne 2361  df-nel 2456  df-ral 2473  df-rex 2474  df-reu 2475  df-rab 2477  df-v 2754  df-sbc 2978  df-dif 3146  df-un 3148  df-in 3150  df-ss 3157  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-int 3860  df-br 4019  df-opab 4080  df-id 4308  df-xp 4647  df-rel 4648  df-cnv 4649  df-co 4650  df-dm 4651  df-iota 5193  df-fun 5233  df-fv 5239  df-riota 5847  df-ov 5894  df-oprab 5895  df-mpo 5896  df-pnf 8012  df-mnf 8013  df-xr 8014  df-ltxr 8015  df-le 8016  df-sub 8148  df-neg 8149  df-inn 8938  df-n0 9195  df-z 9272

This theorem is referenced by:  zaddcllemneg  9310  zlem1lt  9327  zltlem1  9328  zextlt  9363  zeo  9376  eluzp1m1  9569  fz01en  10071  fzsuc2  10097  elfzm11  10109  uzdisj  10111  fzof  10162  fzoval  10166  elfzo  10167  fzodcel  10170  fzon  10184  fzoss2  10190  fzossrbm1  10191  fzosplitsnm1  10227  ubmelm1fzo  10244  elfzom1b  10247  fzosplitprm1  10252  fzoshftral  10256  fzofig  10450  uzsinds  10460  ser3mono  10496  iseqf1olemqcl  10504  iseqf1olemnab  10506  iseqf1olemab  10507  seq3f1olemqsumkj  10516  seq3f1olemqsum  10518  bcm1k  10758  bcn2  10762  bcp1m1  10763  bcpasc  10764  bccl  10765  zfz1isolemiso  10837  seq3coll  10840  resqrexlemcalc3  11043  resqrexlemnm  11045  fsumm1  11442  binomlem  11509  binom1dif  11513  isumsplit  11517  arisum2  11525  pwm1geoserap1  11534  mertenslemi1  11561  fprodm1  11624  fprodeq0  11643  zeo3  11891  oddm1even  11898  oddp1even  11899  zob  11914  nno  11929  isprm3  12136  prmdc  12148  isprm5  12160  phibnd  12235  hashdvds  12239  odzcllem  12260  odzdvds  12263  fldivp1  12364  pockthlem  12372  oddennn  12411  lgslem1  14798  lgsval2lem  14808  lgseisenlem1  14847  lgseisenlem2  14848  2sqlem8  14867