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

Theorem peano2re 9199
Description: A theorem for reals analogous the second Peano postulate peano2nn 9972. (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 9050 . 2  |-  1  e.  RR
2 readdcl 9033 . 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 1721  (class class class)co 6044   RRcr 8949   1c1 8951    + caddc 8953
This theorem is referenced by:  lep1  9809  letrp1  9812  p1le  9813  ledivp1  9872  sup2  9924  nnssre  9964  nnge1  9986  zltp1le  10285  suprzcl  10309  zeo  10315  peano2uz2  10317  uzind  10321  numltc  10362  uzwo  10499  uzwoOLD  10500  ge0p1rp  10600  qbtwnxr  10746  xrsupsslem  10845  supxrunb1  10858  fzp1disj  11065  fzneuz  11087  fllep1  11169  flhalf  11190  ceim1l  11193  uzsup  11203  fsequb  11273  seqf1olem1  11321  seqf1olem2  11322  bernneq3  11466  expnbnd  11467  expmulnbnd  11470  discr1  11474  discr  11475  facwordi  11539  faclbnd  11540  hashfun  11659  seqcoll2  11672  rexuzre  12115  caubnd  12121  rlim2lt  12250  lo1bddrp  12278  rlimo1  12369  o1rlimmul  12371  o1fsum  12551  harmonic  12597  expcnv  12602  geomulcvg  12612  mertenslem1  12620  nonsq  13110  eulerthlem2  13130  pcprendvds  13173  pcmpt  13220  pcfac  13227  vdwlem6  13313  vdwlem11  13318  tgioo  18784  zcld  18801  iocopnst  18922  cnheibor  18937  bndth  18940  cncmet  19232  pjthlem1  19295  ovolicc2lem3  19372  ovolicopnf  19377  ioorcl2  19421  dyadf  19440  dyadovol  19442  dyadss  19443  dyaddisjlem  19444  dyadmaxlem  19446  opnmbllem  19450  volsup2  19454  vitalilem2  19458  itg2const2  19590  itg2cnlem1  19610  dvfsumle  19862  dvfsumabs  19864  dvfsumlem1  19867  dvfsumlem3  19869  dvfsumrlim  19872  fta1glem2  20046  fta1lem  20181  aalioulem3  20208  ulmbdd  20271  itgulm  20281  psercnlem1  20298  abelthlem2  20305  abelthlem7  20311  reeff1olem  20319  logtayl  20508  loglesqr  20599  atanlogsublem  20712  leibpi  20739  efrlim  20765  harmonicubnd  20805  fsumharmonic  20807  ftalem5  20816  basellem2  20821  basellem3  20822  chtnprm  20894  chpp1  20895  ppip1le  20901  ppiub  20945  logfaclbnd  20963  logfacrlim  20965  perfectlem2  20971  bcmono  21018  lgsvalmod  21056  lgseisen  21094  lgsquadlem1  21095  lgsquadlem2  21096  chebbnd1lem2  21121  chtppilimlem1  21124  rplogsumlem2  21136  dchrisumlema  21139  dchrisumlem1  21140  dchrisumlem3  21142  dchrisum0lem1  21167  chpdifbndlem1  21204  logdivbnd  21207  pntrmax  21215  pntrsumo1  21216  pntpbnd1a  21236  pntpbnd1  21237  pntpbnd2  21238  pntibndlem2  21242  pntlemg  21249  pntlemr  21253  pntlemj  21254  pntlemk  21257  ostth2lem1  21269  qabvle  21276  ostth2lem3  21286  ostth2lem4  21287  eupath2lem3  21658  eupath2  21659  smcnlem  22150  minvecolem4  22339  pjhthlem1  22850  cvmliftlem7  24935  fznatpl1  25155  fzp1nel  25167  axlowdimlem16  25804  bpoly4  26013  ltflcei  26144  lxflflp1  26146  mblfinlem  26147  mblfinlem3  26149  itg2addnclem2  26160  itg2addnclem3  26161  incsequz  26346  isbnd3  26387  rrntotbnd  26439  irrapxlem4  26782  pellexlem5  26790  pell14qrgapw  26833  pellfundgt1  26840  jm3.1lem2  26983  expdiophlem1  26986  fmul01lt1lem1  27585
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389  ax-1cn 9008  ax-icn 9009  ax-addcl 9010  ax-addrcl 9011  ax-mulcl 9012  ax-mulrcl 9013  ax-i2m1 9018  ax-1ne0 9019  ax-rrecex 9022  ax-cnre 9023
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 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ne 2573  df-ral 2675  df-rex 2676  df-rab 2679  df-v 2922  df-dif 3287  df-un 3289  df-in 3291  df-ss 3298  df-nul 3593  df-if 3704  df-sn 3784  df-pr 3785  df-op 3787  df-uni 3980  df-br 4177  df-iota 5381  df-fv 5425  df-ov 6047
  Copyright terms: Public domain W3C validator