Theorem peano2rem

Description: "Reverse" second Peano postulate analogue for reals. (Contributed by NM, 6-Feb-2007)

	Ref	Expression
Assertion	peano2rem	$$⊢N\in ℝ\to N-1\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		1re	$$⊢1\in ℝ$$
2		resubcl	$$⊢\left(N\in ℝ\wedge 1\in ℝ\right)\to N-1\in ℝ$$
3	1 2	mpan2	$$⊢N\in ℝ\to N-1\in ℝ$$