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

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

Proof of Theorem peano2re
StepHypRef Expression
1 1re 9895 . 2 1 ∈ ℝ
2 readdcl 9875 . 2 ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐴 + 1) ∈ ℝ)
31, 2mpan2 702 1 (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  (class class class)co 6526  cr 9791  1c1 9793   + caddc 9795
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-i2m1 9860  ax-1ne0 9861  ax-rrecex 9864  ax-cnre 9865
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-iota 5753  df-fv 5797  df-ov 6529
This theorem is referenced by:  lep1  10713  letrp1  10716  p1le  10717  ledivp1  10776  sup2  10830  nnssre  10873  nnge1  10895  div4p1lem1div2  11136  zltp1le  11262  suprzcl  11291  zeo  11297  peano2uz2  11299  uzind  11303  numltc  11362  uzwo  11585  ge0p1rp  11696  qbtwnxr  11866  xrsupsslem  11967  supxrunb1  11979  fznatpl1  12222  fzp1disj  12226  fzneuz  12247  fzp1nel  12250  ubmelm1fzo  12387  fllep1  12421  flflp1  12427  flhalf  12450  ltdifltdiv  12454  fldiv4p1lem1div2  12455  dfceil2  12459  ceim1l  12465  uzsup  12481  modltm1p1mod  12541  addmodlteq  12564  fsequb  12593  seqf1olem1  12659  seqf1olem2  12660  bernneq3  12811  expnbnd  12812  expmulnbnd  12815  discr1  12819  discr  12820  facwordi  12895  faclbnd  12896  hashfun  13038  seqcoll2  13060  rexuzre  13888  caubnd  13894  rlim2lt  14024  lo1bddrp  14052  rlimo1  14143  o1rlimmul  14145  o1fsum  14334  harmonic  14378  expcnv  14383  geomulcvg  14394  mertenslem1  14403  bpoly4  14577  nonsq  15253  eulerthlem2  15273  pcprendvds  15331  pcmpt  15382  pcfac  15389  vdwlem6  15476  vdwlem11  15481  chfacffsupp  20427  chfacfscmul0  20429  chfacfpmmul0  20433  tgioo  22354  zcld  22371  iocopnst  22494  cnheibor  22509  bndth  22512  cncmet  22871  pjthlem1  22960  ovolicc2lem3  23038  ovolicopnf  23043  ioorcl2  23090  dyadf  23109  dyadovol  23111  dyadss  23112  dyaddisjlem  23113  dyadmaxlem  23115  opnmbllem  23119  volsup2  23123  vitalilem2  23128  itg2const2  23258  itg2cnlem1  23278  dvfsumle  23532  dvfsumabs  23534  dvfsumlem1  23537  dvfsumlem3  23539  dvfsumrlim  23542  fta1glem2  23674  fta1lem  23810  aalioulem3  23837  ulmbdd  23900  itgulm  23910  psercnlem1  23927  abelthlem2  23934  abelthlem7  23940  reeff1olem  23948  logtayl  24150  loglesqrt  24243  atanlogsublem  24386  leibpi  24413  efrlim  24440  harmonicubnd  24480  fsumharmonic  24482  ftalem5  24547  basellem2  24552  basellem3  24553  chtnprm  24624  chpp1  24625  ppip1le  24631  ppiub  24673  logfaclbnd  24691  logfacrlim  24693  perfectlem2  24699  bcmono  24746  lgsvalmod  24785  gausslemma2dlem3  24837  lgseisen  24848  lgsquadlem1  24849  lgsquadlem2  24850  chebbnd1lem2  24903  chtppilimlem1  24906  rplogsumlem2  24918  dchrisumlema  24921  dchrisumlem1  24922  dchrisumlem3  24924  dchrisum0lem1  24949  chpdifbndlem1  24986  logdivbnd  24989  pntrmax  24997  pntrsumo1  24998  pntpbnd1a  25018  pntpbnd1  25019  pntpbnd2  25020  pntibndlem2  25024  pntlemg  25031  pntlemr  25035  pntlemj  25036  pntlemk  25039  ostth2lem1  25051  qabvle  25058  ostth2lem3  25068  ostth2lem4  25069  axlowdimlem16  25582  wwlknredwwlkn  26047  wwlkextproplem1  26062  wwlkextproplem3  26064  wwlkext2clwwlk  26124  wwlksubclwwlk  26125  clwlkfclwwlk  26164  eupath2lem3  26299  eupath2  26300  extwwlkfablem2  26398  smcnlem  26729  minvecolem4  26913  pjhthlem1  27427  cvmliftlem7  30320  dnibndlem13  31443  knoppndvlem19  31484  knoppndvlem21  31486  icoreunrn  32166  relowlssretop  32170  ltflcei  32350  poimirlem1  32363  poimirlem2  32364  poimirlem4  32366  poimirlem6  32368  poimirlem7  32369  poimirlem8  32370  opnmbllem0  32398  mblfinlem1  32399  mblfinlem2  32400  mblfinlem4  32402  itg2addnclem2  32415  itg2addnclem3  32416  incsequz  32497  isbnd3  32536  rrntotbnd  32588  irrapxlem4  36190  pellexlem5  36198  pell14qrgapw  36241  pellfundgt1  36248  jm3.1lem2  36386  expdiophlem1  36389  zltlesub  38221  suplesup  38279  fmul01lt1lem1  38434  ioodvbdlimc1lem1  38604  dvnxpaek  38615  dvnmul  38616  fourierdlem4  38787  fourierdlem11  38794  fourierdlem25  38808  fourierdlem50  38832  fourierdlem64  38846  fourierdlem65  38847  fourierdlem77  38859  fourierdlem79  38861  iinhoiicclem  39347  smfresal  39456  fmtno4prmfac  39806  lighneallem4a  39847  perfectALTVlem2  39949  wwlksnredwwlkn  41082  wwlksnextproplem3  41098  wwlksext2clwwlk  41212  wwlksubclwwlks  41213  clwlksfclwwlk  41250  eupth2lems  41387  logbpw2m1  42140
  Copyright terms: Public domain W3C validator