Theorem 0cn 8035

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 8001	. 2 |- ( ( _i x. _i ) + 1 ) = 0
2		ax-icn 7991	. . . 4 |- _i e. CC
3		mulcl 8023	. . . 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 7989	. . 3 |- 1 e. CC
6		addcl 8021	. . 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 2270	1 |- 0 e. CC

Syntax hints:   e. wcel 2167  (class class class)co 5925   CCcc 7894   0cc0 7896   1c1 7897   _ici 7898   + caddc 7899   x. cmul 7901

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178  ax-1cn 7989  ax-icn 7991  ax-addcl 7992  ax-mulcl 7994  ax-i2m1 8001

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

This theorem is referenced by:  0cnd  8036  c0ex  8037  addlid  8182  00id  8184  cnegexlem2  8219  negcl  8243  subid  8262  subid1  8263  neg0  8289  negid  8290  negsub  8291  subneg  8292  negneg  8293  negeq0  8297  negsubdi  8299  renegcl  8304  mul02  8430  mul01  8432  mulneg1  8438  ixi  8627  negap0  8674  muleqadd  8712  divvalap  8718  div0ap  8746  recgt0  8894  0m0e0  9119  2muline0  9233  elznn0  9358  ser0  10642  0exp0e1  10653  expeq0  10679  0exp  10683  sq0  10739  bcval5  10872  shftval3  11009  shftidt2  11014  cjap0  11089  cjne0  11090  abs0  11240  abs2dif  11288  clim0  11467  climz  11474  serclim0  11487  sumrbdclem  11559  fsum3cvg  11560  summodclem3  11562  summodclem2a  11563  fisumss  11574  fsumrelem  11653  ef0  11854  eftlub  11872  sin0  11911  tan0  11913  4sqlem11  12595  cncrng  14201  cnfld0  14203  cnbl0  14854  cnblcld  14855  dvconst  15014  dvconstre  15016  dvconstss  15018  dvcnp2cntop  15019  dvrecap  15033  dveflem  15046  plyun0  15056  plycjlemc  15080  plycj  15081  dvply2g  15086  sinhalfpilem  15111  sin2kpi  15131  cos2kpi  15132  sinkpi  15167  1sgm2ppw  15315  dcapnconst  15792