Theorem peano2re 11398

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

Assertion

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

Proof of Theorem peano2re

Step	Hyp	Ref	Expression
1		1re 11223	. 2 ⊢ 1 ∈ ℝ
2		readdcl 11198	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐴 + 1) ∈ ℝ)
3	1, 2	mpan2 704	1 ⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  (class class class)co 7419  ℝcr 11114  1c1 11116   + caddc 11118

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-1cn 11173  ax-icn 11174  ax-addcl 11175  ax-addrcl 11176  ax-mulcl 11177  ax-mulrcl 11178  ax-i2m1 11183  ax-1ne0 11184  ax-rrecex 11187  ax-cnre 11188

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7422

This theorem is used by:  lep1  12071  letrp1  12074  p1le  12075  ledivp1  12132  sup2  12186  nnssre  12252  nnge1  12279  div4p1lem1div2  12514  zltp1le  12659  suprzcl  12692  zeo  12698  peano2uz2  12700  uzind  12704  numltc  12758  uzwo  12951  ge0p1rp  13065  qbtwnxr  13242  xrsupsslem  13349  supxrunb1  13361  fznatpl1  13623  fzp1disj  13628  fzneuz  13653  fzp1nel  13656  ubmelm1fzo  13809  fllep1  13852  flflp1  13858  flhalf  13881  ltdifltdiv  13885  fldiv4p1lem1div2  13886  dfceil2  13890  ceim1l  13898  uzsup  13914  modltm1p1mod  13977  addmodlteq  14000  fsequb  14029  seqf1olem1  14095  seqf1olem2  14096  bernneq3  14285  expnbnd  14286  expmulnbnd  14289  discr1  14293  discr  14294  facwordi  14343  faclbnd  14344  hashfun  14492  seqcoll2  14520  rexuzre  15428  caubnd  15434  rlim2lt  15572  lo1bddrp  15600  rlimo1  15692  o1rlimmul  15694  o1fsum  15888  harmonic  15936  expcnv  15941  geomulcvg  15953  mertenslem1  15961  bpoly4  16135  nonsq  16840  eulerthlem2  16863  pcprendvds  16922  pcmpt  16974  pcfac  16981  vdwlem6  17068  vdwlem11  17073  chnccat  18704  chfacffsupp  23063  chfacfscmul0  23065  chfacfpmmul0  23069  tgioo  25004  zcld  25022  iocopnst  25150  cnheibor  25165  bndth  25168  cncmet  25532  pjthlem1  25647  ovolicc2lem3  25729  ovolicopnf  25734  ioorcl2  25782  dyadf  25801  dyadovol  25803  dyadss  25804  dyaddisjlem  25805  dyadmaxlem  25807  opnmbllem  25811  volsup2  25815  vitalilem2  25819  itg2const2  25951  itg2cnlem1  25971  dvfsumle  26231  dvfsumabs  26233  dvfsumlem1  26236  dvfsumlem3  26238  dvfsumrlim  26241  fta1glem2  26377  fta1lem  26519  aalioulem3  26548  ulmbdd  26612  itgulm  26622  psercnlem1  26639  abelthlem2  26646  abelthlem7  26652  reeff1olem  26660  logtayl  26876  loglesqrt  26977  atanlogsublem  27131  leibpi  27158  efrlim  27185  harmonicubnd  27225  fsumharmonic  27227  ftalem5  27292  basellem2  27297  basellem3  27298  chtnprm  27369  chpp1  27370  ppip1le  27376  ppiub  27419  logfaclbnd  27437  logfacrlim  27439  perfectlem2  27445  bcmono  27492  lgsvalmod  27531  gausslemma2dlem3  27583  lgseisen  27594  lgsquadlem1  27595  lgsquadlem2  27596  chebbnd1lem2  27685  chtppilimlem1  27688  rplogsumlem2  27700  dchrisumlema  27703  dchrisumlem1  27704  dchrisumlem3  27706  dchrisum0lem1  27731  chpdifbndlem1  27768  logdivbnd  27771  pntrmax  27779  pntrsumo1  27780  pntpbnd1a  27800  pntpbnd1  27801  pntpbnd2  27802  pntibndlem2  27806  pntlemg  27813  pntlemr  27817  pntlemj  27818  pntlemk  27821  ostth2lem1  27833  qabvle  27840  ostth2lem3  27850  ostth2lem4  27851  axlowdimlem16  29362  wwlksnredwwlkn  30311  wwlksnextproplem3  30327  wwlksext2clwwlk  30475  wwlksubclwwlk  30476  eupth2lems  30660  smcnlem  31120  minvecolem4  31303  pjhthlem1  31814  zltp1ne  35658  cvmliftlem7  35820  dnibndlem13  37136  knoppndvlem19  37176  knoppndvlem21  37178  icoreunrn  38062  relowlssretop  38066  ltflcei  38316  poimirlem1  38329  poimirlem2  38330  poimirlem4  38332  poimirlem6  38334  poimirlem7  38335  poimirlem8  38336  opnmbllem0  38364  mblfinlem1  38365  mblfinlem2  38366  mblfinlem4  38368  itg2addnclem2  38380  itg2addnclem3  38381  incsequz  38457  isbnd3  38493  rrntotbnd  38545  sn-sup2  43323  3cubeslem1  43473  3cubeslem2  43474  irrapxlem4  43610  pellexlem5  43618  pell14qrgapw  43661  pellfundgt1  43668  jm3.1lem2  43803  expdiophlem1  43806  fzuntgd  44242  zltlesub  46062  suplesup  46113  supxrunb3  46172  xrpnf  46257  fmul01lt1lem1  46358  limsupre3lem  46504  xlimxrre  46603  xlimpnfv  46610  ioodvbdlimc1lem1  46703  dvnxpaek  46714  dvnmul  46715  fourierdlem4  46883  fourierdlem11  46890  fourierdlem25  46904  fourierdlem50  46928  fourierdlem64  46942  fourierdlem65  46943  fourierdlem77  46955  fourierdlem79  46957  iinhoiicclem  47445  smfresal  47560  natglobalincr  47651  fmtno4prmfac  48382  lighneallem4a  48418  evenltle  48540  perfectALTVlem2  48545  logbpw2m1  49404