Theorem peano2re 8315

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

Assertion

Ref	Expression
peano2re	|- ( A e. RR -> ( A + 1 ) e. RR )

Proof of Theorem peano2re

Step	Hyp	Ref	Expression
1		1re 8178	. 2 |- 1 e. RR
2		readdcl 8158	. 2 |- ( ( A e. RR /\ 1 e. RR ) -> ( A + 1 ) e. RR )
3	1, 2	mpan2 425	1 |- ( A e. RR -> ( A + 1 ) e. RR )

Syntax hints:   -> wi 4   e. wcel 2202  (class class class)co 6018   RRcr 8031   1c1 8033   + caddc 8035

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-1re 8126  ax-addrcl 8129

This theorem is referenced by:  lep1  9025  letrp1  9028  p1le  9029  ledivp1  9083  nnssre  9147  nn1suc  9162  nnge1  9166  div4p1lem1div2  9398  zltp1le  9534  suprzclex  9578  zeo  9585  peano2uz2  9587  uzind  9591  btwnapz  9610  numltc  9636  ge0p1rp  9920  fznatpl1  10311  ubmelm1fzo  10472  infssuzex  10494  qbtwnxr  10518  flhalf  10563  fldiv4p1lem1div2  10566  seq3split  10751  seq3f1olemqsumk  10775  seqf1oglem1  10782  seqf1oglem2  10783  bernneq3  10925  facwordi  11003  faclbnd  11004  expcnvap0  12081  cvgratnnlemfm  12108  cvgratnnlemrate  12109  cvgratz  12111  mertenslemi1  12114  fprodntrivap  12163  divalglemnqt  12499  nonsq  12797  eulerthlema  12820  pcfac  12941  1arith  12958  ennnfonelemkh  13051  tgioo  15297  suplociccreex  15367  hoverb  15391  reeff1olem  15514  lgsvalmod  15767  gausslemma2dlem3  15811  lgsquadlem2  15826  eupth2lemsfi  16348