Theorem peano2zd 12750

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

Syntax hints:   → wi 4   ∈ wcel 2108  (class class class)co 7448  1c1 11185   + caddc 11187  ℤcz 12639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260  ax-pre-mulgt0 11261

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-om 7904  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-er 8763  df-en 9004  df-dom 9005  df-sdom 9006  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11522  df-neg 11523  df-nn 12294  df-n0 12554  df-z 12640

This theorem is referenced by:  rpnnen1lem5  13046  fznatpl1  13638  elfzom1elp1fzo1  13817  flge  13856  2tnp1ge0ge0  13880  uzsup  13914  seqf1olem1  14092  bcp1nk  14366  bcval5  14367  cshimadifsn0  14879  rexuzre  15401  limsupgre  15527  rlimclim1  15591  iseraltlem2  15731  telfsumo  15850  fsumparts  15854  climcnds  15899  geo2sum  15921  clim2prod  15936  clim2div  15937  fprodntriv  15990  dvdsfac  16374  2tp1odd  16400  opoe  16411  bits0o  16476  bitsp1o  16479  bitsinv1lem  16487  smupvallem  16529  smueqlem  16536  hashdvds  16822  prmreclem4  16966  prmreclem5  16967  vdwnnlem3  17044  prmgaplem7  17104  prmgaplem8  17105  sylow1lem1  19640  telgsumfzs  20031  srgbinomlem3  20255  chfacfscmul0  22885  chfacfpmmul0  22889  ovoliunlem2  25557  ovolicc2lem4  25574  uniioombllem3  25639  dyaddisjlem  25649  dvfsumlem1  26086  dvfsumlem3  26089  plyco0  26251  abelthlem6  26498  birthdaylem2  27013  wilthlem1  27129  wilth  27132  wilthimp  27133  basellem3  27144  chpp1  27216  perfect  27293  bcmono  27339  lgslem1  27359  lgsval2lem  27369  gausslemma2dlem5  27433  lgseisenlem1  27437  lgsquadlem1  27442  m1lgs  27450  2lgslem1a  27453  2lgslem3c  27460  2lgslem3d  27461  2lgslem3b1  27463  2lgslem3c1  27464  2sqblem  27493  rplogsumlem2  27547  rpvmasumlem  27549  dchrisumlema  27550  dchrisumlem2  27552  pntpbnd1  27648  pntpbnd2  27649  pntlemq  27663  pntlemr  27664  pntlemj  27665  pntlemf  27667  axlowdimlem16  28990  crctcshwlkn0lem3  29845  crctcshwlkn0lem6  29848  clwwlkf  30079  eucrct2eupth  30277  chnub  32984  cycpmco2lem3  33121  cycpmco2lem4  33122  cycpmco2lem5  33123  cycpmco2lem6  33124  cycpmco2  33126  isarchi3  33167  archirngz  33169  archiabllem1a  33171  archiabllem2c  33175  submateqlem1  33753  ballotlemsf1o  34478  ballotlemsima  34480  signstfvn  34546  fsum2dsub  34584  breprexplemc  34609  dnizphlfeqhlf  36442  dnibndlem13  36456  knoppndvlem10  36487  knoppndvlem14  36491  knoppndvlem15  36492  knoppndvlem17  36494  ltflcei  37568  poimirlem2  37582  poimirlem10  37590  poimirlem15  37595  poimirlem19  37599  poimirlem23  37603  poimirlem28  37608  fdc  37705  incsequz  37708  cntotbnd  37756  lcmineqlem11  41996  lcmineqlem18  42003  lcmineqlem22  42007  aks4d1p7d1  42039  aks6d1c1  42073  2np3bcnp1  42101  sticksstones6  42108  sticksstones7  42109  sticksstones10  42112  sticksstones12a  42114  sticksstones12  42115  sticksstones22  42125  aks6d1c7lem1  42137  metakunt2  42163  metakunt4  42165  metakunt12  42173  fltnltalem  42617  lzunuz  42724  lzenom  42726  ltrmxnn0  42906  jm2.17a  42917  jm2.17b  42918  jm2.17c  42919  jm2.24  42920  rmygeid  42921  jm2.25  42956  jm2.27a  42962  jm3.1lem1  42974  expdiophlem1  42978  monoords  45212  fmul01lt1lem1  45505  climsuselem1  45528  sumnnodd  45551  supcnvlimsup  45661  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  dvnmul  45864  iblspltprt  45894  itgspltprt  45900  stoweidlem26  45947  wallispilem4  45989  stirlinglem4  45998  stirlinglem8  46002  stirlinglem11  46005  stirlinglem13  46007  dirkertrigeqlem1  46019  dirkercncflem2  46025  fourierdlem11  46039  fourierdlem12  46040  fourierdlem15  46043  fourierdlem41  46069  fourierdlem50  46077  fourierdlem64  46091  fourierdlem65  46092  fourierdlem79  46106  caratheodorylem1  46447  smflimsuplem4  46744  natglobalincr  46796  iccpartgtprec  47294  iccpartiltu  47296  iccpartgt  47301  iccpartnel  47312  fmtnodvds  47418  fmtnoprmfac2lem1  47440  evenp1odd  47514  oddp1eveni  47515  opoeALTV  47557  evenltle  47591  perfectALTV  47597  fllogbd  48294  nnpw2blen  48314  dignn0flhalflem2  48350  nn0sumshdiglemA  48353  aacllem  48895