Theorem peano2zd 12636

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

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7367  1c1 11039   + caddc 11041  ℤcz 12524

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3062  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-riota 7324  df-ov 7370  df-oprab 7371  df-mpo 7372  df-om 7818  df-2nd 7943  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-er 8643  df-en 8894  df-dom 8895  df-sdom 8896  df-pnf 11181  df-mnf 11182  df-xr 11183  df-ltxr 11184  df-le 11185  df-sub 11379  df-neg 11380  df-nn 12175  df-n0 12438  df-z 12525

This theorem is referenced by:  rpnnen1lem5  12931  fznatpl1  13532  elfzom1elp1fzo1  13722  flge  13764  2tnp1ge0ge0  13788  uzsup  13822  seqf1olem1  14003  bcp1nk  14279  bcval5  14280  cshimadifsn0  14792  rexuzre  15315  limsupgre  15443  rlimclim1  15507  iseraltlem2  15645  telfsumo  15765  fsumparts  15769  climcnds  15816  geo2sum  15838  clim2prod  15853  clim2div  15854  fprodntriv  15907  dvdsfac  16295  2tp1odd  16321  opoe  16332  bits0o  16399  bitsp1o  16402  bitsinv1lem  16410  smupvallem  16452  smueqlem  16459  hashdvds  16745  prmreclem4  16890  prmreclem5  16891  vdwnnlem3  16968  prmgaplem7  17028  prmgaplem8  17029  chnub  18588  sylow1lem1  19573  telgsumfzs  19964  srgbinomlem3  20209  chfacfscmul0  22823  chfacfpmmul0  22827  ovoliunlem2  25470  ovolicc2lem4  25487  uniioombllem3  25552  dyaddisjlem  25562  dvfsumlem1  25993  dvfsumlem3  25995  plyco0  26157  abelthlem6  26401  birthdaylem2  26916  wilthlem1  27031  wilth  27034  wilthimp  27035  basellem3  27046  chpp1  27118  perfect  27194  bcmono  27240  lgslem1  27260  lgsval2lem  27270  gausslemma2dlem5  27334  lgseisenlem1  27338  lgsquadlem1  27343  m1lgs  27351  2lgslem1a  27354  2lgslem3c  27361  2lgslem3d  27362  2lgslem3b1  27364  2lgslem3c1  27365  2sqblem  27394  rplogsumlem2  27448  rpvmasumlem  27450  dchrisumlema  27451  dchrisumlem2  27453  pntpbnd1  27549  pntpbnd2  27550  pntlemq  27564  pntlemr  27565  pntlemj  27566  pntlemf  27568  axlowdimlem16  29026  crctcshwlkn0lem3  29880  crctcshwlkn0lem6  29883  clwwlkf  30117  eucrct2eupth  30315  cycpmco2lem3  33189  cycpmco2lem4  33190  cycpmco2lem5  33191  cycpmco2lem6  33192  cycpmco2  33194  isarchi3  33248  archirngz  33250  archiabllem1a  33252  archiabllem2c  33256  submateqlem1  33951  ballotlemsf1o  34658  ballotlemsima  34660  signstfvn  34713  fsum2dsub  34751  breprexplemc  34776  dnizphlfeqhlf  36736  dnibndlem13  36750  knoppndvlem10  36781  knoppndvlem14  36785  knoppndvlem15  36786  knoppndvlem17  36788  ltflcei  37929  poimirlem2  37943  poimirlem10  37951  poimirlem15  37956  poimirlem19  37960  poimirlem23  37964  poimirlem28  37969  fdc  38066  incsequz  38069  cntotbnd  38117  lcmineqlem11  42478  lcmineqlem18  42485  lcmineqlem22  42489  aks4d1p7d1  42521  aks6d1c1  42555  2np3bcnp1  42583  sticksstones6  42590  sticksstones7  42591  sticksstones10  42594  sticksstones12a  42596  sticksstones12  42597  sticksstones22  42607  aks6d1c7lem1  42619  fltnltalem  43095  lzunuz  43200  lzenom  43202  ltrmxnn0  43377  jm2.17a  43388  jm2.17b  43389  jm2.17c  43390  jm2.24  43391  rmygeid  43392  jm2.25  43427  jm2.27a  43433  jm3.1lem1  43445  expdiophlem1  43449  monoords  45730  fmul01lt1lem1  46014  climsuselem1  46037  sumnnodd  46060  supcnvlimsup  46168  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  dvnmul  46371  iblspltprt  46401  itgspltprt  46407  stoweidlem26  46454  wallispilem4  46496  stirlinglem4  46505  stirlinglem8  46509  stirlinglem11  46512  stirlinglem13  46514  dirkertrigeqlem1  46526  dirkercncflem2  46532  fourierdlem11  46546  fourierdlem12  46547  fourierdlem15  46550  fourierdlem41  46576  fourierdlem50  46584  fourierdlem64  46598  fourierdlem65  46599  fourierdlem79  46613  caratheodorylem1  46954  smflimsuplem4  47251  ormkglobd  47305  natglobalincr  47307  iccpartgtprec  47880  iccpartiltu  47882  iccpartgt  47887  iccpartnel  47898  fmtnodvds  48007  fmtnoprmfac2lem1  48029  ppivalnnprm  48088  evenp1odd  48116  oddp1eveni  48117  opoeALTV  48159  evenltle  48193  perfectALTV  48199  gpgiedgdmellem  48522  gpgvtx0  48529  pgnbgreunbgrlem2lem2  48591  fllogbd  49036  nnpw2blen  49056  dignn0flhalflem2  49092  nn0sumshdiglemA  49095  aacllem  50276