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

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

Proof of Theorem peano2re
StepHypRef Expression
1 1re 7816 . 2 1 ∈ ℝ
2 readdcl 7797 . 2 ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐴 + 1) ∈ ℝ)
31, 2mpan2 422 1 (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∈ wcel 1481  (class class class)co 5785  ℝcr 7670  1c1 7672   + caddc 7674 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107  ax-1re 7765  ax-addrcl 7768 This theorem is referenced by:  lep1  8654  letrp1  8657  p1le  8658  ledivp1  8712  nnssre  8775  nn1suc  8790  nnge1  8794  div4p1lem1div2  9024  zltp1le  9159  suprzclex  9200  zeo  9207  peano2uz2  9209  uzind  9213  btwnapz  9232  numltc  9258  ge0p1rp  9529  fznatpl1  9914  ubmelm1fzo  10061  qbtwnxr  10093  flhalf  10133  fldiv4p1lem1div2  10136  seq3split  10310  seq3f1olemqsumk  10330  bernneq3  10472  facwordi  10545  faclbnd  10546  expcnvap0  11330  cvgratnnlemfm  11357  cvgratnnlemrate  11358  cvgratz  11360  mertenslemi1  11363  fprodntrivap  11412  divalglemnqt  11687  infssuzex  11712  nonsq  11955  ennnfonelemkh  11995  tgioo  12788  suplociccreex  12844  reeff1olem  12934
 Copyright terms: Public domain W3C validator