Theorem peano2re 8469

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

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209  (class class class)co 6088   RRcr 8184   1c1 8186   + caddc 8188

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-1re 8279  ax-addrcl 8282

This theorem is used by:  lep1  9183  letrp1  9186  p1le  9187  ledivp1  9241  nnssre  9317  nn1suc  9332  nnge1  9336  div4p1lem1div2  9570  zltp1le  9710  suprzclex  9755  zeo  9762  peano2uz2  9764  uzind  9768  btwnapz  9787  numltc  9818  ge0p1rp  10103  fznatpl1  10500  ubmelm1fzo  10661  infssuzex  10683  qbtwnxr  10709  flaplt  10739  flhalf  10758  fldiv4p1lem1div2  10761  seq3split  10946  seq3f1olemqsumk  10970  seqf1oglem1  10977  seqf1oglem2  10978  bernneq3  11121  facwordi  11200  faclbnd  11201  expcnvap0  12294  cvgratnnlemfm  12321  cvgratnnlemrate  12322  cvgratz  12324  mertenslemi1  12327  fprodntrivap  12376  divalglemnqt  12712  nonsq  13012  eulerthlema  13037  pcfac  13158  1arith  13175  ennnfonelemkh  13361  tgioo  15780  suplociccreex  15850  hoverb  15874  reeff1olem  15997  ppiqltx  16281  ppiqub  16293  bcmono  16304  lgsvalmod  16343  gausslemma2dlem3  16387  lgsquadlem2  16402  eupth2lemsfi  16924