Theorem peano2zd 12084

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

Syntax hints:   → wi 4   ∈ wcel 2110  (class class class)co 7150  1c1 10532   + caddc 10534  ℤcz 11975

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793  ax-sep 5196  ax-nul 5203  ax-pow 5259  ax-pr 5322  ax-un 7455  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607  ax-pre-mulgt0 10608

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3497  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4562  df-pr 4564  df-tp 4566  df-op 4568  df-uni 4833  df-iun 4914  df-br 5060  df-opab 5122  df-mpt 5140  df-tr 5166  df-id 5455  df-eprel 5460  df-po 5469  df-so 5470  df-fr 5509  df-we 5511  df-xp 5556  df-rel 5557  df-cnv 5558  df-co 5559  df-dm 5560  df-rn 5561  df-res 5562  df-ima 5563  df-pred 6143  df-ord 6189  df-on 6190  df-lim 6191  df-suc 6192  df-iota 6309  df-fun 6352  df-fn 6353  df-f 6354  df-f1 6355  df-fo 6356  df-f1o 6357  df-fv 6358  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7575  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-er 8283  df-en 8504  df-dom 8505  df-sdom 8506  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-sub 10866  df-neg 10867  df-nn 11633  df-n0 11892  df-z 11976

This theorem is referenced by:  rpnnen1lem5  12374  fznatpl1  12955  elfzom1elp1fzo1  13131  flge  13169  2tnp1ge0ge0  13193  uzsup  13225  seqf1olem1  13403  bcp1nk  13671  bcval5  13672  cshimadifsn0  14186  rexuzre  14706  limsupgre  14832  rlimclim1  14896  iseraltlem2  15033  telfsumo  15151  fsumparts  15155  climcnds  15200  geo2sum  15223  clim2prod  15238  clim2div  15239  fprodntriv  15290  dvdsfac  15670  2tp1odd  15695  opoe  15706  bits0o  15773  bitsp1o  15776  bitsinv1lem  15784  smupvallem  15826  smueqlem  15833  hashdvds  16106  prmreclem4  16249  prmreclem5  16250  vdwnnlem3  16327  prmgaplem7  16387  prmgaplem8  16388  sylow1lem1  18717  telgsumfzs  19103  srgbinomlem3  19286  chfacfscmul0  21460  chfacfpmmul0  21464  ovoliunlem2  24098  ovolicc2lem4  24115  uniioombllem3  24180  dyaddisjlem  24190  dvfsumlem1  24617  dvfsumlem3  24619  plyco0  24776  abelthlem6  25018  birthdaylem2  25524  wilthlem1  25639  wilth  25642  wilthimp  25643  basellem3  25654  chpp1  25726  perfect  25801  bcmono  25847  lgslem1  25867  lgsval2lem  25877  gausslemma2dlem5  25941  lgseisenlem1  25945  lgsquadlem1  25950  m1lgs  25958  2lgslem1a  25961  2lgslem3c  25968  2lgslem3d  25969  2lgslem3b1  25971  2lgslem3c1  25972  2sqblem  26001  rplogsumlem2  26055  rpvmasumlem  26057  dchrisumlema  26058  dchrisumlem2  26060  pntpbnd1  26156  pntpbnd2  26157  pntlemq  26171  pntlemr  26172  pntlemj  26173  pntlemf  26175  axlowdimlem16  26737  crctcshwlkn0lem3  27584  crctcshwlkn0lem6  27587  clwwlkf  27820  eucrct2eupth  28018  cycpmco2lem3  30765  cycpmco2lem4  30766  cycpmco2lem5  30767  cycpmco2lem6  30768  cycpmco2  30770  isarchi3  30811  archirngz  30813  archiabllem1a  30815  archiabllem2c  30819  submateqlem1  31067  ballotlemsf1o  31766  ballotlemsima  31768  signstfvn  31834  fsum2dsub  31873  breprexplemc  31898  dnizphlfeqhlf  33810  dnibndlem13  33824  knoppndvlem10  33855  knoppndvlem14  33859  knoppndvlem15  33860  knoppndvlem17  33862  ltflcei  34874  poimirlem2  34888  poimirlem10  34896  poimirlem15  34901  poimirlem19  34905  poimirlem23  34909  poimirlem28  34914  fdc  35014  incsequz  35017  cntotbnd  35068  fltnltalem  39267  lzunuz  39358  lzenom  39360  ltrmxnn0  39539  jm2.17a  39550  jm2.17b  39551  jm2.17c  39552  jm2.24  39553  rmygeid  39554  jm2.25  39589  jm2.27a  39595  jm3.1lem1  39607  expdiophlem1  39611  monoords  41556  fmul01lt1lem1  41857  climsuselem1  41880  sumnnodd  41903  supcnvlimsup  42013  ioodvbdlimc1lem2  42209  ioodvbdlimc2lem  42211  dvnmul  42220  iblspltprt  42250  itgspltprt  42256  stoweidlem26  42304  wallispilem4  42346  stirlinglem4  42355  stirlinglem8  42359  stirlinglem11  42362  stirlinglem13  42364  dirkertrigeqlem1  42376  dirkercncflem2  42382  fourierdlem11  42396  fourierdlem12  42397  fourierdlem15  42400  fourierdlem41  42426  fourierdlem50  42434  fourierdlem64  42448  fourierdlem65  42449  fourierdlem79  42463  caratheodorylem1  42801  smflimsuplem4  43090  iccpartgtprec  43573  iccpartiltu  43575  iccpartgt  43580  iccpartnel  43591  fmtnodvds  43699  fmtnoprmfac2lem1  43721  evenp1odd  43798  oddp1eveni  43799  opoeALTV  43841  evenltle  43875  perfectALTV  43881  fllogbd  44613  nnpw2blen  44633  dignn0flhalflem2  44669  nn0sumshdiglemA  44672  aacllem  44895