Theorem peano2re 11387

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

Assertion

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

Proof of Theorem peano2re

Step	Hyp	Ref	Expression
1		1re 11214	. 2 ⊢ 1 ∈ ℝ
2		readdcl 11193	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐴 + 1) ∈ ℝ)
3	1, 2	mpan2 690	1 ⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2107  (class class class)co 7409  ℝcr 11109  1c1 11111   + caddc 11113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-i2m1 11178  ax-1ne0 11179  ax-rrecex 11182  ax-cnre 11183

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412

This theorem is referenced by:  lep1  12055  letrp1  12058  p1le  12059  ledivp1  12116  sup2  12170  nnssre  12216  nnge1  12240  div4p1lem1div2  12467  zltp1le  12612  suprzcl  12642  zeo  12648  peano2uz2  12650  uzind  12654  numltc  12703  uzwo  12895  ge0p1rp  13005  qbtwnxr  13179  xrsupsslem  13286  supxrunb1  13298  fznatpl1  13555  fzp1disj  13560  fzneuz  13582  fzp1nel  13585  ubmelm1fzo  13728  fllep1  13766  flflp1  13772  flhalf  13795  ltdifltdiv  13799  fldiv4p1lem1div2  13800  dfceil2  13804  ceim1l  13812  uzsup  13828  modltm1p1mod  13888  addmodlteq  13911  fsequb  13940  seqf1olem1  14007  seqf1olem2  14008  bernneq3  14194  expnbnd  14195  expmulnbnd  14198  discr1  14202  discr  14203  facwordi  14249  faclbnd  14250  hashfun  14397  seqcoll2  14426  rexuzre  15299  caubnd  15305  rlim2lt  15441  lo1bddrp  15469  rlimo1  15561  o1rlimmul  15563  o1fsum  15759  harmonic  15805  expcnv  15810  geomulcvg  15822  mertenslem1  15830  bpoly4  16003  nonsq  16695  eulerthlem2  16715  pcprendvds  16773  pcmpt  16825  pcfac  16832  vdwlem6  16919  vdwlem11  16924  chfacffsupp  22358  chfacfscmul0  22360  chfacfpmmul0  22364  tgioo  24312  zcld  24329  iocopnst  24456  cnheibor  24471  bndth  24474  cncmet  24839  pjthlem1  24954  ovolicc2lem3  25036  ovolicopnf  25041  ioorcl2  25089  dyadf  25108  dyadovol  25110  dyadss  25111  dyaddisjlem  25112  dyadmaxlem  25114  opnmbllem  25118  volsup2  25122  vitalilem2  25126  itg2const2  25259  itg2cnlem1  25279  dvfsumle  25538  dvfsumabs  25540  dvfsumlem1  25543  dvfsumlem3  25545  dvfsumrlim  25548  fta1glem2  25684  fta1lem  25820  aalioulem3  25847  ulmbdd  25910  itgulm  25920  psercnlem1  25937  abelthlem2  25944  abelthlem7  25950  reeff1olem  25958  logtayl  26168  loglesqrt  26266  atanlogsublem  26420  leibpi  26447  efrlim  26474  harmonicubnd  26514  fsumharmonic  26516  ftalem5  26581  basellem2  26586  basellem3  26587  chtnprm  26658  chpp1  26659  ppip1le  26665  ppiub  26707  logfaclbnd  26725  logfacrlim  26727  perfectlem2  26733  bcmono  26780  lgsvalmod  26819  gausslemma2dlem3  26871  lgseisen  26882  lgsquadlem1  26883  lgsquadlem2  26884  chebbnd1lem2  26973  chtppilimlem1  26976  rplogsumlem2  26988  dchrisumlema  26991  dchrisumlem1  26992  dchrisumlem3  26994  dchrisum0lem1  27019  chpdifbndlem1  27056  logdivbnd  27059  pntrmax  27067  pntrsumo1  27068  pntpbnd1a  27088  pntpbnd1  27089  pntpbnd2  27090  pntibndlem2  27094  pntlemg  27101  pntlemr  27105  pntlemj  27106  pntlemk  27109  ostth2lem1  27121  qabvle  27128  ostth2lem3  27138  ostth2lem4  27139  axlowdimlem16  28215  wwlksnredwwlkn  29149  wwlksnextproplem3  29165  wwlksext2clwwlk  29310  wwlksubclwwlk  29311  eupth2lems  29491  smcnlem  29950  minvecolem4  30133  pjhthlem1  30644  zltp1ne  34099  cvmliftlem7  34282  gg-dvfsumle  35182  dnibndlem13  35366  knoppndvlem19  35406  knoppndvlem21  35408  icoreunrn  36240  relowlssretop  36244  ltflcei  36476  poimirlem1  36489  poimirlem2  36490  poimirlem4  36492  poimirlem6  36494  poimirlem7  36495  poimirlem8  36496  opnmbllem0  36524  mblfinlem1  36525  mblfinlem2  36526  mblfinlem4  36528  itg2addnclem2  36540  itg2addnclem3  36541  incsequz  36616  isbnd3  36652  rrntotbnd  36704  sn-sup2  41342  3cubeslem1  41422  3cubeslem2  41423  irrapxlem4  41563  pellexlem5  41571  pell14qrgapw  41614  pellfundgt1  41621  jm3.1lem2  41757  expdiophlem1  41760  fzuntgd  42209  zltlesub  43995  suplesup  44049  supxrunb3  44109  xrpnf  44196  fmul01lt1lem1  44300  limsupre3lem  44448  xlimxrre  44547  xlimpnfv  44554  ioodvbdlimc1lem1  44647  dvnxpaek  44658  dvnmul  44659  fourierdlem4  44827  fourierdlem11  44834  fourierdlem25  44848  fourierdlem50  44872  fourierdlem64  44886  fourierdlem65  44887  fourierdlem77  44899  fourierdlem79  44901  iinhoiicclem  45389  smfresal  45504  natglobalincr  45591  fmtno4prmfac  46240  lighneallem4a  46276  evenltle  46385  perfectALTVlem2  46390  logbpw2m1  47253