Theorem peano2re 8087

Description: A theorem for reals analogous the second Peano postulate peano2 4592. (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 7951	. 2 |- 1 e. RR
2		readdcl 7932	. 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 2148  (class class class)co 5870   RRcr 7805   1c1 7807   + caddc 7809

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

This theorem is referenced by:  lep1  8796  letrp1  8799  p1le  8800  ledivp1  8854  nnssre  8917  nn1suc  8932  nnge1  8936  div4p1lem1div2  9166  zltp1le  9301  suprzclex  9345  zeo  9352  peano2uz2  9354  uzind  9358  btwnapz  9377  numltc  9403  ge0p1rp  9679  fznatpl1  10069  ubmelm1fzo  10219  qbtwnxr  10251  flhalf  10295  fldiv4p1lem1div2  10298  seq3split  10472  seq3f1olemqsumk  10492  bernneq3  10635  facwordi  10711  faclbnd  10712  expcnvap0  11501  cvgratnnlemfm  11528  cvgratnnlemrate  11529  cvgratz  11531  mertenslemi1  11534  fprodntrivap  11583  divalglemnqt  11915  infssuzex  11940  nonsq  12197  eulerthlema  12220  pcfac  12338  1arith  12355  ennnfonelemkh  12403  tgioo  13828  suplociccreex  13884  reeff1olem  13974  lgsvalmod  14202