Theorem peano2re 10813

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

Assertion

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

Proof of Theorem peano2re

Step	Hyp	Ref	Expression
1		1re 10641	. 2 ⊢ 1 ∈ ℝ
2		readdcl 10620	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐴 + 1) ∈ ℝ)
3	1, 2	mpan2 689	1 ⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7156  ℝcr 10536  1c1 10538   + caddc 10540

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-addrcl 10598  ax-mulcl 10599  ax-mulrcl 10600  ax-i2m1 10605  ax-1ne0 10606  ax-rrecex 10609  ax-cnre 10610

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-iota 6314  df-fv 6363  df-ov 7159

This theorem is referenced by:  lep1  11481  letrp1  11484  p1le  11485  ledivp1  11542  sup2  11597  nnssre  11642  nnge1  11666  div4p1lem1div2  11893  zltp1le  12033  suprzcl  12063  zeo  12069  peano2uz2  12071  uzind  12075  numltc  12125  uzwo  12312  ge0p1rp  12421  qbtwnxr  12594  xrsupsslem  12701  supxrunb1  12713  fznatpl1  12962  fzp1disj  12967  fzneuz  12989  fzp1nel  12992  ubmelm1fzo  13134  fllep1  13172  flflp1  13178  flhalf  13201  ltdifltdiv  13205  fldiv4p1lem1div2  13206  dfceil2  13210  ceim1l  13216  uzsup  13232  modltm1p1mod  13292  addmodlteq  13315  fsequb  13344  seqf1olem1  13410  seqf1olem2  13411  bernneq3  13593  expnbnd  13594  expmulnbnd  13597  discr1  13601  discr  13602  facwordi  13650  faclbnd  13651  hashfun  13799  seqcoll2  13824  rexuzre  14712  caubnd  14718  rlim2lt  14854  lo1bddrp  14882  rlimo1  14973  o1rlimmul  14975  o1fsum  15168  harmonic  15214  expcnv  15219  geomulcvg  15232  mertenslem1  15240  bpoly4  15413  nonsq  16099  eulerthlem2  16119  pcprendvds  16177  pcmpt  16228  pcfac  16235  vdwlem6  16322  vdwlem11  16327  chfacffsupp  21464  chfacfscmul0  21466  chfacfpmmul0  21470  tgioo  23404  zcld  23421  iocopnst  23544  cnheibor  23559  bndth  23562  cncmet  23925  pjthlem1  24040  ovolicc2lem3  24120  ovolicopnf  24125  ioorcl2  24173  dyadf  24192  dyadovol  24194  dyadss  24195  dyaddisjlem  24196  dyadmaxlem  24198  opnmbllem  24202  volsup2  24206  vitalilem2  24210  itg2const2  24342  itg2cnlem1  24362  dvfsumle  24618  dvfsumabs  24620  dvfsumlem1  24623  dvfsumlem3  24625  dvfsumrlim  24628  fta1glem2  24760  fta1lem  24896  aalioulem3  24923  ulmbdd  24986  itgulm  24996  psercnlem1  25013  abelthlem2  25020  abelthlem7  25026  reeff1olem  25034  logtayl  25243  loglesqrt  25339  atanlogsublem  25493  leibpi  25520  efrlim  25547  harmonicubnd  25587  fsumharmonic  25589  ftalem5  25654  basellem2  25659  basellem3  25660  chtnprm  25731  chpp1  25732  ppip1le  25738  ppiub  25780  logfaclbnd  25798  logfacrlim  25800  perfectlem2  25806  bcmono  25853  lgsvalmod  25892  gausslemma2dlem3  25944  lgseisen  25955  lgsquadlem1  25956  lgsquadlem2  25957  chebbnd1lem2  26046  chtppilimlem1  26049  rplogsumlem2  26061  dchrisumlema  26064  dchrisumlem1  26065  dchrisumlem3  26067  dchrisum0lem1  26092  chpdifbndlem1  26129  logdivbnd  26132  pntrmax  26140  pntrsumo1  26141  pntpbnd1a  26161  pntpbnd1  26162  pntpbnd2  26163  pntibndlem2  26167  pntlemg  26174  pntlemr  26178  pntlemj  26179  pntlemk  26182  ostth2lem1  26194  qabvle  26201  ostth2lem3  26211  ostth2lem4  26212  axlowdimlem16  26743  wwlksnredwwlkn  27673  wwlksnextproplem3  27690  wwlksext2clwwlk  27836  wwlksubclwwlk  27837  eupth2lems  28017  smcnlem  28474  minvecolem4  28657  pjhthlem1  29168  zltp1ne  32348  cvmliftlem7  32538  dnibndlem13  33829  knoppndvlem19  33869  knoppndvlem21  33871  icoreunrn  34643  relowlssretop  34647  ltflcei  34895  poimirlem1  34908  poimirlem2  34909  poimirlem4  34911  poimirlem6  34913  poimirlem7  34914  poimirlem8  34915  opnmbllem0  34943  mblfinlem1  34944  mblfinlem2  34945  mblfinlem4  34947  itg2addnclem2  34959  itg2addnclem3  34960  incsequz  35038  isbnd3  35077  rrntotbnd  35129  3cubeslem1  39301  3cubeslem2  39302  irrapxlem4  39442  pellexlem5  39450  pell14qrgapw  39493  pellfundgt1  39500  jm3.1lem2  39635  expdiophlem1  39638  zltlesub  41571  suplesup  41627  supxrunb3  41692  xrpnf  41782  fmul01lt1lem1  41885  limsupre3lem  42033  xlimxrre  42132  xlimpnfv  42139  ioodvbdlimc1lem1  42236  dvnxpaek  42247  dvnmul  42248  fourierdlem4  42416  fourierdlem11  42423  fourierdlem25  42437  fourierdlem50  42461  fourierdlem64  42475  fourierdlem65  42476  fourierdlem77  42488  fourierdlem79  42490  iinhoiicclem  42975  smfresal  43083  fmtno4prmfac  43754  lighneallem4a  43793  evenltle  43902  perfectALTVlem2  43907  logbpw2m1  44647