Theorem peano2re 8208

Description: A theorem for reals analogous the second Peano postulate peano2 4643. (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 8071	. 2 |- 1 e. RR
2		readdcl 8051	. 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 2176  (class class class)co 5944   RRcr 7924   1c1 7926   + caddc 7928

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

This theorem is referenced by:  lep1  8918  letrp1  8921  p1le  8922  ledivp1  8976  nnssre  9040  nn1suc  9055  nnge1  9059  div4p1lem1div2  9291  zltp1le  9427  suprzclex  9471  zeo  9478  peano2uz2  9480  uzind  9484  btwnapz  9503  numltc  9529  ge0p1rp  9807  fznatpl1  10198  ubmelm1fzo  10355  infssuzex  10376  qbtwnxr  10400  flhalf  10445  fldiv4p1lem1div2  10448  seq3split  10633  seq3f1olemqsumk  10657  seqf1oglem1  10664  seqf1oglem2  10665  bernneq3  10807  facwordi  10885  faclbnd  10886  expcnvap0  11813  cvgratnnlemfm  11840  cvgratnnlemrate  11841  cvgratz  11843  mertenslemi1  11846  fprodntrivap  11895  divalglemnqt  12231  nonsq  12529  eulerthlema  12552  pcfac  12673  1arith  12690  ennnfonelemkh  12783  tgioo  15026  suplociccreex  15096  hoverb  15120  reeff1olem  15243  lgsvalmod  15496  gausslemma2dlem3  15540  lgsquadlem2  15555