Theorem 0cn 8149

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 8115	. 2 |- ( ( _i x. _i ) + 1 ) = 0
2		ax-icn 8105	. . . 4 |- _i e. CC
3		mulcl 8137	. . . 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 8103	. . 3 |- 1 e. CC
6		addcl 8135	. . 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 6007   CCcc 8008   0cc0 8010   1c1 8011   _ici 8012   + caddc 8013   x. cmul 8015

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 8103  ax-icn 8105  ax-addcl 8106  ax-mulcl 8108  ax-i2m1 8115

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

This theorem is referenced by:  0cnd  8150  c0ex  8151  addlid  8296  00id  8298  cnegexlem2  8333  negcl  8357  subid  8376  subid1  8377  neg0  8403  negid  8404  negsub  8405  subneg  8406  negneg  8407  negeq0  8411  negsubdi  8413  renegcl  8418  mul02  8544  mul01  8546  mulneg1  8552  ixi  8741  negap0  8788  muleqadd  8826  divvalap  8832  div0ap  8860  recgt0  9008  0m0e0  9233  2muline0  9347  elznn0  9472  ser0  10767  0exp0e1  10778  expeq0  10804  0exp  10808  sq0  10864  bcval5  10997  shftval3  11354  shftidt2  11359  cjap0  11434  cjne0  11435  abs0  11585  abs2dif  11633  clim0  11812  climz  11819  serclim0  11832  sumrbdclem  11904  fsum3cvg  11905  summodclem3  11907  summodclem2a  11908  fisumss  11919  fsumrelem  11998  ef0  12199  eftlub  12217  sin0  12256  tan0  12258  4sqlem11  12940  cncrng  14549  cnfld0  14551  cnbl0  15224  cnblcld  15225  dvconst  15384  dvconstre  15386  dvconstss  15388  dvcnp2cntop  15389  dvrecap  15403  dveflem  15416  plyun0  15426  plycjlemc  15450  plycj  15451  dvply2g  15456  sinhalfpilem  15481  sin2kpi  15501  cos2kpi  15502  sinkpi  15537  1sgm2ppw  15685  dcapnconst  16517