Theorem 0cn 7541

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 7511	. 2 |- ( ( _i x. _i ) + 1 ) = 0
2		ax-icn 7501	. . . 4 |- _i e. CC
3		mulcl 7530	. . . 4 |- ( ( _i e. CC /\ _i e. CC ) -> ( _i x. _i ) e. CC )
4	2, 2, 3	mp2an 418	. . 3 |- ( _i x. _i ) e. CC
5		ax-1cn 7499	. . 3 |- 1 e. CC
6		addcl 7528	. . 3 |- ( ( ( _i x. _i ) e. CC /\ 1 e. CC ) -> ( ( _i x. _i ) + 1 ) e. CC )
7	4, 5, 6	mp2an 418	. 2 |- ( ( _i x. _i ) + 1 ) e. CC
8	1, 7	eqeltrri 2162	1 |- 0 e. CC

Syntax hints:   e. wcel 1439  (class class class)co 5666   CCcc 7409   0cc0 7411   1c1 7412   _ici 7413   + caddc 7414   x. cmul 7416

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1382  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-4 1446  ax-17 1465  ax-ial 1473  ax-ext 2071  ax-1cn 7499  ax-icn 7501  ax-addcl 7502  ax-mulcl 7504  ax-i2m1 7511

This theorem depends on definitions:  df-bi 116  df-cleq 2082  df-clel 2085

This theorem is referenced by:  0cnd  7542  c0ex  7543  addid2  7682  00id  7684  cnegexlem2  7719  negcl  7743  subid  7762  subid1  7763  neg0  7789  negid  7790  negsub  7791  subneg  7792  negneg  7793  negeq0  7797  negsubdi  7799  renegcl  7804  mul02  7926  mul01  7928  mulneg1  7934  ixi  8121  negap0  8167  muleqadd  8198  divvalap  8202  div0ap  8230  recgt0  8372  0m0e0  8595  2muline0  8702  elznn0  8826  iser0  10008  ser0  10010  0exp0e1  10021  expeq0  10047  0exp  10051  sq0  10106  ibcval5  10232  shftval3  10322  shftidt2  10327  cjap0  10402  cjne0  10403  abs0  10552  abs00  10558  abs2dif  10600  clim0  10734  climz  10741  serclim0  10754  iserclim0  10755  isumrblem  10826  fisumcvg  10827  fsum3cvg  10828  isummolem3  10831  isummolem2a  10832  fisumss  10845  fsumrelem  10926  ef0  11023  eftlub  11041  sin0  11081  tan0  11083