Theorem peano2re 11391

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

Assertion

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

Proof of Theorem peano2re

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

Syntax hints:   → wi 4   ∈ wcel 2104  (class class class)co 7411  ℝcr 11111  1c1 11113   + caddc 11115

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-i2m1 11180  ax-1ne0 11181  ax-rrecex 11184  ax-cnre 11185

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6494  df-fv 6550  df-ov 7414

This theorem is referenced by:  lep1  12059  letrp1  12062  p1le  12063  ledivp1  12120  sup2  12174  nnssre  12220  nnge1  12244  div4p1lem1div2  12471  zltp1le  12616  suprzcl  12646  zeo  12652  peano2uz2  12654  uzind  12658  numltc  12707  uzwo  12899  ge0p1rp  13009  qbtwnxr  13183  xrsupsslem  13290  supxrunb1  13302  fznatpl1  13559  fzp1disj  13564  fzneuz  13586  fzp1nel  13589  ubmelm1fzo  13732  fllep1  13770  flflp1  13776  flhalf  13799  ltdifltdiv  13803  fldiv4p1lem1div2  13804  dfceil2  13808  ceim1l  13816  uzsup  13832  modltm1p1mod  13892  addmodlteq  13915  fsequb  13944  seqf1olem1  14011  seqf1olem2  14012  bernneq3  14198  expnbnd  14199  expmulnbnd  14202  discr1  14206  discr  14207  facwordi  14253  faclbnd  14254  hashfun  14401  seqcoll2  14430  rexuzre  15303  caubnd  15309  rlim2lt  15445  lo1bddrp  15473  rlimo1  15565  o1rlimmul  15567  o1fsum  15763  harmonic  15809  expcnv  15814  geomulcvg  15826  mertenslem1  15834  bpoly4  16007  nonsq  16699  eulerthlem2  16719  pcprendvds  16777  pcmpt  16829  pcfac  16836  vdwlem6  16923  vdwlem11  16928  chfacffsupp  22578  chfacfscmul0  22580  chfacfpmmul0  22584  tgioo  24532  zcld  24549  iocopnst  24684  cnheibor  24701  bndth  24704  cncmet  25070  pjthlem1  25185  ovolicc2lem3  25268  ovolicopnf  25273  ioorcl2  25321  dyadf  25340  dyadovol  25342  dyadss  25343  dyaddisjlem  25344  dyadmaxlem  25346  opnmbllem  25350  volsup2  25354  vitalilem2  25358  itg2const2  25491  itg2cnlem1  25511  dvfsumle  25773  dvfsumabs  25775  dvfsumlem1  25778  dvfsumlem3  25780  dvfsumrlim  25783  fta1glem2  25919  fta1lem  26056  aalioulem3  26083  ulmbdd  26146  itgulm  26156  psercnlem1  26173  abelthlem2  26180  abelthlem7  26186  reeff1olem  26194  logtayl  26404  loglesqrt  26502  atanlogsublem  26656  leibpi  26683  efrlim  26710  harmonicubnd  26750  fsumharmonic  26752  ftalem5  26817  basellem2  26822  basellem3  26823  chtnprm  26894  chpp1  26895  ppip1le  26901  ppiub  26943  logfaclbnd  26961  logfacrlim  26963  perfectlem2  26969  bcmono  27016  lgsvalmod  27055  gausslemma2dlem3  27107  lgseisen  27118  lgsquadlem1  27119  lgsquadlem2  27120  chebbnd1lem2  27209  chtppilimlem1  27212  rplogsumlem2  27224  dchrisumlema  27227  dchrisumlem1  27228  dchrisumlem3  27230  dchrisum0lem1  27255  chpdifbndlem1  27292  logdivbnd  27295  pntrmax  27303  pntrsumo1  27304  pntpbnd1a  27324  pntpbnd1  27325  pntpbnd2  27326  pntibndlem2  27330  pntlemg  27337  pntlemr  27341  pntlemj  27342  pntlemk  27345  ostth2lem1  27357  qabvle  27364  ostth2lem3  27374  ostth2lem4  27375  axlowdimlem16  28482  wwlksnredwwlkn  29416  wwlksnextproplem3  29432  wwlksext2clwwlk  29577  wwlksubclwwlk  29578  eupth2lems  29758  smcnlem  30217  minvecolem4  30400  pjhthlem1  30911  zltp1ne  34397  cvmliftlem7  34580  gg-dvfsumle  35468  dnibndlem13  35669  knoppndvlem19  35709  knoppndvlem21  35711  icoreunrn  36543  relowlssretop  36547  ltflcei  36779  poimirlem1  36792  poimirlem2  36793  poimirlem4  36795  poimirlem6  36797  poimirlem7  36798  poimirlem8  36799  opnmbllem0  36827  mblfinlem1  36828  mblfinlem2  36829  mblfinlem4  36831  itg2addnclem2  36843  itg2addnclem3  36844  incsequz  36919  isbnd3  36955  rrntotbnd  37007  sn-sup2  41644  3cubeslem1  41724  3cubeslem2  41725  irrapxlem4  41865  pellexlem5  41873  pell14qrgapw  41916  pellfundgt1  41923  jm3.1lem2  42059  expdiophlem1  42062  fzuntgd  42511  zltlesub  44293  suplesup  44347  supxrunb3  44407  xrpnf  44494  fmul01lt1lem1  44598  limsupre3lem  44746  xlimxrre  44845  xlimpnfv  44852  ioodvbdlimc1lem1  44945  dvnxpaek  44956  dvnmul  44957  fourierdlem4  45125  fourierdlem11  45132  fourierdlem25  45146  fourierdlem50  45170  fourierdlem64  45184  fourierdlem65  45185  fourierdlem77  45197  fourierdlem79  45199  iinhoiicclem  45687  smfresal  45802  natglobalincr  45889  fmtno4prmfac  46538  lighneallem4a  46574  evenltle  46683  perfectALTVlem2  46688  logbpw2m1  47340