Theorem peano2zd 12583

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7349  1c1 11010   + caddc 11012  ℤcz 12471

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-i2m1 11077  ax-1ne0 11078  ax-1rid 11079  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084  ax-pre-ltadd 11085  ax-pre-mulgt0 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5174  df-tr 5200  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6249  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-riota 7306  df-ov 7352  df-oprab 7353  df-mpo 7354  df-om 7800  df-2nd 7925  df-frecs 8214  df-wrecs 8245  df-recs 8294  df-rdg 8332  df-er 8625  df-en 8873  df-dom 8874  df-sdom 8875  df-pnf 11151  df-mnf 11152  df-xr 11153  df-ltxr 11154  df-le 11155  df-sub 11349  df-neg 11350  df-nn 12129  df-n0 12385  df-z 12472

This theorem is referenced by:  rpnnen1lem5  12882  fznatpl1  13481  elfzom1elp1fzo1  13670  flge  13709  2tnp1ge0ge0  13733  uzsup  13767  seqf1olem1  13948  bcp1nk  14224  bcval5  14225  cshimadifsn0  14737  rexuzre  15260  limsupgre  15388  rlimclim1  15452  iseraltlem2  15590  telfsumo  15709  fsumparts  15713  climcnds  15758  geo2sum  15780  clim2prod  15795  clim2div  15796  fprodntriv  15849  dvdsfac  16237  2tp1odd  16263  opoe  16274  bits0o  16341  bitsp1o  16344  bitsinv1lem  16352  smupvallem  16394  smueqlem  16401  hashdvds  16686  prmreclem4  16831  prmreclem5  16832  vdwnnlem3  16909  prmgaplem7  16969  prmgaplem8  16970  sylow1lem1  19477  telgsumfzs  19868  srgbinomlem3  20113  chfacfscmul0  22743  chfacfpmmul0  22747  ovoliunlem2  25402  ovolicc2lem4  25419  uniioombllem3  25484  dyaddisjlem  25494  dvfsumlem1  25930  dvfsumlem3  25933  plyco0  26095  abelthlem6  26344  birthdaylem2  26860  wilthlem1  26976  wilth  26979  wilthimp  26980  basellem3  26991  chpp1  27063  perfect  27140  bcmono  27186  lgslem1  27206  lgsval2lem  27216  gausslemma2dlem5  27280  lgseisenlem1  27284  lgsquadlem1  27289  m1lgs  27297  2lgslem1a  27300  2lgslem3c  27307  2lgslem3d  27308  2lgslem3b1  27310  2lgslem3c1  27311  2sqblem  27340  rplogsumlem2  27394  rpvmasumlem  27396  dchrisumlema  27397  dchrisumlem2  27399  pntpbnd1  27495  pntpbnd2  27496  pntlemq  27510  pntlemr  27511  pntlemj  27512  pntlemf  27514  axlowdimlem16  28902  crctcshwlkn0lem3  29757  crctcshwlkn0lem6  29760  clwwlkf  29991  eucrct2eupth  30189  chnub  32954  cycpmco2lem3  33070  cycpmco2lem4  33071  cycpmco2lem5  33072  cycpmco2lem6  33073  cycpmco2  33075  isarchi3  33129  archirngz  33131  archiabllem1a  33133  archiabllem2c  33137  submateqlem1  33774  ballotlemsf1o  34482  ballotlemsima  34484  signstfvn  34537  fsum2dsub  34575  breprexplemc  34600  dnizphlfeqhlf  36454  dnibndlem13  36468  knoppndvlem10  36499  knoppndvlem14  36503  knoppndvlem15  36504  knoppndvlem17  36506  ltflcei  37592  poimirlem2  37606  poimirlem10  37614  poimirlem15  37619  poimirlem19  37623  poimirlem23  37627  poimirlem28  37632  fdc  37729  incsequz  37732  cntotbnd  37780  lcmineqlem11  42016  lcmineqlem18  42023  lcmineqlem22  42027  aks4d1p7d1  42059  aks6d1c1  42093  2np3bcnp1  42121  sticksstones6  42128  sticksstones7  42129  sticksstones10  42132  sticksstones12a  42134  sticksstones12  42135  sticksstones22  42145  aks6d1c7lem1  42157  fltnltalem  42639  lzunuz  42745  lzenom  42747  ltrmxnn0  42926  jm2.17a  42937  jm2.17b  42938  jm2.17c  42939  jm2.24  42940  rmygeid  42941  jm2.25  42976  jm2.27a  42982  jm3.1lem1  42994  expdiophlem1  42998  monoords  45283  fmul01lt1lem1  45569  climsuselem1  45592  sumnnodd  45615  supcnvlimsup  45725  ioodvbdlimc1lem2  45917  ioodvbdlimc2lem  45919  dvnmul  45928  iblspltprt  45958  itgspltprt  45964  stoweidlem26  46011  wallispilem4  46053  stirlinglem4  46062  stirlinglem8  46066  stirlinglem11  46069  stirlinglem13  46071  dirkertrigeqlem1  46083  dirkercncflem2  46089  fourierdlem11  46103  fourierdlem12  46104  fourierdlem15  46107  fourierdlem41  46133  fourierdlem50  46141  fourierdlem64  46155  fourierdlem65  46156  fourierdlem79  46170  caratheodorylem1  46511  smflimsuplem4  46808  ormkglobd  46860  natglobalincr  46862  iccpartgtprec  47408  iccpartiltu  47410  iccpartgt  47415  iccpartnel  47426  fmtnodvds  47532  fmtnoprmfac2lem1  47554  evenp1odd  47628  oddp1eveni  47629  opoeALTV  47671  evenltle  47705  perfectALTV  47711  gpgiedgdmellem  48034  gpgvtx0  48041  pgnbgreunbgrlem2lem2  48103  fllogbd  48549  nnpw2blen  48569  dignn0flhalflem2  48605  nn0sumshdiglemA  48608  aacllem  49790