Metamath Proof Explorer


Theorem 0cn

Description: Zero is a complex number. See also 0cnALT . (Contributed by NM, 19-Feb-2005)

Ref Expression
Assertion 0cn 0 ∈ ℂ

Proof

Step Hyp Ref Expression
1 ax-i2m1 ( ( i · i ) + 1 ) = 0
2 ax-icn i ∈ ℂ
3 mulcl ( ( i ∈ ℂ ∧ i ∈ ℂ ) → ( i · i ) ∈ ℂ )
4 2 2 3 mp2an ( i · i ) ∈ ℂ
5 ax-1cn 1 ∈ ℂ
6 addcl ( ( ( i · i ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( i · i ) + 1 ) ∈ ℂ )
7 4 5 6 mp2an ( ( i · i ) + 1 ) ∈ ℂ
8 1 7 eqeltrri 0 ∈ ℂ