Theorem peano2re

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

	Ref	Expression
Assertion	peano2re	$$⊢A\in ℝ\to A+1\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		1re	$$⊢1\in ℝ$$
2		readdcl	$$⊢\left(A\in ℝ\wedge 1\in ℝ\right)\to A+1\in ℝ$$
3	1 2	mpan2	$$⊢A\in ℝ\to A+1\in ℝ$$