Theorem peano2re 11286

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

Assertion

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

Proof of Theorem peano2re

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

Syntax hints:   → wi 4   ∈ wcel 2111  (class class class)co 7346  ℝcr 11005  1c1 11007   + caddc 11009

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-1cn 11064  ax-icn 11065  ax-addcl 11066  ax-addrcl 11067  ax-mulcl 11068  ax-mulrcl 11069  ax-i2m1 11074  ax-1ne0 11075  ax-rrecex 11078  ax-cnre 11079

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-iota 6437  df-fv 6489  df-ov 7349

This theorem is referenced by:  lep1  11962  letrp1  11965  p1le  11966  ledivp1  12024  sup2  12078  nnssre  12129  nnge1  12153  div4p1lem1div2  12376  zltp1le  12522  suprzcl  12553  zeo  12559  peano2uz2  12561  uzind  12565  numltc  12614  uzwo  12809  ge0p1rp  12923  qbtwnxr  13099  xrsupsslem  13206  supxrunb1  13218  fznatpl1  13478  fzp1disj  13483  fzneuz  13508  fzp1nel  13511  ubmelm1fzo  13663  fllep1  13705  flflp1  13711  flhalf  13734  ltdifltdiv  13738  fldiv4p1lem1div2  13739  dfceil2  13743  ceim1l  13751  uzsup  13767  modltm1p1mod  13830  addmodlteq  13853  fsequb  13882  seqf1olem1  13948  seqf1olem2  13949  bernneq3  14138  expnbnd  14139  expmulnbnd  14142  discr1  14146  discr  14147  facwordi  14196  faclbnd  14197  hashfun  14344  seqcoll2  14372  rexuzre  15260  caubnd  15266  rlim2lt  15404  lo1bddrp  15432  rlimo1  15524  o1rlimmul  15526  o1fsum  15720  harmonic  15766  expcnv  15771  geomulcvg  15783  mertenslem1  15791  bpoly4  15966  nonsq  16670  eulerthlem2  16693  pcprendvds  16752  pcmpt  16804  pcfac  16811  vdwlem6  16898  vdwlem11  16903  chnccat  18532  chfacffsupp  22771  chfacfscmul0  22773  chfacfpmmul0  22777  tgioo  24711  zcld  24729  iocopnst  24864  cnheibor  24881  bndth  24884  cncmet  25249  pjthlem1  25364  ovolicc2lem3  25447  ovolicopnf  25452  ioorcl2  25500  dyadf  25519  dyadovol  25521  dyadss  25522  dyaddisjlem  25523  dyadmaxlem  25525  opnmbllem  25529  volsup2  25533  vitalilem2  25537  itg2const2  25669  itg2cnlem1  25689  dvfsumle  25953  dvfsumleOLD  25954  dvfsumabs  25956  dvfsumlem1  25959  dvfsumlem3  25962  dvfsumrlim  25965  fta1glem2  26101  fta1lem  26242  aalioulem3  26269  ulmbdd  26334  itgulm  26344  psercnlem1  26362  abelthlem2  26369  abelthlem7  26375  reeff1olem  26383  logtayl  26596  loglesqrt  26698  atanlogsublem  26852  leibpi  26879  efrlim  26906  efrlimOLD  26907  harmonicubnd  26947  fsumharmonic  26949  ftalem5  27014  basellem2  27019  basellem3  27020  chtnprm  27091  chpp1  27092  ppip1le  27098  ppiub  27142  logfaclbnd  27160  logfacrlim  27162  perfectlem2  27168  bcmono  27215  lgsvalmod  27254  gausslemma2dlem3  27306  lgseisen  27317  lgsquadlem1  27318  lgsquadlem2  27319  chebbnd1lem2  27408  chtppilimlem1  27411  rplogsumlem2  27423  dchrisumlema  27426  dchrisumlem1  27427  dchrisumlem3  27429  dchrisum0lem1  27454  chpdifbndlem1  27491  logdivbnd  27494  pntrmax  27502  pntrsumo1  27503  pntpbnd1a  27523  pntpbnd1  27524  pntpbnd2  27525  pntibndlem2  27529  pntlemg  27536  pntlemr  27540  pntlemj  27541  pntlemk  27544  ostth2lem1  27556  qabvle  27563  ostth2lem3  27573  ostth2lem4  27574  axlowdimlem16  28935  wwlksnredwwlkn  29873  wwlksnextproplem3  29889  wwlksext2clwwlk  30037  wwlksubclwwlk  30038  eupth2lems  30218  smcnlem  30677  minvecolem4  30860  pjhthlem1  31371  zltp1ne  35154  cvmliftlem7  35335  dnibndlem13  36532  knoppndvlem19  36572  knoppndvlem21  36574  icoreunrn  37401  relowlssretop  37405  ltflcei  37656  poimirlem1  37669  poimirlem2  37670  poimirlem4  37672  poimirlem6  37674  poimirlem7  37675  poimirlem8  37676  opnmbllem0  37704  mblfinlem1  37705  mblfinlem2  37706  mblfinlem4  37708  itg2addnclem2  37720  itg2addnclem3  37721  incsequz  37796  isbnd3  37832  rrntotbnd  37884  sn-sup2  42532  3cubeslem1  42725  3cubeslem2  42726  irrapxlem4  42866  pellexlem5  42874  pell14qrgapw  42917  pellfundgt1  42924  jm3.1lem2  43059  expdiophlem1  43062  fzuntgd  43499  zltlesub  45334  suplesup  45386  supxrunb3  45445  xrpnf  45531  fmul01lt1lem1  45632  limsupre3lem  45778  xlimxrre  45877  xlimpnfv  45884  ioodvbdlimc1lem1  45977  dvnxpaek  45988  dvnmul  45989  fourierdlem4  46157  fourierdlem11  46164  fourierdlem25  46178  fourierdlem50  46202  fourierdlem64  46216  fourierdlem65  46217  fourierdlem77  46229  fourierdlem79  46231  iinhoiicclem  46719  smfresal  46834  natglobalincr  46923  fmtno4prmfac  47611  lighneallem4a  47647  evenltle  47756  perfectALTVlem2  47761  logbpw2m1  48607