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

Theorem peano2re 9277
Description: A theorem for reals analogous the second Peano postulate peano2nn 10050. (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 9128 . 2  |-  1  e.  RR
2 readdcl 9111 . 2  |-  ( ( A  e.  RR  /\  1  e.  RR )  ->  ( A  +  1 )  e.  RR )
31, 2mpan2 654 1  |-  ( A  e.  RR  ->  ( A  +  1 )  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1728  (class class class)co 6117   RRcr 9027   1c1 9029    + caddc 9031
This theorem is referenced by:  lep1  9887  letrp1  9890  p1le  9891  ledivp1  9950  sup2  10002  nnssre  10042  nnge1  10064  zltp1le  10363  suprzcl  10387  zeo  10393  peano2uz2  10395  uzind  10399  numltc  10440  uzwo  10577  uzwoOLD  10578  ge0p1rp  10678  qbtwnxr  10824  xrsupsslem  10923  supxrunb1  10936  fzp1disj  11143  fzneuz  11166  fllep1  11248  flhalf  11269  ceim1l  11272  uzsup  11282  fsequb  11352  seqf1olem1  11400  seqf1olem2  11401  bernneq3  11545  expnbnd  11546  expmulnbnd  11549  discr1  11553  discr  11554  facwordi  11618  faclbnd  11619  hashfun  11738  seqcoll2  11751  rexuzre  12194  caubnd  12200  rlim2lt  12329  lo1bddrp  12357  rlimo1  12448  o1rlimmul  12450  o1fsum  12630  harmonic  12676  expcnv  12681  geomulcvg  12691  mertenslem1  12699  nonsq  13189  eulerthlem2  13209  pcprendvds  13252  pcmpt  13299  pcfac  13306  vdwlem6  13392  vdwlem11  13397  tgioo  18865  zcld  18882  iocopnst  19003  cnheibor  19018  bndth  19021  cncmet  19313  pjthlem1  19376  ovolicc2lem3  19453  ovolicopnf  19458  ioorcl2  19502  dyadf  19521  dyadovol  19523  dyadss  19524  dyaddisjlem  19525  dyadmaxlem  19527  opnmbllem  19531  volsup2  19535  vitalilem2  19539  itg2const2  19669  itg2cnlem1  19689  dvfsumle  19943  dvfsumabs  19945  dvfsumlem1  19948  dvfsumlem3  19950  dvfsumrlim  19953  fta1glem2  20127  fta1lem  20262  aalioulem3  20289  ulmbdd  20352  itgulm  20362  psercnlem1  20379  abelthlem2  20386  abelthlem7  20392  reeff1olem  20400  logtayl  20589  loglesqr  20680  atanlogsublem  20793  leibpi  20820  efrlim  20846  harmonicubnd  20886  fsumharmonic  20888  ftalem5  20897  basellem2  20902  basellem3  20903  chtnprm  20975  chpp1  20976  ppip1le  20982  ppiub  21026  logfaclbnd  21044  logfacrlim  21046  perfectlem2  21052  bcmono  21099  lgsvalmod  21137  lgseisen  21175  lgsquadlem1  21176  lgsquadlem2  21177  chebbnd1lem2  21202  chtppilimlem1  21205  rplogsumlem2  21217  dchrisumlema  21220  dchrisumlem1  21221  dchrisumlem3  21223  dchrisum0lem1  21248  chpdifbndlem1  21285  logdivbnd  21288  pntrmax  21296  pntrsumo1  21297  pntpbnd1a  21317  pntpbnd1  21318  pntpbnd2  21319  pntibndlem2  21323  pntlemg  21330  pntlemr  21334  pntlemj  21335  pntlemk  21338  ostth2lem1  21350  qabvle  21357  ostth2lem3  21367  ostth2lem4  21368  eupath2lem3  21739  eupath2  21740  smcnlem  22231  minvecolem4  22420  pjhthlem1  22931  cvmliftlem7  25013  fznatpl1  25233  fzp1nel  25245  axlowdimlem16  25931  bpoly4  26140  ltflcei  26275  lxflflp1  26277  opnmbllem0  26282  mblfinlem1  26283  mblfinlem2  26284  mblfinlem4  26286  dvtanlem  26296  itg2addnclem2  26299  itg2addnclem3  26300  incsequz  26494  isbnd3  26535  rrntotbnd  26587  irrapxlem4  27000  pellexlem5  27008  pell14qrgapw  27051  pellfundgt1  27058  jm3.1lem2  27201  expdiophlem1  27204  fmul01lt1lem1  27802  ltdifltdiv  28269
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424  ax-1cn 9086  ax-icn 9087  ax-addcl 9088  ax-addrcl 9089  ax-mulcl 9090  ax-mulrcl 9091  ax-i2m1 9096  ax-1ne0 9097  ax-rrecex 9100  ax-cnre 9101
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2717  df-rex 2718  df-rab 2721  df-v 2967  df-dif 3312  df-un 3314  df-in 3316  df-ss 3323  df-nul 3617  df-if 3768  df-sn 3849  df-pr 3850  df-op 3852  df-uni 4045  df-br 4244  df-iota 5453  df-fv 5497  df-ov 6120
  Copyright terms: Public domain W3C validator