Theorem peano2re 11483

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

Assertion

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

Proof of Theorem peano2re

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  (class class class)co 7420  ℝcr 11199  1c1 11201   + caddc 11203

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 2147  ax-9 2155  ax-ext 2733  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-i2m1 11268  ax-1ne0 11269  ax-rrecex 11272  ax-cnre 11273

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 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6494  df-fv 6546  df-ov 7423

This theorem is used by:  lep1  12158  letrp1  12161  p1le  12162  ledivp1  12219  sup2  12273  nnssre  12339  nnge1  12366  div4p1lem1div2  12601  zltp1le  12746  suprzcl  12779  zeo  12785  peano2uz2  12787  uzind  12791  numltc  12845  uzwo  13038  ge0p1rp  13153  qbtwnxr  13330  xrsupsslem  13437  supxrunb1  13449  fznatpl1  13712  fzp1disj  13717  fzneuz  13742  fzp1nel  13745  ubmelm1fzo  13898  fllep1  13941  flflp1  13947  flhalf  13970  ltdifltdiv  13974  fldiv4p1lem1div2  13975  dfceil2  13979  ceim1l  13987  uzsup  14003  modltm1p1mod  14066  addmodlteq  14089  fsequb  14118  seqf1olem1  14184  seqf1olem2  14185  bernneq3  14375  expnbnd  14376  expmulnbnd  14379  discr1  14383  discr  14384  facwordi  14433  faclbnd  14434  hashfun  14582  seqcoll2  14610  rexuzre  15520  caubnd  15526  rlim2lt  15664  lo1bddrp  15692  rlimo1  15784  o1rlimmul  15786  o1fsum  15980  harmonic  16028  expcnv  16033  geomulcvg  16045  mertenslem1  16053  bpoly4  16225  nonsq  16935  eulerthlem2  16959  pcprendvds  17018  pcmpt  17070  pcfac  17077  vdwlem6  17164  vdwlem11  17169  chnccat  18800  chfacffsupp  23174  chfacfscmul0  23176  chfacfpmmul0  23180  tgioo  25115  zcld  25133  iocopnst  25261  cnheibor  25276  bndth  25279  cncmet  25643  pjthlem1  25758  ovolicc2lem3  25840  ovolicopnf  25845  ioorcl2  25893  dyadf  25912  dyadovol  25914  dyadss  25915  dyaddisjlem  25916  dyadmaxlem  25918  opnmbllem  25922  volsup2  25926  vitalilem2  25930  itg2const2  26062  itg2cnlem1  26082  dvfsumle  26341  dvfsumabs  26343  dvfsumlem1  26346  dvfsumlem3  26348  dvfsumrlim  26351  fta1glem2  26487  fta1lem  26628  aalioulem3  26661  ulmbdd  26725  itgulm  26735  psercnlem1  26752  abelthlem2  26759  abelthlem7  26765  reeff1olem  26773  logtayl  26988  loglesqrt  27089  atanlogsublem  27243  leibpi  27270  efrlim  27297  harmonicubnd  27337  fsumharmonic  27339  ftalem5  27404  basellem2  27409  basellem3  27410  chtnprm  27481  chpp1  27482  ppip1le  27488  ppiub  27531  logfaclbnd  27549  logfacrlim  27551  perfectlem2  27557  bcmono  27604  lgsvalmod  27643  gausslemma2dlem3  27695  lgseisen  27706  lgsquadlem1  27707  lgsquadlem2  27708  chebbnd1lem2  27797  chtppilimlem1  27800  rplogsumlem2  27812  dchrisumlema  27815  dchrisumlem1  27816  dchrisumlem3  27818  dchrisum0lem1  27843  chpdifbndlem1  27880  logdivbnd  27883  pntrmax  27891  pntrsumo1  27892  pntpbnd1a  27912  pntpbnd1  27913  pntpbnd2  27914  pntibndlem2  27918  pntlemg  27925  pntlemr  27929  pntlemj  27930  pntlemk  27933  ostth2lem1  27945  qabvle  27952  ostth2lem3  27962  ostth2lem4  27963  axlowdimlem16  29535  wwlksnredwwlkn  30484  wwlksnextproplem3  30500  wwlksext2clwwlk  30648  wwlksubclwwlk  30649  eupth2lems  30839  smcnlem  31299  minvecolem4  31482  pjhthlem1  31993  zltp1ne  35900  cvmliftlem7  36056  dnibndlem13  37356  knoppndvlem19  37396  knoppndvlem21  37398  icoreunrn  38282  relowlssretop  38286  ltflcei  38531  poimirlem1  38539  poimirlem2  38540  poimirlem4  38542  poimirlem6  38544  poimirlem7  38545  poimirlem8  38546  opnmbllem0  38574  mblfinlem1  38575  mblfinlem2  38576  mblfinlem4  38578  itg2addnclem2  38590  itg2addnclem3  38591  incsequz  38682  isbnd3  38718  rrntotbnd  38770  sn-sup2  43555  3cubeslem1  43694  3cubeslem2  43695  irrapxlem4  43831  pellexlem5  43839  pell14qrgapw  43882  pellfundgt1  43889  jm3.1lem2  44024  expdiophlem1  44027  fzuntgd  44458  zltlesub  46300  suplesup  46350  supxrunb3  46409  xrpnf  46494  fmul01lt1lem1  46595  limsupre3lem  46741  xlimxrre  46840  xlimpnfv  46847  ioodvbdlimc1lem1  46940  dvnxpaek  46951  dvnmul  46952  fourierdlem4  47120  fourierdlem11  47127  fourierdlem25  47141  fourierdlem50  47165  fourierdlem64  47179  fourierdlem65  47180  fourierdlem77  47192  fourierdlem79  47194  iinhoiicclem  47682  smfresal  47797  fmtno4prmfac  48656  lighneallem4a  48692  evenltle  48814  perfectALTVlem2  48819  logbpw2m1  49678