This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem peano2rem

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

Ref Expression
Assertion peano2rem ⊢ N ∈ ℝ → N − 1 ∈ ℝ

Proof

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