Theorem 0cn 7758

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 7725	. 2 |- ( ( _i x. _i ) + 1 ) = 0
2		ax-icn 7715	. . . 4 |- _i e. CC
3		mulcl 7747	. . . 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 7713	. . 3 |- 1 e. CC
6		addcl 7745	. . 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 2213	1 |- 0 e. CC

Syntax hints:   e. wcel 1480  (class class class)co 5774   CCcc 7618   0cc0 7620   1c1 7621   _ici 7622   + caddc 7623   x. cmul 7625

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 2121  ax-1cn 7713  ax-icn 7715  ax-addcl 7716  ax-mulcl 7718  ax-i2m1 7725

This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135

This theorem is referenced by:  0cnd  7759  c0ex  7760  addid2  7901  00id  7903  cnegexlem2  7938  negcl  7962  subid  7981  subid1  7982  neg0  8008  negid  8009  negsub  8010  subneg  8011  negneg  8012  negeq0  8016  negsubdi  8018  renegcl  8023  mul02  8149  mul01  8151  mulneg1  8157  ixi  8345  negap0  8392  muleqadd  8429  divvalap  8434  div0ap  8462  recgt0  8608  0m0e0  8832  2muline0  8945  elznn0  9069  ser0  10287  0exp0e1  10298  expeq0  10324  0exp  10328  sq0  10383  bcval5  10509  shftval3  10599  shftidt2  10604  cjap0  10679  cjne0  10680  abs0  10830  abs2dif  10878  clim0  11054  climz  11061  serclim0  11074  sumrbdclem  11146  fsum3cvg  11147  summodclem3  11149  summodclem2a  11150  fisumss  11161  fsumrelem  11240  ef0  11378  eftlub  11396  sin0  11436  tan0  11438  cnbl0  12703  cnblcld  12704  dvconst  12830  dvcnp2cntop  12832  dvrecap  12846  dveflem  12855  sinhalfpilem  12872  sin2kpi  12892  cos2kpi  12893  sinkpi  12928