Theorem peano2re 8452

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

Syntax hints:   -> wi 4   e. wcel 2209  (class class class)co 6075   RRcr 8168   1c1 8170   + caddc 8172

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

This theorem is referenced by:  lep1  9165  letrp1  9168  p1le  9169  ledivp1  9223  nnssre  9287  nn1suc  9302  nnge1  9306  div4p1lem1div2  9538  zltp1le  9678  suprzclex  9723  zeo  9730  peano2uz2  9732  uzind  9736  btwnapz  9755  numltc  9781  ge0p1rp  10065  fznatpl1  10461  ubmelm1fzo  10622  infssuzex  10644  qbtwnxr  10670  flhalf  10715  fldiv4p1lem1div2  10718  seq3split  10903  seq3f1olemqsumk  10927  seqf1oglem1  10934  seqf1oglem2  10935  bernneq3  11078  facwordi  11156  faclbnd  11157  expcnvap0  12247  cvgratnnlemfm  12274  cvgratnnlemrate  12275  cvgratz  12277  mertenslemi1  12280  fprodntrivap  12329  divalglemnqt  12665  nonsq  12963  eulerthlema  12986  pcfac  13107  1arith  13124  ennnfonelemkh  13281  tgioo  15578  suplociccreex  15648  hoverb  15672  reeff1olem  15795  lgsvalmod  16052  gausslemma2dlem3  16096  lgsquadlem2  16111  eupth2lemsfi  16633