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

Theorem peano2re 9741
Description: A theorem for reals analogous the second Peano postulate peano2nn 10537. (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 9584 . 2  |-  1  e.  RR
2 readdcl 9564 . 2  |-  ( ( A  e.  RR  /\  1  e.  RR )  ->  ( A  +  1 )  e.  RR )
31, 2mpan2 671 1  |-  ( A  e.  RR  ->  ( A  +  1 )  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1762  (class class class)co 6275   RRcr 9480   1c1 9482    + caddc 9484
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-addrcl 9542  ax-mulcl 9543  ax-mulrcl 9544  ax-i2m1 9549  ax-1ne0 9550  ax-rrecex 9553  ax-cnre 9554
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-br 4441  df-iota 5542  df-fv 5587  df-ov 6278
This theorem is referenced by:  lep1  10370  letrp1  10373  p1le  10374  ledivp1  10436  sup2  10488  nnssre  10529  nnge1  10551  zltp1le  10901  suprzcl  10929  zeo  10935  peano2uz2  10937  uzind  10941  numltc  10985  uzwo  11133  uzwoOLD  11134  ge0p1rp  11237  qbtwnxr  11388  xrsupsslem  11487  supxrunb1  11500  fznatpl1  11723  fzp1disj  11727  fzneuz  11748  ubmelm1fzo  11865  fllep1  11895  flhalf  11918  ltdifltdiv  11922  dfceil2  11924  ceim1l  11930  uzsup  11946  modltm1p1mod  11995  fsequb  12041  seqf1olem1  12102  seqf1olem2  12103  bernneq3  12249  expnbnd  12250  expmulnbnd  12253  discr1  12257  discr  12258  facwordi  12322  faclbnd  12323  hashfun  12448  seqcoll2  12466  rexuzre  13134  caubnd  13140  rlim2lt  13269  lo1bddrp  13297  rlimo1  13388  o1rlimmul  13390  o1fsum  13576  harmonic  13622  expcnv  13627  geomulcvg  13637  mertenslem1  13645  nonsq  14140  eulerthlem2  14160  pcprendvds  14212  pcmpt  14259  pcfac  14266  vdwlem6  14352  vdwlem11  14357  chfacffsupp  19117  chfacfscmul0  19119  chfacfpmmul0  19123  tgioo  21029  zcld  21046  iocopnst  21168  cnheibor  21183  bndth  21186  cncmet  21489  pjthlem1  21580  ovolicc2lem3  21658  ovolicopnf  21663  ioorcl2  21709  dyadf  21728  dyadovol  21730  dyadss  21731  dyaddisjlem  21732  dyadmaxlem  21734  opnmbllem  21738  volsup2  21742  vitalilem2  21746  itg2const2  21876  itg2cnlem1  21896  dvfsumle  22150  dvfsumabs  22152  dvfsumlem1  22155  dvfsumlem3  22157  dvfsumrlim  22160  fta1glem2  22295  fta1lem  22430  aalioulem3  22457  ulmbdd  22520  itgulm  22530  psercnlem1  22547  abelthlem2  22554  abelthlem7  22560  reeff1olem  22568  logtayl  22762  loglesqr  22853  atanlogsublem  22967  leibpi  22994  efrlim  23020  harmonicubnd  23060  fsumharmonic  23062  ftalem5  23071  basellem2  23076  basellem3  23077  chtnprm  23149  chpp1  23150  ppip1le  23156  ppiub  23200  logfaclbnd  23218  logfacrlim  23220  perfectlem2  23226  bcmono  23273  lgsvalmod  23311  lgseisen  23349  lgsquadlem1  23350  lgsquadlem2  23351  chebbnd1lem2  23376  chtppilimlem1  23379  rplogsumlem2  23391  dchrisumlema  23394  dchrisumlem1  23395  dchrisumlem3  23397  dchrisum0lem1  23422  chpdifbndlem1  23459  logdivbnd  23462  pntrmax  23470  pntrsumo1  23471  pntpbnd1a  23491  pntpbnd1  23492  pntpbnd2  23493  pntibndlem2  23497  pntlemg  23504  pntlemr  23508  pntlemj  23509  pntlemk  23512  ostth2lem1  23524  qabvle  23531  ostth2lem3  23541  ostth2lem4  23542  axlowdimlem16  23929  wwlknredwwlkn  24388  wwlkextproplem1  24403  wwlkextproplem3  24405  wwlkext2clwwlk  24465  wwlksubclwwlk  24466  clwlkfclwwlk  24506  eupath2lem3  24641  eupath2  24642  smcnlem  25133  minvecolem4  25322  pjhthlem1  25835  cvmliftlem7  28226  fzp1nel  28443  bpoly4  29248  ltflcei  29470  lxflflp1  29472  opnmbllem0  29478  mblfinlem1  29479  mblfinlem2  29480  mblfinlem4  29482  dvtanlem  29492  itg2addnclem2  29495  itg2addnclem3  29496  incsequz  29695  isbnd3  29734  rrntotbnd  29786  irrapxlem4  30216  pellexlem5  30224  pell14qrgapw  30267  pellfundgt1  30274  jm3.1lem2  30417  expdiophlem1  30420  zltlesub  30864  fmul01lt1lem1  30953  ioodvbdlimc1lem1  31080  fourierdlem4  31230  fourierdlem11  31237  fourierdlem25  31251  fourierdlem45  31271  fourierdlem50  31276  fourierdlem64  31290  fourierdlem65  31291  fourierdlem77  31303  fourierdlem79  31305  extwwlkfablem2  31797
  Copyright terms: Public domain W3C validator