Theorem 0cn 8308

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 8274	. 2 |- ( ( _i x. _i ) + 1 ) = 0
2		ax-icn 8264	. . . 4 |- _i e. CC
3		mulcl 8296	. . . 4 |- ( ( _i e. CC /\ _i e. CC ) -> ( _i x. _i ) e. CC )
4	2, 2, 3	mp2an 430	. . 3 |- ( _i x. _i ) e. CC
5		ax-1cn 8262	. . 3 |- 1 e. CC
6		addcl 8294	. . 3 |- ( ( ( _i x. _i ) e. CC /\ 1 e. CC ) -> ( ( _i x. _i ) + 1 ) e. CC )
7	4, 5, 6	mp2an 430	. 2 |- ( ( _i x. _i ) + 1 ) e. CC
8	1, 7	eqeltrri 2312	1 |- 0 e. CC

Syntax hints:   e. wcel 2209  (class class class)co 6075   CCcc 8167   0cc0 8169   1c1 8170   _ici 8171   + caddc 8172   x. cmul 8174

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220  ax-1cn 8262  ax-icn 8264  ax-addcl 8265  ax-mulcl 8267  ax-i2m1 8274

This theorem depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is referenced by:  0cnd  8309  c0ex  8310  addlid  8455  00id  8457  cnegexlem2  8492  negcl  8516  subid  8535  subid1  8536  neg0  8562  negid  8563  negsub  8564  subneg  8565  negneg  8566  negeq0  8570  negsubdi  8572  renegcl  8577  mul02  8704  mul01  8706  mulneg1  8712  ixi  8901  negap0  8948  muleqadd  8988  divvalap  8994  div0ap  9022  recgt0  9170  0m0e0  9395  2muline0  9509  elznn0  9638  ser0  10948  0exp0e1  10959  expeq0  10985  0exp  10989  sq0  11045  bcval5  11179  shftval3  11570  shftidt2  11575  cjap0  11651  cjne0  11652  abs0  11802  abs2dif  11850  clim0  12029  climz  12036  serclim0  12049  sumrbdclem  12122  fsum3cvg  12123  summodclem3  12125  summodclem2a  12126  fisumss  12137  fsumrelem  12216  ef0  12417  eftlub  12435  sin0  12474  tan0  12476  4sqlem11  13158  cncrng  14878  cnfld0  14880  cnbl0  15558  cnblcld  15559  dvconst  15718  dvconstre  15720  dvconstss  15722  dvcnp2cntop  15723  dvrecap  15737  dveflem  15750  plyun0  15760  plycjlemc  15784  plycj  15785  dvply2g  15790  sinhalfpilem  15815  sin2kpi  15835  cos2kpi  15836  sinkpi  15871  1sgm2ppw  16023  dcapnconst  17016