Theorem 0cn 8171

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 8137	. 2 |- ( ( _i x. _i ) + 1 ) = 0
2		ax-icn 8127	. . . 4 |- _i e. CC
3		mulcl 8159	. . . 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 8125	. . 3 |- 1 e. CC
6		addcl 8157	. . 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 2305	1 |- 0 e. CC

Syntax hints:   e. wcel 2202  (class class class)co 6018   CCcc 8030   0cc0 8032   1c1 8033   _ici 8034   + caddc 8035   x. cmul 8037

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213  ax-1cn 8125  ax-icn 8127  ax-addcl 8128  ax-mulcl 8130  ax-i2m1 8137

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227

This theorem is referenced by:  0cnd  8172  c0ex  8173  addlid  8318  00id  8320  cnegexlem2  8355  negcl  8379  subid  8398  subid1  8399  neg0  8425  negid  8426  negsub  8427  subneg  8428  negneg  8429  negeq0  8433  negsubdi  8435  renegcl  8440  mul02  8566  mul01  8568  mulneg1  8574  ixi  8763  negap0  8810  muleqadd  8848  divvalap  8854  div0ap  8882  recgt0  9030  0m0e0  9255  2muline0  9369  elznn0  9494  ser0  10796  0exp0e1  10807  expeq0  10833  0exp  10837  sq0  10893  bcval5  11026  shftval3  11405  shftidt2  11410  cjap0  11485  cjne0  11486  abs0  11636  abs2dif  11684  clim0  11863  climz  11870  serclim0  11883  sumrbdclem  11956  fsum3cvg  11957  summodclem3  11959  summodclem2a  11960  fisumss  11971  fsumrelem  12050  ef0  12251  eftlub  12269  sin0  12308  tan0  12310  4sqlem11  12992  cncrng  14602  cnfld0  14604  cnbl0  15277  cnblcld  15278  dvconst  15437  dvconstre  15439  dvconstss  15441  dvcnp2cntop  15442  dvrecap  15456  dveflem  15469  plyun0  15479  plycjlemc  15503  plycj  15504  dvply2g  15509  sinhalfpilem  15534  sin2kpi  15554  cos2kpi  15555  sinkpi  15590  1sgm2ppw  15738  dcapnconst  16717