Theorem 0cn 8018

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 7984	. 2 |- ( ( _i x. _i ) + 1 ) = 0
2		ax-icn 7974	. . . 4 |- _i e. CC
3		mulcl 8006	. . . 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 7972	. . 3 |- 1 e. CC
6		addcl 8004	. . 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 5922   CCcc 7877   0cc0 7879   1c1 7880   _ici 7881   + caddc 7882   x. cmul 7884

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 7972  ax-icn 7974  ax-addcl 7975  ax-mulcl 7977  ax-i2m1 7984

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

This theorem is referenced by:  0cnd  8019  c0ex  8020  addlid  8165  00id  8167  cnegexlem2  8202  negcl  8226  subid  8245  subid1  8246  neg0  8272  negid  8273  negsub  8274  subneg  8275  negneg  8276  negeq0  8280  negsubdi  8282  renegcl  8287  mul02  8413  mul01  8415  mulneg1  8421  ixi  8610  negap0  8657  muleqadd  8695  divvalap  8701  div0ap  8729  recgt0  8877  0m0e0  9102  2muline0  9216  elznn0  9341  ser0  10625  0exp0e1  10636  expeq0  10662  0exp  10666  sq0  10722  bcval5  10855  shftval3  10992  shftidt2  10997  cjap0  11072  cjne0  11073  abs0  11223  abs2dif  11271  clim0  11450  climz  11457  serclim0  11470  sumrbdclem  11542  fsum3cvg  11543  summodclem3  11545  summodclem2a  11546  fisumss  11557  fsumrelem  11636  ef0  11837  eftlub  11855  sin0  11894  tan0  11896  4sqlem11  12570  cncrng  14125  cnfld0  14127  cnbl0  14770  cnblcld  14771  dvconst  14930  dvconstre  14932  dvconstss  14934  dvcnp2cntop  14935  dvrecap  14949  dveflem  14962  plyun0  14972  plycjlemc  14996  plycj  14997  dvply2g  15002  sinhalfpilem  15027  sin2kpi  15047  cos2kpi  15048  sinkpi  15083  1sgm2ppw  15231  dcapnconst  15705