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  22776  chfacfscmul0  22778  chfacfpmmul0  22782  tgioo  24717  zcld  24735  iocopnst  24870  cnheibor  24887  bndth  24890  cncmet  25255  pjthlem1  25370  ovolicc2lem3  25453  ovolicopnf  25458  ioorcl2  25506  dyadf  25525  dyadovol  25527  dyadss  25528  dyaddisjlem  25529  dyadmaxlem  25531  opnmbllem  25535  volsup2  25539  vitalilem2  25543  itg2const2  25675  itg2cnlem1  25695  dvfsumle  25959  dvfsumleOLD  25960  dvfsumabs  25962  dvfsumlem1  25965  dvfsumlem3  25968  dvfsumrlim  25971  fta1glem2  26107  fta1lem  26248  aalioulem3  26275  ulmbdd  26340  itgulm  26350  psercnlem1  26368  abelthlem2  26375  abelthlem7  26381  reeff1olem  26389  logtayl  26602  loglesqrt  26704  atanlogsublem  26858  leibpi  26885  efrlim  26912  efrlimOLD  26913  harmonicubnd  26953  fsumharmonic  26955  ftalem5  27020  basellem2  27025  basellem3  27026  chtnprm  27097  chpp1  27098  ppip1le  27104  ppiub  27148  logfaclbnd  27166  logfacrlim  27168  perfectlem2  27174  bcmono  27221  lgsvalmod  27260  gausslemma2dlem3  27312  lgseisen  27323  lgsquadlem1  27324  lgsquadlem2  27325  chebbnd1lem2  27414  chtppilimlem1  27417  rplogsumlem2  27429  dchrisumlema  27432  dchrisumlem1  27433  dchrisumlem3  27435  dchrisum0lem1  27460  chpdifbndlem1  27497  logdivbnd  27500  pntrmax  27508  pntrsumo1  27509  pntpbnd1a  27529  pntpbnd1  27530  pntpbnd2  27531  pntibndlem2  27535  pntlemg  27542  pntlemr  27546  pntlemj  27547  pntlemk  27550  ostth2lem1  27562  qabvle  27569  ostth2lem3  27579  ostth2lem4  27580  axlowdimlem16  28937  wwlksnredwwlkn  29875  wwlksnextproplem3  29891  wwlksext2clwwlk  30036  wwlksubclwwlk  30037  eupth2lems  30217  smcnlem  30676  minvecolem4  30859  pjhthlem1  31370  zltp1ne  35090  cvmliftlem7  35271  dnibndlem13  36471  knoppndvlem19  36511  knoppndvlem21  36513  icoreunrn  37340  relowlssretop  37344  ltflcei  37595  poimirlem1  37608  poimirlem2  37609  poimirlem4  37611  poimirlem6  37613  poimirlem7  37614  poimirlem8  37615  opnmbllem0  37643  mblfinlem1  37644  mblfinlem2  37645  mblfinlem4  37647  itg2addnclem2  37659  itg2addnclem3  37660  incsequz  37735  isbnd3  37771  rrntotbnd  37823  sn-sup2  42472  3cubeslem1  42665  3cubeslem2  42666  irrapxlem4  42806  pellexlem5  42814  pell14qrgapw  42857  pellfundgt1  42864  jm3.1lem2  43000  expdiophlem1  43003  fzuntgd  43440  zltlesub  45276  suplesup  45328  supxrunb3  45388  xrpnf  45474  fmul01lt1lem1  45575  limsupre3lem  45723  xlimxrre  45822  xlimpnfv  45829  ioodvbdlimc1lem1  45922  dvnxpaek  45933  dvnmul  45934  fourierdlem4  46102  fourierdlem11  46109  fourierdlem25  46123  fourierdlem50  46147  fourierdlem64  46161  fourierdlem65  46162  fourierdlem77  46174  fourierdlem79  46176  iinhoiicclem  46664  smfresal  46779  natglobalincr  46868  fmtno4prmfac  47566  lighneallem4a  47602  evenltle  47711  perfectALTVlem2  47716  logbpw2m1  48549