Theorem peano2re 10088

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

Assertion

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

Proof of Theorem peano2re

Step	Hyp	Ref	Expression
1		1re 9918	. 2 ⊢ 1 ∈ ℝ
2		readdcl 9898	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐴 + 1) ∈ ℝ)
3	1, 2	mpan2 703	1 ⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 1977  (class class class)co 6549  ℝcr 9814  1c1 9816   + caddc 9818

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-i2m1 9883  ax-1ne0 9884  ax-rrecex 9887  ax-cnre 9888

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552

This theorem is referenced by:  lep1  10741  letrp1  10744  p1le  10745  ledivp1  10804  sup2  10858  nnssre  10901  nnge1  10923  div4p1lem1div2  11164  zltp1le  11304  suprzcl  11333  zeo  11339  peano2uz2  11341  uzind  11345  numltc  11404  uzwo  11627  ge0p1rp  11738  qbtwnxr  11905  xrsupsslem  12009  supxrunb1  12021  fznatpl1  12265  fzp1disj  12269  fzneuz  12290  fzp1nel  12293  ubmelm1fzo  12430  fllep1  12464  flflp1  12470  flhalf  12493  ltdifltdiv  12497  fldiv4p1lem1div2  12498  dfceil2  12502  ceim1l  12508  uzsup  12524  modltm1p1mod  12584  addmodlteq  12607  fsequb  12636  seqf1olem1  12702  seqf1olem2  12703  bernneq3  12854  expnbnd  12855  expmulnbnd  12858  discr1  12862  discr  12863  facwordi  12938  faclbnd  12939  hashfun  13084  seqcoll2  13106  rexuzre  13940  caubnd  13946  rlim2lt  14076  lo1bddrp  14104  rlimo1  14195  o1rlimmul  14197  o1fsum  14386  harmonic  14430  expcnv  14435  geomulcvg  14446  mertenslem1  14455  bpoly4  14629  nonsq  15305  eulerthlem2  15325  pcprendvds  15383  pcmpt  15434  pcfac  15441  vdwlem6  15528  vdwlem11  15533  chfacffsupp  20480  chfacfscmul0  20482  chfacfpmmul0  20486  tgioo  22407  zcld  22424  iocopnst  22547  cnheibor  22562  bndth  22565  cncmet  22927  pjthlem1  23016  ovolicc2lem3  23094  ovolicopnf  23099  ioorcl2  23146  dyadf  23165  dyadovol  23167  dyadss  23168  dyaddisjlem  23169  dyadmaxlem  23171  opnmbllem  23175  volsup2  23179  vitalilem2  23184  itg2const2  23314  itg2cnlem1  23334  dvfsumle  23588  dvfsumabs  23590  dvfsumlem1  23593  dvfsumlem3  23595  dvfsumrlim  23598  fta1glem2  23730  fta1lem  23866  aalioulem3  23893  ulmbdd  23956  itgulm  23966  psercnlem1  23983  abelthlem2  23990  abelthlem7  23996  reeff1olem  24004  logtayl  24206  loglesqrt  24299  atanlogsublem  24442  leibpi  24469  efrlim  24496  harmonicubnd  24536  fsumharmonic  24538  ftalem5  24603  basellem2  24608  basellem3  24609  chtnprm  24680  chpp1  24681  ppip1le  24687  ppiub  24729  logfaclbnd  24747  logfacrlim  24749  perfectlem2  24755  bcmono  24802  lgsvalmod  24841  gausslemma2dlem3  24893  lgseisen  24904  lgsquadlem1  24905  lgsquadlem2  24906  chebbnd1lem2  24959  chtppilimlem1  24962  rplogsumlem2  24974  dchrisumlema  24977  dchrisumlem1  24978  dchrisumlem3  24980  dchrisum0lem1  25005  chpdifbndlem1  25042  logdivbnd  25045  pntrmax  25053  pntrsumo1  25054  pntpbnd1a  25074  pntpbnd1  25075  pntpbnd2  25076  pntibndlem2  25080  pntlemg  25087  pntlemr  25091  pntlemj  25092  pntlemk  25095  ostth2lem1  25107  qabvle  25114  ostth2lem3  25124  ostth2lem4  25125  axlowdimlem16  25637  wwlknredwwlkn  26254  wwlkextproplem1  26269  wwlkextproplem3  26271  wwlkext2clwwlk  26331  wwlksubclwwlk  26332  clwlkfclwwlk  26371  eupath2lem3  26506  eupath2  26507  extwwlkfablem2  26605  smcnlem  26936  minvecolem4  27120  pjhthlem1  27634  cvmliftlem7  30527  dnibndlem13  31650  knoppndvlem19  31691  knoppndvlem21  31693  icoreunrn  32383  relowlssretop  32387  ltflcei  32567  poimirlem1  32580  poimirlem2  32581  poimirlem4  32583  poimirlem6  32585  poimirlem7  32586  poimirlem8  32587  opnmbllem0  32615  mblfinlem1  32616  mblfinlem2  32617  mblfinlem4  32619  itg2addnclem2  32632  itg2addnclem3  32633  incsequz  32714  isbnd3  32753  rrntotbnd  32805  irrapxlem4  36407  pellexlem5  36415  pell14qrgapw  36458  pellfundgt1  36465  jm3.1lem2  36603  expdiophlem1  36606  zltlesub  38438  suplesup  38496  fmul01lt1lem1  38651  ioodvbdlimc1lem1  38821  dvnxpaek  38832  dvnmul  38833  fourierdlem4  39004  fourierdlem11  39011  fourierdlem25  39025  fourierdlem50  39049  fourierdlem64  39063  fourierdlem65  39064  fourierdlem77  39076  fourierdlem79  39078  iinhoiicclem  39564  smfresal  39673  fmtno4prmfac  40022  lighneallem4a  40063  perfectALTVlem2  40165  wwlksnredwwlkn  41101  wwlksnextproplem3  41117  wwlksext2clwwlk  41231  wwlksubclwwlks  41232  clwlksfclwwlk  41269  eupth2lems  41406  logbpw2m1  42159