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\in ℂ\to N-1\in ℂ$$

Proof

Step	Hyp	Ref	Expression
1		ax-1cn	$$⊢1\in ℂ$$
2		subcl	$$⊢\left(N\in ℂ\wedge 1\in ℂ\right)\to N-1\in ℂ$$
3	1 2	mpan2	$$⊢N\in ℂ\to N-1\in ℂ$$