Theorem peano2zd 12708

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 2107  (class class class)co 7413  1c1 11138   + caddc 11140  ℤcz 12596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5276  ax-nul 5286  ax-pow 5345  ax-pr 5412  ax-un 7737  ax-resscn 11194  ax-1cn 11195  ax-icn 11196  ax-addcl 11197  ax-addrcl 11198  ax-mulcl 11199  ax-mulrcl 11200  ax-mulcom 11201  ax-addass 11202  ax-mulass 11203  ax-distr 11204  ax-i2m1 11205  ax-1ne0 11206  ax-1rid 11207  ax-rnegex 11208  ax-rrecex 11209  ax-cnre 11210  ax-pre-lttri 11211  ax-pre-lttrn 11212  ax-pre-ltadd 11213  ax-pre-mulgt0 11214

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3060  df-reu 3364  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-iun 4973  df-br 5124  df-opab 5186  df-mpt 5206  df-tr 5240  df-id 5558  df-eprel 5564  df-po 5572  df-so 5573  df-fr 5617  df-we 5619  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-res 5677  df-ima 5678  df-pred 6301  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-riota 7370  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7870  df-2nd 7997  df-frecs 8288  df-wrecs 8319  df-recs 8393  df-rdg 8432  df-er 8727  df-en 8968  df-dom 8969  df-sdom 8970  df-pnf 11279  df-mnf 11280  df-xr 11281  df-ltxr 11282  df-le 11283  df-sub 11476  df-neg 11477  df-nn 12249  df-n0 12510  df-z 12597

This theorem is referenced by:  rpnnen1lem5  13005  fznatpl1  13600  elfzom1elp1fzo1  13788  flge  13827  2tnp1ge0ge0  13851  uzsup  13885  seqf1olem1  14064  bcp1nk  14338  bcval5  14339  cshimadifsn0  14851  rexuzre  15373  limsupgre  15499  rlimclim1  15563  iseraltlem2  15701  telfsumo  15820  fsumparts  15824  climcnds  15869  geo2sum  15891  clim2prod  15906  clim2div  15907  fprodntriv  15960  dvdsfac  16345  2tp1odd  16371  opoe  16382  bits0o  16449  bitsp1o  16452  bitsinv1lem  16460  smupvallem  16502  smueqlem  16509  hashdvds  16794  prmreclem4  16939  prmreclem5  16940  vdwnnlem3  17017  prmgaplem7  17077  prmgaplem8  17078  sylow1lem1  19584  telgsumfzs  19975  srgbinomlem3  20193  chfacfscmul0  22812  chfacfpmmul0  22816  ovoliunlem2  25474  ovolicc2lem4  25491  uniioombllem3  25556  dyaddisjlem  25566  dvfsumlem1  26002  dvfsumlem3  26005  plyco0  26167  abelthlem6  26416  birthdaylem2  26931  wilthlem1  27047  wilth  27050  wilthimp  27051  basellem3  27062  chpp1  27134  perfect  27211  bcmono  27257  lgslem1  27277  lgsval2lem  27287  gausslemma2dlem5  27351  lgseisenlem1  27355  lgsquadlem1  27360  m1lgs  27368  2lgslem1a  27371  2lgslem3c  27378  2lgslem3d  27379  2lgslem3b1  27381  2lgslem3c1  27382  2sqblem  27411  rplogsumlem2  27465  rpvmasumlem  27467  dchrisumlema  27468  dchrisumlem2  27470  pntpbnd1  27566  pntpbnd2  27567  pntlemq  27581  pntlemr  27582  pntlemj  27583  pntlemf  27585  axlowdimlem16  28902  crctcshwlkn0lem3  29760  crctcshwlkn0lem6  29763  clwwlkf  29994  eucrct2eupth  30192  chnub  32941  cycpmco2lem3  33087  cycpmco2lem4  33088  cycpmco2lem5  33089  cycpmco2lem6  33090  cycpmco2  33092  isarchi3  33133  archirngz  33135  archiabllem1a  33137  archiabllem2c  33141  submateqlem1  33765  ballotlemsf1o  34475  ballotlemsima  34477  signstfvn  34543  fsum2dsub  34581  breprexplemc  34606  dnizphlfeqhlf  36436  dnibndlem13  36450  knoppndvlem10  36481  knoppndvlem14  36485  knoppndvlem15  36486  knoppndvlem17  36488  ltflcei  37574  poimirlem2  37588  poimirlem10  37596  poimirlem15  37601  poimirlem19  37605  poimirlem23  37609  poimirlem28  37614  fdc  37711  incsequz  37714  cntotbnd  37762  lcmineqlem11  41999  lcmineqlem18  42006  lcmineqlem22  42010  aks4d1p7d1  42042  aks6d1c1  42076  2np3bcnp1  42104  sticksstones6  42111  sticksstones7  42112  sticksstones10  42115  sticksstones12a  42117  sticksstones12  42118  sticksstones22  42128  aks6d1c7lem1  42140  metakunt2  42166  metakunt4  42168  metakunt12  42176  fltnltalem  42635  lzunuz  42742  lzenom  42744  ltrmxnn0  42924  jm2.17a  42935  jm2.17b  42936  jm2.17c  42937  jm2.24  42938  rmygeid  42939  jm2.25  42974  jm2.27a  42980  jm3.1lem1  42992  expdiophlem1  42996  monoords  45266  fmul01lt1lem1  45556  climsuselem1  45579  sumnnodd  45602  supcnvlimsup  45712  ioodvbdlimc1lem2  45904  ioodvbdlimc2lem  45906  dvnmul  45915  iblspltprt  45945  itgspltprt  45951  stoweidlem26  45998  wallispilem4  46040  stirlinglem4  46049  stirlinglem8  46053  stirlinglem11  46056  stirlinglem13  46058  dirkertrigeqlem1  46070  dirkercncflem2  46076  fourierdlem11  46090  fourierdlem12  46091  fourierdlem15  46094  fourierdlem41  46120  fourierdlem50  46128  fourierdlem64  46142  fourierdlem65  46143  fourierdlem79  46157  caratheodorylem1  46498  smflimsuplem4  46795  ormkglobd  46847  natglobalincr  46849  iccpartgtprec  47365  iccpartiltu  47367  iccpartgt  47372  iccpartnel  47383  fmtnodvds  47489  fmtnoprmfac2lem1  47511  evenp1odd  47585  oddp1eveni  47586  opoeALTV  47628  evenltle  47662  perfectALTV  47668  gpgedgel  47965  gpgvtx0  47966  fllogbd  48439  nnpw2blen  48459  dignn0flhalflem2  48495  nn0sumshdiglemA  48498  aacllem  49328