Theorem 0cn 6777

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

Assertion

Ref	Expression
0cn	⊢ 0 ∈ ℂ

Proof of Theorem 0cn

Step	Hyp	Ref	Expression
1		ax-i2m1 6748	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 6738	. . . 4 ⊢ i ∈ ℂ
3		mulcl 6766	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 402	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 6736	. . 3 ⊢ 1 ∈ ℂ
6		addcl 6764	. . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
7	4, 5, 6	mp2an 402	. 2 ⊢ ((i · i) + 1) ∈ ℂ
8	1, 7	eqeltrri 2108	1 ⊢ 0 ∈ ℂ

Syntax hints:   ∈ wcel 1390  (class class class)co 5455  ℂcc 6669  0cc0 6671  1c1 6672  ici 6673   + caddc 6674   · cmul 6676

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-17 1416  ax-ial 1424  ax-ext 2019  ax-1cn 6736  ax-icn 6738  ax-addcl 6739  ax-mulcl 6741  ax-i2m1 6748

This theorem depends on definitions:  df-bi 110  df-cleq 2030  df-clel 2033

This theorem is referenced by:  0cnd  6778  c0ex  6779  addid2  6909  00id  6911  cnegexlem2  6944  negcl  6968  subid  6986  subid1  6987  neg0  7013  negid  7014  negsub  7015  subneg  7016  negneg  7017  negeq0  7021  negsubdi  7023  renegcl  7028  mul02  7140  mul01  7142  mulneg1  7148  ixi  7327  negap0  7372  muleqadd  7391  divvalap  7395  div0ap  7421  recgt0  7557  0m0e0  7767  2muline0  7887  elznn0  7996  0exp0e1  8874  expeq0  8900  0exp  8904  sq0  8957  cjap0  9095  cjne0  9096