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

Theorem peano2re 9132
Description: A theorem for reals analogous the second Peano postulate peano2nn 9905. (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 8984 . 2  |-  1  e.  RR
2 readdcl 8967 . 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 1715  (class class class)co 5981   RRcr 8883   1c1 8885    + caddc 8887
This theorem is referenced by:  lep1  9742  letrp1  9745  p1le  9746  ledivp1  9805  sup2  9857  nnssre  9897  nnge1  9919  zltp1le  10218  suprzcl  10242  zeo  10248  peano2uz2  10250  uzind  10254  numltc  10295  uzwo  10432  uzwoOLD  10433  ge0p1rp  10533  qbtwnxr  10679  xrsupsslem  10778  supxrunb1  10791  fzp1disj  10996  fzneuz  11018  fllep1  11097  flhalf  11118  ceim1l  11121  uzsup  11131  fsequb  11201  seqf1olem1  11249  seqf1olem2  11250  bernneq3  11394  expnbnd  11395  expmulnbnd  11398  discr1  11402  discr  11403  facwordi  11467  faclbnd  11468  hashfun  11587  seqcoll2  11600  rexuzre  12043  caubnd  12049  rlim2lt  12178  lo1bddrp  12206  rlimo1  12297  o1rlimmul  12299  o1fsum  12479  harmonic  12525  expcnv  12530  geomulcvg  12540  mertenslem1  12548  nonsq  13038  eulerthlem2  13058  pcprendvds  13101  pcmpt  13148  pcfac  13155  vdwlem6  13241  vdwlem11  13246  tgioo  18515  zcld  18532  iocopnst  18653  cnheibor  18668  bndth  18671  cncmet  18959  pjthlem1  19016  ovolicc2lem3  19093  ovolicopnf  19098  ioorcl2  19142  dyadf  19161  dyadovol  19163  dyadss  19164  dyaddisjlem  19165  dyadmaxlem  19167  opnmbllem  19171  volsup2  19175  vitalilem2  19179  itg2const2  19311  itg2cnlem1  19331  dvfsumle  19583  dvfsumabs  19585  dvfsumlem1  19588  dvfsumlem3  19590  dvfsumrlim  19593  fta1glem2  19767  fta1lem  19902  aalioulem3  19929  ulmbdd  19992  itgulm  20002  psercnlem1  20019  abelthlem2  20026  abelthlem7  20032  reeff1olem  20040  logtayl  20229  loglesqr  20320  atanlogsublem  20433  leibpi  20460  efrlim  20486  harmonicubnd  20526  fsumharmonic  20528  ftalem5  20537  basellem2  20542  basellem3  20543  chtnprm  20615  chpp1  20616  ppip1le  20622  ppiub  20666  logfaclbnd  20684  logfacrlim  20686  perfectlem2  20692  bcmono  20739  lgsvalmod  20777  lgseisen  20815  lgsquadlem1  20816  lgsquadlem2  20817  chebbnd1lem2  20842  chtppilimlem1  20845  rplogsumlem2  20857  dchrisumlema  20860  dchrisumlem1  20861  dchrisumlem3  20863  dchrisum0lem1  20888  chpdifbndlem1  20925  logdivbnd  20928  pntrmax  20936  pntrsumo1  20937  pntpbnd1a  20957  pntpbnd1  20958  pntpbnd2  20959  pntibndlem2  20963  pntlemg  20970  pntlemr  20974  pntlemj  20975  pntlemk  20978  ostth2lem1  20990  qabvle  20997  ostth2lem3  21007  ostth2lem4  21008  smcnlem  21583  minvecolem4  21772  pjhthlem1  22283  cvmliftlem7  24425  eupath2lem3  24490  eupath2  24491  fznatpl1  24682  fzp1nel  24694  axlowdimlem16  25327  bpoly4  25536  ltflcei  25668  lxflflp1  25670  itg2addnclem2  25676  itg2addnc  25677  incsequz  25965  isbnd3  26014  rrntotbnd  26066  irrapxlem4  26416  pellexlem5  26424  pell14qrgapw  26467  pellfundgt1  26474  jm3.1lem2  26617  expdiophlem1  26620  fmul01lt1lem1  27220
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347  ax-1cn 8942  ax-icn 8943  ax-addcl 8944  ax-addrcl 8945  ax-mulcl 8946  ax-mulrcl 8947  ax-i2m1 8952  ax-1ne0 8953  ax-rrecex 8956  ax-cnre 8957
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 937  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-ne 2531  df-ral 2633  df-rex 2634  df-rab 2637  df-v 2875  df-dif 3241  df-un 3243  df-in 3245  df-ss 3252  df-nul 3544  df-if 3655  df-sn 3735  df-pr 3736  df-op 3738  df-uni 3930  df-br 4126  df-iota 5322  df-fv 5366  df-ov 5984
  Copyright terms: Public domain W3C validator