Theorem peano2re 11318

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

Assertion

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

Proof of Theorem peano2re

Step	Hyp	Ref	Expression
1		1re 11144	. 2 ⊢ 1 ∈ ℝ
2		readdcl 11121	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐴 + 1) ∈ ℝ)
3	1, 2	mpan2 692	1 ⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7368  ℝcr 11037  1c1 11039   + caddc 11041

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-i2m1 11106  ax-1ne0 11107  ax-rrecex 11110  ax-cnre 11111

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371

This theorem is referenced by:  lep1  11994  letrp1  11997  p1le  11998  ledivp1  12056  sup2  12110  nnssre  12161  nnge1  12185  div4p1lem1div2  12408  zltp1le  12553  suprzcl  12584  zeo  12590  peano2uz2  12592  uzind  12596  numltc  12645  uzwo  12836  ge0p1rp  12950  qbtwnxr  13127  xrsupsslem  13234  supxrunb1  13246  fznatpl1  13506  fzp1disj  13511  fzneuz  13536  fzp1nel  13539  ubmelm1fzo  13691  fllep1  13733  flflp1  13739  flhalf  13762  ltdifltdiv  13766  fldiv4p1lem1div2  13767  dfceil2  13771  ceim1l  13779  uzsup  13795  modltm1p1mod  13858  addmodlteq  13881  fsequb  13910  seqf1olem1  13976  seqf1olem2  13977  bernneq3  14166  expnbnd  14167  expmulnbnd  14170  discr1  14174  discr  14175  facwordi  14224  faclbnd  14225  hashfun  14372  seqcoll2  14400  rexuzre  15288  caubnd  15294  rlim2lt  15432  lo1bddrp  15460  rlimo1  15552  o1rlimmul  15554  o1fsum  15748  harmonic  15794  expcnv  15799  geomulcvg  15811  mertenslem1  15819  bpoly4  15994  nonsq  16698  eulerthlem2  16721  pcprendvds  16780  pcmpt  16832  pcfac  16839  vdwlem6  16926  vdwlem11  16931  chnccat  18561  chfacffsupp  22812  chfacfscmul0  22814  chfacfpmmul0  22818  tgioo  24752  zcld  24770  iocopnst  24905  cnheibor  24922  bndth  24925  cncmet  25290  pjthlem1  25405  ovolicc2lem3  25488  ovolicopnf  25493  ioorcl2  25541  dyadf  25560  dyadovol  25562  dyadss  25563  dyaddisjlem  25564  dyadmaxlem  25566  opnmbllem  25570  volsup2  25574  vitalilem2  25578  itg2const2  25710  itg2cnlem1  25730  dvfsumle  25994  dvfsumleOLD  25995  dvfsumabs  25997  dvfsumlem1  26000  dvfsumlem3  26003  dvfsumrlim  26006  fta1glem2  26142  fta1lem  26283  aalioulem3  26310  ulmbdd  26375  itgulm  26385  psercnlem1  26403  abelthlem2  26410  abelthlem7  26416  reeff1olem  26424  logtayl  26637  loglesqrt  26739  atanlogsublem  26893  leibpi  26920  efrlim  26947  efrlimOLD  26948  harmonicubnd  26988  fsumharmonic  26990  ftalem5  27055  basellem2  27060  basellem3  27061  chtnprm  27132  chpp1  27133  ppip1le  27139  ppiub  27183  logfaclbnd  27201  logfacrlim  27203  perfectlem2  27209  bcmono  27256  lgsvalmod  27295  gausslemma2dlem3  27347  lgseisen  27358  lgsquadlem1  27359  lgsquadlem2  27360  chebbnd1lem2  27449  chtppilimlem1  27452  rplogsumlem2  27464  dchrisumlema  27467  dchrisumlem1  27468  dchrisumlem3  27470  dchrisum0lem1  27495  chpdifbndlem1  27532  logdivbnd  27535  pntrmax  27543  pntrsumo1  27544  pntpbnd1a  27564  pntpbnd1  27565  pntpbnd2  27566  pntibndlem2  27570  pntlemg  27577  pntlemr  27581  pntlemj  27582  pntlemk  27585  ostth2lem1  27597  qabvle  27604  ostth2lem3  27614  ostth2lem4  27615  axlowdimlem16  29042  wwlksnredwwlkn  29980  wwlksnextproplem3  29996  wwlksext2clwwlk  30144  wwlksubclwwlk  30145  eupth2lems  30325  smcnlem  30785  minvecolem4  30968  pjhthlem1  31479  zltp1ne  35326  cvmliftlem7  35507  dnibndlem13  36712  knoppndvlem19  36752  knoppndvlem21  36754  icoreunrn  37614  relowlssretop  37618  ltflcei  37859  poimirlem1  37872  poimirlem2  37873  poimirlem4  37875  poimirlem6  37877  poimirlem7  37878  poimirlem8  37879  opnmbllem0  37907  mblfinlem1  37908  mblfinlem2  37909  mblfinlem4  37911  itg2addnclem2  37923  itg2addnclem3  37924  incsequz  37999  isbnd3  38035  rrntotbnd  38087  sn-sup2  42861  3cubeslem1  43041  3cubeslem2  43042  irrapxlem4  43182  pellexlem5  43190  pell14qrgapw  43233  pellfundgt1  43240  jm3.1lem2  43375  expdiophlem1  43378  fzuntgd  43814  zltlesub  45647  suplesup  45698  supxrunb3  45757  xrpnf  45843  fmul01lt1lem1  45944  limsupre3lem  46090  xlimxrre  46189  xlimpnfv  46196  ioodvbdlimc1lem1  46289  dvnxpaek  46300  dvnmul  46301  fourierdlem4  46469  fourierdlem11  46476  fourierdlem25  46490  fourierdlem50  46514  fourierdlem64  46528  fourierdlem65  46529  fourierdlem77  46541  fourierdlem79  46543  iinhoiicclem  47031  smfresal  47146  natglobalincr  47235  fmtno4prmfac  47932  lighneallem4a  47968  evenltle  48077  perfectALTVlem2  48082  logbpw2m1  48927