Theorem 0cn 7751

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 7718	. 2 |- ( ( _i x. _i ) + 1 ) = 0
2		ax-icn 7708	. . . 4 |- _i e. CC
3		mulcl 7740	. . . 4 |- ( ( _i e. CC /\ _i e. CC ) -> ( _i x. _i ) e. CC )
4	2, 2, 3	mp2an 422	. . 3 |- ( _i x. _i ) e. CC
5		ax-1cn 7706	. . 3 |- 1 e. CC
6		addcl 7738	. . 3 |- ( ( ( _i x. _i ) e. CC /\ 1 e. CC ) -> ( ( _i x. _i ) + 1 ) e. CC )
7	4, 5, 6	mp2an 422	. 2 |- ( ( _i x. _i ) + 1 ) e. CC
8	1, 7	eqeltrri 2211	1 |- 0 e. CC

Syntax hints:   e. wcel 1480  (class class class)co 5767   CCcc 7611   0cc0 7613   1c1 7614   _ici 7615   + caddc 7616   x. cmul 7618

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2119  ax-1cn 7706  ax-icn 7708  ax-addcl 7709  ax-mulcl 7711  ax-i2m1 7718

This theorem depends on definitions:  df-bi 116  df-cleq 2130  df-clel 2133

This theorem is referenced by:  0cnd  7752  c0ex  7753  addid2  7894  00id  7896  cnegexlem2  7931  negcl  7955  subid  7974  subid1  7975  neg0  8001  negid  8002  negsub  8003  subneg  8004  negneg  8005  negeq0  8009  negsubdi  8011  renegcl  8016  mul02  8142  mul01  8144  mulneg1  8150  ixi  8338  negap0  8385  muleqadd  8422  divvalap  8427  div0ap  8455  recgt0  8601  0m0e0  8825  2muline0  8938  elznn0  9062  ser0  10280  0exp0e1  10291  expeq0  10317  0exp  10321  sq0  10376  bcval5  10502  shftval3  10592  shftidt2  10597  cjap0  10672  cjne0  10673  abs0  10823  abs2dif  10871  clim0  11047  climz  11054  serclim0  11067  sumrbdclem  11138  fsum3cvg  11139  summodclem3  11142  summodclem2a  11143  fisumss  11154  fsumrelem  11233  ef0  11367  eftlub  11385  sin0  11425  tan0  11427  cnbl0  12692  cnblcld  12693  dvconst  12819  dvcnp2cntop  12821  dvrecap  12835  dveflem  12844  sinhalfpilem  12861  sin2kpi  12881  cos2kpi  12882  sinkpi  12917