ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  peano2re Unicode version

Theorem peano2re 8095
Description: A theorem for reals analogous the second Peano postulate peano2 4596. (Contributed by NM, 5-Jul-2005.)
Assertion
Ref Expression
peano2re  |-  ( A  e.  RR  ->  ( A  +  1 )  e.  RR )

Proof of Theorem peano2re
StepHypRef Expression
1 1re 7958 . 2  |-  1  e.  RR
2 readdcl 7939 . 2  |-  ( ( A  e.  RR  /\  1  e.  RR )  ->  ( A  +  1 )  e.  RR )
31, 2mpan2 425 1  |-  ( A  e.  RR  ->  ( A  +  1 )  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 2148  (class class class)co 5877   RRcr 7812   1c1 7814    + caddc 7816
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108  ax-1re 7907  ax-addrcl 7910
This theorem is referenced by:  lep1  8804  letrp1  8807  p1le  8808  ledivp1  8862  nnssre  8925  nn1suc  8940  nnge1  8944  div4p1lem1div2  9174  zltp1le  9309  suprzclex  9353  zeo  9360  peano2uz2  9362  uzind  9366  btwnapz  9385  numltc  9411  ge0p1rp  9687  fznatpl1  10078  ubmelm1fzo  10228  qbtwnxr  10260  flhalf  10304  fldiv4p1lem1div2  10307  seq3split  10481  seq3f1olemqsumk  10501  bernneq3  10645  facwordi  10722  faclbnd  10723  expcnvap0  11512  cvgratnnlemfm  11539  cvgratnnlemrate  11540  cvgratz  11542  mertenslemi1  11545  fprodntrivap  11594  divalglemnqt  11927  infssuzex  11952  nonsq  12209  eulerthlema  12232  pcfac  12350  1arith  12367  ennnfonelemkh  12415  tgioo  14085  suplociccreex  14141  reeff1olem  14231  lgsvalmod  14459
  Copyright terms: Public domain W3C validator