Metamath Proof Explorer
Theorem 0cn
Description: Zero is a complex number. See also 0cnALT . (Contributed by NM, 19Feb2005)


Ref 
Expression 

Assertion 
0cn 
⊢ 0 ∈ ℂ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

axi2m1 
⊢ ( ( i · i ) + 1 ) = 0 
2 

axicn 
⊢ i ∈ ℂ 
3 

mulcl 
⊢ ( ( i ∈ ℂ ∧ i ∈ ℂ ) → ( i · i ) ∈ ℂ ) 
4 
2 2 3

mp2an 
⊢ ( i · i ) ∈ ℂ 
5 

ax1cn 
⊢ 1 ∈ ℂ 
6 

addcl 
⊢ ( ( ( i · i ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( i · i ) + 1 ) ∈ ℂ ) 
7 
4 5 6

mp2an 
⊢ ( ( i · i ) + 1 ) ∈ ℂ 
8 
1 7

eqeltrri 
⊢ 0 ∈ ℂ 