Theorem peano2zd 12627

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

Syntax hints:   → wi 4   ∈ wcel 2119  (class class class)co 7356  1c1 11030   + caddc 11032  ℤcz 12515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-er 8633  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-nn 12166  df-n0 12429  df-z 12516

This theorem is referenced by:  rpnnen1lem5  12922  fznatpl1  13523  elfzom1elp1fzo1  13713  flge  13755  2tnp1ge0ge0  13779  uzsup  13813  seqf1olem1  13994  bcp1nk  14270  bcval5  14271  cshimadifsn0  14783  rexuzre  15306  limsupgre  15434  rlimclim1  15498  iseraltlem2  15636  telfsumo  15756  fsumparts  15760  climcnds  15807  geo2sum  15829  clim2prod  15844  clim2div  15845  fprodntriv  15898  dvdsfac  16286  2tp1odd  16312  opoe  16323  bits0o  16390  bitsp1o  16393  bitsinv1lem  16401  smupvallem  16443  smueqlem  16450  hashdvds  16736  prmreclem4  16881  prmreclem5  16882  vdwnnlem3  16959  prmgaplem7  17019  prmgaplem8  17020  chnub  18579  sylow1lem1  19564  telgsumfzs  19955  srgbinomlem3  20200  chfacfscmul0  22841  chfacfpmmul0  22845  ovoliunlem2  25488  ovolicc2lem4  25505  uniioombllem3  25570  dyaddisjlem  25580  dvfsumlem1  26011  dvfsumlem3  26013  plyco0  26175  abelthlem6  26419  birthdaylem2  26934  wilthlem1  27049  wilth  27052  wilthimp  27053  basellem3  27064  chpp1  27136  perfect  27212  bcmono  27258  lgslem1  27278  lgsval2lem  27288  gausslemma2dlem5  27352  lgseisenlem1  27356  lgsquadlem1  27361  m1lgs  27369  2lgslem1a  27372  2lgslem3c  27379  2lgslem3d  27380  2lgslem3b1  27382  2lgslem3c1  27383  2sqblem  27412  rplogsumlem2  27466  rpvmasumlem  27468  dchrisumlema  27469  dchrisumlem2  27471  pntpbnd1  27567  pntpbnd2  27568  pntlemq  27582  pntlemr  27583  pntlemj  27584  pntlemf  27586  axlowdimlem16  29044  crctcshwlkn0lem3  29898  crctcshwlkn0lem6  29901  clwwlkf  30135  eucrct2eupth  30333  cycpmco2lem3  33209  cycpmco2lem4  33210  cycpmco2lem5  33211  cycpmco2lem6  33212  cycpmco2  33214  isarchi3  33268  archirngz  33270  archiabllem1a  33272  archiabllem2c  33276  submateqlem1  33991  ballotlemsf1o  34698  ballotlemsima  34700  signstfvn  34753  fsum2dsub  34791  breprexplemc  34816  dnizphlfeqhlf  36782  dnibndlem13  36796  knoppndvlem10  36827  knoppndvlem14  36831  knoppndvlem15  36832  knoppndvlem17  36834  ltflcei  37975  poimirlem2  37989  poimirlem10  37997  poimirlem15  38002  poimirlem19  38006  poimirlem23  38010  poimirlem28  38015  fdc  38112  incsequz  38115  cntotbnd  38163  lcmineqlem11  42524  lcmineqlem18  42531  lcmineqlem22  42535  aks4d1p7d1  42567  aks6d1c1  42601  2np3bcnp1  42629  sticksstones6  42636  sticksstones7  42637  sticksstones10  42640  sticksstones12a  42642  sticksstones12  42643  sticksstones22  42653  aks6d1c7lem1  42665  fltnltalem  43112  lzunuz  43217  lzenom  43219  ltrmxnn0  43394  jm2.17a  43405  jm2.17b  43406  jm2.17c  43407  jm2.24  43408  rmygeid  43409  jm2.25  43444  jm2.27a  43450  jm3.1lem1  43462  expdiophlem1  43466  monoords  45745  fmul01lt1lem1  46029  climsuselem1  46052  sumnnodd  46075  supcnvlimsup  46183  ioodvbdlimc1lem2  46375  ioodvbdlimc2lem  46377  dvnmul  46386  iblspltprt  46416  itgspltprt  46422  stoweidlem26  46469  wallispilem4  46511  stirlinglem4  46520  stirlinglem8  46524  stirlinglem11  46527  stirlinglem13  46529  dirkertrigeqlem1  46541  dirkercncflem2  46547  fourierdlem11  46561  fourierdlem12  46562  fourierdlem15  46565  fourierdlem41  46591  fourierdlem50  46599  fourierdlem64  46613  fourierdlem65  46614  fourierdlem79  46628  caratheodorylem1  46969  smflimsuplem4  47266  ormkglobd  47320  natglobalincr  47322  iccpartgtprec  47895  iccpartiltu  47897  iccpartgt  47902  iccpartnel  47913  fmtnodvds  48022  fmtnoprmfac2lem1  48044  ppivalnnprm  48103  evenp1odd  48131  oddp1eveni  48132  opoeALTV  48174  evenltle  48208  perfectALTV  48214  gpgiedgdmellem  48537  gpgvtx0  48544  pgnbgreunbgrlem2lem2  48606  fllogbd  49051  nnpw2blen  49071  dignn0flhalflem2  49107  nn0sumshdiglemA  49110  aacllem  50291