Theorem peano2re 8411

Description: A theorem for reals analogous the second Peano postulate peano2 4719. (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 8275	. 2 |- 1 e. RR
2		readdcl 8255	. 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 2205  (class class class)co 6052   RRcr 8128   1c1 8130   + caddc 8132

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

This theorem is referenced by:  lep1  9121  letrp1  9124  p1le  9125  ledivp1  9179  nnssre  9243  nn1suc  9258  nnge1  9262  div4p1lem1div2  9494  zltp1le  9634  suprzclex  9679  zeo  9686  peano2uz2  9688  uzind  9692  btwnapz  9711  numltc  9737  ge0p1rp  10021  fznatpl1  10414  ubmelm1fzo  10575  infssuzex  10597  qbtwnxr  10621  flhalf  10666  fldiv4p1lem1div2  10669  seq3split  10854  seq3f1olemqsumk  10878  seqf1oglem1  10885  seqf1oglem2  10886  bernneq3  11028  facwordi  11106  faclbnd  11107  expcnvap0  12192  cvgratnnlemfm  12219  cvgratnnlemrate  12220  cvgratz  12222  mertenslemi1  12225  fprodntrivap  12274  divalglemnqt  12610  nonsq  12908  eulerthlema  12931  pcfac  13052  1arith  13069  ennnfonelemkh  13180  tgioo  15436  suplociccreex  15506  hoverb  15530  reeff1olem  15653  lgsvalmod  15909  gausslemma2dlem3  15953  lgsquadlem2  15968  eupth2lemsfi  16490