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

Theorem peano2re 9751
Description: A theorem for reals analogous the second Peano postulate peano2nn 10549. (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 9593 . 2  |-  1  e.  RR
2 readdcl 9573 . 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 1802  (class class class)co 6277   RRcr 9489   1c1 9491    + caddc 9493
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-1cn 9548  ax-icn 9549  ax-addcl 9550  ax-addrcl 9551  ax-mulcl 9552  ax-mulrcl 9553  ax-i2m1 9558  ax-1ne0 9559  ax-rrecex 9562  ax-cnre 9563
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3095  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-if 3923  df-sn 4011  df-pr 4013  df-op 4017  df-uni 4231  df-br 4434  df-iota 5537  df-fv 5582  df-ov 6280
This theorem is referenced by:  lep1  10382  letrp1  10385  p1le  10386  ledivp1  10448  sup2  10500  nnssre  10541  nnge1  10563  zltp1le  10914  suprzcl  10943  zeo  10949  peano2uz2  10951  uzind  10955  numltc  10999  uzwo  11148  uzwoOLD  11149  ge0p1rp  11252  qbtwnxr  11403  xrsupsslem  11502  supxrunb1  11515  fznatpl1  11738  fzp1disj  11742  fzneuz  11763  ubmelm1fzo  11882  fllep1  11912  flflp1  11918  flhalf  11936  ltdifltdiv  11940  dfceil2  11942  ceim1l  11948  uzsup  11964  modltm1p1mod  12013  fsequb  12059  seqf1olem1  12120  seqf1olem2  12121  bernneq3  12268  expnbnd  12269  expmulnbnd  12272  discr1  12276  discr  12277  facwordi  12341  faclbnd  12342  hashfun  12469  seqcoll2  12487  rexuzre  13159  caubnd  13165  rlim2lt  13294  lo1bddrp  13322  rlimo1  13413  o1rlimmul  13415  o1fsum  13601  harmonic  13644  expcnv  13649  geomulcvg  13659  mertenslem1  13667  nonsq  14164  eulerthlem2  14184  pcprendvds  14236  pcmpt  14283  pcfac  14290  vdwlem6  14376  vdwlem11  14381  chfacffsupp  19224  chfacfscmul0  19226  chfacfpmmul0  19230  tgioo  21167  zcld  21184  iocopnst  21306  cnheibor  21321  bndth  21324  cncmet  21627  pjthlem1  21718  ovolicc2lem3  21796  ovolicopnf  21801  ioorcl2  21847  dyadf  21866  dyadovol  21868  dyadss  21869  dyaddisjlem  21870  dyadmaxlem  21872  opnmbllem  21876  volsup2  21880  vitalilem2  21884  itg2const2  22014  itg2cnlem1  22034  dvfsumle  22288  dvfsumabs  22290  dvfsumlem1  22293  dvfsumlem3  22295  dvfsumrlim  22298  fta1glem2  22433  fta1lem  22568  aalioulem3  22595  ulmbdd  22658  itgulm  22668  psercnlem1  22685  abelthlem2  22692  abelthlem7  22698  reeff1olem  22706  logtayl  22906  loglesqrt  22997  atanlogsublem  23111  leibpi  23138  efrlim  23164  harmonicubnd  23204  fsumharmonic  23206  ftalem5  23215  basellem2  23220  basellem3  23221  chtnprm  23293  chpp1  23294  ppip1le  23300  ppiub  23344  logfaclbnd  23362  logfacrlim  23364  perfectlem2  23370  bcmono  23417  lgsvalmod  23455  lgseisen  23493  lgsquadlem1  23494  lgsquadlem2  23495  chebbnd1lem2  23520  chtppilimlem1  23523  rplogsumlem2  23535  dchrisumlema  23538  dchrisumlem1  23539  dchrisumlem3  23541  dchrisum0lem1  23566  chpdifbndlem1  23603  logdivbnd  23606  pntrmax  23614  pntrsumo1  23615  pntpbnd1a  23635  pntpbnd1  23636  pntpbnd2  23637  pntibndlem2  23641  pntlemg  23648  pntlemr  23652  pntlemj  23653  pntlemk  23656  ostth2lem1  23668  qabvle  23675  ostth2lem3  23685  ostth2lem4  23686  axlowdimlem16  24125  wwlknredwwlkn  24591  wwlkextproplem1  24606  wwlkextproplem3  24608  wwlkext2clwwlk  24668  wwlksubclwwlk  24669  clwlkfclwwlk  24709  eupath2lem3  24844  eupath2  24845  extwwlkfablem2  24943  smcnlem  25472  minvecolem4  25661  pjhthlem1  26174  cvmliftlem7  28602  fzp1nel  28984  bpoly4  29789  ltflcei  30011  opnmbllem0  30018  mblfinlem1  30019  mblfinlem2  30020  mblfinlem4  30022  dvtanlem  30032  itg2addnclem2  30035  itg2addnclem3  30036  incsequz  30209  isbnd3  30248  rrntotbnd  30300  irrapxlem4  30729  pellexlem5  30737  pell14qrgapw  30780  pellfundgt1  30787  jm3.1lem2  30928  expdiophlem1  30931  zltlesub  31413  fmul01lt1lem1  31502  ioodvbdlimc1lem1  31628  fourierdlem4  31778  fourierdlem11  31785  fourierdlem25  31799  fourierdlem50  31824  fourierdlem64  31838  fourierdlem65  31839  fourierdlem77  31851  fourierdlem79  31853
  Copyright terms: Public domain W3C validator