Theorem peano2re 11157

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

Assertion

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

Proof of Theorem peano2re

Step	Hyp	Ref	Expression
1		1re 10984	. 2 ⊢ 1 ∈ ℝ
2		readdcl 10963	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐴 + 1) ∈ ℝ)
3	1, 2	mpan2 688	1 ⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2107  (class class class)co 7284  ℝcr 10879  1c1 10881   + caddc 10883

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 2710  ax-1cn 10938  ax-icn 10939  ax-addcl 10940  ax-addrcl 10941  ax-mulcl 10942  ax-mulrcl 10943  ax-i2m1 10948  ax-1ne0 10949  ax-rrecex 10952  ax-cnre 10953

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-ne 2945  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-iota 6395  df-fv 6445  df-ov 7287

This theorem is referenced by:  lep1  11825  letrp1  11828  p1le  11829  ledivp1  11886  sup2  11940  nnssre  11986  nnge1  12010  div4p1lem1div2  12237  zltp1le  12379  suprzcl  12409  zeo  12415  peano2uz2  12417  uzind  12421  numltc  12472  uzwo  12660  ge0p1rp  12770  qbtwnxr  12943  xrsupsslem  13050  supxrunb1  13062  fznatpl1  13319  fzp1disj  13324  fzneuz  13346  fzp1nel  13349  ubmelm1fzo  13492  fllep1  13530  flflp1  13536  flhalf  13559  ltdifltdiv  13563  fldiv4p1lem1div2  13564  dfceil2  13568  ceim1l  13576  uzsup  13592  modltm1p1mod  13652  addmodlteq  13675  fsequb  13704  seqf1olem1  13771  seqf1olem2  13772  bernneq3  13955  expnbnd  13956  expmulnbnd  13959  discr1  13963  discr  13964  facwordi  14012  faclbnd  14013  hashfun  14161  seqcoll2  14188  rexuzre  15073  caubnd  15079  rlim2lt  15215  lo1bddrp  15243  rlimo1  15335  o1rlimmul  15337  o1fsum  15534  harmonic  15580  expcnv  15585  geomulcvg  15597  mertenslem1  15605  bpoly4  15778  nonsq  16472  eulerthlem2  16492  pcprendvds  16550  pcmpt  16602  pcfac  16609  vdwlem6  16696  vdwlem11  16701  chfacffsupp  22014  chfacfscmul0  22016  chfacfpmmul0  22020  tgioo  23968  zcld  23985  iocopnst  24112  cnheibor  24127  bndth  24130  cncmet  24495  pjthlem1  24610  ovolicc2lem3  24692  ovolicopnf  24697  ioorcl2  24745  dyadf  24764  dyadovol  24766  dyadss  24767  dyaddisjlem  24768  dyadmaxlem  24770  opnmbllem  24774  volsup2  24778  vitalilem2  24782  itg2const2  24915  itg2cnlem1  24935  dvfsumle  25194  dvfsumabs  25196  dvfsumlem1  25199  dvfsumlem3  25201  dvfsumrlim  25204  fta1glem2  25340  fta1lem  25476  aalioulem3  25503  ulmbdd  25566  itgulm  25576  psercnlem1  25593  abelthlem2  25600  abelthlem7  25606  reeff1olem  25614  logtayl  25824  loglesqrt  25920  atanlogsublem  26074  leibpi  26101  efrlim  26128  harmonicubnd  26168  fsumharmonic  26170  ftalem5  26235  basellem2  26240  basellem3  26241  chtnprm  26312  chpp1  26313  ppip1le  26319  ppiub  26361  logfaclbnd  26379  logfacrlim  26381  perfectlem2  26387  bcmono  26434  lgsvalmod  26473  gausslemma2dlem3  26525  lgseisen  26536  lgsquadlem1  26537  lgsquadlem2  26538  chebbnd1lem2  26627  chtppilimlem1  26630  rplogsumlem2  26642  dchrisumlema  26645  dchrisumlem1  26646  dchrisumlem3  26648  dchrisum0lem1  26673  chpdifbndlem1  26710  logdivbnd  26713  pntrmax  26721  pntrsumo1  26722  pntpbnd1a  26742  pntpbnd1  26743  pntpbnd2  26744  pntibndlem2  26748  pntlemg  26755  pntlemr  26759  pntlemj  26760  pntlemk  26763  ostth2lem1  26775  qabvle  26782  ostth2lem3  26792  ostth2lem4  26793  axlowdimlem16  27334  wwlksnredwwlkn  28269  wwlksnextproplem3  28285  wwlksext2clwwlk  28430  wwlksubclwwlk  28431  eupth2lems  28611  smcnlem  29068  minvecolem4  29251  pjhthlem1  29762  zltp1ne  33077  cvmliftlem7  33262  dnibndlem13  34679  knoppndvlem19  34719  knoppndvlem21  34721  icoreunrn  35539  relowlssretop  35543  ltflcei  35774  poimirlem1  35787  poimirlem2  35788  poimirlem4  35790  poimirlem6  35792  poimirlem7  35793  poimirlem8  35794  opnmbllem0  35822  mblfinlem1  35823  mblfinlem2  35824  mblfinlem4  35826  itg2addnclem2  35838  itg2addnclem3  35839  incsequz  35915  isbnd3  35951  rrntotbnd  36003  sn-sup2  40446  3cubeslem1  40513  3cubeslem2  40514  irrapxlem4  40654  pellexlem5  40662  pell14qrgapw  40705  pellfundgt1  40712  jm3.1lem2  40847  expdiophlem1  40850  fzuntgd  41072  zltlesub  42831  suplesup  42885  supxrunb3  42946  xrpnf  43033  fmul01lt1lem1  43132  limsupre3lem  43280  xlimxrre  43379  xlimpnfv  43386  ioodvbdlimc1lem1  43479  dvnxpaek  43490  dvnmul  43491  fourierdlem4  43659  fourierdlem11  43666  fourierdlem25  43680  fourierdlem50  43704  fourierdlem64  43718  fourierdlem65  43719  fourierdlem77  43731  fourierdlem79  43733  iinhoiicclem  44218  smfresal  44333  fmtno4prmfac  45035  lighneallem4a  45071  evenltle  45180  perfectALTVlem2  45185  logbpw2m1  45924  natglobalincr  46523