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

Metamath Proof Explorer

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 ∈ ℂ → A + 1 ∈ ℂ

Proof

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