Theorem 0cn 7891

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 7858	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 7848	. . . 4 ⊢ i ∈ ℂ
3		mulcl 7880	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 423	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 7846	. . 3 ⊢ 1 ∈ ℂ
6		addcl 7878	. . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
7	4, 5, 6	mp2an 423	. 2 ⊢ ((i · i) + 1) ∈ ℂ
8	1, 7	eqeltrri 2240	1 ⊢ 0 ∈ ℂ

Syntax hints:   ∈ wcel 2136  (class class class)co 5842  ℂcc 7751  0cc0 7753  1c1 7754  ici 7755   + caddc 7756   · cmul 7758

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 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522  ax-ext 2147  ax-1cn 7846  ax-icn 7848  ax-addcl 7849  ax-mulcl 7851  ax-i2m1 7858

This theorem depends on definitions:  df-bi 116  df-cleq 2158  df-clel 2161

This theorem is referenced by:  0cnd  7892  c0ex  7893  addid2  8037  00id  8039  cnegexlem2  8074  negcl  8098  subid  8117  subid1  8118  neg0  8144  negid  8145  negsub  8146  subneg  8147  negneg  8148  negeq0  8152  negsubdi  8154  renegcl  8159  mul02  8285  mul01  8287  mulneg1  8293  ixi  8481  negap0  8528  muleqadd  8565  divvalap  8570  div0ap  8598  recgt0  8745  0m0e0  8969  2muline0  9082  elznn0  9206  ser0  10449  0exp0e1  10460  expeq0  10486  0exp  10490  sq0  10545  bcval5  10676  shftval3  10769  shftidt2  10774  cjap0  10849  cjne0  10850  abs0  11000  abs2dif  11048  clim0  11226  climz  11233  serclim0  11246  sumrbdclem  11318  fsum3cvg  11319  summodclem3  11321  summodclem2a  11322  fisumss  11333  fsumrelem  11412  ef0  11613  eftlub  11631  sin0  11670  tan0  11672  cnbl0  13174  cnblcld  13175  dvconst  13301  dvcnp2cntop  13303  dvrecap  13317  dveflem  13327  sinhalfpilem  13352  sin2kpi  13372  cos2kpi  13373  sinkpi  13408  dcapnconst  13939