Theorem peano2re 8243

Description: A theorem for reals analogous the second Peano postulate peano2 4661. (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 8106	. 2 |- 1 e. RR
2		readdcl 8086	. 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 2178  (class class class)co 5967   RRcr 7959   1c1 7961   + caddc 7963

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

This theorem is referenced by:  lep1  8953  letrp1  8956  p1le  8957  ledivp1  9011  nnssre  9075  nn1suc  9090  nnge1  9094  div4p1lem1div2  9326  zltp1le  9462  suprzclex  9506  zeo  9513  peano2uz2  9515  uzind  9519  btwnapz  9538  numltc  9564  ge0p1rp  9842  fznatpl1  10233  ubmelm1fzo  10392  infssuzex  10413  qbtwnxr  10437  flhalf  10482  fldiv4p1lem1div2  10485  seq3split  10670  seq3f1olemqsumk  10694  seqf1oglem1  10701  seqf1oglem2  10702  bernneq3  10844  facwordi  10922  faclbnd  10923  expcnvap0  11928  cvgratnnlemfm  11955  cvgratnnlemrate  11956  cvgratz  11958  mertenslemi1  11961  fprodntrivap  12010  divalglemnqt  12346  nonsq  12644  eulerthlema  12667  pcfac  12788  1arith  12805  ennnfonelemkh  12898  tgioo  15141  suplociccreex  15211  hoverb  15235  reeff1olem  15358  lgsvalmod  15611  gausslemma2dlem3  15655  lgsquadlem2  15670