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

Theorem peano2re 9172
Description: A theorem for reals analogous the second Peano postulate peano2nn 9945. (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 9024 . 2  |-  1  e.  RR
2 readdcl 9007 . 2  |-  ( ( A  e.  RR  /\  1  e.  RR )  ->  ( A  +  1 )  e.  RR )
31, 2mpan2 653 1  |-  ( A  e.  RR  ->  ( A  +  1 )  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1717  (class class class)co 6021   RRcr 8923   1c1 8925    + caddc 8927
This theorem is referenced by:  lep1  9782  letrp1  9785  p1le  9786  ledivp1  9845  sup2  9897  nnssre  9937  nnge1  9959  zltp1le  10258  suprzcl  10282  zeo  10288  peano2uz2  10290  uzind  10294  numltc  10335  uzwo  10472  uzwoOLD  10473  ge0p1rp  10573  qbtwnxr  10719  xrsupsslem  10818  supxrunb1  10831  fzp1disj  11037  fzneuz  11059  fllep1  11138  flhalf  11159  ceim1l  11162  uzsup  11172  fsequb  11242  seqf1olem1  11290  seqf1olem2  11291  bernneq3  11435  expnbnd  11436  expmulnbnd  11439  discr1  11443  discr  11444  facwordi  11508  faclbnd  11509  hashfun  11628  seqcoll2  11641  rexuzre  12084  caubnd  12090  rlim2lt  12219  lo1bddrp  12247  rlimo1  12338  o1rlimmul  12340  o1fsum  12520  harmonic  12566  expcnv  12571  geomulcvg  12581  mertenslem1  12589  nonsq  13079  eulerthlem2  13099  pcprendvds  13142  pcmpt  13189  pcfac  13196  vdwlem6  13282  vdwlem11  13287  tgioo  18699  zcld  18716  iocopnst  18837  cnheibor  18852  bndth  18855  cncmet  19145  pjthlem1  19206  ovolicc2lem3  19283  ovolicopnf  19288  ioorcl2  19332  dyadf  19351  dyadovol  19353  dyadss  19354  dyaddisjlem  19355  dyadmaxlem  19357  opnmbllem  19361  volsup2  19365  vitalilem2  19369  itg2const2  19501  itg2cnlem1  19521  dvfsumle  19773  dvfsumabs  19775  dvfsumlem1  19778  dvfsumlem3  19780  dvfsumrlim  19783  fta1glem2  19957  fta1lem  20092  aalioulem3  20119  ulmbdd  20182  itgulm  20192  psercnlem1  20209  abelthlem2  20216  abelthlem7  20222  reeff1olem  20230  logtayl  20419  loglesqr  20510  atanlogsublem  20623  leibpi  20650  efrlim  20676  harmonicubnd  20716  fsumharmonic  20718  ftalem5  20727  basellem2  20732  basellem3  20733  chtnprm  20805  chpp1  20806  ppip1le  20812  ppiub  20856  logfaclbnd  20874  logfacrlim  20876  perfectlem2  20882  bcmono  20929  lgsvalmod  20967  lgseisen  21005  lgsquadlem1  21006  lgsquadlem2  21007  chebbnd1lem2  21032  chtppilimlem1  21035  rplogsumlem2  21047  dchrisumlema  21050  dchrisumlem1  21051  dchrisumlem3  21053  dchrisum0lem1  21078  chpdifbndlem1  21115  logdivbnd  21118  pntrmax  21126  pntrsumo1  21127  pntpbnd1a  21147  pntpbnd1  21148  pntpbnd2  21149  pntibndlem2  21153  pntlemg  21160  pntlemr  21164  pntlemj  21165  pntlemk  21168  ostth2lem1  21180  qabvle  21187  ostth2lem3  21197  ostth2lem4  21198  eupath2lem3  21550  eupath2  21551  smcnlem  22042  minvecolem4  22231  pjhthlem1  22742  cvmliftlem7  24758  fznatpl1  24978  fzp1nel  24990  axlowdimlem16  25611  bpoly4  25820  ltflcei  25951  lxflflp1  25953  itg2addnclem2  25959  itg2addnc  25960  incsequz  26144  isbnd3  26185  rrntotbnd  26237  irrapxlem4  26580  pellexlem5  26588  pell14qrgapw  26631  pellfundgt1  26638  jm3.1lem2  26781  expdiophlem1  26784  fmul01lt1lem1  27383
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369  ax-1cn 8982  ax-icn 8983  ax-addcl 8984  ax-addrcl 8985  ax-mulcl 8986  ax-mulrcl 8987  ax-i2m1 8992  ax-1ne0 8993  ax-rrecex 8996  ax-cnre 8997
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-ne 2553  df-ral 2655  df-rex 2656  df-rab 2659  df-v 2902  df-dif 3267  df-un 3269  df-in 3271  df-ss 3278  df-nul 3573  df-if 3684  df-sn 3764  df-pr 3765  df-op 3767  df-uni 3959  df-br 4155  df-iota 5359  df-fv 5403  df-ov 6024
  Copyright terms: Public domain W3C validator