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 ( 𝑁 ∈ ℂ → ( 𝑁 − 1 ) ∈ ℂ )

Proof

Step Hyp Ref Expression
1 ax-1cn 1 ∈ ℂ
2 subcl ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝑁 − 1 ) ∈ ℂ )
3 1 2 mpan2 ( 𝑁 ∈ ℂ → ( 𝑁 − 1 ) ∈ ℂ )