Theorem peano2re 11356

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

Assertion

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

Proof of Theorem peano2re

Step	Hyp	Ref	Expression
1		1re 11181	. 2 ⊢ 1 ∈ ℝ
2		readdcl 11156	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐴 + 1) ∈ ℝ)
3	1, 2	mpan2 701	1 ⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2142  (class class class)co 7396  ℝcr 11072  1c1 11074   + caddc 11076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-1cn 11131  ax-icn 11132  ax-addcl 11133  ax-addrcl 11134  ax-mulcl 11135  ax-mulrcl 11136  ax-i2m1 11141  ax-1ne0 11142  ax-rrecex 11145  ax-cnre 11146

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6477  df-fv 6529  df-ov 7399

This theorem is referenced by:  lep1  12032  letrp1  12035  p1le  12036  ledivp1  12094  sup2  12148  nnssre  12214  nnge1  12241  div4p1lem1div2  12476  zltp1le  12621  suprzcl  12653  zeo  12659  peano2uz2  12661  uzind  12665  numltc  12719  uzwo  12912  ge0p1rp  13026  qbtwnxr  13203  xrsupsslem  13310  supxrunb1  13322  fznatpl1  13583  fzp1disj  13588  fzneuz  13613  fzp1nel  13616  ubmelm1fzo  13769  fllep1  13811  flflp1  13817  flhalf  13840  ltdifltdiv  13844  fldiv4p1lem1div2  13845  dfceil2  13849  ceim1l  13857  uzsup  13873  modltm1p1mod  13936  addmodlteq  13959  fsequb  13988  seqf1olem1  14054  seqf1olem2  14055  bernneq3  14244  expnbnd  14245  expmulnbnd  14248  discr1  14252  discr  14253  facwordi  14302  faclbnd  14303  hashfun  14450  seqcoll2  14478  rexuzre  15380  caubnd  15386  rlim2lt  15524  lo1bddrp  15552  rlimo1  15644  o1rlimmul  15646  o1fsum  15841  harmonic  15889  expcnv  15894  geomulcvg  15906  mertenslem1  15914  bpoly4  16089  nonsq  16794  eulerthlem2  16817  pcprendvds  16876  pcmpt  16928  pcfac  16935  vdwlem6  17022  vdwlem11  17027  chnccat  18658  chfacffsupp  22916  chfacfscmul0  22918  chfacfpmmul0  22922  tgioo  24856  zcld  24874  iocopnst  25002  cnheibor  25017  bndth  25020  cncmet  25384  pjthlem1  25499  ovolicc2lem3  25581  ovolicopnf  25586  ioorcl2  25634  dyadf  25653  dyadovol  25655  dyadss  25656  dyaddisjlem  25657  dyadmaxlem  25659  opnmbllem  25663  volsup2  25667  vitalilem2  25671  itg2const2  25803  itg2cnlem1  25823  dvfsumle  26083  dvfsumabs  26085  dvfsumlem1  26088  dvfsumlem3  26090  dvfsumrlim  26093  fta1glem2  26229  fta1lem  26371  aalioulem3  26398  ulmbdd  26461  itgulm  26471  psercnlem1  26488  abelthlem2  26495  abelthlem7  26501  reeff1olem  26509  logtayl  26725  loglesqrt  26826  atanlogsublem  26980  leibpi  27007  efrlim  27034  harmonicubnd  27074  fsumharmonic  27076  ftalem5  27141  basellem2  27146  basellem3  27147  chtnprm  27218  chpp1  27219  ppip1le  27225  ppiub  27268  logfaclbnd  27286  logfacrlim  27288  perfectlem2  27294  bcmono  27341  lgsvalmod  27380  gausslemma2dlem3  27432  lgseisen  27443  lgsquadlem1  27444  lgsquadlem2  27445  chebbnd1lem2  27534  chtppilimlem1  27537  rplogsumlem2  27549  dchrisumlema  27552  dchrisumlem1  27553  dchrisumlem3  27555  dchrisum0lem1  27580  chpdifbndlem1  27617  logdivbnd  27620  pntrmax  27628  pntrsumo1  27629  pntpbnd1a  27649  pntpbnd1  27650  pntpbnd2  27651  pntibndlem2  27655  pntlemg  27662  pntlemr  27666  pntlemj  27667  pntlemk  27670  ostth2lem1  27682  qabvle  27689  ostth2lem3  27699  ostth2lem4  27700  axlowdimlem16  29158  wwlksnredwwlkn  30095  wwlksnextproplem3  30111  wwlksext2clwwlk  30259  wwlksubclwwlk  30260  eupth2lems  30440  smcnlem  30900  minvecolem4  31083  pjhthlem1  31594  zltp1ne  35460  cvmliftlem7  35641  dnibndlem13  36928  knoppndvlem19  36968  knoppndvlem21  36970  icoreunrn  37853  relowlssretop  37857  ltflcei  38107  poimirlem1  38120  poimirlem2  38121  poimirlem4  38123  poimirlem6  38125  poimirlem7  38126  poimirlem8  38127  opnmbllem0  38155  mblfinlem1  38156  mblfinlem2  38157  mblfinlem4  38159  itg2addnclem2  38171  itg2addnclem3  38172  incsequz  38247  isbnd3  38283  rrntotbnd  38335  sn-sup2  43113  3cubeslem1  43265  3cubeslem2  43266  irrapxlem4  43402  pellexlem5  43410  pell14qrgapw  43453  pellfundgt1  43460  jm3.1lem2  43595  expdiophlem1  43598  fzuntgd  44034  zltlesub  45864  suplesup  45915  supxrunb3  45974  xrpnf  46059  fmul01lt1lem1  46160  limsupre3lem  46306  xlimxrre  46405  xlimpnfv  46412  ioodvbdlimc1lem1  46505  dvnxpaek  46516  dvnmul  46517  fourierdlem4  46685  fourierdlem11  46692  fourierdlem25  46706  fourierdlem50  46730  fourierdlem64  46744  fourierdlem65  46745  fourierdlem77  46757  fourierdlem79  46759  iinhoiicclem  47247  smfresal  47362  natglobalincr  47453  fmtno4prmfac  48181  lighneallem4a  48217  evenltle  48339  perfectALTVlem2  48344  logbpw2m1  49189