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

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

Proof of Theorem peano2re
StepHypRef Expression
1 1re 10630 . 2 1 ∈ ℝ
2 readdcl 10609 . 2 ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐴 + 1) ∈ ℝ)
31, 2mpan2 687 1 (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  (class class class)co 7145  cr 10525  1c1 10527   + caddc 10529
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-i2m1 10594  ax-1ne0 10595  ax-rrecex 10598  ax-cnre 10599
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4833  df-br 5059  df-iota 6308  df-fv 6357  df-ov 7148
This theorem is referenced by:  lep1  11470  letrp1  11473  p1le  11474  ledivp1  11531  sup2  11586  nnssre  11631  nnge1  11654  div4p1lem1div2  11881  zltp1le  12021  suprzcl  12051  zeo  12057  peano2uz2  12059  uzind  12063  numltc  12113  uzwo  12300  ge0p1rp  12410  qbtwnxr  12583  xrsupsslem  12690  supxrunb1  12702  fznatpl1  12951  fzp1disj  12956  fzneuz  12978  fzp1nel  12981  ubmelm1fzo  13123  fllep1  13161  flflp1  13167  flhalf  13190  ltdifltdiv  13194  fldiv4p1lem1div2  13195  dfceil2  13199  ceim1l  13205  uzsup  13221  modltm1p1mod  13281  addmodlteq  13304  fsequb  13333  seqf1olem1  13399  seqf1olem2  13400  bernneq3  13582  expnbnd  13583  expmulnbnd  13586  discr1  13590  discr  13591  facwordi  13639  faclbnd  13640  hashfun  13788  seqcoll2  13813  rexuzre  14702  caubnd  14708  rlim2lt  14844  lo1bddrp  14872  rlimo1  14963  o1rlimmul  14965  o1fsum  15158  harmonic  15204  expcnv  15209  geomulcvg  15222  mertenslem1  15230  bpoly4  15403  nonsq  16089  eulerthlem2  16109  pcprendvds  16167  pcmpt  16218  pcfac  16225  vdwlem6  16312  vdwlem11  16317  chfacffsupp  21394  chfacfscmul0  21396  chfacfpmmul0  21400  tgioo  23333  zcld  23350  iocopnst  23473  cnheibor  23488  bndth  23491  cncmet  23854  pjthlem1  23969  ovolicc2lem3  24049  ovolicopnf  24054  ioorcl2  24102  dyadf  24121  dyadovol  24123  dyadss  24124  dyaddisjlem  24125  dyadmaxlem  24127  opnmbllem  24131  volsup2  24135  vitalilem2  24139  itg2const2  24271  itg2cnlem1  24291  dvfsumle  24547  dvfsumabs  24549  dvfsumlem1  24552  dvfsumlem3  24554  dvfsumrlim  24557  fta1glem2  24689  fta1lem  24825  aalioulem3  24852  ulmbdd  24915  itgulm  24925  psercnlem1  24942  abelthlem2  24949  abelthlem7  24955  reeff1olem  24963  logtayl  25170  loglesqrt  25266  atanlogsublem  25420  leibpi  25448  efrlim  25475  harmonicubnd  25515  fsumharmonic  25517  ftalem5  25582  basellem2  25587  basellem3  25588  chtnprm  25659  chpp1  25660  ppip1le  25666  ppiub  25708  logfaclbnd  25726  logfacrlim  25728  perfectlem2  25734  bcmono  25781  lgsvalmod  25820  gausslemma2dlem3  25872  lgseisen  25883  lgsquadlem1  25884  lgsquadlem2  25885  chebbnd1lem2  25974  chtppilimlem1  25977  rplogsumlem2  25989  dchrisumlema  25992  dchrisumlem1  25993  dchrisumlem3  25995  dchrisum0lem1  26020  chpdifbndlem1  26057  logdivbnd  26060  pntrmax  26068  pntrsumo1  26069  pntpbnd1a  26089  pntpbnd1  26090  pntpbnd2  26091  pntibndlem2  26095  pntlemg  26102  pntlemr  26106  pntlemj  26107  pntlemk  26110  ostth2lem1  26122  qabvle  26129  ostth2lem3  26139  ostth2lem4  26140  axlowdimlem16  26671  wwlksnredwwlkn  27601  wwlksnextproplem3  27618  wwlksext2clwwlk  27764  wwlksubclwwlk  27765  eupth2lems  27945  smcnlem  28402  minvecolem4  28585  pjhthlem1  29096  zltp1ne  32246  cvmliftlem7  32436  dnibndlem13  33727  knoppndvlem19  33767  knoppndvlem21  33769  icoreunrn  34523  relowlssretop  34527  ltflcei  34762  poimirlem1  34775  poimirlem2  34776  poimirlem4  34778  poimirlem6  34780  poimirlem7  34781  poimirlem8  34782  opnmbllem0  34810  mblfinlem1  34811  mblfinlem2  34812  mblfinlem4  34814  itg2addnclem2  34826  itg2addnclem3  34827  incsequz  34906  isbnd3  34945  rrntotbnd  34997  3cubeslem1  39161  3cubeslem2  39162  irrapxlem4  39302  pellexlem5  39310  pell14qrgapw  39353  pellfundgt1  39360  jm3.1lem2  39495  expdiophlem1  39498  zltlesub  41431  suplesup  41487  supxrunb3  41552  xrpnf  41642  fmul01lt1lem1  41745  limsupre3lem  41893  xlimxrre  41992  xlimpnfv  41999  ioodvbdlimc1lem1  42096  dvnxpaek  42107  dvnmul  42108  fourierdlem4  42277  fourierdlem11  42284  fourierdlem25  42298  fourierdlem50  42322  fourierdlem64  42336  fourierdlem65  42337  fourierdlem77  42349  fourierdlem79  42351  iinhoiicclem  42836  smfresal  42944  fmtno4prmfac  43581  lighneallem4a  43620  evenltle  43729  perfectALTVlem2  43734  logbpw2m1  44525
  Copyright terms: Public domain W3C validator