Theorem peano2re 11347

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

Assertion

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

Proof of Theorem peano2re

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

Syntax hints:   → wi 4   ∈ wcel 2109  (class class class)co 7387  ℝcr 11067  1c1 11069   + caddc 11071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-i2m1 11136  ax-1ne0 11137  ax-rrecex 11140  ax-cnre 11141

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390

This theorem is referenced by:  lep1  12023  letrp1  12026  p1le  12027  ledivp1  12085  sup2  12139  nnssre  12190  nnge1  12214  div4p1lem1div2  12437  zltp1le  12583  suprzcl  12614  zeo  12620  peano2uz2  12622  uzind  12626  numltc  12675  uzwo  12870  ge0p1rp  12984  qbtwnxr  13160  xrsupsslem  13267  supxrunb1  13279  fznatpl1  13539  fzp1disj  13544  fzneuz  13569  fzp1nel  13572  ubmelm1fzo  13724  fllep1  13763  flflp1  13769  flhalf  13792  ltdifltdiv  13796  fldiv4p1lem1div2  13797  dfceil2  13801  ceim1l  13809  uzsup  13825  modltm1p1mod  13888  addmodlteq  13911  fsequb  13940  seqf1olem1  14006  seqf1olem2  14007  bernneq3  14196  expnbnd  14197  expmulnbnd  14200  discr1  14204  discr  14205  facwordi  14254  faclbnd  14255  hashfun  14402  seqcoll2  14430  rexuzre  15319  caubnd  15325  rlim2lt  15463  lo1bddrp  15491  rlimo1  15583  o1rlimmul  15585  o1fsum  15779  harmonic  15825  expcnv  15830  geomulcvg  15842  mertenslem1  15850  bpoly4  16025  nonsq  16729  eulerthlem2  16752  pcprendvds  16811  pcmpt  16863  pcfac  16870  vdwlem6  16957  vdwlem11  16962  chfacffsupp  22743  chfacfscmul0  22745  chfacfpmmul0  22749  tgioo  24684  zcld  24702  iocopnst  24837  cnheibor  24854  bndth  24857  cncmet  25222  pjthlem1  25337  ovolicc2lem3  25420  ovolicopnf  25425  ioorcl2  25473  dyadf  25492  dyadovol  25494  dyadss  25495  dyaddisjlem  25496  dyadmaxlem  25498  opnmbllem  25502  volsup2  25506  vitalilem2  25510  itg2const2  25642  itg2cnlem1  25662  dvfsumle  25926  dvfsumleOLD  25927  dvfsumabs  25929  dvfsumlem1  25932  dvfsumlem3  25935  dvfsumrlim  25938  fta1glem2  26074  fta1lem  26215  aalioulem3  26242  ulmbdd  26307  itgulm  26317  psercnlem1  26335  abelthlem2  26342  abelthlem7  26348  reeff1olem  26356  logtayl  26569  loglesqrt  26671  atanlogsublem  26825  leibpi  26852  efrlim  26879  efrlimOLD  26880  harmonicubnd  26920  fsumharmonic  26922  ftalem5  26987  basellem2  26992  basellem3  26993  chtnprm  27064  chpp1  27065  ppip1le  27071  ppiub  27115  logfaclbnd  27133  logfacrlim  27135  perfectlem2  27141  bcmono  27188  lgsvalmod  27227  gausslemma2dlem3  27279  lgseisen  27290  lgsquadlem1  27291  lgsquadlem2  27292  chebbnd1lem2  27381  chtppilimlem1  27384  rplogsumlem2  27396  dchrisumlema  27399  dchrisumlem1  27400  dchrisumlem3  27402  dchrisum0lem1  27427  chpdifbndlem1  27464  logdivbnd  27467  pntrmax  27475  pntrsumo1  27476  pntpbnd1a  27496  pntpbnd1  27497  pntpbnd2  27498  pntibndlem2  27502  pntlemg  27509  pntlemr  27513  pntlemj  27514  pntlemk  27517  ostth2lem1  27529  qabvle  27536  ostth2lem3  27546  ostth2lem4  27547  axlowdimlem16  28884  wwlksnredwwlkn  29825  wwlksnextproplem3  29841  wwlksext2clwwlk  29986  wwlksubclwwlk  29987  eupth2lems  30167  smcnlem  30626  minvecolem4  30809  pjhthlem1  31320  zltp1ne  35097  cvmliftlem7  35278  dnibndlem13  36478  knoppndvlem19  36518  knoppndvlem21  36520  icoreunrn  37347  relowlssretop  37351  ltflcei  37602  poimirlem1  37615  poimirlem2  37616  poimirlem4  37618  poimirlem6  37620  poimirlem7  37621  poimirlem8  37622  opnmbllem0  37650  mblfinlem1  37651  mblfinlem2  37652  mblfinlem4  37654  itg2addnclem2  37666  itg2addnclem3  37667  incsequz  37742  isbnd3  37778  rrntotbnd  37830  sn-sup2  42479  3cubeslem1  42672  3cubeslem2  42673  irrapxlem4  42813  pellexlem5  42821  pell14qrgapw  42864  pellfundgt1  42871  jm3.1lem2  43007  expdiophlem1  43010  fzuntgd  43447  zltlesub  45283  suplesup  45335  supxrunb3  45395  xrpnf  45481  fmul01lt1lem1  45582  limsupre3lem  45730  xlimxrre  45829  xlimpnfv  45836  ioodvbdlimc1lem1  45929  dvnxpaek  45940  dvnmul  45941  fourierdlem4  46109  fourierdlem11  46116  fourierdlem25  46130  fourierdlem50  46154  fourierdlem64  46168  fourierdlem65  46169  fourierdlem77  46181  fourierdlem79  46183  iinhoiicclem  46671  smfresal  46786  natglobalincr  46875  fmtno4prmfac  47573  lighneallem4a  47609  evenltle  47718  perfectALTVlem2  47723  logbpw2m1  48556