Theorem 0cn 8013

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

Assertion

Ref	Expression
0cn	|- 0 e. CC

Proof of Theorem 0cn

Step	Hyp	Ref	Expression
1		ax-i2m1 7979	. 2 |- ( ( _i x. _i ) + 1 ) = 0
2		ax-icn 7969	. . . 4 |- _i e. CC
3		mulcl 8001	. . . 4 |- ( ( _i e. CC /\ _i e. CC ) -> ( _i x. _i ) e. CC )
4	2, 2, 3	mp2an 426	. . 3 |- ( _i x. _i ) e. CC
5		ax-1cn 7967	. . 3 |- 1 e. CC
6		addcl 7999	. . 3 |- ( ( ( _i x. _i ) e. CC /\ 1 e. CC ) -> ( ( _i x. _i ) + 1 ) e. CC )
7	4, 5, 6	mp2an 426	. 2 |- ( ( _i x. _i ) + 1 ) e. CC
8	1, 7	eqeltrri 2267	1 |- 0 e. CC

Syntax hints:   e. wcel 2164  (class class class)co 5919   CCcc 7872   0cc0 7874   1c1 7875   _ici 7876   + caddc 7877   x. cmul 7879

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2175  ax-1cn 7967  ax-icn 7969  ax-addcl 7970  ax-mulcl 7972  ax-i2m1 7979

This theorem depends on definitions:  df-bi 117  df-cleq 2186  df-clel 2189

This theorem is referenced by:  0cnd  8014  c0ex  8015  addlid  8160  00id  8162  cnegexlem2  8197  negcl  8221  subid  8240  subid1  8241  neg0  8267  negid  8268  negsub  8269  subneg  8270  negneg  8271  negeq0  8275  negsubdi  8277  renegcl  8282  mul02  8408  mul01  8410  mulneg1  8416  ixi  8604  negap0  8651  muleqadd  8689  divvalap  8695  div0ap  8723  recgt0  8871  0m0e0  9096  2muline0  9210  elznn0  9335  ser0  10607  0exp0e1  10618  expeq0  10644  0exp  10648  sq0  10704  bcval5  10837  shftval3  10974  shftidt2  10979  cjap0  11054  cjne0  11055  abs0  11205  abs2dif  11253  clim0  11431  climz  11438  serclim0  11451  sumrbdclem  11523  fsum3cvg  11524  summodclem3  11526  summodclem2a  11527  fisumss  11538  fsumrelem  11617  ef0  11818  eftlub  11836  sin0  11875  tan0  11877  4sqlem11  12542  cncrng  14068  cnfld0  14070  cnbl0  14713  cnblcld  14714  dvconst  14873  dvconstre  14875  dvconstss  14877  dvcnp2cntop  14878  dvrecap  14892  dveflem  14905  plyun0  14915  plycjlemc  14938  plycj  14939  sinhalfpilem  14967  sin2kpi  14987  cos2kpi  14988  sinkpi  15023  dcapnconst  15621