Theorem peano2re 11306

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

Assertion

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

Proof of Theorem peano2re

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

Syntax hints:   → wi 4   ∈ wcel 2113  (class class class)co 7358  ℝcr 11025  1c1 11027   + caddc 11029

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 2115  ax-9 2123  ax-ext 2708  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-i2m1 11094  ax-1ne0 11095  ax-rrecex 11098  ax-cnre 11099

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 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361

This theorem is referenced by:  lep1  11982  letrp1  11985  p1le  11986  ledivp1  12044  sup2  12098  nnssre  12149  nnge1  12173  div4p1lem1div2  12396  zltp1le  12541  suprzcl  12572  zeo  12578  peano2uz2  12580  uzind  12584  numltc  12633  uzwo  12824  ge0p1rp  12938  qbtwnxr  13115  xrsupsslem  13222  supxrunb1  13234  fznatpl1  13494  fzp1disj  13499  fzneuz  13524  fzp1nel  13527  ubmelm1fzo  13679  fllep1  13721  flflp1  13727  flhalf  13750  ltdifltdiv  13754  fldiv4p1lem1div2  13755  dfceil2  13759  ceim1l  13767  uzsup  13783  modltm1p1mod  13846  addmodlteq  13869  fsequb  13898  seqf1olem1  13964  seqf1olem2  13965  bernneq3  14154  expnbnd  14155  expmulnbnd  14158  discr1  14162  discr  14163  facwordi  14212  faclbnd  14213  hashfun  14360  seqcoll2  14388  rexuzre  15276  caubnd  15282  rlim2lt  15420  lo1bddrp  15448  rlimo1  15540  o1rlimmul  15542  o1fsum  15736  harmonic  15782  expcnv  15787  geomulcvg  15799  mertenslem1  15807  bpoly4  15982  nonsq  16686  eulerthlem2  16709  pcprendvds  16768  pcmpt  16820  pcfac  16827  vdwlem6  16914  vdwlem11  16919  chnccat  18549  chfacffsupp  22800  chfacfscmul0  22802  chfacfpmmul0  22806  tgioo  24740  zcld  24758  iocopnst  24893  cnheibor  24910  bndth  24913  cncmet  25278  pjthlem1  25393  ovolicc2lem3  25476  ovolicopnf  25481  ioorcl2  25529  dyadf  25548  dyadovol  25550  dyadss  25551  dyaddisjlem  25552  dyadmaxlem  25554  opnmbllem  25558  volsup2  25562  vitalilem2  25566  itg2const2  25698  itg2cnlem1  25718  dvfsumle  25982  dvfsumleOLD  25983  dvfsumabs  25985  dvfsumlem1  25988  dvfsumlem3  25991  dvfsumrlim  25994  fta1glem2  26130  fta1lem  26271  aalioulem3  26298  ulmbdd  26363  itgulm  26373  psercnlem1  26391  abelthlem2  26398  abelthlem7  26404  reeff1olem  26412  logtayl  26625  loglesqrt  26727  atanlogsublem  26881  leibpi  26908  efrlim  26935  efrlimOLD  26936  harmonicubnd  26976  fsumharmonic  26978  ftalem5  27043  basellem2  27048  basellem3  27049  chtnprm  27120  chpp1  27121  ppip1le  27127  ppiub  27171  logfaclbnd  27189  logfacrlim  27191  perfectlem2  27197  bcmono  27244  lgsvalmod  27283  gausslemma2dlem3  27335  lgseisen  27346  lgsquadlem1  27347  lgsquadlem2  27348  chebbnd1lem2  27437  chtppilimlem1  27440  rplogsumlem2  27452  dchrisumlema  27455  dchrisumlem1  27456  dchrisumlem3  27458  dchrisum0lem1  27483  chpdifbndlem1  27520  logdivbnd  27523  pntrmax  27531  pntrsumo1  27532  pntpbnd1a  27552  pntpbnd1  27553  pntpbnd2  27554  pntibndlem2  27558  pntlemg  27565  pntlemr  27569  pntlemj  27570  pntlemk  27573  ostth2lem1  27585  qabvle  27592  ostth2lem3  27602  ostth2lem4  27603  axlowdimlem16  29030  wwlksnredwwlkn  29968  wwlksnextproplem3  29984  wwlksext2clwwlk  30132  wwlksubclwwlk  30133  eupth2lems  30313  smcnlem  30772  minvecolem4  30955  pjhthlem1  31466  zltp1ne  35304  cvmliftlem7  35485  dnibndlem13  36690  knoppndvlem19  36730  knoppndvlem21  36732  icoreunrn  37564  relowlssretop  37568  ltflcei  37809  poimirlem1  37822  poimirlem2  37823  poimirlem4  37825  poimirlem6  37827  poimirlem7  37828  poimirlem8  37829  opnmbllem0  37857  mblfinlem1  37858  mblfinlem2  37859  mblfinlem4  37861  itg2addnclem2  37873  itg2addnclem3  37874  incsequz  37949  isbnd3  37985  rrntotbnd  38037  sn-sup2  42746  3cubeslem1  42926  3cubeslem2  42927  irrapxlem4  43067  pellexlem5  43075  pell14qrgapw  43118  pellfundgt1  43125  jm3.1lem2  43260  expdiophlem1  43263  fzuntgd  43699  zltlesub  45533  suplesup  45584  supxrunb3  45643  xrpnf  45729  fmul01lt1lem1  45830  limsupre3lem  45976  xlimxrre  46075  xlimpnfv  46082  ioodvbdlimc1lem1  46175  dvnxpaek  46186  dvnmul  46187  fourierdlem4  46355  fourierdlem11  46362  fourierdlem25  46376  fourierdlem50  46400  fourierdlem64  46414  fourierdlem65  46415  fourierdlem77  46427  fourierdlem79  46429  iinhoiicclem  46917  smfresal  47032  natglobalincr  47121  fmtno4prmfac  47818  lighneallem4a  47854  evenltle  47963  perfectALTVlem2  47968  logbpw2m1  48813