Theorem peano2re 10894

Description: A theorem for reals analogous the second Peano postulate peano2nn 11731. (Contributed by NM, 5-Jul-2005.)

Assertion

Ref	Expression
peano2re	⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ)

Proof of Theorem peano2re

Step	Hyp	Ref	Expression
1		1re 10722	. 2 ⊢ 1 ∈ ℝ
2		readdcl 10701	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐴 + 1) ∈ ℝ)
3	1, 2	mpan2 691	1 ⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7173  ℝcr 10617  1c1 10619   + caddc 10621

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2711  ax-1cn 10676  ax-icn 10677  ax-addcl 10678  ax-addrcl 10679  ax-mulcl 10680  ax-mulrcl 10681  ax-i2m1 10686  ax-1ne0 10687  ax-rrecex 10690  ax-cnre 10691

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-ne 2936  df-ral 3059  df-rex 3060  df-v 3401  df-un 3849  df-in 3851  df-ss 3861  df-sn 4518  df-pr 4520  df-op 4524  df-uni 4798  df-br 5032  df-iota 6298  df-fv 6348  df-ov 7176

This theorem is referenced by:  lep1  11562  letrp1  11565  p1le  11566  ledivp1  11623  sup2  11677  nnssre  11723  nnge1  11747  div4p1lem1div2  11974  zltp1le  12116  suprzcl  12146  zeo  12152  peano2uz2  12154  uzind  12158  numltc  12208  uzwo  12396  ge0p1rp  12506  qbtwnxr  12679  xrsupsslem  12786  supxrunb1  12798  fznatpl1  13055  fzp1disj  13060  fzneuz  13082  fzp1nel  13085  ubmelm1fzo  13227  fllep1  13265  flflp1  13271  flhalf  13294  ltdifltdiv  13298  fldiv4p1lem1div2  13299  dfceil2  13303  ceim1l  13309  uzsup  13325  modltm1p1mod  13385  addmodlteq  13408  fsequb  13437  seqf1olem1  13504  seqf1olem2  13505  bernneq3  13687  expnbnd  13688  expmulnbnd  13691  discr1  13695  discr  13696  facwordi  13744  faclbnd  13745  hashfun  13893  seqcoll2  13920  rexuzre  14805  caubnd  14811  rlim2lt  14947  lo1bddrp  14975  rlimo1  15067  o1rlimmul  15069  o1fsum  15264  harmonic  15310  expcnv  15315  geomulcvg  15327  mertenslem1  15335  bpoly4  15508  nonsq  16202  eulerthlem2  16222  pcprendvds  16280  pcmpt  16331  pcfac  16338  vdwlem6  16425  vdwlem11  16430  chfacffsupp  21610  chfacfscmul0  21612  chfacfpmmul0  21616  tgioo  23551  zcld  23568  iocopnst  23695  cnheibor  23710  bndth  23713  cncmet  24077  pjthlem1  24192  ovolicc2lem3  24274  ovolicopnf  24279  ioorcl2  24327  dyadf  24346  dyadovol  24348  dyadss  24349  dyaddisjlem  24350  dyadmaxlem  24352  opnmbllem  24356  volsup2  24360  vitalilem2  24364  itg2const2  24497  itg2cnlem1  24517  dvfsumle  24776  dvfsumabs  24778  dvfsumlem1  24781  dvfsumlem3  24783  dvfsumrlim  24786  fta1glem2  24922  fta1lem  25058  aalioulem3  25085  ulmbdd  25148  itgulm  25158  psercnlem1  25175  abelthlem2  25182  abelthlem7  25188  reeff1olem  25196  logtayl  25406  loglesqrt  25502  atanlogsublem  25656  leibpi  25683  efrlim  25710  harmonicubnd  25750  fsumharmonic  25752  ftalem5  25817  basellem2  25822  basellem3  25823  chtnprm  25894  chpp1  25895  ppip1le  25901  ppiub  25943  logfaclbnd  25961  logfacrlim  25963  perfectlem2  25969  bcmono  26016  lgsvalmod  26055  gausslemma2dlem3  26107  lgseisen  26118  lgsquadlem1  26119  lgsquadlem2  26120  chebbnd1lem2  26209  chtppilimlem1  26212  rplogsumlem2  26224  dchrisumlema  26227  dchrisumlem1  26228  dchrisumlem3  26230  dchrisum0lem1  26255  chpdifbndlem1  26292  logdivbnd  26295  pntrmax  26303  pntrsumo1  26304  pntpbnd1a  26324  pntpbnd1  26325  pntpbnd2  26326  pntibndlem2  26330  pntlemg  26337  pntlemr  26341  pntlemj  26342  pntlemk  26345  ostth2lem1  26357  qabvle  26364  ostth2lem3  26374  ostth2lem4  26375  axlowdimlem16  26906  wwlksnredwwlkn  27836  wwlksnextproplem3  27852  wwlksext2clwwlk  27997  wwlksubclwwlk  27998  eupth2lems  28178  smcnlem  28635  minvecolem4  28818  pjhthlem1  29329  zltp1ne  32642  cvmliftlem7  32827  dnibndlem13  34316  knoppndvlem19  34356  knoppndvlem21  34358  icoreunrn  35176  relowlssretop  35180  ltflcei  35411  poimirlem1  35424  poimirlem2  35425  poimirlem4  35427  poimirlem6  35429  poimirlem7  35430  poimirlem8  35431  opnmbllem0  35459  mblfinlem1  35460  mblfinlem2  35461  mblfinlem4  35463  itg2addnclem2  35475  itg2addnclem3  35476  incsequz  35552  isbnd3  35588  rrntotbnd  35640  sn-sup2  40039  3cubeslem1  40101  3cubeslem2  40102  irrapxlem4  40242  pellexlem5  40250  pell14qrgapw  40293  pellfundgt1  40300  jm3.1lem2  40435  expdiophlem1  40438  zltlesub  42384  suplesup  42439  supxrunb3  42500  xrpnf  42589  fmul01lt1lem1  42690  limsupre3lem  42838  xlimxrre  42937  xlimpnfv  42944  ioodvbdlimc1lem1  43037  dvnxpaek  43048  dvnmul  43049  fourierdlem4  43217  fourierdlem11  43224  fourierdlem25  43238  fourierdlem50  43262  fourierdlem64  43276  fourierdlem65  43277  fourierdlem77  43289  fourierdlem79  43291  iinhoiicclem  43776  smfresal  43884  fmtno4prmfac  44588  lighneallem4a  44624  evenltle  44733  perfectALTVlem2  44738  logbpw2m1  45477