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

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

Proof of Theorem peano2re
StepHypRef Expression
1 1re 6824 . 2 1
2 readdcl 6805 . 2 ((A 1 ℝ) → (A + 1) ℝ)
31, 2mpan2 401 1 (A ℝ → (A + 1) ℝ)
Colors of variables: wff set class
Syntax hints:  wi 4   wcel 1390  (class class class)co 5455  cr 6710  1c1 6712   + caddc 6714
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101  ax-1re 6777  ax-addrcl 6780
This theorem is referenced by:  lep1  7592  letrp1  7595  p1le  7596  ledivp1  7650  nnssre  7699  nn1suc  7714  nnge1  7718  zltp1le  8074  zeo  8119  peano2uz2  8121  uzind  8125  numltc  8163  ge0p1rp  8389  fznatpl1  8708  ubmelm1fzo  8852  bernneq3  9024
  Copyright terms: Public domain W3C validator