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

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

Proof of Theorem peano2re
StepHypRef Expression
1 1re 10619 . 2 1 ∈ ℝ
2 readdcl 10598 . 2 ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐴 + 1) ∈ ℝ)
31, 2mpan2 689 1 (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2114  (class class class)co 7133  cr 10514  1c1 10516   + caddc 10518
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-1cn 10573  ax-icn 10574  ax-addcl 10575  ax-addrcl 10576  ax-mulcl 10577  ax-mulrcl 10578  ax-i2m1 10583  ax-1ne0 10584  ax-rrecex 10587  ax-cnre 10588
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ne 3007  df-ral 3130  df-rex 3131  df-rab 3134  df-v 3475  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4270  df-if 4444  df-sn 4544  df-pr 4546  df-op 4550  df-uni 4815  df-br 5043  df-iota 6290  df-fv 6339  df-ov 7136
This theorem is referenced by:  lep1  11459  letrp1  11462  p1le  11463  ledivp1  11520  sup2  11575  nnssre  11620  nnge1  11644  div4p1lem1div2  11871  zltp1le  12011  suprzcl  12041  zeo  12047  peano2uz2  12049  uzind  12053  numltc  12103  uzwo  12290  ge0p1rp  12399  qbtwnxr  12572  xrsupsslem  12679  supxrunb1  12691  fznatpl1  12945  fzp1disj  12950  fzneuz  12972  fzp1nel  12975  ubmelm1fzo  13117  fllep1  13155  flflp1  13161  flhalf  13184  ltdifltdiv  13188  fldiv4p1lem1div2  13189  dfceil2  13193  ceim1l  13199  uzsup  13215  modltm1p1mod  13275  addmodlteq  13298  fsequb  13327  seqf1olem1  13394  seqf1olem2  13395  bernneq3  13577  expnbnd  13578  expmulnbnd  13581  discr1  13585  discr  13586  facwordi  13634  faclbnd  13635  hashfun  13783  seqcoll2  13808  rexuzre  14692  caubnd  14698  rlim2lt  14834  lo1bddrp  14862  rlimo1  14953  o1rlimmul  14955  o1fsum  15148  harmonic  15194  expcnv  15199  geomulcvg  15212  mertenslem1  15220  bpoly4  15393  nonsq  16077  eulerthlem2  16097  pcprendvds  16155  pcmpt  16206  pcfac  16213  vdwlem6  16300  vdwlem11  16305  chfacffsupp  21440  chfacfscmul0  21442  chfacfpmmul0  21446  tgioo  23380  zcld  23397  iocopnst  23524  cnheibor  23539  bndth  23542  cncmet  23905  pjthlem1  24020  ovolicc2lem3  24102  ovolicopnf  24107  ioorcl2  24155  dyadf  24174  dyadovol  24176  dyadss  24177  dyaddisjlem  24178  dyadmaxlem  24180  opnmbllem  24184  volsup2  24188  vitalilem2  24192  itg2const2  24324  itg2cnlem1  24344  dvfsumle  24603  dvfsumabs  24605  dvfsumlem1  24608  dvfsumlem3  24610  dvfsumrlim  24613  fta1glem2  24746  fta1lem  24882  aalioulem3  24909  ulmbdd  24972  itgulm  24982  psercnlem1  24999  abelthlem2  25006  abelthlem7  25012  reeff1olem  25020  logtayl  25230  loglesqrt  25326  atanlogsublem  25480  leibpi  25507  efrlim  25534  harmonicubnd  25574  fsumharmonic  25576  ftalem5  25641  basellem2  25646  basellem3  25647  chtnprm  25718  chpp1  25719  ppip1le  25725  ppiub  25767  logfaclbnd  25785  logfacrlim  25787  perfectlem2  25793  bcmono  25840  lgsvalmod  25879  gausslemma2dlem3  25931  lgseisen  25942  lgsquadlem1  25943  lgsquadlem2  25944  chebbnd1lem2  26033  chtppilimlem1  26036  rplogsumlem2  26048  dchrisumlema  26051  dchrisumlem1  26052  dchrisumlem3  26054  dchrisum0lem1  26079  chpdifbndlem1  26116  logdivbnd  26119  pntrmax  26127  pntrsumo1  26128  pntpbnd1a  26148  pntpbnd1  26149  pntpbnd2  26150  pntibndlem2  26154  pntlemg  26161  pntlemr  26165  pntlemj  26166  pntlemk  26169  ostth2lem1  26181  qabvle  26188  ostth2lem3  26198  ostth2lem4  26199  axlowdimlem16  26730  wwlksnredwwlkn  27660  wwlksnextproplem3  27676  wwlksext2clwwlk  27821  wwlksubclwwlk  27822  eupth2lems  28002  smcnlem  28459  minvecolem4  28642  pjhthlem1  29153  zltp1ne  32356  cvmliftlem7  32546  dnibndlem13  33837  knoppndvlem19  33877  knoppndvlem21  33879  icoreunrn  34657  relowlssretop  34661  ltflcei  34921  poimirlem1  34934  poimirlem2  34935  poimirlem4  34937  poimirlem6  34939  poimirlem7  34940  poimirlem8  34941  opnmbllem0  34969  mblfinlem1  34970  mblfinlem2  34971  mblfinlem4  34973  itg2addnclem2  34985  itg2addnclem3  34986  incsequz  35062  isbnd3  35098  rrntotbnd  35150  3cubeslem1  39418  3cubeslem2  39419  irrapxlem4  39559  pellexlem5  39567  pell14qrgapw  39610  pellfundgt1  39617  jm3.1lem2  39752  expdiophlem1  39755  zltlesub  41705  suplesup  41761  supxrunb3  41826  xrpnf  41916  fmul01lt1lem1  42017  limsupre3lem  42165  xlimxrre  42264  xlimpnfv  42271  ioodvbdlimc1lem1  42364  dvnxpaek  42375  dvnmul  42376  fourierdlem4  42544  fourierdlem11  42551  fourierdlem25  42565  fourierdlem50  42589  fourierdlem64  42603  fourierdlem65  42604  fourierdlem77  42616  fourierdlem79  42618  iinhoiicclem  43103  smfresal  43211  fmtno4prmfac  43880  lighneallem4a  43918  evenltle  44027  perfectALTVlem2  44032  logbpw2m1  44772
  Copyright terms: Public domain W3C validator