Theorem peano2re 11289

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

Assertion

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

Proof of Theorem peano2re

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7349  ℝcr 11008  1c1 11010   + caddc 11012

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-i2m1 11077  ax-1ne0 11078  ax-rrecex 11081  ax-cnre 11082

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490  df-ov 7352

This theorem is referenced by:  lep1  11965  letrp1  11968  p1le  11969  ledivp1  12027  sup2  12081  nnssre  12132  nnge1  12156  div4p1lem1div2  12379  zltp1le  12525  suprzcl  12556  zeo  12562  peano2uz2  12564  uzind  12568  numltc  12617  uzwo  12812  ge0p1rp  12926  qbtwnxr  13102  xrsupsslem  13209  supxrunb1  13221  fznatpl1  13481  fzp1disj  13486  fzneuz  13511  fzp1nel  13514  ubmelm1fzo  13666  fllep1  13705  flflp1  13711  flhalf  13734  ltdifltdiv  13738  fldiv4p1lem1div2  13739  dfceil2  13743  ceim1l  13751  uzsup  13767  modltm1p1mod  13830  addmodlteq  13853  fsequb  13882  seqf1olem1  13948  seqf1olem2  13949  bernneq3  14138  expnbnd  14139  expmulnbnd  14142  discr1  14146  discr  14147  facwordi  14196  faclbnd  14197  hashfun  14344  seqcoll2  14372  rexuzre  15260  caubnd  15266  rlim2lt  15404  lo1bddrp  15432  rlimo1  15524  o1rlimmul  15526  o1fsum  15720  harmonic  15766  expcnv  15771  geomulcvg  15783  mertenslem1  15791  bpoly4  15966  nonsq  16670  eulerthlem2  16693  pcprendvds  16752  pcmpt  16804  pcfac  16811  vdwlem6  16898  vdwlem11  16903  chfacffsupp  22741  chfacfscmul0  22743  chfacfpmmul0  22747  tgioo  24682  zcld  24700  iocopnst  24835  cnheibor  24852  bndth  24855  cncmet  25220  pjthlem1  25335  ovolicc2lem3  25418  ovolicopnf  25423  ioorcl2  25471  dyadf  25490  dyadovol  25492  dyadss  25493  dyaddisjlem  25494  dyadmaxlem  25496  opnmbllem  25500  volsup2  25504  vitalilem2  25508  itg2const2  25640  itg2cnlem1  25660  dvfsumle  25924  dvfsumleOLD  25925  dvfsumabs  25927  dvfsumlem1  25930  dvfsumlem3  25933  dvfsumrlim  25936  fta1glem2  26072  fta1lem  26213  aalioulem3  26240  ulmbdd  26305  itgulm  26315  psercnlem1  26333  abelthlem2  26340  abelthlem7  26346  reeff1olem  26354  logtayl  26567  loglesqrt  26669  atanlogsublem  26823  leibpi  26850  efrlim  26877  efrlimOLD  26878  harmonicubnd  26918  fsumharmonic  26920  ftalem5  26985  basellem2  26990  basellem3  26991  chtnprm  27062  chpp1  27063  ppip1le  27069  ppiub  27113  logfaclbnd  27131  logfacrlim  27133  perfectlem2  27139  bcmono  27186  lgsvalmod  27225  gausslemma2dlem3  27277  lgseisen  27288  lgsquadlem1  27289  lgsquadlem2  27290  chebbnd1lem2  27379  chtppilimlem1  27382  rplogsumlem2  27394  dchrisumlema  27397  dchrisumlem1  27398  dchrisumlem3  27400  dchrisum0lem1  27425  chpdifbndlem1  27462  logdivbnd  27465  pntrmax  27473  pntrsumo1  27474  pntpbnd1a  27494  pntpbnd1  27495  pntpbnd2  27496  pntibndlem2  27500  pntlemg  27507  pntlemr  27511  pntlemj  27512  pntlemk  27515  ostth2lem1  27527  qabvle  27534  ostth2lem3  27544  ostth2lem4  27545  axlowdimlem16  28902  wwlksnredwwlkn  29840  wwlksnextproplem3  29856  wwlksext2clwwlk  30001  wwlksubclwwlk  30002  eupth2lems  30182  smcnlem  30641  minvecolem4  30824  pjhthlem1  31335  zltp1ne  35083  cvmliftlem7  35264  dnibndlem13  36464  knoppndvlem19  36504  knoppndvlem21  36506  icoreunrn  37333  relowlssretop  37337  ltflcei  37588  poimirlem1  37601  poimirlem2  37602  poimirlem4  37604  poimirlem6  37606  poimirlem7  37607  poimirlem8  37608  opnmbllem0  37636  mblfinlem1  37637  mblfinlem2  37638  mblfinlem4  37640  itg2addnclem2  37652  itg2addnclem3  37653  incsequz  37728  isbnd3  37764  rrntotbnd  37816  sn-sup2  42464  3cubeslem1  42657  3cubeslem2  42658  irrapxlem4  42798  pellexlem5  42806  pell14qrgapw  42849  pellfundgt1  42856  jm3.1lem2  42991  expdiophlem1  42994  fzuntgd  43431  zltlesub  45267  suplesup  45319  supxrunb3  45378  xrpnf  45464  fmul01lt1lem1  45565  limsupre3lem  45713  xlimxrre  45812  xlimpnfv  45819  ioodvbdlimc1lem1  45912  dvnxpaek  45923  dvnmul  45924  fourierdlem4  46092  fourierdlem11  46099  fourierdlem25  46113  fourierdlem50  46137  fourierdlem64  46151  fourierdlem65  46152  fourierdlem77  46164  fourierdlem79  46166  iinhoiicclem  46654  smfresal  46769  natglobalincr  46858  fmtno4prmfac  47556  lighneallem4a  47592  evenltle  47701  perfectALTVlem2  47706  logbpw2m1  48552