Theorem peano2rem

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

	Ref	Expression
Assertion	peano2rem	⊢ ( 𝑁 ∈ ℝ → ( 𝑁 − 1 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		1re	⊢ 1 ∈ ℝ
2		resubcl	⊢ ( ( 𝑁 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 𝑁 − 1 ) ∈ ℝ )
3	1 2	mpan2	⊢ ( 𝑁 ∈ ℝ → ( 𝑁 − 1 ) ∈ ℝ )