Theorem peano2re 11431

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

Assertion

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

Proof of Theorem peano2re

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

Syntax hints:   → wi 4   ∈ wcel 2105  (class class class)co 7430  ℝcr 11151  1c1 11153   + caddc 11155

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-i2m1 11220  ax-1ne0 11221  ax-rrecex 11224  ax-cnre 11225

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-ov 7433

This theorem is referenced by:  lep1  12105  letrp1  12108  p1le  12109  ledivp1  12167  sup2  12221  nnssre  12267  nnge1  12291  div4p1lem1div2  12518  zltp1le  12664  suprzcl  12695  zeo  12701  peano2uz2  12703  uzind  12707  numltc  12756  uzwo  12950  ge0p1rp  13063  qbtwnxr  13238  xrsupsslem  13345  supxrunb1  13357  fznatpl1  13614  fzp1disj  13619  fzneuz  13644  fzp1nel  13647  ubmelm1fzo  13798  fllep1  13837  flflp1  13843  flhalf  13866  ltdifltdiv  13870  fldiv4p1lem1div2  13871  dfceil2  13875  ceim1l  13883  uzsup  13899  modltm1p1mod  13960  addmodlteq  13983  fsequb  14012  seqf1olem1  14078  seqf1olem2  14079  bernneq3  14266  expnbnd  14267  expmulnbnd  14270  discr1  14274  discr  14275  facwordi  14324  faclbnd  14325  hashfun  14472  seqcoll2  14500  rexuzre  15387  caubnd  15393  rlim2lt  15529  lo1bddrp  15557  rlimo1  15649  o1rlimmul  15651  o1fsum  15845  harmonic  15891  expcnv  15896  geomulcvg  15908  mertenslem1  15916  bpoly4  16091  nonsq  16792  eulerthlem2  16815  pcprendvds  16873  pcmpt  16925  pcfac  16932  vdwlem6  17019  vdwlem11  17024  chfacffsupp  22877  chfacfscmul0  22879  chfacfpmmul0  22883  tgioo  24831  zcld  24848  iocopnst  24983  cnheibor  25000  bndth  25003  cncmet  25369  pjthlem1  25484  ovolicc2lem3  25567  ovolicopnf  25572  ioorcl2  25620  dyadf  25639  dyadovol  25641  dyadss  25642  dyaddisjlem  25643  dyadmaxlem  25645  opnmbllem  25649  volsup2  25653  vitalilem2  25657  itg2const2  25790  itg2cnlem1  25810  dvfsumle  26074  dvfsumleOLD  26075  dvfsumabs  26077  dvfsumlem1  26080  dvfsumlem3  26083  dvfsumrlim  26086  fta1glem2  26222  fta1lem  26363  aalioulem3  26390  ulmbdd  26455  itgulm  26465  psercnlem1  26483  abelthlem2  26490  abelthlem7  26496  reeff1olem  26504  logtayl  26716  loglesqrt  26818  atanlogsublem  26972  leibpi  26999  efrlim  27026  efrlimOLD  27027  harmonicubnd  27067  fsumharmonic  27069  ftalem5  27134  basellem2  27139  basellem3  27140  chtnprm  27211  chpp1  27212  ppip1le  27218  ppiub  27262  logfaclbnd  27280  logfacrlim  27282  perfectlem2  27288  bcmono  27335  lgsvalmod  27374  gausslemma2dlem3  27426  lgseisen  27437  lgsquadlem1  27438  lgsquadlem2  27439  chebbnd1lem2  27528  chtppilimlem1  27531  rplogsumlem2  27543  dchrisumlema  27546  dchrisumlem1  27547  dchrisumlem3  27549  dchrisum0lem1  27574  chpdifbndlem1  27611  logdivbnd  27614  pntrmax  27622  pntrsumo1  27623  pntpbnd1a  27643  pntpbnd1  27644  pntpbnd2  27645  pntibndlem2  27649  pntlemg  27656  pntlemr  27660  pntlemj  27661  pntlemk  27664  ostth2lem1  27676  qabvle  27683  ostth2lem3  27693  ostth2lem4  27694  axlowdimlem16  28986  wwlksnredwwlkn  29924  wwlksnextproplem3  29940  wwlksext2clwwlk  30085  wwlksubclwwlk  30086  eupth2lems  30266  smcnlem  30725  minvecolem4  30908  pjhthlem1  31419  zltp1ne  35093  cvmliftlem7  35275  dnibndlem13  36472  knoppndvlem19  36512  knoppndvlem21  36514  icoreunrn  37341  relowlssretop  37345  ltflcei  37594  poimirlem1  37607  poimirlem2  37608  poimirlem4  37610  poimirlem6  37612  poimirlem7  37613  poimirlem8  37614  opnmbllem0  37642  mblfinlem1  37643  mblfinlem2  37644  mblfinlem4  37646  itg2addnclem2  37658  itg2addnclem3  37659  incsequz  37734  isbnd3  37770  rrntotbnd  37822  sn-sup2  42477  3cubeslem1  42671  3cubeslem2  42672  irrapxlem4  42812  pellexlem5  42820  pell14qrgapw  42863  pellfundgt1  42870  jm3.1lem2  43006  expdiophlem1  43009  fzuntgd  43447  zltlesub  45235  suplesup  45288  supxrunb3  45348  xrpnf  45435  fmul01lt1lem1  45539  limsupre3lem  45687  xlimxrre  45786  xlimpnfv  45793  ioodvbdlimc1lem1  45886  dvnxpaek  45897  dvnmul  45898  fourierdlem4  46066  fourierdlem11  46073  fourierdlem25  46087  fourierdlem50  46111  fourierdlem64  46125  fourierdlem65  46126  fourierdlem77  46138  fourierdlem79  46140  iinhoiicclem  46628  smfresal  46743  natglobalincr  46830  fmtno4prmfac  47496  lighneallem4a  47532  evenltle  47641  perfectALTVlem2  47646  logbpw2m1  48416