Theorem peano2re 11413

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

Assertion

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

Proof of Theorem peano2re

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7410  ℝcr 11133  1c1 11135   + caddc 11137

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 2708  ax-1cn 11192  ax-icn 11193  ax-addcl 11194  ax-addrcl 11195  ax-mulcl 11196  ax-mulrcl 11197  ax-i2m1 11202  ax-1ne0 11203  ax-rrecex 11206  ax-cnre 11207

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 2715  df-cleq 2728  df-clel 2810  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-iota 6489  df-fv 6544  df-ov 7413

This theorem is referenced by:  lep1  12087  letrp1  12090  p1le  12091  ledivp1  12149  sup2  12203  nnssre  12249  nnge1  12273  div4p1lem1div2  12501  zltp1le  12647  suprzcl  12678  zeo  12684  peano2uz2  12686  uzind  12690  numltc  12739  uzwo  12932  ge0p1rp  13045  qbtwnxr  13221  xrsupsslem  13328  supxrunb1  13340  fznatpl1  13600  fzp1disj  13605  fzneuz  13630  fzp1nel  13633  ubmelm1fzo  13784  fllep1  13823  flflp1  13829  flhalf  13852  ltdifltdiv  13856  fldiv4p1lem1div2  13857  dfceil2  13861  ceim1l  13869  uzsup  13885  modltm1p1mod  13946  addmodlteq  13969  fsequb  13998  seqf1olem1  14064  seqf1olem2  14065  bernneq3  14254  expnbnd  14255  expmulnbnd  14258  discr1  14262  discr  14263  facwordi  14312  faclbnd  14313  hashfun  14460  seqcoll2  14488  rexuzre  15376  caubnd  15382  rlim2lt  15518  lo1bddrp  15546  rlimo1  15638  o1rlimmul  15640  o1fsum  15834  harmonic  15880  expcnv  15885  geomulcvg  15897  mertenslem1  15905  bpoly4  16080  nonsq  16783  eulerthlem2  16806  pcprendvds  16865  pcmpt  16917  pcfac  16924  vdwlem6  17011  vdwlem11  17016  chfacffsupp  22799  chfacfscmul0  22801  chfacfpmmul0  22805  tgioo  24740  zcld  24758  iocopnst  24893  cnheibor  24910  bndth  24913  cncmet  25279  pjthlem1  25394  ovolicc2lem3  25477  ovolicopnf  25482  ioorcl2  25530  dyadf  25549  dyadovol  25551  dyadss  25552  dyaddisjlem  25553  dyadmaxlem  25555  opnmbllem  25559  volsup2  25563  vitalilem2  25567  itg2const2  25699  itg2cnlem1  25719  dvfsumle  25983  dvfsumleOLD  25984  dvfsumabs  25986  dvfsumlem1  25989  dvfsumlem3  25992  dvfsumrlim  25995  fta1glem2  26131  fta1lem  26272  aalioulem3  26299  ulmbdd  26364  itgulm  26374  psercnlem1  26392  abelthlem2  26399  abelthlem7  26405  reeff1olem  26413  logtayl  26626  loglesqrt  26728  atanlogsublem  26882  leibpi  26909  efrlim  26936  efrlimOLD  26937  harmonicubnd  26977  fsumharmonic  26979  ftalem5  27044  basellem2  27049  basellem3  27050  chtnprm  27121  chpp1  27122  ppip1le  27128  ppiub  27172  logfaclbnd  27190  logfacrlim  27192  perfectlem2  27198  bcmono  27245  lgsvalmod  27284  gausslemma2dlem3  27336  lgseisen  27347  lgsquadlem1  27348  lgsquadlem2  27349  chebbnd1lem2  27438  chtppilimlem1  27441  rplogsumlem2  27453  dchrisumlema  27456  dchrisumlem1  27457  dchrisumlem3  27459  dchrisum0lem1  27484  chpdifbndlem1  27521  logdivbnd  27524  pntrmax  27532  pntrsumo1  27533  pntpbnd1a  27553  pntpbnd1  27554  pntpbnd2  27555  pntibndlem2  27559  pntlemg  27566  pntlemr  27570  pntlemj  27571  pntlemk  27574  ostth2lem1  27586  qabvle  27593  ostth2lem3  27603  ostth2lem4  27604  axlowdimlem16  28941  wwlksnredwwlkn  29882  wwlksnextproplem3  29898  wwlksext2clwwlk  30043  wwlksubclwwlk  30044  eupth2lems  30224  smcnlem  30683  minvecolem4  30866  pjhthlem1  31377  zltp1ne  35137  cvmliftlem7  35318  dnibndlem13  36513  knoppndvlem19  36553  knoppndvlem21  36555  icoreunrn  37382  relowlssretop  37386  ltflcei  37637  poimirlem1  37650  poimirlem2  37651  poimirlem4  37653  poimirlem6  37655  poimirlem7  37656  poimirlem8  37657  opnmbllem0  37685  mblfinlem1  37686  mblfinlem2  37687  mblfinlem4  37689  itg2addnclem2  37701  itg2addnclem3  37702  incsequz  37777  isbnd3  37813  rrntotbnd  37865  sn-sup2  42489  3cubeslem1  42682  3cubeslem2  42683  irrapxlem4  42823  pellexlem5  42831  pell14qrgapw  42874  pellfundgt1  42881  jm3.1lem2  43017  expdiophlem1  43020  fzuntgd  43457  zltlesub  45294  suplesup  45346  supxrunb3  45406  xrpnf  45492  fmul01lt1lem1  45593  limsupre3lem  45741  xlimxrre  45840  xlimpnfv  45847  ioodvbdlimc1lem1  45940  dvnxpaek  45951  dvnmul  45952  fourierdlem4  46120  fourierdlem11  46127  fourierdlem25  46141  fourierdlem50  46165  fourierdlem64  46179  fourierdlem65  46180  fourierdlem77  46192  fourierdlem79  46194  iinhoiicclem  46682  smfresal  46797  natglobalincr  46886  fmtno4prmfac  47566  lighneallem4a  47602  evenltle  47711  perfectALTVlem2  47716  logbpw2m1  48527