Theorem peano2re 11304

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

Assertion

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

Proof of Theorem peano2re

Step	Hyp	Ref	Expression
1		1re 11130	. 2 ⊢ 1 ∈ ℝ
2		readdcl 11107	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐴 + 1) ∈ ℝ)
3	1, 2	mpan2 691	1 ⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2113  (class class class)co 7356  ℝcr 11023  1c1 11025   + caddc 11027

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-1cn 11082  ax-icn 11083  ax-addcl 11084  ax-addrcl 11085  ax-mulcl 11086  ax-mulrcl 11087  ax-i2m1 11092  ax-1ne0 11093  ax-rrecex 11096  ax-cnre 11097

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-iota 6446  df-fv 6498  df-ov 7359

This theorem is referenced by:  lep1  11980  letrp1  11983  p1le  11984  ledivp1  12042  sup2  12096  nnssre  12147  nnge1  12171  div4p1lem1div2  12394  zltp1le  12539  suprzcl  12570  zeo  12576  peano2uz2  12578  uzind  12582  numltc  12631  uzwo  12822  ge0p1rp  12936  qbtwnxr  13113  xrsupsslem  13220  supxrunb1  13232  fznatpl1  13492  fzp1disj  13497  fzneuz  13522  fzp1nel  13525  ubmelm1fzo  13677  fllep1  13719  flflp1  13725  flhalf  13748  ltdifltdiv  13752  fldiv4p1lem1div2  13753  dfceil2  13757  ceim1l  13765  uzsup  13781  modltm1p1mod  13844  addmodlteq  13867  fsequb  13896  seqf1olem1  13962  seqf1olem2  13963  bernneq3  14152  expnbnd  14153  expmulnbnd  14156  discr1  14160  discr  14161  facwordi  14210  faclbnd  14211  hashfun  14358  seqcoll2  14386  rexuzre  15274  caubnd  15280  rlim2lt  15418  lo1bddrp  15446  rlimo1  15538  o1rlimmul  15540  o1fsum  15734  harmonic  15780  expcnv  15785  geomulcvg  15797  mertenslem1  15805  bpoly4  15980  nonsq  16684  eulerthlem2  16707  pcprendvds  16766  pcmpt  16818  pcfac  16825  vdwlem6  16912  vdwlem11  16917  chnccat  18547  chfacffsupp  22798  chfacfscmul0  22800  chfacfpmmul0  22804  tgioo  24738  zcld  24756  iocopnst  24891  cnheibor  24908  bndth  24911  cncmet  25276  pjthlem1  25391  ovolicc2lem3  25474  ovolicopnf  25479  ioorcl2  25527  dyadf  25546  dyadovol  25548  dyadss  25549  dyaddisjlem  25550  dyadmaxlem  25552  opnmbllem  25556  volsup2  25560  vitalilem2  25564  itg2const2  25696  itg2cnlem1  25716  dvfsumle  25980  dvfsumleOLD  25981  dvfsumabs  25983  dvfsumlem1  25986  dvfsumlem3  25989  dvfsumrlim  25992  fta1glem2  26128  fta1lem  26269  aalioulem3  26296  ulmbdd  26361  itgulm  26371  psercnlem1  26389  abelthlem2  26396  abelthlem7  26402  reeff1olem  26410  logtayl  26623  loglesqrt  26725  atanlogsublem  26879  leibpi  26906  efrlim  26933  efrlimOLD  26934  harmonicubnd  26974  fsumharmonic  26976  ftalem5  27041  basellem2  27046  basellem3  27047  chtnprm  27118  chpp1  27119  ppip1le  27125  ppiub  27169  logfaclbnd  27187  logfacrlim  27189  perfectlem2  27195  bcmono  27242  lgsvalmod  27281  gausslemma2dlem3  27333  lgseisen  27344  lgsquadlem1  27345  lgsquadlem2  27346  chebbnd1lem2  27435  chtppilimlem1  27438  rplogsumlem2  27450  dchrisumlema  27453  dchrisumlem1  27454  dchrisumlem3  27456  dchrisum0lem1  27481  chpdifbndlem1  27518  logdivbnd  27521  pntrmax  27529  pntrsumo1  27530  pntpbnd1a  27550  pntpbnd1  27551  pntpbnd2  27552  pntibndlem2  27556  pntlemg  27563  pntlemr  27567  pntlemj  27568  pntlemk  27571  ostth2lem1  27583  qabvle  27590  ostth2lem3  27600  ostth2lem4  27601  axlowdimlem16  28979  wwlksnredwwlkn  29917  wwlksnextproplem3  29933  wwlksext2clwwlk  30081  wwlksubclwwlk  30082  eupth2lems  30262  smcnlem  30721  minvecolem4  30904  pjhthlem1  31415  zltp1ne  35253  cvmliftlem7  35434  dnibndlem13  36633  knoppndvlem19  36673  knoppndvlem21  36675  icoreunrn  37503  relowlssretop  37507  ltflcei  37748  poimirlem1  37761  poimirlem2  37762  poimirlem4  37764  poimirlem6  37766  poimirlem7  37767  poimirlem8  37768  opnmbllem0  37796  mblfinlem1  37797  mblfinlem2  37798  mblfinlem4  37800  itg2addnclem2  37812  itg2addnclem3  37813  incsequz  37888  isbnd3  37924  rrntotbnd  37976  sn-sup2  42688  3cubeslem1  42868  3cubeslem2  42869  irrapxlem4  43009  pellexlem5  43017  pell14qrgapw  43060  pellfundgt1  43067  jm3.1lem2  43202  expdiophlem1  43205  fzuntgd  43641  zltlesub  45475  suplesup  45526  supxrunb3  45585  xrpnf  45671  fmul01lt1lem1  45772  limsupre3lem  45918  xlimxrre  46017  xlimpnfv  46024  ioodvbdlimc1lem1  46117  dvnxpaek  46128  dvnmul  46129  fourierdlem4  46297  fourierdlem11  46304  fourierdlem25  46318  fourierdlem50  46342  fourierdlem64  46356  fourierdlem65  46357  fourierdlem77  46369  fourierdlem79  46371  iinhoiicclem  46859  smfresal  46974  natglobalincr  47063  fmtno4prmfac  47760  lighneallem4a  47796  evenltle  47905  perfectALTVlem2  47910  logbpw2m1  48755