Theorem peano2zd 12630

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

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7361  1c1 11033   + caddc 11035  ℤcz 12518

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pow 5303  ax-pr 5371  ax-un 7683  ax-resscn 11089  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-addrcl 11093  ax-mulcl 11094  ax-mulrcl 11095  ax-mulcom 11096  ax-addass 11097  ax-mulass 11098  ax-distr 11099  ax-i2m1 11100  ax-1ne0 11101  ax-1rid 11102  ax-rnegex 11103  ax-rrecex 11104  ax-cnre 11105  ax-pre-lttri 11106  ax-pre-lttrn 11107  ax-pre-ltadd 11108  ax-pre-mulgt0 11109

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6260  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-riota 7318  df-ov 7364  df-oprab 7365  df-mpo 7366  df-om 7812  df-2nd 7937  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11175  df-mnf 11176  df-xr 11177  df-ltxr 11178  df-le 11179  df-sub 11373  df-neg 11374  df-nn 12169  df-n0 12432  df-z 12519

This theorem is referenced by:  rpnnen1lem5  12925  fznatpl1  13526  elfzom1elp1fzo1  13716  flge  13758  2tnp1ge0ge0  13782  uzsup  13816  seqf1olem1  13997  bcp1nk  14273  bcval5  14274  cshimadifsn0  14786  rexuzre  15309  limsupgre  15437  rlimclim1  15501  iseraltlem2  15639  telfsumo  15759  fsumparts  15763  climcnds  15810  geo2sum  15832  clim2prod  15847  clim2div  15848  fprodntriv  15901  dvdsfac  16289  2tp1odd  16315  opoe  16326  bits0o  16393  bitsp1o  16396  bitsinv1lem  16404  smupvallem  16446  smueqlem  16453  hashdvds  16739  prmreclem4  16884  prmreclem5  16885  vdwnnlem3  16962  prmgaplem7  17022  prmgaplem8  17023  chnub  18582  sylow1lem1  19567  telgsumfzs  19958  srgbinomlem3  20203  chfacfscmul0  22836  chfacfpmmul0  22840  ovoliunlem2  25483  ovolicc2lem4  25500  uniioombllem3  25565  dyaddisjlem  25575  dvfsumlem1  26006  dvfsumlem3  26008  plyco0  26170  abelthlem6  26417  birthdaylem2  26932  wilthlem1  27048  wilth  27051  wilthimp  27052  basellem3  27063  chpp1  27135  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  29043  crctcshwlkn0lem3  29898  crctcshwlkn0lem6  29901  clwwlkf  30135  eucrct2eupth  30333  cycpmco2lem3  33207  cycpmco2lem4  33208  cycpmco2lem5  33209  cycpmco2lem6  33210  cycpmco2  33212  isarchi3  33266  archirngz  33268  archiabllem1a  33270  archiabllem2c  33274  submateqlem1  33970  ballotlemsf1o  34677  ballotlemsima  34679  signstfvn  34732  fsum2dsub  34770  breprexplemc  34795  dnizphlfeqhlf  36755  dnibndlem13  36769  knoppndvlem10  36800  knoppndvlem14  36804  knoppndvlem15  36805  knoppndvlem17  36807  ltflcei  37946  poimirlem2  37960  poimirlem10  37968  poimirlem15  37973  poimirlem19  37977  poimirlem23  37981  poimirlem28  37986  fdc  38083  incsequz  38086  cntotbnd  38134  lcmineqlem11  42495  lcmineqlem18  42502  lcmineqlem22  42506  aks4d1p7d1  42538  aks6d1c1  42572  2np3bcnp1  42600  sticksstones6  42607  sticksstones7  42608  sticksstones10  42611  sticksstones12a  42613  sticksstones12  42614  sticksstones22  42624  aks6d1c7lem1  42636  fltnltalem  43112  lzunuz  43217  lzenom  43219  ltrmxnn0  43398  jm2.17a  43409  jm2.17b  43410  jm2.17c  43411  jm2.24  43412  rmygeid  43413  jm2.25  43448  jm2.27a  43454  jm3.1lem1  43466  expdiophlem1  43470  monoords  45751  fmul01lt1lem1  46035  climsuselem1  46058  sumnnodd  46081  supcnvlimsup  46189  ioodvbdlimc1lem2  46381  ioodvbdlimc2lem  46383  dvnmul  46392  iblspltprt  46422  itgspltprt  46428  stoweidlem26  46475  wallispilem4  46517  stirlinglem4  46526  stirlinglem8  46530  stirlinglem11  46533  stirlinglem13  46535  dirkertrigeqlem1  46547  dirkercncflem2  46553  fourierdlem11  46567  fourierdlem12  46568  fourierdlem15  46571  fourierdlem41  46597  fourierdlem50  46605  fourierdlem64  46619  fourierdlem65  46620  fourierdlem79  46634  caratheodorylem1  46975  smflimsuplem4  47272  ormkglobd  47324  natglobalincr  47326  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