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

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

Proof of Theorem peano2re
StepHypRef Expression
1 1re 7026 . 2 1 ∈ ℝ
2 readdcl 7007 . 2 ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐴 + 1) ∈ ℝ)
31, 2mpan2 401 1 (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1393  (class class class)co 5512  cr 6888  1c1 6890   + caddc 6892
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101  ax-1re 6978  ax-addrcl 6981
This theorem is referenced by:  lep1  7811  letrp1  7814  p1le  7815  ledivp1  7869  nnssre  7918  nn1suc  7933  nnge1  7937  div4p1lem1div2  8177  zltp1le  8298  zeo  8343  peano2uz2  8345  uzind  8349  numltc  8387  ge0p1rp  8614  fznatpl1  8938  ubmelm1fzo  9082  flhalf  9144  fldiv4p1lem1div2  9147  bernneq3  9371
  Copyright terms: Public domain W3C validator