Theorem peano2re 11310

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

Assertion

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

Proof of Theorem peano2re

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

Syntax hints:   → wi 4   ∈ wcel 2119  (class class class)co 7356  ℝcr 11028  1c1 11030   + caddc 11032

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-i2m1 11097  ax-1ne0 11098  ax-rrecex 11101  ax-cnre 11102

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-iota 6441  df-fv 6493  df-ov 7359

This theorem is referenced by:  lep1  11987  letrp1  11990  p1le  11991  ledivp1  12049  sup2  12103  nnssre  12169  nnge1  12196  div4p1lem1div2  12423  zltp1le  12568  suprzcl  12600  zeo  12606  peano2uz2  12608  uzind  12612  numltc  12661  uzwo  12852  ge0p1rp  12966  qbtwnxr  13143  xrsupsslem  13250  supxrunb1  13262  fznatpl1  13523  fzp1disj  13528  fzneuz  13553  fzp1nel  13556  ubmelm1fzo  13709  fllep1  13751  flflp1  13757  flhalf  13780  ltdifltdiv  13784  fldiv4p1lem1div2  13785  dfceil2  13789  ceim1l  13797  uzsup  13813  modltm1p1mod  13876  addmodlteq  13899  fsequb  13928  seqf1olem1  13994  seqf1olem2  13995  bernneq3  14184  expnbnd  14185  expmulnbnd  14188  discr1  14192  discr  14193  facwordi  14242  faclbnd  14243  hashfun  14390  seqcoll2  14418  rexuzre  15306  caubnd  15312  rlim2lt  15450  lo1bddrp  15478  rlimo1  15570  o1rlimmul  15572  o1fsum  15767  harmonic  15815  expcnv  15820  geomulcvg  15832  mertenslem1  15840  bpoly4  16015  nonsq  16720  eulerthlem2  16743  pcprendvds  16802  pcmpt  16854  pcfac  16861  vdwlem6  16948  vdwlem11  16953  chnccat  18583  chfacffsupp  22839  chfacfscmul0  22841  chfacfpmmul0  22845  tgioo  24779  zcld  24797  iocopnst  24925  cnheibor  24940  bndth  24943  cncmet  25307  pjthlem1  25422  ovolicc2lem3  25504  ovolicopnf  25509  ioorcl2  25557  dyadf  25576  dyadovol  25578  dyadss  25579  dyaddisjlem  25580  dyadmaxlem  25582  opnmbllem  25586  volsup2  25590  vitalilem2  25594  itg2const2  25726  itg2cnlem1  25746  dvfsumle  26006  dvfsumabs  26008  dvfsumlem1  26011  dvfsumlem3  26013  dvfsumrlim  26016  fta1glem2  26152  fta1lem  26291  aalioulem3  26318  ulmbdd  26381  itgulm  26391  psercnlem1  26408  abelthlem2  26415  abelthlem7  26421  reeff1olem  26429  logtayl  26642  loglesqrt  26743  atanlogsublem  26897  leibpi  26924  efrlim  26951  harmonicubnd  26991  fsumharmonic  26993  ftalem5  27058  basellem2  27063  basellem3  27064  chtnprm  27135  chpp1  27136  ppip1le  27142  ppiub  27185  logfaclbnd  27203  logfacrlim  27205  perfectlem2  27211  bcmono  27258  lgsvalmod  27297  gausslemma2dlem3  27349  lgseisen  27360  lgsquadlem1  27361  lgsquadlem2  27362  chebbnd1lem2  27451  chtppilimlem1  27454  rplogsumlem2  27466  dchrisumlema  27469  dchrisumlem1  27470  dchrisumlem3  27472  dchrisum0lem1  27497  chpdifbndlem1  27534  logdivbnd  27537  pntrmax  27545  pntrsumo1  27546  pntpbnd1a  27566  pntpbnd1  27567  pntpbnd2  27568  pntibndlem2  27572  pntlemg  27579  pntlemr  27583  pntlemj  27584  pntlemk  27587  ostth2lem1  27599  qabvle  27606  ostth2lem3  27616  ostth2lem4  27617  axlowdimlem16  29044  wwlksnredwwlkn  29981  wwlksnextproplem3  29997  wwlksext2clwwlk  30145  wwlksubclwwlk  30146  eupth2lems  30326  smcnlem  30786  minvecolem4  30969  pjhthlem1  31480  zltp1ne  35338  cvmliftlem7  35519  dnibndlem13  36796  knoppndvlem19  36836  knoppndvlem21  36838  icoreunrn  37721  relowlssretop  37725  ltflcei  37975  poimirlem1  37988  poimirlem2  37989  poimirlem4  37991  poimirlem6  37993  poimirlem7  37994  poimirlem8  37995  opnmbllem0  38023  mblfinlem1  38024  mblfinlem2  38025  mblfinlem4  38027  itg2addnclem2  38039  itg2addnclem3  38040  incsequz  38115  isbnd3  38151  rrntotbnd  38203  sn-sup2  42981  3cubeslem1  43133  3cubeslem2  43134  irrapxlem4  43270  pellexlem5  43278  pell14qrgapw  43321  pellfundgt1  43328  jm3.1lem2  43463  expdiophlem1  43466  fzuntgd  43902  zltlesub  45733  suplesup  45784  supxrunb3  45843  xrpnf  45928  fmul01lt1lem1  46029  limsupre3lem  46175  xlimxrre  46274  xlimpnfv  46281  ioodvbdlimc1lem1  46374  dvnxpaek  46385  dvnmul  46386  fourierdlem4  46554  fourierdlem11  46561  fourierdlem25  46575  fourierdlem50  46599  fourierdlem64  46613  fourierdlem65  46614  fourierdlem77  46626  fourierdlem79  46628  iinhoiicclem  47116  smfresal  47231  natglobalincr  47322  fmtno4prmfac  48050  lighneallem4a  48086  evenltle  48208  perfectALTVlem2  48213  logbpw2m1  49058