Theorem peano2zd 12703

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

Syntax hints:   → wi 4   ∈ wcel 2149  (class class class)co 7411  1c1 11101   + caddc 11103  ℤcz 12591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733  ax-resscn 11157  ax-1cn 11158  ax-icn 11159  ax-addcl 11160  ax-addrcl 11161  ax-mulcl 11162  ax-mulrcl 11163  ax-mulcom 11164  ax-addass 11165  ax-mulass 11166  ax-distr 11167  ax-i2m1 11168  ax-1ne0 11169  ax-1rid 11170  ax-rnegex 11171  ax-rrecex 11172  ax-cnre 11173  ax-pre-lttri 11174  ax-pre-lttrn 11175  ax-pre-ltadd 11176  ax-pre-mulgt0 11177

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-iun 4962  df-br 5114  df-opab 5178  df-mpt 5197  df-tr 5223  df-id 5557  df-eprel 5562  df-po 5570  df-so 5571  df-fr 5615  df-we 5617  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7368  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7863  df-2nd 7987  df-frecs 8278  df-wrecs 8309  df-recs 8358  df-rdg 8397  df-er 8694  df-en 8944  df-dom 8945  df-sdom 8946  df-pnf 11245  df-mnf 11246  df-xr 11247  df-ltxr 11248  df-le 11249  df-sub 11443  df-neg 11444  df-nn 12234  df-n0 12505  df-z 12592

This theorem is referenced by:  rpnnen1lem5  13005  fznatpl1  13606  elfzom1elp1fzo1  13796  flge  13838  2tnp1ge0ge0  13862  uzsup  13896  seqf1olem1  14077  bcp1nk  14353  bcval5  14354  cshimadifsn0  14867  rexuzre  15404  limsupgre  15532  rlimclim1  15596  iseraltlem2  15734  telfsumo  15854  fsumparts  15858  climcnds  15905  geo2sum  15927  clim2prod  15942  clim2div  15943  fprodntriv  15996  dvdsfac  16384  2tp1odd  16410  opoe  16421  bits0o  16488  bitsp1o  16491  bitsinv1lem  16499  smupvallem  16541  smueqlem  16548  hashdvds  16834  prmreclem4  16979  prmreclem5  16980  vdwnnlem3  17057  prmgaplem7  17117  prmgaplem8  17118  chnub  18678  sylow1lem1  19668  telgsumfzs  20059  srgbinomlem3  20310  chfacfscmul0  22984  chfacfpmmul0  22988  ovoliunlem2  25631  ovolicc2lem4  25648  uniioombllem3  25713  dyaddisjlem  25723  dvfsumlem1  26154  dvfsumlem3  26156  plyco0  26318  abelthlem6  26565  birthdaylem2  27083  wilthlem1  27198  wilth  27201  wilthimp  27202  basellem3  27213  chpp1  27285  perfect  27361  bcmono  27407  lgslem1  27427  lgsval2lem  27437  gausslemma2dlem5  27501  lgseisenlem1  27505  lgsquadlem1  27510  m1lgs  27518  2lgslem1a  27521  2lgslem3c  27528  2lgslem3d  27529  2lgslem3b1  27531  2lgslem3c1  27532  2sqblem  27561  rplogsumlem2  27615  rpvmasumlem  27617  dchrisumlema  27618  dchrisumlem2  27620  pntpbnd1  27716  pntpbnd2  27717  pntlemq  27731  pntlemr  27732  pntlemj  27733  pntlemf  27735  axlowdimlem16  29248  crctcshwlkn0lem3  30102  crctcshwlkn0lem6  30105  clwwlkf  30339  eucrct2eupth  30537  cycpmco2lem3  33389  cycpmco2lem4  33390  cycpmco2lem5  33391  cycpmco2lem6  33392  cycpmco2  33394  isarchi3  33448  archirngz  33450  archiabllem1a  33452  archiabllem2c  33456  submateqlem1  34142  ballotlemsf1o  34849  ballotlemsima  34851  signstfvn  34901  fsum2dsub  34939  breprexplemc  34964  dnizphlfeqhlf  36954  dnibndlem13  36968  knoppndvlem10  36999  knoppndvlem14  37003  knoppndvlem15  37004  knoppndvlem17  37006  ltflcei  38147  poimirlem2  38161  poimirlem10  38169  poimirlem15  38174  poimirlem19  38178  poimirlem23  38182  poimirlem28  38187  fdc  38284  incsequz  38287  cntotbnd  38335  lcmineqlem11  42696  lcmineqlem18  42703  lcmineqlem22  42707  aks4d1p7d1  42739  aks6d1c1  42773  2np3bcnp1  42801  sticksstones6  42808  sticksstones7  42809  sticksstones10  42812  sticksstones12a  42814  sticksstones12  42815  sticksstones22  42825  aks6d1c7lem1  42837  fltnltalem  43286  lzunuz  43391  lzenom  43393  ltrmxnn0  43568  jm2.17a  43579  jm2.17b  43580  jm2.17c  43581  jm2.24  43582  rmygeid  43583  jm2.25  43618  jm2.27a  43624  jm3.1lem1  43636  expdiophlem1  43640  monoords  45908  fmul01lt1lem1  46192  climsuselem1  46215  sumnnodd  46238  supcnvlimsup  46346  ioodvbdlimc1lem2  46538  ioodvbdlimc2lem  46540  dvnmul  46549  iblspltprt  46579  itgspltprt  46585  stoweidlem26  46632  wallispilem4  46674  stirlinglem4  46683  stirlinglem8  46687  stirlinglem11  46690  stirlinglem13  46692  dirkertrigeqlem1  46704  dirkercncflem2  46710  fourierdlem11  46724  fourierdlem12  46725  fourierdlem15  46728  fourierdlem41  46754  fourierdlem50  46762  fourierdlem64  46776  fourierdlem65  46777  fourierdlem79  46791  caratheodorylem1  47132  smflimsuplem4  47429  ormkglobd  47483  natglobalincr  47485  iccpartgtprec  48058  iccpartiltu  48060  iccpartgt  48065  iccpartnel  48076  fmtnodvds  48185  fmtnoprmfac2lem1  48207  ppivalnnprm  48266  evenp1odd  48294  oddp1eveni  48295  opoeALTV  48337  evenltle  48371  perfectALTV  48377  gpgiedgdmellem  48700  gpgvtx0  48707  pgnbgreunbgrlem2lem2  48769  fllogbd  49225  nnpw2blen  49245  dignn0flhalflem2  49281  nn0sumshdiglemA  49284  aacllem  50475