Theorem peano2re 11078

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

Assertion

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

Proof of Theorem peano2re

Step	Hyp	Ref	Expression
1		1re 10906	. 2 ⊢ 1 ∈ ℝ
2		readdcl 10885	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐴 + 1) ∈ ℝ)
3	1, 2	mpan2 687	1 ⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2108  (class class class)co 7255  ℝcr 10801  1c1 10803   + caddc 10805

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-i2m1 10870  ax-1ne0 10871  ax-rrecex 10874  ax-cnre 10875

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426  df-ov 7258

This theorem is referenced by:  lep1  11746  letrp1  11749  p1le  11750  ledivp1  11807  sup2  11861  nnssre  11907  nnge1  11931  div4p1lem1div2  12158  zltp1le  12300  suprzcl  12330  zeo  12336  peano2uz2  12338  uzind  12342  numltc  12392  uzwo  12580  ge0p1rp  12690  qbtwnxr  12863  xrsupsslem  12970  supxrunb1  12982  fznatpl1  13239  fzp1disj  13244  fzneuz  13266  fzp1nel  13269  ubmelm1fzo  13411  fllep1  13449  flflp1  13455  flhalf  13478  ltdifltdiv  13482  fldiv4p1lem1div2  13483  dfceil2  13487  ceim1l  13495  uzsup  13511  modltm1p1mod  13571  addmodlteq  13594  fsequb  13623  seqf1olem1  13690  seqf1olem2  13691  bernneq3  13874  expnbnd  13875  expmulnbnd  13878  discr1  13882  discr  13883  facwordi  13931  faclbnd  13932  hashfun  14080  seqcoll2  14107  rexuzre  14992  caubnd  14998  rlim2lt  15134  lo1bddrp  15162  rlimo1  15254  o1rlimmul  15256  o1fsum  15453  harmonic  15499  expcnv  15504  geomulcvg  15516  mertenslem1  15524  bpoly4  15697  nonsq  16391  eulerthlem2  16411  pcprendvds  16469  pcmpt  16521  pcfac  16528  vdwlem6  16615  vdwlem11  16620  chfacffsupp  21913  chfacfscmul0  21915  chfacfpmmul0  21919  tgioo  23865  zcld  23882  iocopnst  24009  cnheibor  24024  bndth  24027  cncmet  24391  pjthlem1  24506  ovolicc2lem3  24588  ovolicopnf  24593  ioorcl2  24641  dyadf  24660  dyadovol  24662  dyadss  24663  dyaddisjlem  24664  dyadmaxlem  24666  opnmbllem  24670  volsup2  24674  vitalilem2  24678  itg2const2  24811  itg2cnlem1  24831  dvfsumle  25090  dvfsumabs  25092  dvfsumlem1  25095  dvfsumlem3  25097  dvfsumrlim  25100  fta1glem2  25236  fta1lem  25372  aalioulem3  25399  ulmbdd  25462  itgulm  25472  psercnlem1  25489  abelthlem2  25496  abelthlem7  25502  reeff1olem  25510  logtayl  25720  loglesqrt  25816  atanlogsublem  25970  leibpi  25997  efrlim  26024  harmonicubnd  26064  fsumharmonic  26066  ftalem5  26131  basellem2  26136  basellem3  26137  chtnprm  26208  chpp1  26209  ppip1le  26215  ppiub  26257  logfaclbnd  26275  logfacrlim  26277  perfectlem2  26283  bcmono  26330  lgsvalmod  26369  gausslemma2dlem3  26421  lgseisen  26432  lgsquadlem1  26433  lgsquadlem2  26434  chebbnd1lem2  26523  chtppilimlem1  26526  rplogsumlem2  26538  dchrisumlema  26541  dchrisumlem1  26542  dchrisumlem3  26544  dchrisum0lem1  26569  chpdifbndlem1  26606  logdivbnd  26609  pntrmax  26617  pntrsumo1  26618  pntpbnd1a  26638  pntpbnd1  26639  pntpbnd2  26640  pntibndlem2  26644  pntlemg  26651  pntlemr  26655  pntlemj  26656  pntlemk  26659  ostth2lem1  26671  qabvle  26678  ostth2lem3  26688  ostth2lem4  26689  axlowdimlem16  27228  wwlksnredwwlkn  28161  wwlksnextproplem3  28177  wwlksext2clwwlk  28322  wwlksubclwwlk  28323  eupth2lems  28503  smcnlem  28960  minvecolem4  29143  pjhthlem1  29654  zltp1ne  32968  cvmliftlem7  33153  dnibndlem13  34597  knoppndvlem19  34637  knoppndvlem21  34639  icoreunrn  35457  relowlssretop  35461  ltflcei  35692  poimirlem1  35705  poimirlem2  35706  poimirlem4  35708  poimirlem6  35710  poimirlem7  35711  poimirlem8  35712  opnmbllem0  35740  mblfinlem1  35741  mblfinlem2  35742  mblfinlem4  35744  itg2addnclem2  35756  itg2addnclem3  35757  incsequz  35833  isbnd3  35869  rrntotbnd  35921  sn-sup2  40360  3cubeslem1  40422  3cubeslem2  40423  irrapxlem4  40563  pellexlem5  40571  pell14qrgapw  40614  pellfundgt1  40621  jm3.1lem2  40756  expdiophlem1  40759  zltlesub  42713  suplesup  42768  supxrunb3  42829  xrpnf  42916  fmul01lt1lem1  43015  limsupre3lem  43163  xlimxrre  43262  xlimpnfv  43269  ioodvbdlimc1lem1  43362  dvnxpaek  43373  dvnmul  43374  fourierdlem4  43542  fourierdlem11  43549  fourierdlem25  43563  fourierdlem50  43587  fourierdlem64  43601  fourierdlem65  43602  fourierdlem77  43614  fourierdlem79  43616  iinhoiicclem  44101  smfresal  44209  fmtno4prmfac  44912  lighneallem4a  44948  evenltle  45057  perfectALTVlem2  45062  logbpw2m1  45801