Theorem peano2re 11313

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

Assertion

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

Proof of Theorem peano2re

Step	Hyp	Ref	Expression
1		1re 11138	. 2 ⊢ 1 ∈ ℝ
2		readdcl 11115	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐴 + 1) ∈ ℝ)
3	1, 2	mpan2 692	1 ⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7361  ℝcr 11031  1c1 11033   + caddc 11035

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-addrcl 11093  ax-mulcl 11094  ax-mulrcl 11095  ax-i2m1 11100  ax-1ne0 11101  ax-rrecex 11104  ax-cnre 11105

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6449  df-fv 6501  df-ov 7364

This theorem is referenced by:  lep1  11990  letrp1  11993  p1le  11994  ledivp1  12052  sup2  12106  nnssre  12172  nnge1  12199  div4p1lem1div2  12426  zltp1le  12571  suprzcl  12603  zeo  12609  peano2uz2  12611  uzind  12615  numltc  12664  uzwo  12855  ge0p1rp  12969  qbtwnxr  13146  xrsupsslem  13253  supxrunb1  13265  fznatpl1  13526  fzp1disj  13531  fzneuz  13556  fzp1nel  13559  ubmelm1fzo  13712  fllep1  13754  flflp1  13760  flhalf  13783  ltdifltdiv  13787  fldiv4p1lem1div2  13788  dfceil2  13792  ceim1l  13800  uzsup  13816  modltm1p1mod  13879  addmodlteq  13902  fsequb  13931  seqf1olem1  13997  seqf1olem2  13998  bernneq3  14187  expnbnd  14188  expmulnbnd  14191  discr1  14195  discr  14196  facwordi  14245  faclbnd  14246  hashfun  14393  seqcoll2  14421  rexuzre  15309  caubnd  15315  rlim2lt  15453  lo1bddrp  15481  rlimo1  15573  o1rlimmul  15575  o1fsum  15770  harmonic  15818  expcnv  15823  geomulcvg  15835  mertenslem1  15843  bpoly4  16018  nonsq  16723  eulerthlem2  16746  pcprendvds  16805  pcmpt  16857  pcfac  16864  vdwlem6  16951  vdwlem11  16956  chnccat  18586  chfacffsupp  22834  chfacfscmul0  22836  chfacfpmmul0  22840  tgioo  24774  zcld  24792  iocopnst  24920  cnheibor  24935  bndth  24938  cncmet  25302  pjthlem1  25417  ovolicc2lem3  25499  ovolicopnf  25504  ioorcl2  25552  dyadf  25571  dyadovol  25573  dyadss  25574  dyaddisjlem  25575  dyadmaxlem  25577  opnmbllem  25581  volsup2  25585  vitalilem2  25589  itg2const2  25721  itg2cnlem1  25741  dvfsumle  26001  dvfsumabs  26003  dvfsumlem1  26006  dvfsumlem3  26008  dvfsumrlim  26011  fta1glem2  26147  fta1lem  26287  aalioulem3  26314  ulmbdd  26379  itgulm  26389  psercnlem1  26406  abelthlem2  26413  abelthlem7  26419  reeff1olem  26427  logtayl  26640  loglesqrt  26741  atanlogsublem  26895  leibpi  26922  efrlim  26949  efrlimOLD  26950  harmonicubnd  26990  fsumharmonic  26992  ftalem5  27057  basellem2  27062  basellem3  27063  chtnprm  27134  chpp1  27135  ppip1le  27141  ppiub  27184  logfaclbnd  27202  logfacrlim  27204  perfectlem2  27210  bcmono  27257  lgsvalmod  27296  gausslemma2dlem3  27348  lgseisen  27359  lgsquadlem1  27360  lgsquadlem2  27361  chebbnd1lem2  27450  chtppilimlem1  27453  rplogsumlem2  27465  dchrisumlema  27468  dchrisumlem1  27469  dchrisumlem3  27471  dchrisum0lem1  27496  chpdifbndlem1  27533  logdivbnd  27536  pntrmax  27544  pntrsumo1  27545  pntpbnd1a  27565  pntpbnd1  27566  pntpbnd2  27567  pntibndlem2  27571  pntlemg  27578  pntlemr  27582  pntlemj  27583  pntlemk  27586  ostth2lem1  27598  qabvle  27605  ostth2lem3  27615  ostth2lem4  27616  axlowdimlem16  29043  wwlksnredwwlkn  29981  wwlksnextproplem3  29997  wwlksext2clwwlk  30145  wwlksubclwwlk  30146  eupth2lems  30326  smcnlem  30786  minvecolem4  30969  pjhthlem1  31480  zltp1ne  35311  cvmliftlem7  35492  dnibndlem13  36769  knoppndvlem19  36809  knoppndvlem21  36811  icoreunrn  37692  relowlssretop  37696  ltflcei  37946  poimirlem1  37959  poimirlem2  37960  poimirlem4  37962  poimirlem6  37964  poimirlem7  37965  poimirlem8  37966  opnmbllem0  37994  mblfinlem1  37995  mblfinlem2  37996  mblfinlem4  37998  itg2addnclem2  38010  itg2addnclem3  38011  incsequz  38086  isbnd3  38122  rrntotbnd  38174  sn-sup2  42953  3cubeslem1  43133  3cubeslem2  43134  irrapxlem4  43274  pellexlem5  43282  pell14qrgapw  43325  pellfundgt1  43332  jm3.1lem2  43467  expdiophlem1  43470  fzuntgd  43906  zltlesub  45739  suplesup  45790  supxrunb3  45849  xrpnf  45934  fmul01lt1lem1  46035  limsupre3lem  46181  xlimxrre  46280  xlimpnfv  46287  ioodvbdlimc1lem1  46380  dvnxpaek  46391  dvnmul  46392  fourierdlem4  46560  fourierdlem11  46567  fourierdlem25  46581  fourierdlem50  46605  fourierdlem64  46619  fourierdlem65  46620  fourierdlem77  46632  fourierdlem79  46634  iinhoiicclem  47122  smfresal  47237  natglobalincr  47326  fmtno4prmfac  48050  lighneallem4a  48086  evenltle  48208  perfectALTVlem2  48213  logbpw2m1  49058