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

Theorem peano2re 9270
Description: A theorem for reals analogous the second Peano postulate peano2nn 10043. (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 9121 . 2  |-  1  e.  RR
2 readdcl 9104 . 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 1727  (class class class)co 6110   RRcr 9020   1c1 9022    + caddc 9024
This theorem is referenced by:  lep1  9880  letrp1  9883  p1le  9884  ledivp1  9943  sup2  9995  nnssre  10035  nnge1  10057  zltp1le  10356  suprzcl  10380  zeo  10386  peano2uz2  10388  uzind  10392  numltc  10433  uzwo  10570  uzwoOLD  10571  ge0p1rp  10671  qbtwnxr  10817  xrsupsslem  10916  supxrunb1  10929  fzp1disj  11136  fzneuz  11159  fllep1  11241  flhalf  11262  ceim1l  11265  uzsup  11275  fsequb  11345  seqf1olem1  11393  seqf1olem2  11394  bernneq3  11538  expnbnd  11539  expmulnbnd  11542  discr1  11546  discr  11547  facwordi  11611  faclbnd  11612  hashfun  11731  seqcoll2  11744  rexuzre  12187  caubnd  12193  rlim2lt  12322  lo1bddrp  12350  rlimo1  12441  o1rlimmul  12443  o1fsum  12623  harmonic  12669  expcnv  12674  geomulcvg  12684  mertenslem1  12692  nonsq  13182  eulerthlem2  13202  pcprendvds  13245  pcmpt  13292  pcfac  13299  vdwlem6  13385  vdwlem11  13390  tgioo  18858  zcld  18875  iocopnst  18996  cnheibor  19011  bndth  19014  cncmet  19306  pjthlem1  19369  ovolicc2lem3  19446  ovolicopnf  19451  ioorcl2  19495  dyadf  19514  dyadovol  19516  dyadss  19517  dyaddisjlem  19518  dyadmaxlem  19520  opnmbllem  19524  volsup2  19528  vitalilem2  19532  itg2const2  19662  itg2cnlem1  19682  dvfsumle  19936  dvfsumabs  19938  dvfsumlem1  19941  dvfsumlem3  19943  dvfsumrlim  19946  fta1glem2  20120  fta1lem  20255  aalioulem3  20282  ulmbdd  20345  itgulm  20355  psercnlem1  20372  abelthlem2  20379  abelthlem7  20385  reeff1olem  20393  logtayl  20582  loglesqr  20673  atanlogsublem  20786  leibpi  20813  efrlim  20839  harmonicubnd  20879  fsumharmonic  20881  ftalem5  20890  basellem2  20895  basellem3  20896  chtnprm  20968  chpp1  20969  ppip1le  20975  ppiub  21019  logfaclbnd  21037  logfacrlim  21039  perfectlem2  21045  bcmono  21092  lgsvalmod  21130  lgseisen  21168  lgsquadlem1  21169  lgsquadlem2  21170  chebbnd1lem2  21195  chtppilimlem1  21198  rplogsumlem2  21210  dchrisumlema  21213  dchrisumlem1  21214  dchrisumlem3  21216  dchrisum0lem1  21241  chpdifbndlem1  21278  logdivbnd  21281  pntrmax  21289  pntrsumo1  21290  pntpbnd1a  21310  pntpbnd1  21311  pntpbnd2  21312  pntibndlem2  21316  pntlemg  21323  pntlemr  21327  pntlemj  21328  pntlemk  21331  ostth2lem1  21343  qabvle  21350  ostth2lem3  21360  ostth2lem4  21361  eupath2lem3  21732  eupath2  21733  smcnlem  22224  minvecolem4  22413  pjhthlem1  22924  cvmliftlem7  25009  fznatpl1  25229  fzp1nel  25241  axlowdimlem16  25927  bpoly4  26136  ltflcei  26271  lxflflp1  26273  opnmbllem0  26278  mblfinlem1  26279  mblfinlem2  26280  mblfinlem4  26282  dvtanlem  26292  itg2addnclem2  26295  itg2addnclem3  26296  incsequz  26490  isbnd3  26531  rrntotbnd  26583  irrapxlem4  26926  pellexlem5  26934  pell14qrgapw  26977  pellfundgt1  26984  jm3.1lem2  27127  expdiophlem1  27130  fmul01lt1lem1  27728  ltdifltdiv  28195
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 1627  ax-9 1668  ax-8 1689  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423  ax-1cn 9079  ax-icn 9080  ax-addcl 9081  ax-addrcl 9082  ax-mulcl 9083  ax-mulrcl 9084  ax-i2m1 9089  ax-1ne0 9090  ax-rrecex 9093  ax-cnre 9094
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 1660  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-ne 2607  df-ral 2716  df-rex 2717  df-rab 2720  df-v 2964  df-dif 3309  df-un 3311  df-in 3313  df-ss 3320  df-nul 3614  df-if 3764  df-sn 3844  df-pr 3845  df-op 3847  df-uni 4040  df-br 4238  df-iota 5447  df-fv 5491  df-ov 6113
  Copyright terms: Public domain W3C validator