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

Metamath Proof Explorer

Theorem peano2cnm

Description: "Reverse" second Peano postulate analogue for complex numbers: A complex number minus 1 is a complex number. (Contributed by Alexander van der Vekens, 18-Mar-2018)

Ref Expression
Assertion peano2cnm ⊢ N ∈ ℂ → N − 1 ∈ ℂ

Proof

Step Hyp Ref Expression
1 ax-1cn ⊢ 1 ∈ ℂ
2 subcl ⊢ N ∈ ℂ ∧ 1 ∈ ℂ → N − 1 ∈ ℂ
3 1 2 mpan2 ⊢ N ∈ ℂ → N − 1 ∈ ℂ