Theorem peano2re 7815

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

Syntax hints:   -> wi 4   e. wcel 1461  (class class class)co 5726   RRcr 7540   1c1 7542   + caddc 7544

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

This theorem is referenced by:  lep1  8507  letrp1  8510  p1le  8511  ledivp1  8565  nnssre  8628  nn1suc  8643  nnge1  8647  div4p1lem1div2  8871  zltp1le  9006  suprzclex  9047  zeo  9054  peano2uz2  9056  uzind  9060  btwnapz  9079  numltc  9105  ge0p1rp  9368  fznatpl1  9743  ubmelm1fzo  9890  qbtwnxr  9922  flhalf  9962  fldiv4p1lem1div2  9965  seq3split  10139  seq3f1olemqsumk  10159  bernneq3  10301  facwordi  10373  faclbnd  10374  expcnvap0  11157  cvgratnnlemfm  11184  cvgratnnlemrate  11185  cvgratz  11187  mertenslemi1  11190  divalglemnqt  11459  infssuzex  11484  nonsq  11724  ennnfonelemkh  11764  tgioo  12526