Theorem peano2cn

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

	Ref	Expression
Assertion	peano2cn	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 + 1 ) ∈ ℂ )

Proof

Step	Hyp	Ref	Expression
1		ax-1cn	⊢ 1 ∈ ℂ
2		addcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝐴 + 1 ) ∈ ℂ )
3	1 2	mpan2	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 + 1 ) ∈ ℂ )