Theorem peano2zd 12846

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  (class class class)co 7451  1c1 11240   + caddc 11242  ℤcz 12733

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pow 5334  ax-pr 5398  ax-un 7783  ax-resscn 11296  ax-1cn 11297  ax-icn 11298  ax-addcl 11299  ax-addrcl 11300  ax-mulcl 11301  ax-mulrcl 11302  ax-mulcom 11303  ax-addass 11304  ax-mulass 11305  ax-distr 11306  ax-i2m1 11307  ax-1ne0 11308  ax-1rid 11309  ax-rnegex 11310  ax-rrecex 11311  ax-cnre 11312  ax-pre-lttri 11313  ax-pre-lttrn 11314  ax-pre-ltadd 11315  ax-pre-mulgt0 11316

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-iun 4958  df-br 5109  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-pred 6330  df-ord 6391  df-on 6392  df-lim 6393  df-suc 6394  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-riota 7408  df-ov 7454  df-oprab 7455  df-mpo 7456  df-om 7912  df-2nd 8036  df-frecs 8337  df-wrecs 8368  df-recs 8417  df-rdg 8456  df-er 8755  df-en 9012  df-dom 9013  df-sdom 9014  df-pnf 11384  df-mnf 11385  df-xr 11386  df-ltxr 11387  df-le 11388  df-sub 11582  df-neg 11583  df-nn 12376  df-n0 12647  df-z 12734

This theorem is used by:  rpnnen1lem5  13149  fznatpl1  13752  elfzom1elp1fzo1  13942  flge  13985  2tnp1ge0ge0  14009  uzsup  14043  seqf1olem1  14224  bcp1nk  14502  bcval5  14503  cshimadifsn0  15023  rexuzre  15564  limsupgre  15692  rlimclim1  15756  iseraltlem2  15894  telfsumo  16013  fsumparts  16017  climcnds  16064  geo2sum  16086  clim2prod  16101  clim2div  16102  fprodntriv  16153  dvdsfac  16540  2tp1odd  16566  opoe  16577  bits0o  16644  bitsp1o  16647  bitsinv1lem  16655  smupvallem  16697  smueqlem  16704  hashdvds  16996  prmreclem4  17141  prmreclem5  17142  vdwnnlem3  17219  prmgaplem7  17279  prmgaplem8  17280  chnub  18846  sylow1lem1  19863  telgsumfzs  20254  srgbinomlem3  20505  chfacfscmul0  23231  chfacfpmmul0  23235  ovoliunlem2  25879  ovolicc2lem4  25896  uniioombllem3  25961  dyaddisjlem  25971  dvfsumlem1  26401  dvfsumlem3  26403  plyco0  26565  abelthlem6  26820  birthdaylem2  27337  wilthlem1  27452  wilth  27455  wilthimp  27456  basellem3  27467  chpp1  27539  perfect  27615  bcmono  27661  lgslem1  27681  lgsval2lem  27691  gausslemma2dlem5  27755  lgseisenlem1  27759  lgsquadlem1  27764  m1lgs  27772  2lgslem1a  27775  2lgslem3c  27782  2lgslem3d  27783  2lgslem3b1  27785  2lgslem3c1  27786  2sqblem  27815  rplogsumlem2  27869  rpvmasumlem  27871  dchrisumlema  27872  dchrisumlem2  27874  pntpbnd1  27970  pntpbnd2  27971  pntlemq  27985  pntlemr  27986  pntlemj  27987  pntlemf  27989  axlowdimlem16  29592  crctcshwlkn0lem3  30458  crctcshwlkn0lem6  30461  clwwlkf  30695  eucrct2eupth  30903  cycpmco2lem3  33788  cycpmco2lem4  33789  cycpmco2lem5  33790  cycpmco2lem6  33791  cycpmco2  33793  isarchi3  33847  archirngz  33849  archiabllem1a  33851  archiabllem2c  33855  submateqlem1  34550  ballotlemsf1o  35257  ballotlemsima  35259  signstfvn  35309  fsum2dsub  35347  breprexplemc  35372  dnizphlfeqhlf  37557  dnibndlem13  37571  knoppndvlem10  37602  knoppndvlem14  37606  knoppndvlem15  37607  knoppndvlem17  37609  ltflcei  38799  poimirlem2  38808  poimirlem10  38816  poimirlem15  38821  poimirlem19  38825  poimirlem23  38829  poimirlem28  38834  fdc  38945  incsequz  38948  cntotbnd  38996  lcmineqlem11  43355  lcmineqlem18  43362  lcmineqlem22  43366  aks4d1p7d1  43398  aks6d1c1  43432  2np3bcnp1  43460  sticksstones6  43467  sticksstones7  43468  sticksstones10  43471  sticksstones12a  43473  sticksstones12  43474  sticksstones22  43484  aks6d1c7lem1  43496  fltnltalem  43939  lzunuz  44045  lzenom  44047  ltrmxnn0  44222  jm2.17a  44233  jm2.17b  44234  jm2.17c  44235  jm2.24  44236  rmygeid  44237  jm2.25  44272  jm2.27a  44278  jm3.1lem1  44290  expdiophlem1  44294  monoords  46586  fmul01lt1lem1  46869  climsuselem1  46892  sumnnodd  46915  supcnvlimsup  47023  ioodvbdlimc1lem2  47215  ioodvbdlimc2lem  47217  dvnmul  47226  iblspltprt  47256  itgspltprt  47262  stoweidlem26  47309  wallispilem4  47351  stirlinglem4  47360  stirlinglem8  47364  stirlinglem11  47367  stirlinglem13  47369  dirkertrigeqlem1  47381  dirkercncflem2  47387  fourierdlem11  47401  fourierdlem12  47402  fourierdlem15  47405  fourierdlem41  47431  fourierdlem50  47439  fourierdlem64  47453  fourierdlem65  47454  fourierdlem79  47468  caratheodorylem1  47809  smflimsuplem4  48106  ormkglobd  48160  iccpartgtprec  48775  iccpartiltu  48777  iccpartgt  48782  iccpartnel  48793  fmtnodvds  48902  fmtnoprmfac2lem1  48924  ppivalnnprm  48983  evenp1odd  49011  oddp1eveni  49012  opoeALTV  49054  evenltle  49088  perfectALTV  49094  gpgiedgdmellem  49417  gpgvtx0  49424  pgnbgreunbgrlem2lem2  49486  fllogbd  50003  nnpw2blen  50023  dignn0flhalflem2  50059  nn0sumshdiglemA  50062  aacllem  51367