MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  peano2zd Structured version   Visualization version   Unicode version

Theorem peano2zd 11077
Description: Deduction from second Peano postulate generalized to integers. (Contributed by Mario Carneiro, 28-May-2016.)
Hypothesis
Ref Expression
zred.1  |-  ( ph  ->  A  e.  ZZ )
Assertion
Ref Expression
peano2zd  |-  ( ph  ->  ( A  +  1 )  e.  ZZ )

Proof of Theorem peano2zd
StepHypRef Expression
1 zred.1 . 2  |-  ( ph  ->  A  e.  ZZ )
2 peano2z 11012 . 2  |-  ( A  e.  ZZ  ->  ( A  +  1 )  e.  ZZ )
31, 2syl 17 1  |-  ( ph  ->  ( A  +  1 )  e.  ZZ )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1898  (class class class)co 6320   1c1 9571    + caddc 9573   ZZcz 10971
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-un 6615  ax-resscn 9627  ax-1cn 9628  ax-icn 9629  ax-addcl 9630  ax-addrcl 9631  ax-mulcl 9632  ax-mulrcl 9633  ax-mulcom 9634  ax-addass 9635  ax-mulass 9636  ax-distr 9637  ax-i2m1 9638  ax-1ne0 9639  ax-1rid 9640  ax-rnegex 9641  ax-rrecex 9642  ax-cnre 9643  ax-pre-lttri 9644  ax-pre-lttrn 9645  ax-pre-ltadd 9646  ax-pre-mulgt0 9647
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-iun 4294  df-br 4419  df-opab 4478  df-mpt 4479  df-tr 4514  df-eprel 4767  df-id 4771  df-po 4777  df-so 4778  df-fr 4815  df-we 4817  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869  df-pred 5403  df-ord 5449  df-on 5450  df-lim 5451  df-suc 5452  df-iota 5569  df-fun 5607  df-fn 5608  df-f 5609  df-f1 5610  df-fo 5611  df-f1o 5612  df-fv 5613  df-riota 6282  df-ov 6323  df-oprab 6324  df-mpt2 6325  df-om 6725  df-wrecs 7059  df-recs 7121  df-rdg 7159  df-er 7394  df-en 7601  df-dom 7602  df-sdom 7603  df-pnf 9708  df-mnf 9709  df-xr 9710  df-ltxr 9711  df-le 9712  df-sub 9893  df-neg 9894  df-nn 10643  df-n0 10904  df-z 10972
This theorem is referenced by:  rpnnen1lem5  11328  fznatpl1  11885  flge  12079  uzsup  12128  seqf1olem1  12290  bcp1nk  12540  bcval5  12541  rexuzre  13470  limsupgre  13597  limsupgreOLD  13598  rlimclim1  13664  iseraltlem2  13804  telfsumo  13917  fsumparts  13921  climcnds  13964  geo2sum  13984  clim2prod  13999  clim2div  14000  fprodntriv  14051  dvdsfac  14415  bits0o  14458  bitsp1o  14461  bitsinv1lem  14470  smupvallem  14512  smueqlem  14519  hashdvds  14778  opoe  14816  prmreclem4  14918  prmreclem5  14919  vdwnnlem3  15002  prmgaplem7  15082  prmgaplem8  15083  sylow1lem1  17305  telgsumfzs  17674  srgbinomlem3  17830  chfacfscmul0  19937  chfacfpmmul0  19941  ovoliunlem2  22511  ovolicc2lem4OLD  22528  ovolicc2lem4  22529  uniioombllem3  22599  dyaddisjlem  22609  dvfsumlem1  23034  dvfsumlem3  23036  plyco0  23202  abelthlem6  23447  birthdaylem2  23934  wilthlem1  24049  wilth  24052  basellem3  24065  chpp1  24138  perfect  24215  bcmono  24261  lgslem1  24280  lgsval2lem  24290  lgseisenlem1  24333  lgsquadlem1  24338  m1lgs  24346  2sqblem  24361  rplogsumlem2  24379  rpvmasumlem  24381  dchrisumlema  24382  dchrisumlem2  24384  pntpbnd1  24480  pntpbnd2  24481  pntlemq  24495  pntlemr  24496  pntlemj  24497  pntlemf  24499  axlowdimlem16  25043  wwlkextproplem1  25525  clwwlkf  25578  eupath2lem3  25763  isarchi3  28555  archirngz  28557  archiabllem1a  28559  archiabllem2c  28563  submateqlem1  28684  ballotlemsf1o  29396  ballotlemsima  29398  ballotlemsf1oOLD  29434  ballotlemsimaOLD  29436  signstfvn  29508  ltflcei  31979  poimirlem2  31988  poimirlem10  31996  poimirlem15  32001  poimirlem19  32005  poimirlem23  32009  poimirlem28  32014  fdc  32120  incsequz  32123  cntotbnd  32174  lzunuz  35656  lzenom  35658  ltrmxnn0  35845  jm2.17a  35856  jm2.17b  35857  jm2.17c  35858  jm2.24  35859  rmygeid  35860  jm2.25  35900  jm2.27a  35906  jm3.1lem1  35918  expdiophlem1  35922  monoords  37589  fmul01lt1lem1  37748  climsuselem1  37772  sumnnodd  37796  ioodvbdlimc1lem2  37890  ioodvbdlimc1lem2OLD  37892  ioodvbdlimc2lem  37894  ioodvbdlimc2lemOLD  37895  dvnmul  37904  iblspltprt  37936  itgspltprt  37942  stoweidlem26  37987  wallispilem4  38031  stirlinglem4  38040  stirlinglem8  38044  stirlinglem11  38047  stirlinglem13  38049  dirkertrigeqlem1  38061  dirkercncflem2  38067  fourierdlem11  38081  fourierdlem12  38082  fourierdlem15  38085  fourierdlem41  38112  fourierdlem50  38121  fourierdlem64  38135  fourierdlem65  38136  fourierdlem79  38150  caratheodorylem1  38455  iccpartgtprec  38869  iccpartiltu  38871  iccpartgt  38876  iccpartnel  38887  evenp1odd  38905  oddp1eveni  38906  opoeALTV  38947  perfectALTV  38980  fllogbd  40740  nnpw2blen  40760  dignn0flhalflem2  40796  nn0sumshdiglemA  40799  aacllem  40909
  Copyright terms: Public domain W3C validator