Theorem peano2re 8374

Description: A theorem for reals analogous the second Peano postulate peano2 4699. (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 8238	. 2 |- 1 e. RR
2		readdcl 8218	. 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 2202  (class class class)co 6028   RRcr 8091   1c1 8093   + caddc 8095

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

This theorem is referenced by:  lep1  9084  letrp1  9087  p1le  9088  ledivp1  9142  nnssre  9206  nn1suc  9221  nnge1  9225  div4p1lem1div2  9457  zltp1le  9595  suprzclex  9639  zeo  9646  peano2uz2  9648  uzind  9652  btwnapz  9671  numltc  9697  ge0p1rp  9981  fznatpl1  10373  ubmelm1fzo  10534  infssuzex  10556  qbtwnxr  10580  flhalf  10625  fldiv4p1lem1div2  10628  seq3split  10813  seq3f1olemqsumk  10837  seqf1oglem1  10844  seqf1oglem2  10845  bernneq3  10987  facwordi  11065  faclbnd  11066  expcnvap0  12143  cvgratnnlemfm  12170  cvgratnnlemrate  12171  cvgratz  12173  mertenslemi1  12176  fprodntrivap  12225  divalglemnqt  12561  nonsq  12859  eulerthlema  12882  pcfac  13003  1arith  13020  ennnfonelemkh  13113  tgioo  15365  suplociccreex  15435  hoverb  15459  reeff1olem  15582  lgsvalmod  15838  gausslemma2dlem3  15882  lgsquadlem2  15897  eupth2lemsfi  16419