Theorem peano2re 7244

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

Syntax hints:   -> wi 4   e. wcel 1433  (class class class)co 5532   RRcr 6980   1c1 6982   + caddc 6984

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106  ax-1re 7070  ax-addrcl 7073

This theorem is referenced by:  lep1  7923  letrp1  7926  p1le  7927  ledivp1  7981  nnssre  8043  nn1suc  8058  nnge1  8062  div4p1lem1div2  8284  zltp1le  8405  suprzclex  8445  zeo  8452  peano2uz2  8454  uzind  8458  numltc  8502  ge0p1rp  8765  fznatpl1  9093  ubmelm1fzo  9235  qbtwnxr  9266  flhalf  9304  fldiv4p1lem1div2  9307  bernneq3  9595  facwordi  9667  faclbnd  9668  divalglemnqt  10320  infssuzex  10345