Theorem peano2re 8462

Description: A theorem for reals analogous the second Peano postulate peano2 4742. (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 8325	. 2 |- 1 e. RR
2		readdcl 8305	. 2 |- ( ( A e. RR /\ 1 e. RR ) -> ( A + 1 ) e. RR )
3	1, 2	mpan2 429	1 |- ( A e. RR -> ( A + 1 ) e. RR )

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209  (class class class)co 6085   RRcr 8178   1c1 8180   + caddc 8182

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-1re 8273  ax-addrcl 8276

This theorem is used by:  lep1  9175  letrp1  9178  p1le  9179  ledivp1  9233  nnssre  9308  nn1suc  9323  nnge1  9327  div4p1lem1div2  9559  zltp1le  9699  suprzclex  9744  zeo  9751  peano2uz2  9753  uzind  9757  btwnapz  9776  numltc  9802  ge0p1rp  10086  fznatpl1  10483  ubmelm1fzo  10644  infssuzex  10666  qbtwnxr  10692  flhalf  10737  fldiv4p1lem1div2  10740  seq3split  10925  seq3f1olemqsumk  10949  seqf1oglem1  10956  seqf1oglem2  10957  bernneq3  11100  facwordi  11178  faclbnd  11179  expcnvap0  12269  cvgratnnlemfm  12296  cvgratnnlemrate  12297  cvgratz  12299  mertenslemi1  12302  fprodntrivap  12351  divalglemnqt  12687  nonsq  12985  eulerthlema  13008  pcfac  13129  1arith  13146  ennnfonelemkh  13303  tgioo  15655  suplociccreex  15725  hoverb  15749  reeff1olem  15872  lgsvalmod  16138  gausslemma2dlem3  16182  lgsquadlem2  16197  eupth2lemsfi  16719