Theorem peano2zm 9617

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		zcn 9584	. . . 4 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℂ)
2		1cnd 8292	. . . 4 ⊢ (𝑁 ∈ ℤ → 1 ∈ ℂ)
3	1, 2	negsubdid 8601	. . 3 ⊢ (𝑁 ∈ ℤ → -(𝑁 − 1) = (-𝑁 + 1))
4		znegcl 9610	. . . 4 ⊢ (𝑁 ∈ ℤ → -𝑁 ∈ ℤ)
5		peano2z 9615	. . . 4 ⊢ (-𝑁 ∈ ℤ → (-𝑁 + 1) ∈ ℤ)
6	4, 5	syl 14	. . 3 ⊢ (𝑁 ∈ ℤ → (-𝑁 + 1) ∈ ℤ)
7	3, 6	eqeltrd 2311	. 2 ⊢ (𝑁 ∈ ℤ → -(𝑁 − 1) ∈ ℤ)
8	1, 2	subcld 8586	. . 3 ⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℂ)
9		znegclb 9612	. . 3 ⊢ ((𝑁 − 1) ∈ ℂ → ((𝑁 − 1) ∈ ℤ ↔ -(𝑁 − 1) ∈ ℤ))
10	8, 9	syl 14	. 2 ⊢ (𝑁 ∈ ℤ → ((𝑁 − 1) ∈ ℤ ↔ -(𝑁 − 1) ∈ ℤ))
11	7, 10	mpbird 167	1 ⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)

Syntax hints:   → wi 4   ↔ wb 105   ∈ wcel 2205  (class class class)co 6052  ℂcc 8127  1c1 8130   + caddc 8132   − cmin 8446  -cneg 8447  ℤcz 9579

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 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2207  ax-14 2208  ax-ext 2216  ax-sep 4230  ax-pow 4289  ax-pr 4324  ax-un 4556  ax-setind 4661  ax-cnex 8220  ax-resscn 8221  ax-1cn 8222  ax-1re 8223  ax-icn 8224  ax-addcl 8225  ax-addrcl 8226  ax-mulcl 8227  ax-addcom 8229  ax-addass 8231  ax-distr 8233  ax-i2m1 8234  ax-0lt1 8235  ax-0id 8237  ax-rnegex 8238  ax-cnre 8240  ax-pre-ltirr 8241  ax-pre-ltwlin 8242  ax-pre-lttrn 8243  ax-pre-ltadd 8245

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1812  df-eu 2085  df-mo 2086  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ne 2415  df-nel 2510  df-ral 2527  df-rex 2528  df-reu 2529  df-rab 2531  df-v 2817  df-sbc 3045  df-dif 3215  df-un 3217  df-in 3219  df-ss 3226  df-pw 3673  df-sn 3697  df-pr 3698  df-op 3700  df-uni 3917  df-int 3952  df-br 4112  df-opab 4174  df-id 4416  df-xp 4757  df-rel 4758  df-cnv 4759  df-co 4760  df-dm 4761  df-iota 5314  df-fun 5356  df-fv 5362  df-riota 6005  df-ov 6055  df-oprab 6056  df-mpo 6057  df-pnf 8312  df-mnf 8313  df-xr 8314  df-ltxr 8315  df-le 8316  df-sub 8448  df-neg 8449  df-inn 9240  df-n0 9499  df-z 9580

This theorem is referenced by:  zaddcllemneg  9618  zlem1lt  9636  zltlem1  9637  zextlt  9673  zeo  9686  eluzp1m1  9881  fz01en  10390  fzsuc2  10417  elfzm11  10429  uzdisj  10431  fzof  10482  fzoval  10486  elfzo  10487  fzodcel  10491  fzon  10505  fzoss2  10512  fzossrbm1  10513  fzosplitsnm1  10558  ubmelm1fzo  10575  elfzom1b  10578  fzosplitprm1  10584  fzoshftral  10588  fzofig  10798  uzsinds  10810  ser3mono  10853  iseqf1olemqcl  10865  iseqf1olemnab  10867  iseqf1olemab  10868  seq3f1olemqsumkj  10877  seq3f1olemqsum  10879  seqf1oglem1  10885  seqf1oglem2  10886  bcm1k  11126  bcn2  11130  bcp1m1  11131  bcpasc  11132  bccl  11133  hashfibclem  11210  zfz1isolemiso  11215  seq3coll  11218  wrdred1  11271  wrdred1hash  11272  lswwrd  11275  lsw0  11276  resqrexlemcalc3  11705  resqrexlemnm  11707  fsumm1  12106  binomlem  12173  binom1dif  12177  isumsplit  12181  arisum2  12189  pwm1geoserap1  12198  mertenslemi1  12225  fprodm1  12288  fprodeq0  12307  3dvds  12554  zeo3  12558  oddm1even  12565  oddp1even  12566  zob  12581  nno  12596  bitsfzolem  12644  isprm3  12819  prmdc  12831  isprm5  12843  phibnd  12918  hashdvds  12922  odzcllem  12944  odzdvds  12947  fldivp1  13050  pockthlem  13058  4sqlemffi  13098  4sqleminfi  13099  4sqlem11  13103  4sqlem12  13104  ballotfilemfp1  13152  ballotfilemfcc  13154  oddennn  13160  gsumsplit0  14080  znunit  14824  wilthlem1  15865  mersenne  15882  perfectlem1  15884  lgslem1  15890  lgsval2lem  15900  lgseisenlem1  15960  lgseisenlem2  15961  lgseisenlem3  15962  lgsquadlem1  15967  lgsquadlem3  15969  lgsquad2lem1  15971  lgsquad3  15974  2sqlem8  16013  wlk1walkdom  16371  clwwlkccatlem  16412