Theorem peano2re 10815

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

Assertion

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

Proof of Theorem peano2re

Step	Hyp	Ref	Expression
1		1re 10643	. 2 ⊢ 1 ∈ ℝ
2		readdcl 10622	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐴 + 1) ∈ ℝ)
3	1, 2	mpan2 689	1 ⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2114  (class class class)co 7158  ℝcr 10538  1c1 10540   + caddc 10542

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-1cn 10597  ax-icn 10598  ax-addcl 10599  ax-addrcl 10600  ax-mulcl 10601  ax-mulrcl 10602  ax-i2m1 10607  ax-1ne0 10608  ax-rrecex 10611  ax-cnre 10612

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-iota 6316  df-fv 6365  df-ov 7161

This theorem is referenced by:  lep1  11483  letrp1  11486  p1le  11487  ledivp1  11544  sup2  11599  nnssre  11644  nnge1  11668  div4p1lem1div2  11895  zltp1le  12035  suprzcl  12065  zeo  12071  peano2uz2  12073  uzind  12077  numltc  12127  uzwo  12314  ge0p1rp  12423  qbtwnxr  12596  xrsupsslem  12703  supxrunb1  12715  fznatpl1  12964  fzp1disj  12969  fzneuz  12991  fzp1nel  12994  ubmelm1fzo  13136  fllep1  13174  flflp1  13180  flhalf  13203  ltdifltdiv  13207  fldiv4p1lem1div2  13208  dfceil2  13212  ceim1l  13218  uzsup  13234  modltm1p1mod  13294  addmodlteq  13317  fsequb  13346  seqf1olem1  13412  seqf1olem2  13413  bernneq3  13595  expnbnd  13596  expmulnbnd  13599  discr1  13603  discr  13604  facwordi  13652  faclbnd  13653  hashfun  13801  seqcoll2  13826  rexuzre  14714  caubnd  14720  rlim2lt  14856  lo1bddrp  14884  rlimo1  14975  o1rlimmul  14977  o1fsum  15170  harmonic  15216  expcnv  15221  geomulcvg  15234  mertenslem1  15242  bpoly4  15415  nonsq  16101  eulerthlem2  16121  pcprendvds  16179  pcmpt  16230  pcfac  16237  vdwlem6  16324  vdwlem11  16329  chfacffsupp  21466  chfacfscmul0  21468  chfacfpmmul0  21472  tgioo  23406  zcld  23423  iocopnst  23546  cnheibor  23561  bndth  23564  cncmet  23927  pjthlem1  24042  ovolicc2lem3  24122  ovolicopnf  24127  ioorcl2  24175  dyadf  24194  dyadovol  24196  dyadss  24197  dyaddisjlem  24198  dyadmaxlem  24200  opnmbllem  24204  volsup2  24208  vitalilem2  24212  itg2const2  24344  itg2cnlem1  24364  dvfsumle  24620  dvfsumabs  24622  dvfsumlem1  24625  dvfsumlem3  24627  dvfsumrlim  24630  fta1glem2  24762  fta1lem  24898  aalioulem3  24925  ulmbdd  24988  itgulm  24998  psercnlem1  25015  abelthlem2  25022  abelthlem7  25028  reeff1olem  25036  logtayl  25245  loglesqrt  25341  atanlogsublem  25495  leibpi  25522  efrlim  25549  harmonicubnd  25589  fsumharmonic  25591  ftalem5  25656  basellem2  25661  basellem3  25662  chtnprm  25733  chpp1  25734  ppip1le  25740  ppiub  25782  logfaclbnd  25800  logfacrlim  25802  perfectlem2  25808  bcmono  25855  lgsvalmod  25894  gausslemma2dlem3  25946  lgseisen  25957  lgsquadlem1  25958  lgsquadlem2  25959  chebbnd1lem2  26048  chtppilimlem1  26051  rplogsumlem2  26063  dchrisumlema  26066  dchrisumlem1  26067  dchrisumlem3  26069  dchrisum0lem1  26094  chpdifbndlem1  26131  logdivbnd  26134  pntrmax  26142  pntrsumo1  26143  pntpbnd1a  26163  pntpbnd1  26164  pntpbnd2  26165  pntibndlem2  26169  pntlemg  26176  pntlemr  26180  pntlemj  26181  pntlemk  26184  ostth2lem1  26196  qabvle  26203  ostth2lem3  26213  ostth2lem4  26214  axlowdimlem16  26745  wwlksnredwwlkn  27675  wwlksnextproplem3  27692  wwlksext2clwwlk  27838  wwlksubclwwlk  27839  eupth2lems  28019  smcnlem  28476  minvecolem4  28659  pjhthlem1  29170  zltp1ne  32350  cvmliftlem7  32540  dnibndlem13  33831  knoppndvlem19  33871  knoppndvlem21  33873  icoreunrn  34642  relowlssretop  34646  ltflcei  34882  poimirlem1  34895  poimirlem2  34896  poimirlem4  34898  poimirlem6  34900  poimirlem7  34901  poimirlem8  34902  opnmbllem0  34930  mblfinlem1  34931  mblfinlem2  34932  mblfinlem4  34934  itg2addnclem2  34946  itg2addnclem3  34947  incsequz  35025  isbnd3  35064  rrntotbnd  35116  3cubeslem1  39288  3cubeslem2  39289  irrapxlem4  39429  pellexlem5  39437  pell14qrgapw  39480  pellfundgt1  39487  jm3.1lem2  39622  expdiophlem1  39625  zltlesub  41558  suplesup  41614  supxrunb3  41679  xrpnf  41769  fmul01lt1lem1  41872  limsupre3lem  42020  xlimxrre  42119  xlimpnfv  42126  ioodvbdlimc1lem1  42223  dvnxpaek  42234  dvnmul  42235  fourierdlem4  42403  fourierdlem11  42410  fourierdlem25  42424  fourierdlem50  42448  fourierdlem64  42462  fourierdlem65  42463  fourierdlem77  42475  fourierdlem79  42477  iinhoiicclem  42962  smfresal  43070  fmtno4prmfac  43741  lighneallem4a  43780  evenltle  43889  perfectALTVlem2  43894  logbpw2m1  44634