Theorem peano2re 11382

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

Assertion

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

Proof of Theorem peano2re

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

Syntax hints:   → wi 4   ∈ wcel 2149  (class class class)co 7411  ℝcr 11098  1c1 11100   + caddc 11102

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-1cn 11157  ax-icn 11158  ax-addcl 11159  ax-addrcl 11160  ax-mulcl 11161  ax-mulrcl 11162  ax-i2m1 11167  ax-1ne0 11168  ax-rrecex 11171  ax-cnre 11172

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-iota 6493  df-fv 6545  df-ov 7414

This theorem is referenced by:  lep1  12055  letrp1  12058  p1le  12059  ledivp1  12116  sup2  12170  nnssre  12236  nnge1  12263  div4p1lem1div2  12498  zltp1le  12643  suprzcl  12675  zeo  12681  peano2uz2  12683  uzind  12687  numltc  12741  uzwo  12934  ge0p1rp  13048  qbtwnxr  13225  xrsupsslem  13332  supxrunb1  13344  fznatpl1  13605  fzp1disj  13610  fzneuz  13635  fzp1nel  13638  ubmelm1fzo  13791  fllep1  13833  flflp1  13839  flhalf  13862  ltdifltdiv  13866  fldiv4p1lem1div2  13867  dfceil2  13871  ceim1l  13879  uzsup  13895  modltm1p1mod  13958  addmodlteq  13981  fsequb  14010  seqf1olem1  14076  seqf1olem2  14077  bernneq3  14266  expnbnd  14267  expmulnbnd  14270  discr1  14274  discr  14275  facwordi  14324  faclbnd  14325  hashfun  14473  seqcoll2  14501  rexuzre  15403  caubnd  15409  rlim2lt  15547  lo1bddrp  15575  rlimo1  15667  o1rlimmul  15669  o1fsum  15864  harmonic  15912  expcnv  15917  geomulcvg  15929  mertenslem1  15937  bpoly4  16112  nonsq  16817  eulerthlem2  16840  pcprendvds  16899  pcmpt  16951  pcfac  16958  vdwlem6  17045  vdwlem11  17050  chnccat  18681  chfacffsupp  22981  chfacfscmul0  22983  chfacfpmmul0  22987  tgioo  24921  zcld  24939  iocopnst  25067  cnheibor  25082  bndth  25085  cncmet  25449  pjthlem1  25564  ovolicc2lem3  25646  ovolicopnf  25651  ioorcl2  25699  dyadf  25718  dyadovol  25720  dyadss  25721  dyaddisjlem  25722  dyadmaxlem  25724  opnmbllem  25728  volsup2  25732  vitalilem2  25736  itg2const2  25868  itg2cnlem1  25888  dvfsumle  26148  dvfsumabs  26150  dvfsumlem1  26153  dvfsumlem3  26155  dvfsumrlim  26158  fta1glem2  26294  fta1lem  26436  aalioulem3  26463  ulmbdd  26526  itgulm  26536  psercnlem1  26553  abelthlem2  26560  abelthlem7  26566  reeff1olem  26574  logtayl  26790  loglesqrt  26891  atanlogsublem  27045  leibpi  27072  efrlim  27099  harmonicubnd  27139  fsumharmonic  27141  ftalem5  27206  basellem2  27211  basellem3  27212  chtnprm  27283  chpp1  27284  ppip1le  27290  ppiub  27333  logfaclbnd  27351  logfacrlim  27353  perfectlem2  27359  bcmono  27406  lgsvalmod  27445  gausslemma2dlem3  27497  lgseisen  27508  lgsquadlem1  27509  lgsquadlem2  27510  chebbnd1lem2  27599  chtppilimlem1  27602  rplogsumlem2  27614  dchrisumlema  27617  dchrisumlem1  27618  dchrisumlem3  27620  dchrisum0lem1  27645  chpdifbndlem1  27682  logdivbnd  27685  pntrmax  27693  pntrsumo1  27694  pntpbnd1a  27714  pntpbnd1  27715  pntpbnd2  27716  pntibndlem2  27720  pntlemg  27727  pntlemr  27731  pntlemj  27732  pntlemk  27735  ostth2lem1  27747  qabvle  27754  ostth2lem3  27764  ostth2lem4  27765  axlowdimlem16  29247  wwlksnredwwlkn  30184  wwlksnextproplem3  30200  wwlksext2clwwlk  30348  wwlksubclwwlk  30349  eupth2lems  30529  smcnlem  30989  minvecolem4  31172  pjhthlem1  31683  zltp1ne  35499  cvmliftlem7  35681  dnibndlem13  36967  knoppndvlem19  37007  knoppndvlem21  37009  icoreunrn  37892  relowlssretop  37896  ltflcei  38146  poimirlem1  38159  poimirlem2  38160  poimirlem4  38162  poimirlem6  38164  poimirlem7  38165  poimirlem8  38166  opnmbllem0  38194  mblfinlem1  38195  mblfinlem2  38196  mblfinlem4  38198  itg2addnclem2  38210  itg2addnclem3  38211  incsequz  38286  isbnd3  38322  rrntotbnd  38374  sn-sup2  43154  3cubeslem1  43306  3cubeslem2  43307  irrapxlem4  43443  pellexlem5  43451  pell14qrgapw  43494  pellfundgt1  43501  jm3.1lem2  43636  expdiophlem1  43639  fzuntgd  44075  zltlesub  45895  suplesup  45946  supxrunb3  46005  xrpnf  46090  fmul01lt1lem1  46191  limsupre3lem  46337  xlimxrre  46436  xlimpnfv  46443  ioodvbdlimc1lem1  46536  dvnxpaek  46547  dvnmul  46548  fourierdlem4  46716  fourierdlem11  46723  fourierdlem25  46737  fourierdlem50  46761  fourierdlem64  46775  fourierdlem65  46776  fourierdlem77  46788  fourierdlem79  46790  iinhoiicclem  47278  smfresal  47393  natglobalincr  47484  fmtno4prmfac  48212  lighneallem4a  48248  evenltle  48370  perfectALTVlem2  48375  logbpw2m1  49231