Theorem peano2zd 9605

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

Hypothesis

Ref	Expression
zred.1	⊢ (𝜑 → 𝐴 ∈ ℤ)

Assertion

Ref	Expression
peano2zd	⊢ (𝜑 → (𝐴 + 1) ∈ ℤ)

Proof of Theorem peano2zd

Step	Hyp	Ref	Expression
1		zred.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℤ)
2		peano2z 9515	. 2 ⊢ (𝐴 ∈ ℤ → (𝐴 + 1) ∈ ℤ)
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐴 + 1) ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2202  (class class class)co 6018  1c1 8033   + caddc 8035  ℤcz 9479

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299  ax-setind 4635  ax-cnex 8123  ax-resscn 8124  ax-1cn 8125  ax-1re 8126  ax-icn 8127  ax-addcl 8128  ax-addrcl 8129  ax-mulcl 8130  ax-addcom 8132  ax-addass 8134  ax-distr 8136  ax-i2m1 8137  ax-0id 8140  ax-rnegex 8141  ax-cnre 8143

This theorem depends on definitions:  df-bi 117  df-3or 1005  df-3an 1006  df-tru 1400  df-fal 1403  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ne 2403  df-ral 2515  df-rex 2516  df-reu 2517  df-rab 2519  df-v 2804  df-sbc 3032  df-dif 3202  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-int 3929  df-br 4089  df-opab 4151  df-id 4390  df-xp 4731  df-rel 4732  df-cnv 4733  df-co 4734  df-dm 4735  df-iota 5286  df-fun 5328  df-fv 5334  df-riota 5971  df-ov 6021  df-oprab 6022  df-mpo 6023  df-sub 8352  df-neg 8353  df-inn 9144  df-n0 9403  df-z 9480

This theorem is referenced by:  elfzp1  10307  fznatpl1  10311  fzdifsuc  10316  fseq1p1m1  10329  zsupcllemstep  10490  suprzubdc  10497  flqge  10543  2tnp1ge0ge0  10562  ceiqm1l  10574  addmodlteq  10661  frec2uzzd  10663  frec2uzrdg  10672  uzsinds  10707  seq3f1olemqsumkj  10774  seq3f1olemqsumk  10775  seqf1oglem1  10782  seqf1oglem2  10783  bcp1nk  11025  bcval5  11026  hashfz  11086  swrds1  11253  resqrexlemdecn  11590  telfsumo  12045  fsumparts  12049  binomlem  12062  geo2sum  12093  cvgratnnlemseq  12105  cvgratnnlemabsle  12106  cvgratnnlemsumlt  12107  cvgratnnlemrate  12109  cvgratz  12111  mertenslemub  12113  mertenslemi1  12114  clim2prod  12118  clim2divap  12119  fprodntrivap  12163  fprodeq0  12196  dvdsfac  12439  2tp1odd  12463  opoe  12474  bits0o  12529  bitsp1o  12532  bitsinv1lem  12540  bitsinv1  12541  prmind2  12710  hashdvds  12811  eulerthlemrprm  12819  pcprendvds  12881  nninfdclemcl  13087  nninfdclemp1  13089  gsumsplit1r  13499  gsumprval  13500  gsumfzfsumlemm  14620  elply2  15478  wilthlem1  15723  perfectlem2  15743  perfect  15744  lgslem1  15748  lgsval  15752  lgsfvalg  15753  lgsval2lem  15758  lgsvalmod  15767  gausslemma2dlem5a  15813  gausslemma2dlem5  15814  gausslemma2dlem6  15815  lgseisenlem1  15818  lgsquadlem1  15825  lgsquadlem2  15826  m1lgs  15833  2lgslem1a  15836  2lgslem1  15839  2lgslem3c  15843  2lgslem3d  15844  2lgslem3b1  15846  2lgslem3c1  15847  wlk1walkdom  16229  cvgcmp2nlemabs  16687