Theorem peano2re 7891

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

Syntax hints:   -> wi 4   e. wcel 1480  (class class class)co 5767   RRcr 7612   1c1 7614   + caddc 7616

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107  ax-1re 7707  ax-addrcl 7710

This theorem is referenced by:  lep1  8596  letrp1  8599  p1le  8600  ledivp1  8654  nnssre  8717  nn1suc  8732  nnge1  8736  div4p1lem1div2  8966  zltp1le  9101  suprzclex  9142  zeo  9149  peano2uz2  9151  uzind  9155  btwnapz  9174  numltc  9200  ge0p1rp  9466  fznatpl1  9849  ubmelm1fzo  9996  qbtwnxr  10028  flhalf  10068  fldiv4p1lem1div2  10071  seq3split  10245  seq3f1olemqsumk  10265  bernneq3  10407  facwordi  10479  faclbnd  10480  expcnvap0  11264  cvgratnnlemfm  11291  cvgratnnlemrate  11292  cvgratz  11294  mertenslemi1  11297  divalglemnqt  11606  infssuzex  11631  nonsq  11874  ennnfonelemkh  11914  tgioo  12704  suplociccreex  12760