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

Theorem peano2re 9229
Description: A theorem for reals analogous the second Peano postulate peano2nn 10002. (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 9080 . 2  |-  1  e.  RR
2 readdcl 9063 . 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 1725  (class class class)co 6073   RRcr 8979   1c1 8981    + caddc 8983
This theorem is referenced by:  lep1  9839  letrp1  9842  p1le  9843  ledivp1  9902  sup2  9954  nnssre  9994  nnge1  10016  zltp1le  10315  suprzcl  10339  zeo  10345  peano2uz2  10347  uzind  10351  numltc  10392  uzwo  10529  uzwoOLD  10530  ge0p1rp  10630  qbtwnxr  10776  xrsupsslem  10875  supxrunb1  10888  fzp1disj  11095  fzneuz  11118  fllep1  11200  flhalf  11221  ceim1l  11224  uzsup  11234  fsequb  11304  seqf1olem1  11352  seqf1olem2  11353  bernneq3  11497  expnbnd  11498  expmulnbnd  11501  discr1  11505  discr  11506  facwordi  11570  faclbnd  11571  hashfun  11690  seqcoll2  11703  rexuzre  12146  caubnd  12152  rlim2lt  12281  lo1bddrp  12309  rlimo1  12400  o1rlimmul  12402  o1fsum  12582  harmonic  12628  expcnv  12633  geomulcvg  12643  mertenslem1  12651  nonsq  13141  eulerthlem2  13161  pcprendvds  13204  pcmpt  13251  pcfac  13258  vdwlem6  13344  vdwlem11  13349  tgioo  18817  zcld  18834  iocopnst  18955  cnheibor  18970  bndth  18973  cncmet  19265  pjthlem1  19328  ovolicc2lem3  19405  ovolicopnf  19410  ioorcl2  19454  dyadf  19473  dyadovol  19475  dyadss  19476  dyaddisjlem  19477  dyadmaxlem  19479  opnmbllem  19483  volsup2  19487  vitalilem2  19491  itg2const2  19623  itg2cnlem1  19643  dvfsumle  19895  dvfsumabs  19897  dvfsumlem1  19900  dvfsumlem3  19902  dvfsumrlim  19905  fta1glem2  20079  fta1lem  20214  aalioulem3  20241  ulmbdd  20304  itgulm  20314  psercnlem1  20331  abelthlem2  20338  abelthlem7  20344  reeff1olem  20352  logtayl  20541  loglesqr  20632  atanlogsublem  20745  leibpi  20772  efrlim  20798  harmonicubnd  20838  fsumharmonic  20840  ftalem5  20849  basellem2  20854  basellem3  20855  chtnprm  20927  chpp1  20928  ppip1le  20934  ppiub  20978  logfaclbnd  20996  logfacrlim  20998  perfectlem2  21004  bcmono  21051  lgsvalmod  21089  lgseisen  21127  lgsquadlem1  21128  lgsquadlem2  21129  chebbnd1lem2  21154  chtppilimlem1  21157  rplogsumlem2  21169  dchrisumlema  21172  dchrisumlem1  21173  dchrisumlem3  21175  dchrisum0lem1  21200  chpdifbndlem1  21237  logdivbnd  21240  pntrmax  21248  pntrsumo1  21249  pntpbnd1a  21269  pntpbnd1  21270  pntpbnd2  21271  pntibndlem2  21275  pntlemg  21282  pntlemr  21286  pntlemj  21287  pntlemk  21290  ostth2lem1  21302  qabvle  21309  ostth2lem3  21319  ostth2lem4  21320  eupath2lem3  21691  eupath2  21692  smcnlem  22183  minvecolem4  22372  pjhthlem1  22883  cvmliftlem7  24968  fznatpl1  25188  fzp1nel  25200  axlowdimlem16  25861  bpoly4  26070  ltflcei  26204  lxflflp1  26206  mblfinlem  26207  mblfinlem3  26209  itg2addnclem2  26220  itg2addnclem3  26221  incsequz  26406  isbnd3  26447  rrntotbnd  26499  irrapxlem4  26842  pellexlem5  26850  pell14qrgapw  26893  pellfundgt1  26900  jm3.1lem2  27043  expdiophlem1  27046  fmul01lt1lem1  27645  ltdifltdiv  28090
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-1cn 9038  ax-icn 9039  ax-addcl 9040  ax-addrcl 9041  ax-mulcl 9042  ax-mulrcl 9043  ax-i2m1 9048  ax-1ne0 9049  ax-rrecex 9052  ax-cnre 9053
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-iota 5410  df-fv 5454  df-ov 6076
  Copyright terms: Public domain W3C validator