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

Theorem peano2re 8985
Description: A theorem for reals analogous the second Peano postulate peano2nn 9758. (Contributed by NM, 5-Jul-2005.)
Assertion
Ref Expression
peano2re  |-  ( A  e.  RR  ->  ( A  +  1 )  e.  RR )

Proof of Theorem peano2re
StepHypRef Expression
1 1re 8837 . 2  |-  1  e.  RR
2 readdcl 8820 . 2  |-  ( ( A  e.  RR  /\  1  e.  RR )  ->  ( A  +  1 )  e.  RR )
31, 2mpan2 652 1  |-  ( A  e.  RR  ->  ( A  +  1 )  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684  (class class class)co 5858   RRcr 8736   1c1 8738    + caddc 8740
This theorem is referenced by:  lep1  9595  letrp1  9598  p1le  9599  ledivp1  9658  sup2  9710  nnssre  9750  nnge1  9772  zltp1le  10067  suprzcl  10091  zeo  10097  peano2uz2  10099  uzind  10103  numltc  10144  uzwo  10281  uzwoOLD  10282  ge0p1rp  10382  qbtwnxr  10527  xrsupsslem  10625  supxrunb1  10638  fzp1disj  10843  fzneuz  10863  fllep1  10933  flhalf  10954  ceim1l  10957  uzsup  10967  fsequb  11037  seqf1olem1  11085  seqf1olem2  11086  bernneq3  11229  expnbnd  11230  expmulnbnd  11233  discr1  11237  discr  11238  facwordi  11302  faclbnd  11303  hashfun  11389  seqcoll2  11402  rexuzre  11836  caubnd  11842  rlim2lt  11971  lo1bddrp  11999  rlimo1  12090  o1rlimmul  12092  o1fsum  12271  harmonic  12317  expcnv  12322  geomulcvg  12332  mertenslem1  12340  nonsq  12830  eulerthlem2  12850  pcprendvds  12893  pcmpt  12940  pcfac  12947  vdwlem6  13033  vdwlem11  13038  tgioo  18302  zcld  18319  iocopnst  18438  cnheibor  18453  bndth  18456  cncmet  18744  pjthlem1  18801  ovolicc2lem3  18878  ovolicopnf  18883  ioorcl2  18927  dyadf  18946  dyadovol  18948  dyadss  18949  dyaddisjlem  18950  dyadmaxlem  18952  opnmbllem  18956  volsup2  18960  vitalilem2  18964  itg2const2  19096  itg2cnlem1  19116  dvfsumle  19368  dvfsumabs  19370  dvfsumlem1  19373  dvfsumlem3  19375  dvfsumrlim  19378  fta1glem2  19552  fta1lem  19687  aalioulem3  19714  ulmbdd  19775  itgulm  19784  psercnlem1  19801  abelthlem2  19808  abelthlem7  19814  reeff1olem  19822  logtayl  20007  loglesqr  20098  atanlogsublem  20211  leibpi  20238  efrlim  20264  harmonicubnd  20303  fsumharmonic  20305  ftalem5  20314  basellem2  20319  basellem3  20320  chtnprm  20392  chpp1  20393  ppip1le  20399  ppiub  20443  logfaclbnd  20461  logfacrlim  20463  perfectlem2  20469  bcmono  20516  lgsvalmod  20554  lgseisen  20592  lgsquadlem1  20593  lgsquadlem2  20594  chebbnd1lem2  20619  chtppilimlem1  20622  rplogsumlem2  20634  dchrisumlema  20637  dchrisumlem1  20638  dchrisumlem3  20640  dchrisum0lem1  20665  chpdifbndlem1  20702  logdivbnd  20705  pntrmax  20713  pntrsumo1  20714  pntpbnd1a  20734  pntpbnd1  20735  pntpbnd2  20736  pntibndlem2  20740  pntlemg  20747  pntlemr  20751  pntlemj  20752  pntlemk  20755  ostth2lem1  20767  qabvle  20774  ostth2lem3  20784  ostth2lem4  20785  smcnlem  21270  minvecolem4  21459  pjhthlem1  21970  cvmliftlem7  23822  eupath2lem3  23903  eupath2  23904  fznatpl1  24093  axlowdimlem16  24585  bpoly4  24794  incsequz  26458  isbnd3  26508  rrntotbnd  26560  irrapxlem4  26910  pellexlem5  26918  pell14qrgapw  26961  pellfundgt1  26968  jm3.1lem2  27111  expdiophlem1  27114  fmul01lt1lem1  27714
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-1cn 8795  ax-icn 8796  ax-addcl 8797  ax-addrcl 8798  ax-mulcl 8799  ax-mulrcl 8800  ax-i2m1 8805  ax-1ne0 8806  ax-rrecex 8809  ax-cnre 8810
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-iota 5219  df-fv 5263  df-ov 5861
  Copyright terms: Public domain W3C validator