Theorem peano2zm 9664

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 9631	. . . 4 |- ( N e. ZZ -> N e. CC )
2		1cnd 8335	. . . 4 |- ( N e. ZZ -> 1 e. CC )
3	1, 2	negsubdid 8645	. . 3 |- ( N e. ZZ -> -u ( N - 1 ) = ( -u N + 1 ) )
4		znegcl 9657	. . . 4 |- ( N e. ZZ -> -u N e. ZZ )
5		peano2z 9662	. . . 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 2315	. 2 |- ( N e. ZZ -> -u ( N - 1 ) e. ZZ )
8	1, 2	subcld 8630	. . 3 |- ( N e. ZZ -> ( N - 1 ) e. CC )
9		znegclb 9659	. . 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 2209  (class class class)co 6078   CCcc 8170   1c1 8173   + caddc 8175   - cmin 8490   -ucneg 8491   ZZcz 9626

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 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4247  ax-pow 4309  ax-pr 4344  ax-un 4576  ax-setind 4682  ax-cnex 8263  ax-resscn 8264  ax-1cn 8265  ax-1re 8266  ax-icn 8267  ax-addcl 8268  ax-addrcl 8269  ax-mulcl 8270  ax-addcom 8272  ax-addass 8274  ax-distr 8276  ax-i2m1 8277  ax-0lt1 8278  ax-0id 8280  ax-rnegex 8281  ax-cnre 8283  ax-pre-ltirr 8284  ax-pre-ltwlin 8285  ax-pre-lttrn 8286  ax-pre-ltadd 8288

This theorem depends on definitions:  df-bi 117  df-3or 1010  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-nel 2516  df-ral 2533  df-rex 2534  df-reu 2535  df-rab 2537  df-v 2823  df-sbc 3052  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3714  df-pr 3715  df-op 3717  df-uni 3934  df-int 3969  df-br 4129  df-opab 4191  df-id 4436  df-xp 4778  df-rel 4779  df-cnv 4780  df-co 4781  df-dm 4782  df-iota 5335  df-fun 5377  df-fv 5383  df-riota 6031  df-ov 6081  df-oprab 6082  df-mpo 6083  df-pnf 8355  df-mnf 8356  df-xr 8357  df-ltxr 8358  df-le 8359  df-sub 8492  df-neg 8493  df-inn 9287  df-n0 9546  df-z 9627

This theorem is referenced by:  zaddcllemneg  9665  zlem1lt  9683  zltlem1  9684  zextlt  9720  zeo  9733  eluzp1m1  9928  fzsplit3  10439  fz01en  10440  fzsuc2  10467  elfzm11  10479  uzdisj  10481  fzof  10532  fzoval  10536  elfzo  10537  fzodcel  10541  fzon  10555  fzoss2  10562  fzossrbm1  10563  fzosplitsnm1  10608  ubmelm1fzo  10625  elfzom1b  10628  fzosplitprm1  10634  fzoshftral  10638  fzofig  10850  uzsinds  10862  ser3mono  10905  iseqf1olemqcl  10917  iseqf1olemnab  10919  iseqf1olemab  10920  seq3f1olemqsumkj  10929  seq3f1olemqsum  10931  seqf1oglem1  10937  seqf1oglem2  10938  bcm1k  11179  bcn2  11183  bcp1m1  11184  bcpasc  11185  bccl  11186  hashfibclem  11263  zfz1isolemiso  11272  seq3coll  11275  wrdred1  11328  wrdred1hash  11329  lswwrd  11332  lsw0  11333  resqrexlemcalc3  11763  resqrexlemnm  11765  fsumm1  12164  binomlem  12231  binom1dif  12235  isumsplit  12239  arisum2  12247  pwm1geoserap1  12256  mertenslemi1  12283  fprodm1  12346  fprodeq0  12365  3dvds  12612  zeo3  12616  oddm1even  12623  oddp1even  12624  zob  12639  nno  12654  bitsfzolem  12702  isprm3  12877  prmdc  12889  isprm5  12901  phibnd  12976  hashdvds  12980  odzcllem  13002  odzdvds  13005  fldivp1  13108  pockthlem  13116  4sqlemffi  13156  4sqleminfi  13157  4sqlem11  13161  4sqlem12  13162  ballotfilemfp1  13212  ballotfilemfcc  13214  ballotfilemgun  13249  oddennn  13264  gzsumsplit0  14128  znunit  14969  wilthlem1  16011  mersenne  16028  perfectlem1  16030  lgslem1  16036  lgsval2lem  16046  lgseisenlem1  16106  lgseisenlem2  16107  lgseisenlem3  16108  lgsquadlem1  16113  lgsquadlem3  16115  lgsquad2lem1  16117  lgsquad3  16120  2sqlem8  16159  wlk1walkdom  16517  clwwlkccatlem  16558