Theorem peano2zd 9497

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 9407	. 2 ⊢ (𝐴 ∈ ℤ → (𝐴 + 1) ∈ ℤ)
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐴 + 1) ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2175  (class class class)co 5943  1c1 7925   + caddc 7927  ℤcz 9371

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-14 2178  ax-ext 2186  ax-sep 4161  ax-pow 4217  ax-pr 4252  ax-setind 4584  ax-cnex 8015  ax-resscn 8016  ax-1cn 8017  ax-1re 8018  ax-icn 8019  ax-addcl 8020  ax-addrcl 8021  ax-mulcl 8022  ax-addcom 8024  ax-addass 8026  ax-distr 8028  ax-i2m1 8029  ax-0id 8032  ax-rnegex 8033  ax-cnre 8035

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1375  df-fal 1378  df-nf 1483  df-sb 1785  df-eu 2056  df-mo 2057  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ne 2376  df-ral 2488  df-rex 2489  df-reu 2490  df-rab 2492  df-v 2773  df-sbc 2998  df-dif 3167  df-un 3169  df-in 3171  df-ss 3178  df-pw 3617  df-sn 3638  df-pr 3639  df-op 3641  df-uni 3850  df-int 3885  df-br 4044  df-opab 4105  df-id 4339  df-xp 4680  df-rel 4681  df-cnv 4682  df-co 4683  df-dm 4684  df-iota 5231  df-fun 5272  df-fv 5278  df-riota 5898  df-ov 5946  df-oprab 5947  df-mpo 5948  df-sub 8244  df-neg 8245  df-inn 9036  df-n0 9295  df-z 9372

This theorem is referenced by:  elfzp1  10193  fznatpl1  10197  fzdifsuc  10202  fseq1p1m1  10215  zsupcllemstep  10370  suprzubdc  10377  flqge  10423  2tnp1ge0ge0  10442  ceiqm1l  10454  addmodlteq  10541  frec2uzzd  10543  frec2uzrdg  10552  uzsinds  10587  seq3f1olemqsumkj  10654  seq3f1olemqsumk  10655  seqf1oglem1  10662  seqf1oglem2  10663  bcp1nk  10905  bcval5  10906  hashfz  10964  resqrexlemdecn  11294  telfsumo  11748  fsumparts  11752  binomlem  11765  geo2sum  11796  cvgratnnlemseq  11808  cvgratnnlemabsle  11809  cvgratnnlemsumlt  11810  cvgratnnlemrate  11812  cvgratz  11814  mertenslemub  11816  mertenslemi1  11817  clim2prod  11821  clim2divap  11822  fprodntrivap  11866  fprodeq0  11899  dvdsfac  12142  2tp1odd  12166  opoe  12177  bits0o  12232  bitsp1o  12235  bitsinv1lem  12243  bitsinv1  12244  prmind2  12413  hashdvds  12514  eulerthlemrprm  12522  pcprendvds  12584  nninfdclemcl  12790  nninfdclemp1  12792  gsumsplit1r  13201  gsumprval  13202  gsumfzfsumlemm  14320  elply2  15178  wilthlem1  15423  perfectlem2  15443  perfect  15444  lgslem1  15448  lgsval  15452  lgsfvalg  15453  lgsval2lem  15458  lgsvalmod  15467  gausslemma2dlem5a  15513  gausslemma2dlem5  15514  gausslemma2dlem6  15515  lgseisenlem1  15518  lgsquadlem1  15525  lgsquadlem2  15526  m1lgs  15533  2lgslem1a  15536  2lgslem1  15539  2lgslem3c  15543  2lgslem3d  15544  2lgslem3b1  15546  2lgslem3c1  15547  cvgcmp2nlemabs  15933