Theorem 0cn 8138

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 8104	. 2 |- ( ( _i x. _i ) + 1 ) = 0
2		ax-icn 8094	. . . 4 |- _i e. CC
3		mulcl 8126	. . . 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 8092	. . 3 |- 1 e. CC
6		addcl 8124	. . 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 2303	1 |- 0 e. CC

Syntax hints:   e. wcel 2200  (class class class)co 6001   CCcc 7997   0cc0 7999   1c1 8000   _ici 8001   + caddc 8002   x. cmul 8004

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211  ax-1cn 8092  ax-icn 8094  ax-addcl 8095  ax-mulcl 8097  ax-i2m1 8104

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  0cnd  8139  c0ex  8140  addlid  8285  00id  8287  cnegexlem2  8322  negcl  8346  subid  8365  subid1  8366  neg0  8392  negid  8393  negsub  8394  subneg  8395  negneg  8396  negeq0  8400  negsubdi  8402  renegcl  8407  mul02  8533  mul01  8535  mulneg1  8541  ixi  8730  negap0  8777  muleqadd  8815  divvalap  8821  div0ap  8849  recgt0  8997  0m0e0  9222  2muline0  9336  elznn0  9461  ser0  10755  0exp0e1  10766  expeq0  10792  0exp  10796  sq0  10852  bcval5  10985  shftval3  11338  shftidt2  11343  cjap0  11418  cjne0  11419  abs0  11569  abs2dif  11617  clim0  11796  climz  11803  serclim0  11816  sumrbdclem  11888  fsum3cvg  11889  summodclem3  11891  summodclem2a  11892  fisumss  11903  fsumrelem  11982  ef0  12183  eftlub  12201  sin0  12240  tan0  12242  4sqlem11  12924  cncrng  14533  cnfld0  14535  cnbl0  15208  cnblcld  15209  dvconst  15368  dvconstre  15370  dvconstss  15372  dvcnp2cntop  15373  dvrecap  15387  dveflem  15400  plyun0  15410  plycjlemc  15434  plycj  15435  dvply2g  15440  sinhalfpilem  15465  sin2kpi  15485  cos2kpi  15486  sinkpi  15521  1sgm2ppw  15669  dcapnconst  16429