Theorem peano2re 11320

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

Assertion

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

Proof of Theorem peano2re

Step	Hyp	Ref	Expression
1		1re 11146	. 2 ⊢ 1 ∈ ℝ
2		readdcl 11123	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐴 + 1) ∈ ℝ)
3	1, 2	mpan2 692	1 ⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7370  ℝcr 11039  1c1 11041   + caddc 11043

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-1cn 11098  ax-icn 11099  ax-addcl 11100  ax-addrcl 11101  ax-mulcl 11102  ax-mulrcl 11103  ax-i2m1 11108  ax-1ne0 11109  ax-rrecex 11112  ax-cnre 11113

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6458  df-fv 6510  df-ov 7373

This theorem is referenced by:  lep1  11996  letrp1  11999  p1le  12000  ledivp1  12058  sup2  12112  nnssre  12163  nnge1  12187  div4p1lem1div2  12410  zltp1le  12555  suprzcl  12586  zeo  12592  peano2uz2  12594  uzind  12598  numltc  12647  uzwo  12838  ge0p1rp  12952  qbtwnxr  13129  xrsupsslem  13236  supxrunb1  13248  fznatpl1  13508  fzp1disj  13513  fzneuz  13538  fzp1nel  13541  ubmelm1fzo  13693  fllep1  13735  flflp1  13741  flhalf  13764  ltdifltdiv  13768  fldiv4p1lem1div2  13769  dfceil2  13773  ceim1l  13781  uzsup  13797  modltm1p1mod  13860  addmodlteq  13883  fsequb  13912  seqf1olem1  13978  seqf1olem2  13979  bernneq3  14168  expnbnd  14169  expmulnbnd  14172  discr1  14176  discr  14177  facwordi  14226  faclbnd  14227  hashfun  14374  seqcoll2  14402  rexuzre  15290  caubnd  15296  rlim2lt  15434  lo1bddrp  15462  rlimo1  15554  o1rlimmul  15556  o1fsum  15750  harmonic  15796  expcnv  15801  geomulcvg  15813  mertenslem1  15821  bpoly4  15996  nonsq  16700  eulerthlem2  16723  pcprendvds  16782  pcmpt  16834  pcfac  16841  vdwlem6  16928  vdwlem11  16933  chnccat  18563  chfacffsupp  22817  chfacfscmul0  22819  chfacfpmmul0  22823  tgioo  24757  zcld  24775  iocopnst  24910  cnheibor  24927  bndth  24930  cncmet  25295  pjthlem1  25410  ovolicc2lem3  25493  ovolicopnf  25498  ioorcl2  25546  dyadf  25565  dyadovol  25567  dyadss  25568  dyaddisjlem  25569  dyadmaxlem  25571  opnmbllem  25575  volsup2  25579  vitalilem2  25583  itg2const2  25715  itg2cnlem1  25735  dvfsumle  25999  dvfsumleOLD  26000  dvfsumabs  26002  dvfsumlem1  26005  dvfsumlem3  26008  dvfsumrlim  26011  fta1glem2  26147  fta1lem  26288  aalioulem3  26315  ulmbdd  26380  itgulm  26390  psercnlem1  26408  abelthlem2  26415  abelthlem7  26421  reeff1olem  26429  logtayl  26642  loglesqrt  26744  atanlogsublem  26898  leibpi  26925  efrlim  26952  efrlimOLD  26953  harmonicubnd  26993  fsumharmonic  26995  ftalem5  27060  basellem2  27065  basellem3  27066  chtnprm  27137  chpp1  27138  ppip1le  27144  ppiub  27188  logfaclbnd  27206  logfacrlim  27208  perfectlem2  27214  bcmono  27261  lgsvalmod  27300  gausslemma2dlem3  27352  lgseisen  27363  lgsquadlem1  27364  lgsquadlem2  27365  chebbnd1lem2  27454  chtppilimlem1  27457  rplogsumlem2  27469  dchrisumlema  27472  dchrisumlem1  27473  dchrisumlem3  27475  dchrisum0lem1  27500  chpdifbndlem1  27537  logdivbnd  27540  pntrmax  27548  pntrsumo1  27549  pntpbnd1a  27569  pntpbnd1  27570  pntpbnd2  27571  pntibndlem2  27575  pntlemg  27582  pntlemr  27586  pntlemj  27587  pntlemk  27590  ostth2lem1  27602  qabvle  27609  ostth2lem3  27619  ostth2lem4  27620  axlowdimlem16  29048  wwlksnredwwlkn  29986  wwlksnextproplem3  30002  wwlksext2clwwlk  30150  wwlksubclwwlk  30151  eupth2lems  30331  smcnlem  30791  minvecolem4  30974  pjhthlem1  31485  zltp1ne  35332  cvmliftlem7  35513  dnibndlem13  36718  knoppndvlem19  36758  knoppndvlem21  36760  icoreunrn  37641  relowlssretop  37645  ltflcei  37888  poimirlem1  37901  poimirlem2  37902  poimirlem4  37904  poimirlem6  37906  poimirlem7  37907  poimirlem8  37908  opnmbllem0  37936  mblfinlem1  37937  mblfinlem2  37938  mblfinlem4  37940  itg2addnclem2  37952  itg2addnclem3  37953  incsequz  38028  isbnd3  38064  rrntotbnd  38116  sn-sup2  42890  3cubeslem1  43070  3cubeslem2  43071  irrapxlem4  43211  pellexlem5  43219  pell14qrgapw  43262  pellfundgt1  43269  jm3.1lem2  43404  expdiophlem1  43407  fzuntgd  43843  zltlesub  45676  suplesup  45727  supxrunb3  45786  xrpnf  45872  fmul01lt1lem1  45973  limsupre3lem  46119  xlimxrre  46218  xlimpnfv  46225  ioodvbdlimc1lem1  46318  dvnxpaek  46329  dvnmul  46330  fourierdlem4  46498  fourierdlem11  46505  fourierdlem25  46519  fourierdlem50  46543  fourierdlem64  46557  fourierdlem65  46558  fourierdlem77  46570  fourierdlem79  46572  iinhoiicclem  47060  smfresal  47175  natglobalincr  47264  fmtno4prmfac  47961  lighneallem4a  47997  evenltle  48106  perfectALTVlem2  48111  logbpw2m1  48956