Theorem 0cn 7912

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 7879	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 7869	. . . 4 ⊢ i ∈ ℂ
3		mulcl 7901	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 424	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 7867	. . 3 ⊢ 1 ∈ ℂ
6		addcl 7899	. . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
7	4, 5, 6	mp2an 424	. 2 ⊢ ((i · i) + 1) ∈ ℂ
8	1, 7	eqeltrri 2244	1 ⊢ 0 ∈ ℂ

Syntax hints:   ∈ wcel 2141  (class class class)co 5853  ℂcc 7772  0cc0 7774  1c1 7775  ici 7776   + caddc 7777   · cmul 7779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-ext 2152  ax-1cn 7867  ax-icn 7869  ax-addcl 7870  ax-mulcl 7872  ax-i2m1 7879

This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-clel 2166

This theorem is referenced by:  0cnd  7913  c0ex  7914  addid2  8058  00id  8060  cnegexlem2  8095  negcl  8119  subid  8138  subid1  8139  neg0  8165  negid  8166  negsub  8167  subneg  8168  negneg  8169  negeq0  8173  negsubdi  8175  renegcl  8180  mul02  8306  mul01  8308  mulneg1  8314  ixi  8502  negap0  8549  muleqadd  8586  divvalap  8591  div0ap  8619  recgt0  8766  0m0e0  8990  2muline0  9103  elznn0  9227  ser0  10470  0exp0e1  10481  expeq0  10507  0exp  10511  sq0  10566  bcval5  10697  shftval3  10791  shftidt2  10796  cjap0  10871  cjne0  10872  abs0  11022  abs2dif  11070  clim0  11248  climz  11255  serclim0  11268  sumrbdclem  11340  fsum3cvg  11341  summodclem3  11343  summodclem2a  11344  fisumss  11355  fsumrelem  11434  ef0  11635  eftlub  11653  sin0  11692  tan0  11694  cnbl0  13328  cnblcld  13329  dvconst  13455  dvcnp2cntop  13457  dvrecap  13471  dveflem  13481  sinhalfpilem  13506  sin2kpi  13526  cos2kpi  13527  sinkpi  13562  dcapnconst  14092