Theorem peano2re 11493

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

Assertion

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

Proof of Theorem peano2re

Step	Hyp	Ref	Expression
1		1re 11318	. 2 ⊢ 1 ∈ ℝ
2		readdcl 11293	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐴 + 1) ∈ ℝ)
3	1, 2	mpan2 704	1 ⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  (class class class)co 7427  ℝcr 11209  1c1 11211   + caddc 11213

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-1cn 11268  ax-icn 11269  ax-addcl 11270  ax-addrcl 11271  ax-mulcl 11272  ax-mulrcl 11273  ax-i2m1 11278  ax-1ne0 11279  ax-rrecex 11282  ax-cnre 11283

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3416  df-v 3455  df-ss 3900  df-dif 4049  df-un 4153  df-nul 4281  df-if 4485  df-sn 4588  df-pr 4590  df-op 4838  df-uni 4870  df-br 5106  df-iota 6500  df-fv 6554  df-ov 7430

This theorem is used by:  lep1  12168  letrp1  12171  p1le  12172  ledivp1  12229  sup2  12283  nnssre  12349  nnge1  12376  div4p1lem1div2  12611  zltp1le  12756  suprzcl  12789  zeo  12795  peano2uz2  12797  uzind  12801  numltc  12855  uzwo  13048  ge0p1rp  13163  qbtwnxr  13340  xrsupsslem  13447  supxrunb1  13459  fznatpl1  13722  fzp1disj  13727  fzneuz  13752  fzp1nel  13755  ubmelm1fzo  13908  fllep1  13951  flflp1  13957  flhalf  13980  ltdifltdiv  13984  fldiv4p1lem1div2  13985  dfceil2  13989  ceim1l  13997  uzsup  14013  modltm1p1mod  14076  addmodlteq  14099  fsequb  14128  seqf1olem1  14194  seqf1olem2  14195  bernneq3  14385  expnbnd  14386  expmulnbnd  14389  discr1  14393  discr  14394  facwordi  14443  faclbnd  14444  hashfun  14592  seqcoll2  14620  rexuzre  15532  caubnd  15538  rlim2lt  15676  lo1bddrp  15704  rlimo1  15796  o1rlimmul  15798  o1fsum  15992  harmonic  16040  expcnv  16045  geomulcvg  16057  mertenslem1  16065  bpoly4  16237  nonsq  16947  eulerthlem2  16971  pcprendvds  17030  pcmpt  17082  pcfac  17089  vdwlem6  17176  vdwlem11  17181  chnccat  18812  chfacffsupp  23186  chfacfscmul0  23188  chfacfpmmul0  23192  tgioo  25127  zcld  25145  iocopnst  25273  cnheibor  25288  bndth  25291  cncmet  25655  pjthlem1  25770  ovolicc2lem3  25852  ovolicopnf  25857  ioorcl2  25905  dyadf  25924  dyadovol  25926  dyadss  25927  dyaddisjlem  25928  dyadmaxlem  25930  opnmbllem  25934  volsup2  25938  vitalilem2  25942  itg2const2  26074  itg2cnlem1  26094  dvfsumle  26353  dvfsumabs  26355  dvfsumlem1  26358  dvfsumlem3  26360  dvfsumrlim  26363  fta1glem2  26499  fta1lem  26640  aalioulem3  26673  ulmbdd  26737  itgulm  26747  psercnlem1  26764  abelthlem2  26771  abelthlem7  26777  reeff1olem  26785  logtayl  27000  loglesqrt  27101  atanlogsublem  27255  leibpi  27282  efrlim  27309  harmonicubnd  27349  fsumharmonic  27351  ftalem5  27416  basellem2  27421  basellem3  27422  chtnprm  27493  chpp1  27494  ppip1le  27500  ppiub  27543  logfaclbnd  27561  logfacrlim  27563  perfectlem2  27569  bcmono  27616  lgsvalmod  27655  gausslemma2dlem3  27707  lgseisen  27718  lgsquadlem1  27719  lgsquadlem2  27720  chebbnd1lem2  27809  chtppilimlem1  27812  rplogsumlem2  27824  dchrisumlema  27827  dchrisumlem1  27828  dchrisumlem3  27830  dchrisum0lem1  27855  chpdifbndlem1  27892  logdivbnd  27895  pntrmax  27903  pntrsumo1  27904  pntpbnd1a  27924  pntpbnd1  27925  pntpbnd2  27926  pntibndlem2  27930  pntlemg  27937  pntlemr  27941  pntlemj  27942  pntlemk  27945  ostth2lem1  27957  qabvle  27964  ostth2lem3  27974  ostth2lem4  27975  axlowdimlem16  29547  wwlksnredwwlkn  30496  wwlksnextproplem3  30512  wwlksext2clwwlk  30660  wwlksubclwwlk  30661  eupth2lems  30851  smcnlem  31311  minvecolem4  31494  pjhthlem1  32005  zltp1ne  36011  cvmliftlem7  36177  dnibndlem13  37483  knoppndvlem19  37523  knoppndvlem21  37525  icoreunrn  38422  relowlssretop  38426  ltflcei  38671  poimirlem1  38679  poimirlem2  38680  poimirlem4  38682  poimirlem6  38684  poimirlem7  38685  poimirlem8  38686  opnmbllem0  38714  mblfinlem1  38715  mblfinlem2  38716  mblfinlem4  38718  itg2addnclem2  38730  itg2addnclem3  38731  incsequz  38822  isbnd3  38858  rrntotbnd  38910  sn-sup2  43695  3cubeslem1  43834  3cubeslem2  43835  irrapxlem4  43972  pellexlem5  43980  pell14qrgapw  44023  pellfundgt1  44030  jm3.1lem2  44165  expdiophlem1  44168  fzuntgd  44599  zltlesub  46440  suplesup  46490  supxrunb3  46549  xrpnf  46634  fmul01lt1lem1  46735  limsupre3lem  46881  xlimxrre  46980  xlimpnfv  46987  ioodvbdlimc1lem1  47080  dvnxpaek  47091  dvnmul  47092  fourierdlem4  47260  fourierdlem11  47267  fourierdlem25  47281  fourierdlem50  47305  fourierdlem64  47319  fourierdlem65  47320  fourierdlem77  47332  fourierdlem79  47334  iinhoiicclem  47822  smfresal  47937  fmtno4prmfac  48796  lighneallem4a  48832  evenltle  48954  perfectALTVlem2  48959  logbpw2m1  49818