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

Theorem peano2re 9534
Description: A theorem for reals analogous the second Peano postulate peano2nn 10326. (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 9377 . 2  |-  1  e.  RR
2 readdcl 9357 . 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 1756  (class class class)co 6086   RRcr 9273   1c1 9275    + caddc 9277
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-i2m1 9342  ax-1ne0 9343  ax-rrecex 9346  ax-cnre 9347
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-iota 5376  df-fv 5421  df-ov 6089
This theorem is referenced by:  lep1  10160  letrp1  10163  p1le  10164  ledivp1  10226  sup2  10278  nnssre  10318  nnge1  10340  zltp1le  10686  suprzcl  10713  zeo  10719  peano2uz2  10721  uzind  10725  numltc  10767  uzwo  10909  uzwoOLD  10910  ge0p1rp  11011  qbtwnxr  11162  xrsupsslem  11261  supxrunb1  11274  fznatpl1  11502  fzp1disj  11507  fzneuz  11533  ubmelm1fzo  11615  fllep1  11643  flhalf  11666  ltdifltdiv  11670  dfceil2  11672  ceim1l  11678  uzsup  11694  modltm1p1mod  11743  fsequb  11789  seqf1olem1  11837  seqf1olem2  11838  bernneq3  11984  expnbnd  11985  expmulnbnd  11988  discr1  11992  discr  11993  facwordi  12057  faclbnd  12058  hashfun  12191  seqcoll2  12209  rexuzre  12832  caubnd  12838  rlim2lt  12967  lo1bddrp  12995  rlimo1  13086  o1rlimmul  13088  o1fsum  13268  harmonic  13313  expcnv  13318  geomulcvg  13328  mertenslem1  13336  nonsq  13829  eulerthlem2  13849  pcprendvds  13899  pcmpt  13946  pcfac  13953  vdwlem6  14039  vdwlem11  14044  tgioo  20353  zcld  20370  iocopnst  20492  cnheibor  20507  bndth  20510  cncmet  20813  pjthlem1  20904  ovolicc2lem3  20982  ovolicopnf  20987  ioorcl2  21032  dyadf  21051  dyadovol  21053  dyadss  21054  dyaddisjlem  21055  dyadmaxlem  21057  opnmbllem  21061  volsup2  21065  vitalilem2  21069  itg2const2  21199  itg2cnlem1  21219  dvfsumle  21473  dvfsumabs  21475  dvfsumlem1  21478  dvfsumlem3  21480  dvfsumrlim  21483  fta1glem2  21618  fta1lem  21753  aalioulem3  21780  ulmbdd  21843  itgulm  21853  psercnlem1  21870  abelthlem2  21877  abelthlem7  21883  reeff1olem  21891  logtayl  22085  loglesqr  22176  atanlogsublem  22290  leibpi  22317  efrlim  22343  harmonicubnd  22383  fsumharmonic  22385  ftalem5  22394  basellem2  22399  basellem3  22400  chtnprm  22472  chpp1  22473  ppip1le  22479  ppiub  22523  logfaclbnd  22541  logfacrlim  22543  perfectlem2  22549  bcmono  22596  lgsvalmod  22634  lgseisen  22672  lgsquadlem1  22673  lgsquadlem2  22674  chebbnd1lem2  22699  chtppilimlem1  22702  rplogsumlem2  22714  dchrisumlema  22717  dchrisumlem1  22718  dchrisumlem3  22720  dchrisum0lem1  22745  chpdifbndlem1  22782  logdivbnd  22785  pntrmax  22793  pntrsumo1  22794  pntpbnd1a  22814  pntpbnd1  22815  pntpbnd2  22816  pntibndlem2  22820  pntlemg  22827  pntlemr  22831  pntlemj  22832  pntlemk  22835  ostth2lem1  22847  qabvle  22854  ostth2lem3  22864  ostth2lem4  22865  axlowdimlem16  23171  eupath2lem3  23568  eupath2  23569  smcnlem  24060  minvecolem4  24249  pjhthlem1  24762  cvmliftlem7  27149  fzp1nel  27366  bpoly4  28171  ltflcei  28390  lxflflp1  28392  opnmbllem0  28398  mblfinlem1  28399  mblfinlem2  28400  mblfinlem4  28402  dvtanlem  28412  itg2addnclem2  28415  itg2addnclem3  28416  incsequz  28615  isbnd3  28654  rrntotbnd  28706  irrapxlem4  29137  pellexlem5  29145  pell14qrgapw  29188  pellfundgt1  29195  jm3.1lem2  29338  expdiophlem1  29341  fmul01lt1lem1  29736  wwlknredwwlkn  30329  wwlkext2clwwlk  30436  wwlksubclwwlk  30437  clwlkfclwwlk  30488  wwlkextproplem1  30531  wwlkextproplem3  30533  extwwlkfablem2  30642
  Copyright terms: Public domain W3C validator