Theorem peano2re 8293

Description: A theorem for reals analogous the second Peano postulate peano2 4687. (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 8156	. 2 |- 1 e. RR
2		readdcl 8136	. 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 2200  (class class class)co 6007   RRcr 8009   1c1 8011   + caddc 8013

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

This theorem is referenced by:  lep1  9003  letrp1  9006  p1le  9007  ledivp1  9061  nnssre  9125  nn1suc  9140  nnge1  9144  div4p1lem1div2  9376  zltp1le  9512  suprzclex  9556  zeo  9563  peano2uz2  9565  uzind  9569  btwnapz  9588  numltc  9614  ge0p1rp  9893  fznatpl1  10284  ubmelm1fzo  10444  infssuzex  10465  qbtwnxr  10489  flhalf  10534  fldiv4p1lem1div2  10537  seq3split  10722  seq3f1olemqsumk  10746  seqf1oglem1  10753  seqf1oglem2  10754  bernneq3  10896  facwordi  10974  faclbnd  10975  expcnvap0  12029  cvgratnnlemfm  12056  cvgratnnlemrate  12057  cvgratz  12059  mertenslemi1  12062  fprodntrivap  12111  divalglemnqt  12447  nonsq  12745  eulerthlema  12768  pcfac  12889  1arith  12906  ennnfonelemkh  12999  tgioo  15244  suplociccreex  15314  hoverb  15338  reeff1olem  15461  lgsvalmod  15714  gausslemma2dlem3  15758  lgsquadlem2  15773