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

Step	Hyp	Ref	Expression
1		1re 7026	. 2 ⊢ 1 ∈ ℝ
2		readdcl 7007	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ) → (𝐴 + 1) ∈ ℝ)
3	1, 2	mpan2 401	1 ⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈ ℝ)

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