Theorem peano2zd 12705

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7410  1c1 11135   + caddc 11137  ℤcz 12593

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734  ax-resscn 11191  ax-1cn 11192  ax-icn 11193  ax-addcl 11194  ax-addrcl 11195  ax-mulcl 11196  ax-mulrcl 11197  ax-mulcom 11198  ax-addass 11199  ax-mulass 11200  ax-distr 11201  ax-i2m1 11202  ax-1ne0 11203  ax-1rid 11204  ax-rnegex 11205  ax-rrecex 11206  ax-cnre 11207  ax-pre-lttri 11208  ax-pre-lttrn 11209  ax-pre-ltadd 11210  ax-pre-mulgt0 11211

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-iun 4974  df-br 5125  df-opab 5187  df-mpt 5207  df-tr 5235  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6295  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-om 7867  df-2nd 7994  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-rdg 8429  df-er 8724  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11276  df-mnf 11277  df-xr 11278  df-ltxr 11279  df-le 11280  df-sub 11473  df-neg 11474  df-nn 12246  df-n0 12507  df-z 12594

This theorem is referenced by:  rpnnen1lem5  13002  fznatpl1  13600  elfzom1elp1fzo1  13788  flge  13827  2tnp1ge0ge0  13851  uzsup  13885  seqf1olem1  14064  bcp1nk  14340  bcval5  14341  cshimadifsn0  14854  rexuzre  15376  limsupgre  15502  rlimclim1  15566  iseraltlem2  15704  telfsumo  15823  fsumparts  15827  climcnds  15872  geo2sum  15894  clim2prod  15909  clim2div  15910  fprodntriv  15963  dvdsfac  16350  2tp1odd  16376  opoe  16387  bits0o  16454  bitsp1o  16457  bitsinv1lem  16465  smupvallem  16507  smueqlem  16514  hashdvds  16799  prmreclem4  16944  prmreclem5  16945  vdwnnlem3  17022  prmgaplem7  17082  prmgaplem8  17083  sylow1lem1  19584  telgsumfzs  19975  srgbinomlem3  20193  chfacfscmul0  22801  chfacfpmmul0  22805  ovoliunlem2  25461  ovolicc2lem4  25478  uniioombllem3  25543  dyaddisjlem  25553  dvfsumlem1  25989  dvfsumlem3  25992  plyco0  26154  abelthlem6  26403  birthdaylem2  26919  wilthlem1  27035  wilth  27038  wilthimp  27039  basellem3  27050  chpp1  27122  perfect  27199  bcmono  27245  lgslem1  27265  lgsval2lem  27275  gausslemma2dlem5  27339  lgseisenlem1  27343  lgsquadlem1  27348  m1lgs  27356  2lgslem1a  27359  2lgslem3c  27366  2lgslem3d  27367  2lgslem3b1  27369  2lgslem3c1  27370  2sqblem  27399  rplogsumlem2  27453  rpvmasumlem  27455  dchrisumlema  27456  dchrisumlem2  27458  pntpbnd1  27554  pntpbnd2  27555  pntlemq  27569  pntlemr  27570  pntlemj  27571  pntlemf  27573  axlowdimlem16  28941  crctcshwlkn0lem3  29799  crctcshwlkn0lem6  29802  clwwlkf  30033  eucrct2eupth  30231  chnub  32997  cycpmco2lem3  33144  cycpmco2lem4  33145  cycpmco2lem5  33146  cycpmco2lem6  33147  cycpmco2  33149  isarchi3  33190  archirngz  33192  archiabllem1a  33194  archiabllem2c  33198  submateqlem1  33843  ballotlemsf1o  34551  ballotlemsima  34553  signstfvn  34606  fsum2dsub  34644  breprexplemc  34669  dnizphlfeqhlf  36499  dnibndlem13  36513  knoppndvlem10  36544  knoppndvlem14  36548  knoppndvlem15  36549  knoppndvlem17  36551  ltflcei  37637  poimirlem2  37651  poimirlem10  37659  poimirlem15  37664  poimirlem19  37668  poimirlem23  37672  poimirlem28  37677  fdc  37774  incsequz  37777  cntotbnd  37825  lcmineqlem11  42057  lcmineqlem18  42064  lcmineqlem22  42068  aks4d1p7d1  42100  aks6d1c1  42134  2np3bcnp1  42162  sticksstones6  42169  sticksstones7  42170  sticksstones10  42173  sticksstones12a  42175  sticksstones12  42176  sticksstones22  42186  aks6d1c7lem1  42198  fltnltalem  42660  lzunuz  42766  lzenom  42768  ltrmxnn0  42948  jm2.17a  42959  jm2.17b  42960  jm2.17c  42961  jm2.24  42962  rmygeid  42963  jm2.25  42998  jm2.27a  43004  jm3.1lem1  43016  expdiophlem1  43020  monoords  45306  fmul01lt1lem1  45593  climsuselem1  45616  sumnnodd  45639  supcnvlimsup  45749  ioodvbdlimc1lem2  45941  ioodvbdlimc2lem  45943  dvnmul  45952  iblspltprt  45982  itgspltprt  45988  stoweidlem26  46035  wallispilem4  46077  stirlinglem4  46086  stirlinglem8  46090  stirlinglem11  46093  stirlinglem13  46095  dirkertrigeqlem1  46107  dirkercncflem2  46113  fourierdlem11  46127  fourierdlem12  46128  fourierdlem15  46131  fourierdlem41  46157  fourierdlem50  46165  fourierdlem64  46179  fourierdlem65  46180  fourierdlem79  46194  caratheodorylem1  46535  smflimsuplem4  46832  ormkglobd  46884  natglobalincr  46886  iccpartgtprec  47414  iccpartiltu  47416  iccpartgt  47421  iccpartnel  47432  fmtnodvds  47538  fmtnoprmfac2lem1  47560  evenp1odd  47634  oddp1eveni  47635  opoeALTV  47677  evenltle  47711  perfectALTV  47717  gpgiedgdmellem  48030  gpgvtx0  48037  fllogbd  48520  nnpw2blen  48540  dignn0flhalflem2  48576  nn0sumshdiglemA  48579  aacllem  49645