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

Theorem peano2re 7210
Description: A theorem for reals analogous the second Peano postulate peano2 4346. (Contributed by NM, 5-Jul-2005.)
Assertion
Ref Expression
peano2re (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ)

Proof of Theorem peano2re
StepHypRef Expression
1 1re 7084 . 2 1 ∈ ℝ
2 readdcl 7065 . 2 ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐴 + 1) ∈ ℝ)
31, 2mpan2 409 1 (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1409  (class class class)co 5540  cr 6946  1c1 6948   + caddc 6950
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 105  ax-1re 7036  ax-addrcl 7039
This theorem is referenced by:  lep1  7886  letrp1  7889  p1le  7890  ledivp1  7944  nnssre  7994  nn1suc  8009  nnge1  8013  div4p1lem1div2  8235  zltp1le  8356  zeo  8402  peano2uz2  8404  uzind  8408  numltc  8452  ge0p1rp  8712  fznatpl1  9040  ubmelm1fzo  9184  qbtwnxr  9214  flhalf  9252  fldiv4p1lem1div2  9255  bernneq3  9539  facwordi  9608  faclbnd  9609  divalglemnqt  10232
  Copyright terms: Public domain W3C validator