Theorem peano2zd 12707

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

Syntax hints:   → wi 4   ∈ wcel 2098  (class class class)co 7426  1c1 11147   + caddc 11149  ℤcz 12596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-resscn 11203  ax-1cn 11204  ax-icn 11205  ax-addcl 11206  ax-addrcl 11207  ax-mulcl 11208  ax-mulrcl 11209  ax-mulcom 11210  ax-addass 11211  ax-mulass 11212  ax-distr 11213  ax-i2m1 11214  ax-1ne0 11215  ax-1rid 11216  ax-rnegex 11217  ax-rrecex 11218  ax-cnre 11219  ax-pre-lttri 11220  ax-pre-lttrn 11221  ax-pre-ltadd 11222  ax-pre-mulgt0 11223

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6310  df-ord 6377  df-on 6378  df-lim 6379  df-suc 6380  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-riota 7382  df-ov 7429  df-oprab 7430  df-mpo 7431  df-om 7877  df-2nd 8000  df-frecs 8293  df-wrecs 8324  df-recs 8398  df-rdg 8437  df-er 8731  df-en 8971  df-dom 8972  df-sdom 8973  df-pnf 11288  df-mnf 11289  df-xr 11290  df-ltxr 11291  df-le 11292  df-sub 11484  df-neg 11485  df-nn 12251  df-n0 12511  df-z 12597

This theorem is referenced by:  rpnnen1lem5  13003  fznatpl1  13595  elfzom1elp1fzo1  13772  flge  13810  2tnp1ge0ge0  13834  uzsup  13868  seqf1olem1  14046  bcp1nk  14316  bcval5  14317  cshimadifsn0  14821  rexuzre  15339  limsupgre  15465  rlimclim1  15529  iseraltlem2  15669  telfsumo  15788  fsumparts  15792  climcnds  15837  geo2sum  15859  clim2prod  15874  clim2div  15875  fprodntriv  15926  dvdsfac  16310  2tp1odd  16336  opoe  16347  bits0o  16412  bitsp1o  16415  bitsinv1lem  16423  smupvallem  16465  smueqlem  16472  hashdvds  16751  prmreclem4  16895  prmreclem5  16896  vdwnnlem3  16973  prmgaplem7  17033  prmgaplem8  17034  sylow1lem1  19560  telgsumfzs  19951  srgbinomlem3  20175  chfacfscmul0  22780  chfacfpmmul0  22784  ovoliunlem2  25452  ovolicc2lem4  25469  uniioombllem3  25534  dyaddisjlem  25544  dvfsumlem1  25980  dvfsumlem3  25983  plyco0  26146  abelthlem6  26393  birthdaylem2  26904  wilthlem1  27020  wilth  27023  wilthimp  27024  basellem3  27035  chpp1  27107  perfect  27184  bcmono  27230  lgslem1  27250  lgsval2lem  27260  gausslemma2dlem5  27324  lgseisenlem1  27328  lgsquadlem1  27333  m1lgs  27341  2lgslem1a  27344  2lgslem3c  27351  2lgslem3d  27352  2lgslem3b1  27354  2lgslem3c1  27355  2sqblem  27384  rplogsumlem2  27438  rpvmasumlem  27440  dchrisumlema  27441  dchrisumlem2  27443  pntpbnd1  27539  pntpbnd2  27540  pntlemq  27554  pntlemr  27555  pntlemj  27556  pntlemf  27558  axlowdimlem16  28788  crctcshwlkn0lem3  29643  crctcshwlkn0lem6  29646  clwwlkf  29877  eucrct2eupth  30075  cycpmco2lem3  32870  cycpmco2lem4  32871  cycpmco2lem5  32872  cycpmco2lem6  32873  cycpmco2  32875  isarchi3  32916  archirngz  32918  archiabllem1a  32920  archiabllem2c  32924  submateqlem1  33441  ballotlemsf1o  34166  ballotlemsima  34168  signstfvn  34234  fsum2dsub  34272  breprexplemc  34297  dnizphlfeqhlf  35984  dnibndlem13  35998  knoppndvlem10  36029  knoppndvlem14  36033  knoppndvlem15  36034  knoppndvlem17  36036  ltflcei  37114  poimirlem2  37128  poimirlem10  37136  poimirlem15  37141  poimirlem19  37145  poimirlem23  37149  poimirlem28  37154  fdc  37251  incsequz  37254  cntotbnd  37302  lcmineqlem11  41542  lcmineqlem18  41549  lcmineqlem22  41553  aks4d1p7d1  41585  aks6d1c1  41619  2np3bcnp1  41648  sticksstones6  41655  sticksstones7  41656  sticksstones10  41659  sticksstones12a  41661  sticksstones12  41662  sticksstones22  41672  aks6d1c7lem1  41684  metakunt2  41690  metakunt4  41692  metakunt12  41700  fltnltalem  42117  lzunuz  42219  lzenom  42221  ltrmxnn0  42401  jm2.17a  42412  jm2.17b  42413  jm2.17c  42414  jm2.24  42415  rmygeid  42416  jm2.25  42451  jm2.27a  42457  jm3.1lem1  42469  expdiophlem1  42473  monoords  44708  fmul01lt1lem1  45001  climsuselem1  45024  sumnnodd  45047  supcnvlimsup  45157  ioodvbdlimc1lem2  45349  ioodvbdlimc2lem  45351  dvnmul  45360  iblspltprt  45390  itgspltprt  45396  stoweidlem26  45443  wallispilem4  45485  stirlinglem4  45494  stirlinglem8  45498  stirlinglem11  45501  stirlinglem13  45503  dirkertrigeqlem1  45515  dirkercncflem2  45521  fourierdlem11  45535  fourierdlem12  45536  fourierdlem15  45539  fourierdlem41  45565  fourierdlem50  45573  fourierdlem64  45587  fourierdlem65  45588  fourierdlem79  45602  caratheodorylem1  45943  smflimsuplem4  46240  natglobalincr  46292  iccpartgtprec  46789  iccpartiltu  46791  iccpartgt  46796  iccpartnel  46807  fmtnodvds  46913  fmtnoprmfac2lem1  46935  evenp1odd  47009  oddp1eveni  47010  opoeALTV  47052  evenltle  47086  perfectALTV  47092  fllogbd  47711  nnpw2blen  47731  dignn0flhalflem2  47767  nn0sumshdiglemA  47770  aacllem  48312