Theorem peano2zd 12668

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

Syntax hints:   → wi 4   ∈ wcel 2106  (class class class)co 7408  1c1 11110   + caddc 11112  ℤcz 12557

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7724  ax-resscn 11166  ax-1cn 11167  ax-icn 11168  ax-addcl 11169  ax-addrcl 11170  ax-mulcl 11171  ax-mulrcl 11172  ax-mulcom 11173  ax-addass 11174  ax-mulass 11175  ax-distr 11176  ax-i2m1 11177  ax-1ne0 11178  ax-1rid 11179  ax-rnegex 11180  ax-rrecex 11181  ax-cnre 11182  ax-pre-lttri 11183  ax-pre-lttrn 11184  ax-pre-ltadd 11185  ax-pre-mulgt0 11186

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7364  df-ov 7411  df-oprab 7412  df-mpo 7413  df-om 7855  df-2nd 7975  df-frecs 8265  df-wrecs 8296  df-recs 8370  df-rdg 8409  df-er 8702  df-en 8939  df-dom 8940  df-sdom 8941  df-pnf 11249  df-mnf 11250  df-xr 11251  df-ltxr 11252  df-le 11253  df-sub 11445  df-neg 11446  df-nn 12212  df-n0 12472  df-z 12558

This theorem is referenced by:  rpnnen1lem5  12964  fznatpl1  13554  elfzom1elp1fzo1  13731  flge  13769  2tnp1ge0ge0  13793  uzsup  13827  seqf1olem1  14006  bcp1nk  14276  bcval5  14277  cshimadifsn0  14780  rexuzre  15298  limsupgre  15424  rlimclim1  15488  iseraltlem2  15628  telfsumo  15747  fsumparts  15751  climcnds  15796  geo2sum  15818  clim2prod  15833  clim2div  15834  fprodntriv  15885  dvdsfac  16268  2tp1odd  16294  opoe  16305  bits0o  16370  bitsp1o  16373  bitsinv1lem  16381  smupvallem  16423  smueqlem  16430  hashdvds  16707  prmreclem4  16851  prmreclem5  16852  vdwnnlem3  16929  prmgaplem7  16989  prmgaplem8  16990  sylow1lem1  19465  telgsumfzs  19856  srgbinomlem3  20050  chfacfscmul0  22359  chfacfpmmul0  22363  ovoliunlem2  25019  ovolicc2lem4  25036  uniioombllem3  25101  dyaddisjlem  25111  dvfsumlem1  25542  dvfsumlem3  25544  plyco0  25705  abelthlem6  25947  birthdaylem2  26454  wilthlem1  26569  wilth  26572  wilthimp  26573  basellem3  26584  chpp1  26656  perfect  26731  bcmono  26777  lgslem1  26797  lgsval2lem  26807  gausslemma2dlem5  26871  lgseisenlem1  26875  lgsquadlem1  26880  m1lgs  26888  2lgslem1a  26891  2lgslem3c  26898  2lgslem3d  26899  2lgslem3b1  26901  2lgslem3c1  26902  2sqblem  26931  rplogsumlem2  26985  rpvmasumlem  26987  dchrisumlema  26988  dchrisumlem2  26990  pntpbnd1  27086  pntpbnd2  27087  pntlemq  27101  pntlemr  27102  pntlemj  27103  pntlemf  27105  axlowdimlem16  28212  crctcshwlkn0lem3  29063  crctcshwlkn0lem6  29066  clwwlkf  29297  eucrct2eupth  29495  cycpmco2lem3  32282  cycpmco2lem4  32283  cycpmco2lem5  32284  cycpmco2lem6  32285  cycpmco2  32287  isarchi3  32328  archirngz  32330  archiabllem1a  32332  archiabllem2c  32336  submateqlem1  32782  ballotlemsf1o  33507  ballotlemsima  33509  signstfvn  33575  fsum2dsub  33614  breprexplemc  33639  dnizphlfeqhlf  35347  dnibndlem13  35361  knoppndvlem10  35392  knoppndvlem14  35396  knoppndvlem15  35397  knoppndvlem17  35399  ltflcei  36471  poimirlem2  36485  poimirlem10  36493  poimirlem15  36498  poimirlem19  36502  poimirlem23  36506  poimirlem28  36511  fdc  36608  incsequz  36611  cntotbnd  36659  lcmineqlem11  40899  lcmineqlem18  40906  lcmineqlem22  40910  aks4d1p7d1  40942  2np3bcnp1  40955  sticksstones6  40962  sticksstones7  40963  sticksstones10  40966  sticksstones12a  40968  sticksstones12  40969  sticksstones22  40979  metakunt2  40981  metakunt4  40983  metakunt12  40991  fltnltalem  41405  lzunuz  41496  lzenom  41498  ltrmxnn0  41678  jm2.17a  41689  jm2.17b  41690  jm2.17c  41691  jm2.24  41692  rmygeid  41693  jm2.25  41728  jm2.27a  41734  jm3.1lem1  41746  expdiophlem1  41750  monoords  43997  fmul01lt1lem1  44290  climsuselem1  44313  sumnnodd  44336  supcnvlimsup  44446  ioodvbdlimc1lem2  44638  ioodvbdlimc2lem  44640  dvnmul  44649  iblspltprt  44679  itgspltprt  44685  stoweidlem26  44732  wallispilem4  44774  stirlinglem4  44783  stirlinglem8  44787  stirlinglem11  44790  stirlinglem13  44792  dirkertrigeqlem1  44804  dirkercncflem2  44810  fourierdlem11  44824  fourierdlem12  44825  fourierdlem15  44828  fourierdlem41  44854  fourierdlem50  44862  fourierdlem64  44876  fourierdlem65  44877  fourierdlem79  44891  caratheodorylem1  45232  smflimsuplem4  45529  natglobalincr  45581  iccpartgtprec  46078  iccpartiltu  46080  iccpartgt  46085  iccpartnel  46096  fmtnodvds  46202  fmtnoprmfac2lem1  46224  evenp1odd  46298  oddp1eveni  46299  opoeALTV  46341  evenltle  46375  perfectALTV  46381  fllogbd  47236  nnpw2blen  47256  dignn0flhalflem2  47292  nn0sumshdiglemA  47295  aacllem  47838