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

Theorem peano2re 9643
Description: A theorem for reals analogous the second Peano postulate peano2nn 10435. (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 9486 . 2  |-  1  e.  RR
2 readdcl 9466 . 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 1758  (class class class)co 6190   RRcr 9382   1c1 9384    + caddc 9386
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-1cn 9441  ax-icn 9442  ax-addcl 9443  ax-addrcl 9444  ax-mulcl 9445  ax-mulrcl 9446  ax-i2m1 9451  ax-1ne0 9452  ax-rrecex 9455  ax-cnre 9456
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3070  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3736  df-if 3890  df-sn 3976  df-pr 3978  df-op 3982  df-uni 4190  df-br 4391  df-iota 5479  df-fv 5524  df-ov 6193
This theorem is referenced by:  lep1  10269  letrp1  10272  p1le  10273  ledivp1  10335  sup2  10387  nnssre  10427  nnge1  10449  zltp1le  10795  suprzcl  10822  zeo  10828  peano2uz2  10830  uzind  10834  numltc  10876  uzwo  11018  uzwoOLD  11019  ge0p1rp  11120  qbtwnxr  11271  xrsupsslem  11370  supxrunb1  11383  fznatpl1  11611  fzp1disj  11616  fzneuz  11642  ubmelm1fzo  11724  fllep1  11752  flhalf  11775  ltdifltdiv  11779  dfceil2  11781  ceim1l  11787  uzsup  11803  modltm1p1mod  11852  fsequb  11898  seqf1olem1  11946  seqf1olem2  11947  bernneq3  12093  expnbnd  12094  expmulnbnd  12097  discr1  12101  discr  12102  facwordi  12166  faclbnd  12167  hashfun  12301  seqcoll2  12319  rexuzre  12942  caubnd  12948  rlim2lt  13077  lo1bddrp  13105  rlimo1  13196  o1rlimmul  13198  o1fsum  13378  harmonic  13423  expcnv  13428  geomulcvg  13438  mertenslem1  13446  nonsq  13939  eulerthlem2  13959  pcprendvds  14009  pcmpt  14056  pcfac  14063  vdwlem6  14149  vdwlem11  14154  tgioo  20489  zcld  20506  iocopnst  20628  cnheibor  20643  bndth  20646  cncmet  20949  pjthlem1  21040  ovolicc2lem3  21118  ovolicopnf  21123  ioorcl2  21168  dyadf  21187  dyadovol  21189  dyadss  21190  dyaddisjlem  21191  dyadmaxlem  21193  opnmbllem  21197  volsup2  21201  vitalilem2  21205  itg2const2  21335  itg2cnlem1  21355  dvfsumle  21609  dvfsumabs  21611  dvfsumlem1  21614  dvfsumlem3  21616  dvfsumrlim  21619  fta1glem2  21754  fta1lem  21889  aalioulem3  21916  ulmbdd  21979  itgulm  21989  psercnlem1  22006  abelthlem2  22013  abelthlem7  22019  reeff1olem  22027  logtayl  22221  loglesqr  22312  atanlogsublem  22426  leibpi  22453  efrlim  22479  harmonicubnd  22519  fsumharmonic  22521  ftalem5  22530  basellem2  22535  basellem3  22536  chtnprm  22608  chpp1  22609  ppip1le  22615  ppiub  22659  logfaclbnd  22677  logfacrlim  22679  perfectlem2  22685  bcmono  22732  lgsvalmod  22770  lgseisen  22808  lgsquadlem1  22809  lgsquadlem2  22810  chebbnd1lem2  22835  chtppilimlem1  22838  rplogsumlem2  22850  dchrisumlema  22853  dchrisumlem1  22854  dchrisumlem3  22856  dchrisum0lem1  22881  chpdifbndlem1  22918  logdivbnd  22921  pntrmax  22929  pntrsumo1  22930  pntpbnd1a  22950  pntpbnd1  22951  pntpbnd2  22952  pntibndlem2  22956  pntlemg  22963  pntlemr  22967  pntlemj  22968  pntlemk  22971  ostth2lem1  22983  qabvle  22990  ostth2lem3  23000  ostth2lem4  23001  axlowdimlem16  23338  eupath2lem3  23735  eupath2  23736  smcnlem  24227  minvecolem4  24416  pjhthlem1  24929  cvmliftlem7  27314  fzp1nel  27531  bpoly4  28336  ltflcei  28557  lxflflp1  28559  opnmbllem0  28565  mblfinlem1  28566  mblfinlem2  28567  mblfinlem4  28569  dvtanlem  28579  itg2addnclem2  28582  itg2addnclem3  28583  incsequz  28782  isbnd3  28821  rrntotbnd  28873  irrapxlem4  29304  pellexlem5  29312  pell14qrgapw  29355  pellfundgt1  29362  jm3.1lem2  29505  expdiophlem1  29508  fmul01lt1lem1  29903  wwlknredwwlkn  30496  wwlkext2clwwlk  30603  wwlksubclwwlk  30604  clwlkfclwwlk  30655  wwlkextproplem1  30698  wwlkextproplem3  30700  extwwlkfablem2  30809  chfacffsupp  31310  chfacfscmul0  31312  chfacfpmmul0  31316
  Copyright terms: Public domain W3C validator