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

Theorem peano2re 9806
Description: A theorem for reals analogous the second Peano postulate peano2nn 10621. (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 9642 . 2  |-  1  e.  RR
2 readdcl 9622 . 2  |-  ( ( A  e.  RR  /\  1  e.  RR )  ->  ( A  +  1 )  e.  RR )
31, 2mpan2 677 1  |-  ( A  e.  RR  ->  ( A  +  1 )  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1887  (class class class)co 6290   RRcr 9538   1c1 9540    + caddc 9542
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-1cn 9597  ax-icn 9598  ax-addcl 9599  ax-addrcl 9600  ax-mulcl 9601  ax-mulrcl 9602  ax-i2m1 9607  ax-1ne0 9608  ax-rrecex 9611  ax-cnre 9612
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3047  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-sn 3969  df-pr 3971  df-op 3975  df-uni 4199  df-br 4403  df-iota 5546  df-fv 5590  df-ov 6293
This theorem is referenced by:  lep1  10444  letrp1  10447  p1le  10448  ledivp1  10508  sup2  10565  nnssre  10613  nnge1  10635  zltp1le  10986  suprzcl  11015  zeo  11021  peano2uz2  11023  uzind  11027  numltc  11071  uzwo  11222  ge0p1rp  11331  qbtwnxr  11493  xrsupsslem  11592  supxrunb1  11605  fznatpl1  11850  fzp1disj  11854  fzneuz  11875  fzp1nel  11878  ubmelm1fzo  12007  fllep1  12037  flflp1  12043  flhalf  12062  ltdifltdiv  12066  dfceil2  12068  ceim1l  12074  uzsup  12090  modltm1p1mod  12142  fsequb  12188  seqf1olem1  12252  seqf1olem2  12253  bernneq3  12400  expnbnd  12401  expmulnbnd  12404  discr1  12408  discr  12409  facwordi  12474  faclbnd  12475  hashfun  12609  seqcoll2  12628  rexuzre  13415  caubnd  13421  rlim2lt  13561  lo1bddrp  13589  rlimo1  13680  o1rlimmul  13682  o1fsum  13873  harmonic  13917  expcnv  13922  geomulcvg  13932  mertenslem1  13940  bpoly4  14112  nonsq  14708  eulerthlem2  14730  pcprendvds  14790  pcmpt  14837  pcfac  14844  vdwlem6  14936  vdwlem11  14941  chfacffsupp  19880  chfacfscmul0  19882  chfacfpmmul0  19886  tgioo  21814  zcld  21831  iocopnst  21968  cnheibor  21983  bndth  21986  cncmet  22290  pjthlem1  22391  ovolicc2lem3  22472  ovolicopnf  22478  ioorcl2  22524  dyadf  22549  dyadovol  22551  dyadss  22552  dyaddisjlem  22553  dyadmaxlem  22555  opnmbllem  22559  volsup2  22563  vitalilem2  22567  itg2const2  22699  itg2cnlem1  22719  dvfsumle  22973  dvfsumabs  22975  dvfsumlem1  22978  dvfsumlem3  22980  dvfsumrlim  22983  fta1glem2  23117  fta1lem  23260  aalioulem3  23290  ulmbdd  23353  itgulm  23363  psercnlem1  23380  abelthlem2  23387  abelthlem7  23393  reeff1olem  23401  logtayl  23605  loglesqrt  23698  atanlogsublem  23841  leibpi  23868  efrlim  23895  harmonicubnd  23935  fsumharmonic  23937  ftalem5  24001  ftalem5OLD  24003  basellem2  24008  basellem3  24009  chtnprm  24081  chpp1  24082  ppip1le  24088  ppiub  24132  logfaclbnd  24150  logfacrlim  24152  perfectlem2  24158  bcmono  24205  lgsvalmod  24243  lgseisen  24281  lgsquadlem1  24282  lgsquadlem2  24283  chebbnd1lem2  24308  chtppilimlem1  24311  rplogsumlem2  24323  dchrisumlema  24326  dchrisumlem1  24327  dchrisumlem3  24329  dchrisum0lem1  24354  chpdifbndlem1  24391  logdivbnd  24394  pntrmax  24402  pntrsumo1  24403  pntpbnd1a  24423  pntpbnd1  24424  pntpbnd2  24425  pntibndlem2  24429  pntlemg  24436  pntlemr  24440  pntlemj  24441  pntlemk  24444  ostth2lem1  24456  qabvle  24463  ostth2lem3  24473  ostth2lem4  24474  axlowdimlem16  24987  wwlknredwwlkn  25454  wwlkextproplem1  25469  wwlkextproplem3  25471  wwlkext2clwwlk  25531  wwlksubclwwlk  25532  clwlkfclwwlk  25572  eupath2lem3  25707  eupath2  25708  extwwlkfablem2  25806  smcnlem  26333  minvecolem4  26522  minvecolem4OLD  26532  pjhthlem1  27044  cvmliftlem7  30014  icoreunrn  31762  relowlssretop  31766  ltflcei  31933  poimirlem1  31941  poimirlem2  31942  poimirlem4  31944  poimirlem6  31946  poimirlem7  31947  poimirlem8  31948  opnmbllem0  31976  mblfinlem1  31977  mblfinlem2  31978  mblfinlem4  31980  dvtanlemOLD  31991  itg2addnclem2  31994  itg2addnclem3  31995  incsequz  32077  isbnd3  32116  rrntotbnd  32168  irrapxlem4  35669  pellexlem5  35677  pell14qrgapw  35722  pellfundgt1  35731  jm3.1lem2  35873  expdiophlem1  35876  zltlesub  37495  suplesup  37562  fmul01lt1lem1  37662  ioodvbdlimc1lem1  37803  ioodvbdlimc1lem1OLD  37805  dvnxpaek  37817  dvnmul  37818  fourierdlem4  37973  fourierdlem11  37980  fourierdlem25  37994  fourierdlem50  38020  fourierdlem64  38034  fourierdlem65  38035  fourierdlem77  38047  fourierdlem79  38049  perfectALTVlem2  38844  logbpw2m1  40431
  Copyright terms: Public domain W3C validator