Theorem peano2zd 12723

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

Syntax hints:   → wi 4   ∈ wcel 2106  (class class class)co 7431  1c1 11154   + caddc 11156  ℤcz 12611

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-resscn 11210  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-addrcl 11214  ax-mulcl 11215  ax-mulrcl 11216  ax-mulcom 11217  ax-addass 11218  ax-mulass 11219  ax-distr 11220  ax-i2m1 11221  ax-1ne0 11222  ax-1rid 11223  ax-rnegex 11224  ax-rrecex 11225  ax-cnre 11226  ax-pre-lttri 11227  ax-pre-lttrn 11228  ax-pre-ltadd 11229  ax-pre-mulgt0 11230

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-2nd 8014  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-er 8744  df-en 8985  df-dom 8986  df-sdom 8987  df-pnf 11295  df-mnf 11296  df-xr 11297  df-ltxr 11298  df-le 11299  df-sub 11492  df-neg 11493  df-nn 12265  df-n0 12525  df-z 12612

This theorem is referenced by:  rpnnen1lem5  13021  fznatpl1  13615  elfzom1elp1fzo1  13803  flge  13842  2tnp1ge0ge0  13866  uzsup  13900  seqf1olem1  14079  bcp1nk  14353  bcval5  14354  cshimadifsn0  14866  rexuzre  15388  limsupgre  15514  rlimclim1  15578  iseraltlem2  15716  telfsumo  15835  fsumparts  15839  climcnds  15884  geo2sum  15906  clim2prod  15921  clim2div  15922  fprodntriv  15975  dvdsfac  16360  2tp1odd  16386  opoe  16397  bits0o  16464  bitsp1o  16467  bitsinv1lem  16475  smupvallem  16517  smueqlem  16524  hashdvds  16809  prmreclem4  16953  prmreclem5  16954  vdwnnlem3  17031  prmgaplem7  17091  prmgaplem8  17092  sylow1lem1  19631  telgsumfzs  20022  srgbinomlem3  20246  chfacfscmul0  22880  chfacfpmmul0  22884  ovoliunlem2  25552  ovolicc2lem4  25569  uniioombllem3  25634  dyaddisjlem  25644  dvfsumlem1  26081  dvfsumlem3  26084  plyco0  26246  abelthlem6  26495  birthdaylem2  27010  wilthlem1  27126  wilth  27129  wilthimp  27130  basellem3  27141  chpp1  27213  perfect  27290  bcmono  27336  lgslem1  27356  lgsval2lem  27366  gausslemma2dlem5  27430  lgseisenlem1  27434  lgsquadlem1  27439  m1lgs  27447  2lgslem1a  27450  2lgslem3c  27457  2lgslem3d  27458  2lgslem3b1  27460  2lgslem3c1  27461  2sqblem  27490  rplogsumlem2  27544  rpvmasumlem  27546  dchrisumlema  27547  dchrisumlem2  27549  pntpbnd1  27645  pntpbnd2  27646  pntlemq  27660  pntlemr  27661  pntlemj  27662  pntlemf  27664  axlowdimlem16  28987  crctcshwlkn0lem3  29842  crctcshwlkn0lem6  29845  clwwlkf  30076  eucrct2eupth  30274  chnub  32986  cycpmco2lem3  33131  cycpmco2lem4  33132  cycpmco2lem5  33133  cycpmco2lem6  33134  cycpmco2  33136  isarchi3  33177  archirngz  33179  archiabllem1a  33181  archiabllem2c  33185  submateqlem1  33768  ballotlemsf1o  34495  ballotlemsima  34497  signstfvn  34563  fsum2dsub  34601  breprexplemc  34626  dnizphlfeqhlf  36459  dnibndlem13  36473  knoppndvlem10  36504  knoppndvlem14  36508  knoppndvlem15  36509  knoppndvlem17  36511  ltflcei  37595  poimirlem2  37609  poimirlem10  37617  poimirlem15  37622  poimirlem19  37626  poimirlem23  37630  poimirlem28  37635  fdc  37732  incsequz  37735  cntotbnd  37783  lcmineqlem11  42021  lcmineqlem18  42028  lcmineqlem22  42032  aks4d1p7d1  42064  aks6d1c1  42098  2np3bcnp1  42126  sticksstones6  42133  sticksstones7  42134  sticksstones10  42137  sticksstones12a  42139  sticksstones12  42140  sticksstones22  42150  aks6d1c7lem1  42162  metakunt2  42188  metakunt4  42190  metakunt12  42198  fltnltalem  42649  lzunuz  42756  lzenom  42758  ltrmxnn0  42938  jm2.17a  42949  jm2.17b  42950  jm2.17c  42951  jm2.24  42952  rmygeid  42953  jm2.25  42988  jm2.27a  42994  jm3.1lem1  43006  expdiophlem1  43010  monoords  45248  fmul01lt1lem1  45540  climsuselem1  45563  sumnnodd  45586  supcnvlimsup  45696  ioodvbdlimc1lem2  45888  ioodvbdlimc2lem  45890  dvnmul  45899  iblspltprt  45929  itgspltprt  45935  stoweidlem26  45982  wallispilem4  46024  stirlinglem4  46033  stirlinglem8  46037  stirlinglem11  46040  stirlinglem13  46042  dirkertrigeqlem1  46054  dirkercncflem2  46060  fourierdlem11  46074  fourierdlem12  46075  fourierdlem15  46078  fourierdlem41  46104  fourierdlem50  46112  fourierdlem64  46126  fourierdlem65  46127  fourierdlem79  46141  caratheodorylem1  46482  smflimsuplem4  46779  natglobalincr  46831  iccpartgtprec  47345  iccpartiltu  47347  iccpartgt  47352  iccpartnel  47363  fmtnodvds  47469  fmtnoprmfac2lem1  47491  evenp1odd  47565  oddp1eveni  47566  opoeALTV  47608  evenltle  47642  perfectALTV  47648  gpgedgel  47943  gpgvtx0  47944  fllogbd  48410  nnpw2blen  48430  dignn0flhalflem2  48466  nn0sumshdiglemA  48469  aacllem  49032