Theorem peano2zd 12429

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

Syntax hints:   → wi 4   ∈ wcel 2106  (class class class)co 7275  1c1 10872   + caddc 10874  ℤcz 12319

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  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 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-mulcom 10935  ax-addass 10936  ax-mulass 10937  ax-distr 10938  ax-i2m1 10939  ax-1ne0 10940  ax-1rid 10941  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944  ax-pre-lttri 10945  ax-pre-lttrn 10946  ax-pre-ltadd 10947  ax-pre-mulgt0 10948

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-riota 7232  df-ov 7278  df-oprab 7279  df-mpo 7280  df-om 7713  df-2nd 7832  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-er 8498  df-en 8734  df-dom 8735  df-sdom 8736  df-pnf 11011  df-mnf 11012  df-xr 11013  df-ltxr 11014  df-le 11015  df-sub 11207  df-neg 11208  df-nn 11974  df-n0 12234  df-z 12320

This theorem is referenced by:  rpnnen1lem5  12721  fznatpl1  13310  elfzom1elp1fzo1  13487  flge  13525  2tnp1ge0ge0  13549  uzsup  13583  seqf1olem1  13762  bcp1nk  14031  bcval5  14032  cshimadifsn0  14543  rexuzre  15064  limsupgre  15190  rlimclim1  15254  iseraltlem2  15394  telfsumo  15514  fsumparts  15518  climcnds  15563  geo2sum  15585  clim2prod  15600  clim2div  15601  fprodntriv  15652  dvdsfac  16035  2tp1odd  16061  opoe  16072  bits0o  16137  bitsp1o  16140  bitsinv1lem  16148  smupvallem  16190  smueqlem  16197  hashdvds  16476  prmreclem4  16620  prmreclem5  16621  vdwnnlem3  16698  prmgaplem7  16758  prmgaplem8  16759  sylow1lem1  19203  telgsumfzs  19590  srgbinomlem3  19778  chfacfscmul0  22007  chfacfpmmul0  22011  ovoliunlem2  24667  ovolicc2lem4  24684  uniioombllem3  24749  dyaddisjlem  24759  dvfsumlem1  25190  dvfsumlem3  25192  plyco0  25353  abelthlem6  25595  birthdaylem2  26102  wilthlem1  26217  wilth  26220  wilthimp  26221  basellem3  26232  chpp1  26304  perfect  26379  bcmono  26425  lgslem1  26445  lgsval2lem  26455  gausslemma2dlem5  26519  lgseisenlem1  26523  lgsquadlem1  26528  m1lgs  26536  2lgslem1a  26539  2lgslem3c  26546  2lgslem3d  26547  2lgslem3b1  26549  2lgslem3c1  26550  2sqblem  26579  rplogsumlem2  26633  rpvmasumlem  26635  dchrisumlema  26636  dchrisumlem2  26638  pntpbnd1  26734  pntpbnd2  26735  pntlemq  26749  pntlemr  26750  pntlemj  26751  pntlemf  26753  axlowdimlem16  27325  crctcshwlkn0lem3  28177  crctcshwlkn0lem6  28180  clwwlkf  28411  eucrct2eupth  28609  cycpmco2lem3  31395  cycpmco2lem4  31396  cycpmco2lem5  31397  cycpmco2lem6  31398  cycpmco2  31400  isarchi3  31441  archirngz  31443  archiabllem1a  31445  archiabllem2c  31449  submateqlem1  31757  ballotlemsf1o  32480  ballotlemsima  32482  signstfvn  32548  fsum2dsub  32587  breprexplemc  32612  dnizphlfeqhlf  34656  dnibndlem13  34670  knoppndvlem10  34701  knoppndvlem14  34705  knoppndvlem15  34706  knoppndvlem17  34708  ltflcei  35765  poimirlem2  35779  poimirlem10  35787  poimirlem15  35792  poimirlem19  35796  poimirlem23  35800  poimirlem28  35805  fdc  35903  incsequz  35906  cntotbnd  35954  lcmineqlem11  40047  lcmineqlem18  40054  lcmineqlem22  40058  aks4d1p7d1  40090  2np3bcnp1  40100  sticksstones6  40107  sticksstones7  40108  sticksstones10  40111  sticksstones12a  40113  sticksstones12  40114  sticksstones22  40124  metakunt2  40126  metakunt4  40128  metakunt12  40136  fltnltalem  40499  lzunuz  40590  lzenom  40592  ltrmxnn0  40771  jm2.17a  40782  jm2.17b  40783  jm2.17c  40784  jm2.24  40785  rmygeid  40786  jm2.25  40821  jm2.27a  40827  jm3.1lem1  40839  expdiophlem1  40843  monoords  42836  fmul01lt1lem1  43125  climsuselem1  43148  sumnnodd  43171  supcnvlimsup  43281  ioodvbdlimc1lem2  43473  ioodvbdlimc2lem  43475  dvnmul  43484  iblspltprt  43514  itgspltprt  43520  stoweidlem26  43567  wallispilem4  43609  stirlinglem4  43618  stirlinglem8  43622  stirlinglem11  43625  stirlinglem13  43627  dirkertrigeqlem1  43639  dirkercncflem2  43645  fourierdlem11  43659  fourierdlem12  43660  fourierdlem15  43663  fourierdlem41  43689  fourierdlem50  43697  fourierdlem64  43711  fourierdlem65  43712  fourierdlem79  43726  caratheodorylem1  44064  smflimsuplem4  44356  iccpartgtprec  44872  iccpartiltu  44874  iccpartgt  44879  iccpartnel  44890  fmtnodvds  44996  fmtnoprmfac2lem1  45018  evenp1odd  45092  oddp1eveni  45093  opoeALTV  45135  evenltle  45169  perfectALTV  45175  fllogbd  45906  nnpw2blen  45926  dignn0flhalflem2  45962  nn0sumshdiglemA  45965  aacllem  46505  natglobalincr  46512