Theorem peano2cn

Description: A theorem for complex numbers analogous the second Peano postulate peano2nn . (Contributed by NM, 17-Aug-2005)

	Ref	Expression
Assertion	peano2cn	$$⊢A\in ℂ\to A+1\in ℂ$$

Proof

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