Theorem peano2re 8167

Description: A theorem for reals analogous the second Peano postulate peano2 4632. (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 8030	. 2 |- 1 e. RR
2		readdcl 8010	. 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 2167  (class class class)co 5925   RRcr 7883   1c1 7885   + caddc 7887

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

This theorem is referenced by:  lep1  8877  letrp1  8880  p1le  8881  ledivp1  8935  nnssre  8999  nn1suc  9014  nnge1  9018  div4p1lem1div2  9250  zltp1le  9385  suprzclex  9429  zeo  9436  peano2uz2  9438  uzind  9442  btwnapz  9461  numltc  9487  ge0p1rp  9765  fznatpl1  10156  ubmelm1fzo  10307  infssuzex  10328  qbtwnxr  10352  flhalf  10397  fldiv4p1lem1div2  10400  seq3split  10585  seq3f1olemqsumk  10609  seqf1oglem1  10616  seqf1oglem2  10617  bernneq3  10759  facwordi  10837  faclbnd  10838  expcnvap0  11672  cvgratnnlemfm  11699  cvgratnnlemrate  11700  cvgratz  11702  mertenslemi1  11705  fprodntrivap  11754  divalglemnqt  12090  nonsq  12388  eulerthlema  12411  pcfac  12532  1arith  12549  ennnfonelemkh  12642  tgioo  14837  suplociccreex  14907  hoverb  14931  reeff1olem  15054  lgsvalmod  15307  gausslemma2dlem3  15351  lgsquadlem2  15366