Theorem peano2re 8409

Description: A theorem for reals analogous the second Peano postulate peano2 4717. (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 8273	. 2 |- 1 e. RR
2		readdcl 8253	. 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 2203  (class class class)co 6050   RRcr 8126   1c1 8128   + caddc 8130

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

This theorem is referenced by:  lep1  9119  letrp1  9122  p1le  9123  ledivp1  9177  nnssre  9241  nn1suc  9256  nnge1  9260  div4p1lem1div2  9492  zltp1le  9632  suprzclex  9676  zeo  9683  peano2uz2  9685  uzind  9689  btwnapz  9708  numltc  9734  ge0p1rp  10018  fznatpl1  10410  ubmelm1fzo  10571  infssuzex  10593  qbtwnxr  10617  flhalf  10662  fldiv4p1lem1div2  10665  seq3split  10850  seq3f1olemqsumk  10874  seqf1oglem1  10881  seqf1oglem2  10882  bernneq3  11024  facwordi  11102  faclbnd  11103  expcnvap0  12188  cvgratnnlemfm  12215  cvgratnnlemrate  12216  cvgratz  12218  mertenslemi1  12221  fprodntrivap  12270  divalglemnqt  12606  nonsq  12904  eulerthlema  12927  pcfac  13048  1arith  13065  ennnfonelemkh  13163  tgioo  15419  suplociccreex  15489  hoverb  15513  reeff1olem  15636  lgsvalmod  15892  gausslemma2dlem3  15936  lgsquadlem2  15951  eupth2lemsfi  16473