Theorem peano2re

Description: A theorem for reals analogous the second Peano postulate peano2nn . (Contributed by NM, 5-Jul-2005)

	Ref	Expression
Assertion	peano2re	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 + 1 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		1re	⊢ 1 ∈ ℝ
2		readdcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 𝐴 + 1 ) ∈ ℝ )
3	1 2	mpan2	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 + 1 ) ∈ ℝ )