Theorem 0cn 8037

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 8003	. 2 |- ( ( _i x. _i ) + 1 ) = 0
2		ax-icn 7993	. . . 4 |- _i e. CC
3		mulcl 8025	. . . 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 7991	. . 3 |- 1 e. CC
6		addcl 8023	. . 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 2270	1 |- 0 e. CC

Syntax hints:   e. wcel 2167  (class class class)co 5925   CCcc 7896   0cc0 7898   1c1 7899   _ici 7900   + caddc 7901   x. cmul 7903

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178  ax-1cn 7991  ax-icn 7993  ax-addcl 7994  ax-mulcl 7996  ax-i2m1 8003

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

This theorem is referenced by:  0cnd  8038  c0ex  8039  addlid  8184  00id  8186  cnegexlem2  8221  negcl  8245  subid  8264  subid1  8265  neg0  8291  negid  8292  negsub  8293  subneg  8294  negneg  8295  negeq0  8299  negsubdi  8301  renegcl  8306  mul02  8432  mul01  8434  mulneg1  8440  ixi  8629  negap0  8676  muleqadd  8714  divvalap  8720  div0ap  8748  recgt0  8896  0m0e0  9121  2muline0  9235  elznn0  9360  ser0  10644  0exp0e1  10655  expeq0  10681  0exp  10685  sq0  10741  bcval5  10874  shftval3  11011  shftidt2  11016  cjap0  11091  cjne0  11092  abs0  11242  abs2dif  11290  clim0  11469  climz  11476  serclim0  11489  sumrbdclem  11561  fsum3cvg  11562  summodclem3  11564  summodclem2a  11565  fisumss  11576  fsumrelem  11655  ef0  11856  eftlub  11874  sin0  11913  tan0  11915  4sqlem11  12597  cncrng  14203  cnfld0  14205  cnbl0  14856  cnblcld  14857  dvconst  15016  dvconstre  15018  dvconstss  15020  dvcnp2cntop  15021  dvrecap  15035  dveflem  15048  plyun0  15058  plycjlemc  15082  plycj  15083  dvply2g  15088  sinhalfpilem  15113  sin2kpi  15133  cos2kpi  15134  sinkpi  15169  1sgm2ppw  15317  dcapnconst  15796