Theorem peano2re 8011

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

Syntax hints:   -> wi 4   e. wcel 2128  (class class class)co 5824   RRcr 7731   1c1 7733   + caddc 7735

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107  ax-1re 7826  ax-addrcl 7829

This theorem is referenced by:  lep1  8716  letrp1  8719  p1le  8720  ledivp1  8774  nnssre  8837  nn1suc  8852  nnge1  8856  div4p1lem1div2  9086  zltp1le  9221  suprzclex  9262  zeo  9269  peano2uz2  9271  uzind  9275  btwnapz  9294  numltc  9320  ge0p1rp  9592  fznatpl1  9978  ubmelm1fzo  10125  qbtwnxr  10157  flhalf  10201  fldiv4p1lem1div2  10204  seq3split  10378  seq3f1olemqsumk  10398  bernneq3  10540  facwordi  10614  faclbnd  10615  expcnvap0  11399  cvgratnnlemfm  11426  cvgratnnlemrate  11427  cvgratz  11429  mertenslemi1  11432  fprodntrivap  11481  divalglemnqt  11810  infssuzex  11835  nonsq  12081  eulerthlema  12104  ennnfonelemkh  12141  tgioo  12946  suplociccreex  13002  reeff1olem  13092