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

Theorem peano2re 10247
Description: A theorem for reals analogous the second Peano postulate peano2nn 11070. (Contributed by NM, 5-Jul-2005.)
Assertion
Ref Expression
peano2re (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ)

Proof of Theorem peano2re
StepHypRef Expression
1 1re 10077 . 2 1 ∈ ℝ
2 readdcl 10057 . 2 ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐴 + 1) ∈ ℝ)
31, 2mpan2 707 1 (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030  (class class class)co 6690  cr 9973  1c1 9975   + caddc 9977
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-i2m1 10042  ax-1ne0 10043  ax-rrecex 10046  ax-cnre 10047
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-iota 5889  df-fv 5934  df-ov 6693
This theorem is referenced by:  lep1  10900  letrp1  10903  p1le  10904  ledivp1  10963  sup2  11017  nnssre  11062  nnge1  11084  div4p1lem1div2  11325  zltp1le  11465  suprzcl  11495  zeo  11501  peano2uz2  11503  uzind  11507  numltc  11566  uzwo  11789  ge0p1rp  11900  qbtwnxr  12069  xrsupsslem  12175  supxrunb1  12187  fznatpl1  12433  fzp1disj  12437  fzneuz  12459  fzp1nel  12462  ubmelm1fzo  12604  fllep1  12642  flflp1  12648  flhalf  12671  ltdifltdiv  12675  fldiv4p1lem1div2  12676  dfceil2  12680  ceim1l  12686  uzsup  12702  modltm1p1mod  12762  addmodlteq  12785  fsequb  12814  seqf1olem1  12880  seqf1olem2  12881  bernneq3  13032  expnbnd  13033  expmulnbnd  13036  discr1  13040  discr  13041  facwordi  13116  faclbnd  13117  hashfun  13262  seqcoll2  13287  rexuzre  14136  caubnd  14142  rlim2lt  14272  lo1bddrp  14300  rlimo1  14391  o1rlimmul  14393  o1fsum  14589  harmonic  14635  expcnv  14640  geomulcvg  14651  mertenslem1  14660  bpoly4  14834  nonsq  15514  eulerthlem2  15534  pcprendvds  15592  pcmpt  15643  pcfac  15650  vdwlem6  15737  vdwlem11  15742  chfacffsupp  20709  chfacfscmul0  20711  chfacfpmmul0  20715  tgioo  22646  zcld  22663  iocopnst  22786  cnheibor  22801  bndth  22804  cncmet  23165  pjthlem1  23254  ovolicc2lem3  23333  ovolicopnf  23338  ioorcl2  23386  dyadf  23405  dyadovol  23407  dyadss  23408  dyaddisjlem  23409  dyadmaxlem  23411  opnmbllem  23415  volsup2  23419  vitalilem2  23423  itg2const2  23553  itg2cnlem1  23573  dvfsumle  23829  dvfsumabs  23831  dvfsumlem1  23834  dvfsumlem3  23836  dvfsumrlim  23839  fta1glem2  23971  fta1lem  24107  aalioulem3  24134  ulmbdd  24197  itgulm  24207  psercnlem1  24224  abelthlem2  24231  abelthlem7  24237  reeff1olem  24245  logtayl  24451  loglesqrt  24544  atanlogsublem  24687  leibpi  24714  efrlim  24741  harmonicubnd  24781  fsumharmonic  24783  ftalem5  24848  basellem2  24853  basellem3  24854  chtnprm  24925  chpp1  24926  ppip1le  24932  ppiub  24974  logfaclbnd  24992  logfacrlim  24994  perfectlem2  25000  bcmono  25047  lgsvalmod  25086  gausslemma2dlem3  25138  lgseisen  25149  lgsquadlem1  25150  lgsquadlem2  25151  chebbnd1lem2  25204  chtppilimlem1  25207  rplogsumlem2  25219  dchrisumlema  25222  dchrisumlem1  25223  dchrisumlem3  25225  dchrisum0lem1  25250  chpdifbndlem1  25287  logdivbnd  25290  pntrmax  25298  pntrsumo1  25299  pntpbnd1a  25319  pntpbnd1  25320  pntpbnd2  25321  pntibndlem2  25325  pntlemg  25332  pntlemr  25336  pntlemj  25337  pntlemk  25340  ostth2lem1  25352  qabvle  25359  ostth2lem3  25369  ostth2lem4  25370  axlowdimlem16  25882  wwlksnredwwlkn  26858  wwlksnextproplem3  26874  wwlksext2clwwlk  27021  wwlksext2clwwlkOLD  27022  wwlksubclwwlk  27023  clwlksfclwwlk  27049  eupth2lems  27216  smcnlem  27680  minvecolem4  27864  pjhthlem1  28378  cvmliftlem7  31399  dnibndlem13  32605  knoppndvlem19  32646  knoppndvlem21  32648  icoreunrn  33337  relowlssretop  33341  ltflcei  33527  poimirlem1  33540  poimirlem2  33541  poimirlem4  33543  poimirlem6  33545  poimirlem7  33546  poimirlem8  33547  opnmbllem0  33575  mblfinlem1  33576  mblfinlem2  33577  mblfinlem4  33579  itg2addnclem2  33592  itg2addnclem3  33593  incsequz  33674  isbnd3  33713  rrntotbnd  33765  irrapxlem4  37706  pellexlem5  37714  pell14qrgapw  37757  pellfundgt1  37764  jm3.1lem2  37902  expdiophlem1  37905  zltlesub  39811  suplesup  39868  supxrunb3  39936  xrpnf  40029  fmul01lt1lem1  40134  limsupre3lem  40282  xlimxrre  40375  xlimpnfv  40382  ioodvbdlimc1lem1  40464  dvnxpaek  40475  dvnmul  40476  fourierdlem4  40646  fourierdlem11  40653  fourierdlem25  40667  fourierdlem50  40691  fourierdlem64  40705  fourierdlem65  40706  fourierdlem77  40718  fourierdlem79  40720  iinhoiicclem  41208  smfresal  41316  fmtno4prmfac  41809  lighneallem4a  41850  evenltle  41951  perfectALTVlem2  41956  logbpw2m1  42686
  Copyright terms: Public domain W3C validator