Theorem 0cn 8011

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 7977	. 2 |- ( ( _i x. _i ) + 1 ) = 0
2		ax-icn 7967	. . . 4 |- _i e. CC
3		mulcl 7999	. . . 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 7965	. . 3 |- 1 e. CC
6		addcl 7997	. . 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 2267	1 |- 0 e. CC

Syntax hints:   e. wcel 2164  (class class class)co 5918   CCcc 7870   0cc0 7872   1c1 7873   _ici 7874   + caddc 7875   x. cmul 7877

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2175  ax-1cn 7965  ax-icn 7967  ax-addcl 7968  ax-mulcl 7970  ax-i2m1 7977

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

This theorem is referenced by:  0cnd  8012  c0ex  8013  addlid  8158  00id  8160  cnegexlem2  8195  negcl  8219  subid  8238  subid1  8239  neg0  8265  negid  8266  negsub  8267  subneg  8268  negneg  8269  negeq0  8273  negsubdi  8275  renegcl  8280  mul02  8406  mul01  8408  mulneg1  8414  ixi  8602  negap0  8649  muleqadd  8687  divvalap  8693  div0ap  8721  recgt0  8869  0m0e0  9094  2muline0  9207  elznn0  9332  ser0  10604  0exp0e1  10615  expeq0  10641  0exp  10645  sq0  10701  bcval5  10834  shftval3  10971  shftidt2  10976  cjap0  11051  cjne0  11052  abs0  11202  abs2dif  11250  clim0  11428  climz  11435  serclim0  11448  sumrbdclem  11520  fsum3cvg  11521  summodclem3  11523  summodclem2a  11524  fisumss  11535  fsumrelem  11614  ef0  11815  eftlub  11833  sin0  11872  tan0  11874  4sqlem11  12539  cncrng  14057  cnfld0  14059  cnbl0  14702  cnblcld  14703  dvconst  14846  dvcnp2cntop  14848  dvrecap  14862  dveflem  14872  plyun0  14882  sinhalfpilem  14926  sin2kpi  14946  cos2kpi  14947  sinkpi  14982  dcapnconst  15551