Theorem peano2zd 9721

Description: Deduction from second Peano postulate generalized to integers. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
zred.1	|- ( ph -> A e. ZZ )

Assertion

Ref	Expression
peano2zd	|- ( ph -> ( A + 1 ) e. ZZ )

Proof of Theorem peano2zd

Step	Hyp	Ref	Expression
1		zred.1	. 2 |- ( ph -> A e. ZZ )
2		peano2z 9630	. 2 |- ( A e. ZZ -> ( A + 1 ) e. ZZ )
3	1, 2	syl 14	1 |- ( ph -> ( A + 1 ) e. ZZ )

Syntax hints:   -> wi 4   e. wcel 2205  (class class class)co 6058   1c1 8144   + caddc 8146   ZZcz 9594

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-14 2208  ax-ext 2216  ax-sep 4233  ax-pow 4292  ax-pr 4327  ax-setind 4664  ax-cnex 8234  ax-resscn 8235  ax-1cn 8236  ax-1re 8237  ax-icn 8238  ax-addcl 8239  ax-addrcl 8240  ax-mulcl 8241  ax-addcom 8243  ax-addass 8245  ax-distr 8247  ax-i2m1 8248  ax-0id 8251  ax-rnegex 8252  ax-cnre 8254

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-ral 2527  df-rex 2528  df-reu 2529  df-rab 2531  df-v 2817  df-sbc 3046  df-dif 3216  df-un 3218  df-in 3220  df-ss 3227  df-pw 3676  df-sn 3700  df-pr 3701  df-op 3703  df-uni 3920  df-int 3955  df-br 4115  df-opab 4177  df-id 4419  df-xp 4760  df-rel 4761  df-cnv 4762  df-co 4763  df-dm 4764  df-iota 5317  df-fun 5359  df-fv 5365  df-riota 6011  df-ov 6061  df-oprab 6062  df-mpo 6063  df-sub 8462  df-neg 8463  df-inn 9255  df-n0 9514  df-z 9595

This theorem is referenced by:  elfzp1  10428  fznatpl1  10432  fzdifsuc  10437  fseq1p1m1  10450  zsupcllemstep  10611  suprzubdc  10620  flqge  10666  2tnp1ge0ge0  10685  ceiqm1l  10697  addmodlteq  10784  frec2uzzd  10786  frec2uzrdg  10795  uzsinds  10830  seq3f1olemqsumkj  10897  seq3f1olemqsumk  10898  seqf1oglem1  10905  seqf1oglem2  10906  bcp1nk  11149  bcval5  11150  hashfz  11211  swrds1  11385  resqrexlemdecn  11722  telfsumo  12177  fsumparts  12181  binomlem  12194  geo2sum  12225  cvgratnnlemseq  12237  cvgratnnlemabsle  12238  cvgratnnlemsumlt  12239  cvgratnnlemrate  12241  cvgratz  12243  mertenslemub  12245  mertenslemi1  12246  clim2prod  12250  clim2divap  12251  fprodntrivap  12295  fprodeq0  12328  dvdsfac  12571  2tp1odd  12595  opoe  12606  bits0o  12661  bitsp1o  12664  bitsinv1lem  12672  bitsinv1  12673  prmind2  12842  hashdvds  12943  eulerthlemrprm  12951  pcprendvds  13013  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemsv  13197  ballotfilemsf1o  13201  ballotfilemsima  13203  nninfdclemcl  13283  nninfdclemp1  13285  gsumsplit1r  13661  gsumprval  13662  gsumfzfsumlemm  14861  elply2  15726  wilthlem1  15974  perfectlem2  15994  perfect  15995  lgslem1  15999  lgsval  16003  lgsfvalg  16004  lgsval2lem  16009  lgsvalmod  16018  gausslemma2dlem5a  16064  gausslemma2dlem5  16065  gausslemma2dlem6  16066  lgseisenlem1  16069  lgsquadlem1  16076  lgsquadlem2  16077  m1lgs  16084  2lgslem1a  16087  2lgslem1  16090  2lgslem3c  16094  2lgslem3d  16095  2lgslem3b1  16097  2lgslem3c1  16098  wlk1walkdom  16480  cvgcmp2nlemabs  16942