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

Theorem peano2re 9530
Description: A theorem for reals analogous the second Peano postulate peano2nn 10322. (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 9373 . 2  |-  1  e.  RR
2 readdcl 9353 . 2  |-  ( ( A  e.  RR  /\  1  e.  RR )  ->  ( A  +  1 )  e.  RR )
31, 2mpan2 664 1  |-  ( A  e.  RR  ->  ( A  +  1 )  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1755  (class class class)co 6080   RRcr 9269   1c1 9271    + caddc 9273
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-1cn 9328  ax-icn 9329  ax-addcl 9330  ax-addrcl 9331  ax-mulcl 9332  ax-mulrcl 9333  ax-i2m1 9338  ax-1ne0 9339  ax-rrecex 9342  ax-cnre 9343
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-iota 5369  df-fv 5414  df-ov 6083
This theorem is referenced by:  lep1  10156  letrp1  10159  p1le  10160  ledivp1  10222  sup2  10274  nnssre  10314  nnge1  10336  zltp1le  10682  suprzcl  10709  zeo  10715  peano2uz2  10717  uzind  10721  numltc  10763  uzwo  10905  uzwoOLD  10906  ge0p1rp  11007  qbtwnxr  11158  xrsupsslem  11257  supxrunb1  11270  fznatpl1  11495  fzp1disj  11500  fzneuz  11525  ubmelm1fzo  11607  fllep1  11635  flhalf  11658  ltdifltdiv  11662  dfceil2  11664  ceim1l  11670  uzsup  11686  modltm1p1mod  11735  fsequb  11781  seqf1olem1  11829  seqf1olem2  11830  bernneq3  11976  expnbnd  11977  expmulnbnd  11980  discr1  11984  discr  11985  facwordi  12049  faclbnd  12050  hashfun  12183  seqcoll2  12201  rexuzre  12824  caubnd  12830  rlim2lt  12959  lo1bddrp  12987  rlimo1  13078  o1rlimmul  13080  o1fsum  13259  harmonic  13304  expcnv  13309  geomulcvg  13319  mertenslem1  13327  nonsq  13820  eulerthlem2  13840  pcprendvds  13890  pcmpt  13937  pcfac  13944  vdwlem6  14030  vdwlem11  14035  tgioo  20215  zcld  20232  iocopnst  20354  cnheibor  20369  bndth  20372  cncmet  20675  pjthlem1  20766  ovolicc2lem3  20844  ovolicopnf  20849  ioorcl2  20894  dyadf  20913  dyadovol  20915  dyadss  20916  dyaddisjlem  20917  dyadmaxlem  20919  opnmbllem  20923  volsup2  20927  vitalilem2  20931  itg2const2  21061  itg2cnlem1  21081  dvfsumle  21335  dvfsumabs  21337  dvfsumlem1  21340  dvfsumlem3  21342  dvfsumrlim  21345  fta1glem2  21523  fta1lem  21658  aalioulem3  21685  ulmbdd  21748  itgulm  21758  psercnlem1  21775  abelthlem2  21782  abelthlem7  21788  reeff1olem  21796  logtayl  21990  loglesqr  22081  atanlogsublem  22195  leibpi  22222  efrlim  22248  harmonicubnd  22288  fsumharmonic  22290  ftalem5  22299  basellem2  22304  basellem3  22305  chtnprm  22377  chpp1  22378  ppip1le  22384  ppiub  22428  logfaclbnd  22446  logfacrlim  22448  perfectlem2  22454  bcmono  22501  lgsvalmod  22539  lgseisen  22577  lgsquadlem1  22578  lgsquadlem2  22579  chebbnd1lem2  22604  chtppilimlem1  22607  rplogsumlem2  22619  dchrisumlema  22622  dchrisumlem1  22623  dchrisumlem3  22625  dchrisum0lem1  22650  chpdifbndlem1  22687  logdivbnd  22690  pntrmax  22698  pntrsumo1  22699  pntpbnd1a  22719  pntpbnd1  22720  pntpbnd2  22721  pntibndlem2  22725  pntlemg  22732  pntlemr  22736  pntlemj  22737  pntlemk  22740  ostth2lem1  22752  qabvle  22759  ostth2lem3  22769  ostth2lem4  22770  axlowdimlem16  23026  eupath2lem3  23423  eupath2  23424  smcnlem  23915  minvecolem4  24104  pjhthlem1  24617  cvmliftlem7  27028  fzp1nel  27244  bpoly4  28049  ltflcei  28263  lxflflp1  28265  opnmbllem0  28271  mblfinlem1  28272  mblfinlem2  28273  mblfinlem4  28275  dvtanlem  28285  itg2addnclem2  28288  itg2addnclem3  28289  incsequz  28488  isbnd3  28527  rrntotbnd  28579  irrapxlem4  29011  pellexlem5  29019  pell14qrgapw  29062  pellfundgt1  29069  jm3.1lem2  29212  expdiophlem1  29215  fmul01lt1lem1  29610  wwlknredwwlkn  30204  wwlkext2clwwlk  30311  wwlksubclwwlk  30312  clwlkfclwwlk  30363  wwlkextproplem1  30406  wwlkextproplem3  30408  extwwlkfablem2  30517
  Copyright terms: Public domain W3C validator