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

Step	Hyp	Ref	Expression
1		1re 6824	. 2 ⊢ 1 ∈ ℝ
2		readdcl 6805	. 2 ⊢ ((A ∈ ℝ ∧ 1 ∈ ℝ) → (A + 1) ∈ ℝ)
3	1, 2	mpan2 401	1 ⊢ (A ∈ ℝ → (A + 1) ∈ ℝ)

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