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

Theorem peano2re 9742
Description: A theorem for reals analogous the second Peano postulate peano2nn 10543. (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 669 1  |-  ( A  e.  RR  ->  ( A  +  1 )  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1823  (class class class)co 6270   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 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  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 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-iota 5534  df-fv 5578  df-ov 6273
This theorem is referenced by:  lep1  10377  letrp1  10380  p1le  10381  ledivp1  10442  sup2  10494  nnssre  10535  nnge1  10557  zltp1le  10909  suprzcl  10938  zeo  10944  peano2uz2  10946  uzind  10950  numltc  10996  uzwo  11145  uzwoOLD  11146  ge0p1rp  11250  qbtwnxr  11402  xrsupsslem  11501  supxrunb1  11514  fznatpl1  11738  fzp1disj  11742  fzneuz  11763  fzp1nel  11766  ubmelm1fzo  11889  fllep1  11919  flflp1  11925  flhalf  11944  ltdifltdiv  11948  dfceil2  11950  ceim1l  11956  uzsup  11972  modltm1p1mod  12021  fsequb  12067  seqf1olem1  12128  seqf1olem2  12129  bernneq3  12276  expnbnd  12277  expmulnbnd  12280  discr1  12284  discr  12285  facwordi  12349  faclbnd  12350  hashfun  12479  seqcoll2  12497  rexuzre  13267  caubnd  13273  rlim2lt  13402  lo1bddrp  13430  rlimo1  13521  o1rlimmul  13523  o1fsum  13709  harmonic  13752  expcnv  13757  geomulcvg  13767  mertenslem1  13775  nonsq  14376  eulerthlem2  14396  pcprendvds  14448  pcmpt  14495  pcfac  14502  vdwlem6  14588  vdwlem11  14593  chfacffsupp  19524  chfacfscmul0  19526  chfacfpmmul0  19530  tgioo  21467  zcld  21484  iocopnst  21606  cnheibor  21621  bndth  21624  cncmet  21927  pjthlem1  22018  ovolicc2lem3  22096  ovolicopnf  22101  ioorcl2  22147  dyadf  22166  dyadovol  22168  dyadss  22169  dyaddisjlem  22170  dyadmaxlem  22172  opnmbllem  22176  volsup2  22180  vitalilem2  22184  itg2const2  22314  itg2cnlem1  22334  dvfsumle  22588  dvfsumabs  22590  dvfsumlem1  22593  dvfsumlem3  22595  dvfsumrlim  22598  fta1glem2  22733  fta1lem  22869  aalioulem3  22896  ulmbdd  22959  itgulm  22969  psercnlem1  22986  abelthlem2  22993  abelthlem7  22999  reeff1olem  23007  logtayl  23209  loglesqrt  23300  atanlogsublem  23443  leibpi  23470  efrlim  23497  harmonicubnd  23537  fsumharmonic  23539  ftalem5  23548  basellem2  23553  basellem3  23554  chtnprm  23626  chpp1  23627  ppip1le  23633  ppiub  23677  logfaclbnd  23695  logfacrlim  23697  perfectlem2  23703  bcmono  23750  lgsvalmod  23788  lgseisen  23826  lgsquadlem1  23827  lgsquadlem2  23828  chebbnd1lem2  23853  chtppilimlem1  23856  rplogsumlem2  23868  dchrisumlema  23871  dchrisumlem1  23872  dchrisumlem3  23874  dchrisum0lem1  23899  chpdifbndlem1  23936  logdivbnd  23939  pntrmax  23947  pntrsumo1  23948  pntpbnd1a  23968  pntpbnd1  23969  pntpbnd2  23970  pntibndlem2  23974  pntlemg  23981  pntlemr  23985  pntlemj  23986  pntlemk  23989  ostth2lem1  24001  qabvle  24008  ostth2lem3  24018  ostth2lem4  24019  axlowdimlem16  24462  wwlknredwwlkn  24928  wwlkextproplem1  24943  wwlkextproplem3  24945  wwlkext2clwwlk  25005  wwlksubclwwlk  25006  clwlkfclwwlk  25046  eupath2lem3  25181  eupath2  25182  extwwlkfablem2  25280  smcnlem  25805  minvecolem4  25994  pjhthlem1  26507  cvmliftlem7  29000  bpoly4  30049  ltflcei  30283  opnmbllem0  30290  mblfinlem1  30291  mblfinlem2  30292  mblfinlem4  30294  dvtanlem  30304  itg2addnclem2  30307  itg2addnclem3  30308  incsequz  30481  isbnd3  30520  rrntotbnd  30572  irrapxlem4  31000  pellexlem5  31008  pell14qrgapw  31051  pellfundgt1  31058  jm3.1lem2  31199  expdiophlem1  31202  zltlesub  31708  fmul01lt1lem1  31817  ioodvbdlimc1lem1  31967  dvnxpaek  31978  dvnmul  31979  fourierdlem4  32132  fourierdlem11  32139  fourierdlem25  32153  fourierdlem50  32178  fourierdlem64  32192  fourierdlem65  32193  fourierdlem77  32205  fourierdlem79  32207  logbpw2m1  33442
  Copyright terms: Public domain W3C validator