Theorem peano2re 10802

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

Assertion

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

Proof of Theorem peano2re

Step	Hyp	Ref	Expression
1		1re 10630	. 2 ⊢ 1 ∈ ℝ
2		readdcl 10609	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐴 + 1) ∈ ℝ)
3	1, 2	mpan2 690	1 ⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2111  (class class class)co 7135  ℝcr 10525  1c1 10527   + caddc 10529

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-i2m1 10594  ax-1ne0 10595  ax-rrecex 10598  ax-cnre 10599

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ne 2988  df-ral 3111  df-rex 3112  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-ov 7138

This theorem is referenced by:  lep1  11470  letrp1  11473  p1le  11474  ledivp1  11531  sup2  11584  nnssre  11629  nnge1  11653  div4p1lem1div2  11880  zltp1le  12020  suprzcl  12050  zeo  12056  peano2uz2  12058  uzind  12062  numltc  12112  uzwo  12299  ge0p1rp  12408  qbtwnxr  12581  xrsupsslem  12688  supxrunb1  12700  fznatpl1  12956  fzp1disj  12961  fzneuz  12983  fzp1nel  12986  ubmelm1fzo  13128  fllep1  13166  flflp1  13172  flhalf  13195  ltdifltdiv  13199  fldiv4p1lem1div2  13200  dfceil2  13204  ceim1l  13210  uzsup  13226  modltm1p1mod  13286  addmodlteq  13309  fsequb  13338  seqf1olem1  13405  seqf1olem2  13406  bernneq3  13588  expnbnd  13589  expmulnbnd  13592  discr1  13596  discr  13597  facwordi  13645  faclbnd  13646  hashfun  13794  seqcoll2  13819  rexuzre  14704  caubnd  14710  rlim2lt  14846  lo1bddrp  14874  rlimo1  14965  o1rlimmul  14967  o1fsum  15160  harmonic  15206  expcnv  15211  geomulcvg  15224  mertenslem1  15232  bpoly4  15405  nonsq  16089  eulerthlem2  16109  pcprendvds  16167  pcmpt  16218  pcfac  16225  vdwlem6  16312  vdwlem11  16317  chfacffsupp  21461  chfacfscmul0  21463  chfacfpmmul0  21467  tgioo  23401  zcld  23418  iocopnst  23545  cnheibor  23560  bndth  23563  cncmet  23926  pjthlem1  24041  ovolicc2lem3  24123  ovolicopnf  24128  ioorcl2  24176  dyadf  24195  dyadovol  24197  dyadss  24198  dyaddisjlem  24199  dyadmaxlem  24201  opnmbllem  24205  volsup2  24209  vitalilem2  24213  itg2const2  24345  itg2cnlem1  24365  dvfsumle  24624  dvfsumabs  24626  dvfsumlem1  24629  dvfsumlem3  24631  dvfsumrlim  24634  fta1glem2  24767  fta1lem  24903  aalioulem3  24930  ulmbdd  24993  itgulm  25003  psercnlem1  25020  abelthlem2  25027  abelthlem7  25033  reeff1olem  25041  logtayl  25251  loglesqrt  25347  atanlogsublem  25501  leibpi  25528  efrlim  25555  harmonicubnd  25595  fsumharmonic  25597  ftalem5  25662  basellem2  25667  basellem3  25668  chtnprm  25739  chpp1  25740  ppip1le  25746  ppiub  25788  logfaclbnd  25806  logfacrlim  25808  perfectlem2  25814  bcmono  25861  lgsvalmod  25900  gausslemma2dlem3  25952  lgseisen  25963  lgsquadlem1  25964  lgsquadlem2  25965  chebbnd1lem2  26054  chtppilimlem1  26057  rplogsumlem2  26069  dchrisumlema  26072  dchrisumlem1  26073  dchrisumlem3  26075  dchrisum0lem1  26100  chpdifbndlem1  26137  logdivbnd  26140  pntrmax  26148  pntrsumo1  26149  pntpbnd1a  26169  pntpbnd1  26170  pntpbnd2  26171  pntibndlem2  26175  pntlemg  26182  pntlemr  26186  pntlemj  26187  pntlemk  26190  ostth2lem1  26202  qabvle  26209  ostth2lem3  26219  ostth2lem4  26220  axlowdimlem16  26751  wwlksnredwwlkn  27681  wwlksnextproplem3  27697  wwlksext2clwwlk  27842  wwlksubclwwlk  27843  eupth2lems  28023  smcnlem  28480  minvecolem4  28663  pjhthlem1  29174  zltp1ne  32458  cvmliftlem7  32651  dnibndlem13  33942  knoppndvlem19  33982  knoppndvlem21  33984  icoreunrn  34776  relowlssretop  34780  ltflcei  35045  poimirlem1  35058  poimirlem2  35059  poimirlem4  35061  poimirlem6  35063  poimirlem7  35064  poimirlem8  35065  opnmbllem0  35093  mblfinlem1  35094  mblfinlem2  35095  mblfinlem4  35097  itg2addnclem2  35109  itg2addnclem3  35110  incsequz  35186  isbnd3  35222  rrntotbnd  35274  sn-sup2  39594  3cubeslem1  39625  3cubeslem2  39626  irrapxlem4  39766  pellexlem5  39774  pell14qrgapw  39817  pellfundgt1  39824  jm3.1lem2  39959  expdiophlem1  39962  zltlesub  41916  suplesup  41971  supxrunb3  42036  xrpnf  42125  fmul01lt1lem1  42226  limsupre3lem  42374  xlimxrre  42473  xlimpnfv  42480  ioodvbdlimc1lem1  42573  dvnxpaek  42584  dvnmul  42585  fourierdlem4  42753  fourierdlem11  42760  fourierdlem25  42774  fourierdlem50  42798  fourierdlem64  42812  fourierdlem65  42813  fourierdlem77  42825  fourierdlem79  42827  iinhoiicclem  43312  smfresal  43420  fmtno4prmfac  44089  lighneallem4a  44126  evenltle  44235  perfectALTVlem2  44240  logbpw2m1  44981