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

Theorem peano2re 7311
Description: A theorem for reals analogous the second Peano postulate peano2 4344. (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 7180 . 2  |-  1  e.  RR
2 readdcl 7161 . 2  |-  ( ( A  e.  RR  /\  1  e.  RR )  ->  ( A  +  1 )  e.  RR )
31, 2mpan2 416 1  |-  ( A  e.  RR  ->  ( A  +  1 )  e.  RR )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1434  (class class class)co 5543   RRcr 7042   1c1 7044    + caddc 7046
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106  ax-1re 7132  ax-addrcl 7135
This theorem is referenced by:  lep1  7990  letrp1  7993  p1le  7994  ledivp1  8048  nnssre  8110  nn1suc  8125  nnge1  8129  div4p1lem1div2  8351  zltp1le  8486  suprzclex  8526  zeo  8533  peano2uz2  8535  uzind  8539  numltc  8583  ge0p1rp  8846  fznatpl1  9169  ubmelm1fzo  9312  qbtwnxr  9344  flhalf  9384  fldiv4p1lem1div2  9387  bernneq3  9692  facwordi  9764  faclbnd  9765  divalglemnqt  10464  infssuzex  10489
  Copyright terms: Public domain W3C validator