Theorem 0cn 7944

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 7911	. 2 |- ( ( _i x. _i ) + 1 ) = 0
2		ax-icn 7901	. . . 4 |- _i e. CC
3		mulcl 7933	. . . 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 7899	. . 3 |- 1 e. CC
6		addcl 7931	. . 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 2251	1 |- 0 e. CC

Syntax hints:   e. wcel 2148  (class class class)co 5870   CCcc 7804   0cc0 7806   1c1 7807   _ici 7808   + caddc 7809   x. cmul 7811

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159  ax-1cn 7899  ax-icn 7901  ax-addcl 7902  ax-mulcl 7904  ax-i2m1 7911

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173

This theorem is referenced by:  0cnd  7945  c0ex  7946  addlid  8090  00id  8092  cnegexlem2  8127  negcl  8151  subid  8170  subid1  8171  neg0  8197  negid  8198  negsub  8199  subneg  8200  negneg  8201  negeq0  8205  negsubdi  8207  renegcl  8212  mul02  8338  mul01  8340  mulneg1  8346  ixi  8534  negap0  8581  muleqadd  8619  divvalap  8625  div0ap  8653  recgt0  8801  0m0e0  9025  2muline0  9138  elznn0  9262  ser0  10507  0exp0e1  10518  expeq0  10544  0exp  10548  sq0  10603  bcval5  10734  shftval3  10827  shftidt2  10832  cjap0  10907  cjne0  10908  abs0  11058  abs2dif  11106  clim0  11284  climz  11291  serclim0  11304  sumrbdclem  11376  fsum3cvg  11377  summodclem3  11379  summodclem2a  11380  fisumss  11391  fsumrelem  11470  ef0  11671  eftlub  11689  sin0  11728  tan0  11730  cncrng  13268  cnfld0  13270  cnbl0  13816  cnblcld  13817  dvconst  13943  dvcnp2cntop  13945  dvrecap  13959  dveflem  13969  sinhalfpilem  13994  sin2kpi  14014  cos2kpi  14015  sinkpi  14050  dcapnconst  14579