Theorem peano2zd 12721

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  (class class class)co 7419  1c1 11118   + caddc 11120  ℤcz 12608

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742  ax-resscn 11174  ax-1cn 11175  ax-icn 11176  ax-addcl 11177  ax-addrcl 11178  ax-mulcl 11179  ax-mulrcl 11180  ax-mulcom 11181  ax-addass 11182  ax-mulass 11183  ax-distr 11184  ax-i2m1 11185  ax-1ne0 11186  ax-1rid 11187  ax-rnegex 11188  ax-rrecex 11189  ax-cnre 11190  ax-pre-lttri 11191  ax-pre-lttrn 11192  ax-pre-ltadd 11193  ax-pre-mulgt0 11194

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7376  df-ov 7422  df-oprab 7423  df-mpo 7424  df-om 7869  df-2nd 7993  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-er 8700  df-en 8950  df-dom 8951  df-sdom 8952  df-pnf 11262  df-mnf 11263  df-xr 11264  df-ltxr 11265  df-le 11266  df-sub 11460  df-neg 11461  df-nn 12251  df-n0 12522  df-z 12609

This theorem is used by:  rpnnen1lem5  13023  fznatpl1  13625  elfzom1elp1fzo1  13815  flge  13858  2tnp1ge0ge0  13882  uzsup  13916  seqf1olem1  14097  bcp1nk  14373  bcval5  14374  cshimadifsn0  14893  rexuzre  15430  limsupgre  15558  rlimclim1  15622  iseraltlem2  15760  telfsumo  15879  fsumparts  15883  climcnds  15930  geo2sum  15952  clim2prod  15967  clim2div  15968  fprodntriv  16021  dvdsfac  16408  2tp1odd  16434  opoe  16445  bits0o  16512  bitsp1o  16515  bitsinv1lem  16523  smupvallem  16565  smueqlem  16572  hashdvds  16858  prmreclem4  17003  prmreclem5  17004  vdwnnlem3  17081  prmgaplem7  17141  prmgaplem8  17142  chnub  18702  sylow1lem1  19714  telgsumfzs  20105  srgbinomlem3  20356  chfacfscmul0  23067  chfacfpmmul0  23071  ovoliunlem2  25715  ovolicc2lem4  25732  uniioombllem3  25797  dyaddisjlem  25807  dvfsumlem1  26238  dvfsumlem3  26240  plyco0  26402  abelthlem6  26652  birthdaylem2  27170  wilthlem1  27285  wilth  27288  wilthimp  27289  basellem3  27300  chpp1  27372  perfect  27448  bcmono  27494  lgslem1  27514  lgsval2lem  27524  gausslemma2dlem5  27588  lgseisenlem1  27592  lgsquadlem1  27597  m1lgs  27605  2lgslem1a  27608  2lgslem3c  27615  2lgslem3d  27616  2lgslem3b1  27618  2lgslem3c1  27619  2sqblem  27648  rplogsumlem2  27702  rpvmasumlem  27704  dchrisumlema  27705  dchrisumlem2  27707  pntpbnd1  27803  pntpbnd2  27804  pntlemq  27818  pntlemr  27819  pntlemj  27820  pntlemf  27822  axlowdimlem16  29364  crctcshwlkn0lem3  30230  crctcshwlkn0lem6  30233  clwwlkf  30467  eucrct2eupth  30669  cycpmco2lem3  33514  cycpmco2lem4  33515  cycpmco2lem5  33516  cycpmco2lem6  33517  cycpmco2  33519  isarchi3  33573  archirngz  33575  archiabllem1a  33577  archiabllem2c  33581  submateqlem1  34263  ballotlemsf1o  34971  ballotlemsima  34973  signstfvn  35023  fsum2dsub  35061  breprexplemc  35086  dnizphlfeqhlf  37124  dnibndlem13  37138  knoppndvlem10  37169  knoppndvlem14  37173  knoppndvlem15  37174  knoppndvlem17  37176  ltflcei  38318  poimirlem2  38332  poimirlem10  38340  poimirlem15  38345  poimirlem19  38349  poimirlem23  38353  poimirlem28  38358  fdc  38456  incsequz  38459  cntotbnd  38507  lcmineqlem11  42866  lcmineqlem18  42873  lcmineqlem22  42877  aks4d1p7d1  42909  aks6d1c1  42943  2np3bcnp1  42971  sticksstones6  42978  sticksstones7  42979  sticksstones10  42982  sticksstones12a  42984  sticksstones12  42985  sticksstones22  42995  aks6d1c7lem1  43007  fltnltalem  43454  lzunuz  43559  lzenom  43561  ltrmxnn0  43736  jm2.17a  43747  jm2.17b  43748  jm2.17c  43749  jm2.24  43750  rmygeid  43751  jm2.25  43786  jm2.27a  43792  jm3.1lem1  43804  expdiophlem1  43808  monoords  46076  fmul01lt1lem1  46360  climsuselem1  46383  sumnnodd  46406  supcnvlimsup  46514  ioodvbdlimc1lem2  46706  ioodvbdlimc2lem  46708  dvnmul  46717  iblspltprt  46747  itgspltprt  46753  stoweidlem26  46800  wallispilem4  46842  stirlinglem4  46851  stirlinglem8  46855  stirlinglem11  46858  stirlinglem13  46860  dirkertrigeqlem1  46872  dirkercncflem2  46878  fourierdlem11  46892  fourierdlem12  46893  fourierdlem15  46896  fourierdlem41  46922  fourierdlem50  46930  fourierdlem64  46944  fourierdlem65  46945  fourierdlem79  46959  caratheodorylem1  47300  smflimsuplem4  47597  ormkglobd  47651  natglobalincr  47653  iccpartgtprec  48229  iccpartiltu  48231  iccpartgt  48236  iccpartnel  48247  fmtnodvds  48356  fmtnoprmfac2lem1  48378  ppivalnnprm  48437  evenp1odd  48465  oddp1eveni  48466  opoeALTV  48508  evenltle  48542  perfectALTV  48548  gpgiedgdmellem  48871  gpgvtx0  48878  pgnbgreunbgrlem2lem2  48940  fllogbd  49399  nnpw2blen  49419  dignn0flhalflem2  49455  nn0sumshdiglemA  49458  aacllem  50680