Theorem peano2re 11323

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

Assertion

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

Proof of Theorem peano2re

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7369  ℝcr 11043  1c1 11045   + caddc 11047

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 11102  ax-icn 11103  ax-addcl 11104  ax-addrcl 11105  ax-mulcl 11106  ax-mulrcl 11107  ax-i2m1 11112  ax-1ne0 11113  ax-rrecex 11116  ax-cnre 11117

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-ov 7372

This theorem is referenced by:  lep1  11999  letrp1  12002  p1le  12003  ledivp1  12061  sup2  12115  nnssre  12166  nnge1  12190  div4p1lem1div2  12413  zltp1le  12559  suprzcl  12590  zeo  12596  peano2uz2  12598  uzind  12602  numltc  12651  uzwo  12846  ge0p1rp  12960  qbtwnxr  13136  xrsupsslem  13243  supxrunb1  13255  fznatpl1  13515  fzp1disj  13520  fzneuz  13545  fzp1nel  13548  ubmelm1fzo  13700  fllep1  13739  flflp1  13745  flhalf  13768  ltdifltdiv  13772  fldiv4p1lem1div2  13773  dfceil2  13777  ceim1l  13785  uzsup  13801  modltm1p1mod  13864  addmodlteq  13887  fsequb  13916  seqf1olem1  13982  seqf1olem2  13983  bernneq3  14172  expnbnd  14173  expmulnbnd  14176  discr1  14180  discr  14181  facwordi  14230  faclbnd  14231  hashfun  14378  seqcoll2  14406  rexuzre  15295  caubnd  15301  rlim2lt  15439  lo1bddrp  15467  rlimo1  15559  o1rlimmul  15561  o1fsum  15755  harmonic  15801  expcnv  15806  geomulcvg  15818  mertenslem1  15826  bpoly4  16001  nonsq  16705  eulerthlem2  16728  pcprendvds  16787  pcmpt  16839  pcfac  16846  vdwlem6  16933  vdwlem11  16938  chfacffsupp  22719  chfacfscmul0  22721  chfacfpmmul0  22725  tgioo  24660  zcld  24678  iocopnst  24813  cnheibor  24830  bndth  24833  cncmet  25198  pjthlem1  25313  ovolicc2lem3  25396  ovolicopnf  25401  ioorcl2  25449  dyadf  25468  dyadovol  25470  dyadss  25471  dyaddisjlem  25472  dyadmaxlem  25474  opnmbllem  25478  volsup2  25482  vitalilem2  25486  itg2const2  25618  itg2cnlem1  25638  dvfsumle  25902  dvfsumleOLD  25903  dvfsumabs  25905  dvfsumlem1  25908  dvfsumlem3  25911  dvfsumrlim  25914  fta1glem2  26050  fta1lem  26191  aalioulem3  26218  ulmbdd  26283  itgulm  26293  psercnlem1  26311  abelthlem2  26318  abelthlem7  26324  reeff1olem  26332  logtayl  26545  loglesqrt  26647  atanlogsublem  26801  leibpi  26828  efrlim  26855  efrlimOLD  26856  harmonicubnd  26896  fsumharmonic  26898  ftalem5  26963  basellem2  26968  basellem3  26969  chtnprm  27040  chpp1  27041  ppip1le  27047  ppiub  27091  logfaclbnd  27109  logfacrlim  27111  perfectlem2  27117  bcmono  27164  lgsvalmod  27203  gausslemma2dlem3  27255  lgseisen  27266  lgsquadlem1  27267  lgsquadlem2  27268  chebbnd1lem2  27357  chtppilimlem1  27360  rplogsumlem2  27372  dchrisumlema  27375  dchrisumlem1  27376  dchrisumlem3  27378  dchrisum0lem1  27403  chpdifbndlem1  27440  logdivbnd  27443  pntrmax  27451  pntrsumo1  27452  pntpbnd1a  27472  pntpbnd1  27473  pntpbnd2  27474  pntibndlem2  27478  pntlemg  27485  pntlemr  27489  pntlemj  27490  pntlemk  27493  ostth2lem1  27505  qabvle  27512  ostth2lem3  27522  ostth2lem4  27523  axlowdimlem16  28860  wwlksnredwwlkn  29798  wwlksnextproplem3  29814  wwlksext2clwwlk  29959  wwlksubclwwlk  29960  eupth2lems  30140  smcnlem  30599  minvecolem4  30782  pjhthlem1  31293  zltp1ne  35070  cvmliftlem7  35251  dnibndlem13  36451  knoppndvlem19  36491  knoppndvlem21  36493  icoreunrn  37320  relowlssretop  37324  ltflcei  37575  poimirlem1  37588  poimirlem2  37589  poimirlem4  37591  poimirlem6  37593  poimirlem7  37594  poimirlem8  37595  opnmbllem0  37623  mblfinlem1  37624  mblfinlem2  37625  mblfinlem4  37627  itg2addnclem2  37639  itg2addnclem3  37640  incsequz  37715  isbnd3  37751  rrntotbnd  37803  sn-sup2  42452  3cubeslem1  42645  3cubeslem2  42646  irrapxlem4  42786  pellexlem5  42794  pell14qrgapw  42837  pellfundgt1  42844  jm3.1lem2  42980  expdiophlem1  42983  fzuntgd  43420  zltlesub  45256  suplesup  45308  supxrunb3  45368  xrpnf  45454  fmul01lt1lem1  45555  limsupre3lem  45703  xlimxrre  45802  xlimpnfv  45809  ioodvbdlimc1lem1  45902  dvnxpaek  45913  dvnmul  45914  fourierdlem4  46082  fourierdlem11  46089  fourierdlem25  46103  fourierdlem50  46127  fourierdlem64  46141  fourierdlem65  46142  fourierdlem77  46154  fourierdlem79  46156  iinhoiicclem  46644  smfresal  46759  natglobalincr  46848  fmtno4prmfac  47546  lighneallem4a  47582  evenltle  47691  perfectALTVlem2  47696  logbpw2m1  48529