Theorem peano2zd 12680

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

Syntax hints:   → wi 4   ∈ wcel 2142  (class class class)co 7396  1c1 11074   + caddc 11076  ℤcz 12568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pow 5322  ax-pr 5390  ax-un 7718  ax-resscn 11130  ax-1cn 11131  ax-icn 11132  ax-addcl 11133  ax-addrcl 11134  ax-mulcl 11135  ax-mulrcl 11136  ax-mulcom 11137  ax-addass 11138  ax-mulass 11139  ax-distr 11140  ax-i2m1 11141  ax-1ne0 11142  ax-1rid 11143  ax-rnegex 11144  ax-rrecex 11145  ax-cnre 11146  ax-pre-lttri 11147  ax-pre-lttrn 11148  ax-pre-ltadd 11149  ax-pre-mulgt0 11150

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3368  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5542  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-we 5602  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-pred 6288  df-ord 6349  df-on 6350  df-lim 6351  df-suc 6352  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-riota 7353  df-ov 7399  df-oprab 7400  df-mpo 7401  df-om 7847  df-2nd 7971  df-frecs 8262  df-wrecs 8293  df-recs 8342  df-rdg 8381  df-er 8678  df-en 8928  df-dom 8929  df-sdom 8930  df-pnf 11218  df-mnf 11219  df-xr 11220  df-ltxr 11221  df-le 11222  df-sub 11416  df-neg 11417  df-nn 12211  df-n0 12482  df-z 12569

This theorem is referenced by:  rpnnen1lem5  12982  fznatpl1  13583  elfzom1elp1fzo1  13773  flge  13815  2tnp1ge0ge0  13839  uzsup  13873  seqf1olem1  14054  bcp1nk  14330  bcval5  14331  cshimadifsn0  14843  rexuzre  15380  limsupgre  15508  rlimclim1  15572  iseraltlem2  15710  telfsumo  15830  fsumparts  15834  climcnds  15881  geo2sum  15903  clim2prod  15918  clim2div  15919  fprodntriv  15972  dvdsfac  16360  2tp1odd  16386  opoe  16397  bits0o  16464  bitsp1o  16467  bitsinv1lem  16475  smupvallem  16517  smueqlem  16524  hashdvds  16810  prmreclem4  16955  prmreclem5  16956  vdwnnlem3  17033  prmgaplem7  17093  prmgaplem8  17094  chnub  18654  sylow1lem1  19638  telgsumfzs  20029  srgbinomlem3  20278  chfacfscmul0  22918  chfacfpmmul0  22922  ovoliunlem2  25565  ovolicc2lem4  25582  uniioombllem3  25647  dyaddisjlem  25657  dvfsumlem1  26088  dvfsumlem3  26090  plyco0  26252  abelthlem6  26499  birthdaylem2  27017  wilthlem1  27132  wilth  27135  wilthimp  27136  basellem3  27147  chpp1  27219  perfect  27295  bcmono  27341  lgslem1  27361  lgsval2lem  27371  gausslemma2dlem5  27435  lgseisenlem1  27439  lgsquadlem1  27444  m1lgs  27452  2lgslem1a  27455  2lgslem3c  27462  2lgslem3d  27463  2lgslem3b1  27465  2lgslem3c1  27466  2sqblem  27495  rplogsumlem2  27549  rpvmasumlem  27551  dchrisumlema  27552  dchrisumlem2  27554  pntpbnd1  27650  pntpbnd2  27651  pntlemq  27665  pntlemr  27666  pntlemj  27667  pntlemf  27669  axlowdimlem16  29158  crctcshwlkn0lem3  30012  crctcshwlkn0lem6  30015  clwwlkf  30249  eucrct2eupth  30447  cycpmco2lem3  33308  cycpmco2lem4  33309  cycpmco2lem5  33310  cycpmco2lem6  33311  cycpmco2  33313  isarchi3  33367  archirngz  33369  archiabllem1a  33371  archiabllem2c  33375  submateqlem1  34104  ballotlemsf1o  34811  ballotlemsima  34813  signstfvn  34863  fsum2dsub  34901  breprexplemc  34926  dnizphlfeqhlf  36914  dnibndlem13  36928  knoppndvlem10  36959  knoppndvlem14  36963  knoppndvlem15  36964  knoppndvlem17  36966  ltflcei  38107  poimirlem2  38121  poimirlem10  38129  poimirlem15  38134  poimirlem19  38138  poimirlem23  38142  poimirlem28  38147  fdc  38244  incsequz  38247  cntotbnd  38295  lcmineqlem11  42656  lcmineqlem18  42663  lcmineqlem22  42667  aks4d1p7d1  42699  aks6d1c1  42733  2np3bcnp1  42761  sticksstones6  42768  sticksstones7  42769  sticksstones10  42772  sticksstones12a  42774  sticksstones12  42775  sticksstones22  42785  aks6d1c7lem1  42797  fltnltalem  43244  lzunuz  43349  lzenom  43351  ltrmxnn0  43526  jm2.17a  43537  jm2.17b  43538  jm2.17c  43539  jm2.24  43540  rmygeid  43541  jm2.25  43576  jm2.27a  43582  jm3.1lem1  43594  expdiophlem1  43598  monoords  45876  fmul01lt1lem1  46160  climsuselem1  46183  sumnnodd  46206  supcnvlimsup  46314  ioodvbdlimc1lem2  46506  ioodvbdlimc2lem  46508  dvnmul  46517  iblspltprt  46547  itgspltprt  46553  stoweidlem26  46600  wallispilem4  46642  stirlinglem4  46651  stirlinglem8  46655  stirlinglem11  46658  stirlinglem13  46660  dirkertrigeqlem1  46672  dirkercncflem2  46678  fourierdlem11  46692  fourierdlem12  46693  fourierdlem15  46696  fourierdlem41  46722  fourierdlem50  46730  fourierdlem64  46744  fourierdlem65  46745  fourierdlem79  46759  caratheodorylem1  47100  smflimsuplem4  47397  ormkglobd  47451  natglobalincr  47453  iccpartgtprec  48026  iccpartiltu  48028  iccpartgt  48033  iccpartnel  48044  fmtnodvds  48153  fmtnoprmfac2lem1  48175  ppivalnnprm  48234  evenp1odd  48262  oddp1eveni  48263  opoeALTV  48305  evenltle  48339  perfectALTV  48345  gpgiedgdmellem  48668  gpgvtx0  48675  pgnbgreunbgrlem2lem2  48737  fllogbd  49182  nnpw2blen  49202  dignn0flhalflem2  49238  nn0sumshdiglemA  49241  aacllem  50422