Theorem 0cn 9624

Description: 0 is a complex number. See also 0cnALT 9853. (Contributed by NM, 19-Feb-2005.)

Assertion

Ref	Expression
0cn	|- 0 e. CC

Proof of Theorem 0cn

Step	Hyp	Ref	Expression
1		ax-i2m1 9596	. 2 |- ( ( _i x. _i ) + 1 ) = 0
2		ax-icn 9587	. . . 4 |- _i e. CC
3		mulcl 9612	. . . 4 |- ( ( _i e. CC /\ _i e. CC ) -> ( _i x. _i ) e. CC )
4	2, 2, 3	mp2an 676	. . 3 |- ( _i x. _i ) e. CC
5		ax-1cn 9586	. . 3 |- 1 e. CC
6		addcl 9610	. . 3 |- ( ( ( _i x. _i ) e. CC /\ 1 e. CC ) -> ( ( _i x. _i ) + 1 ) e. CC )
7	4, 5, 6	mp2an 676	. 2 |- ( ( _i x. _i ) + 1 ) e. CC
8	1, 7	eqeltrri 2505	1 |- 0 e. CC

Syntax hints:   e. wcel 1867  (class class class)co 6296   CCcc 9526   0cc0 9528   1c1 9529   _ici 9530   + caddc 9531   x. cmul 9533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-ext 2398  ax-1cn 9586  ax-icn 9587  ax-addcl 9588  ax-mulcl 9590  ax-i2m1 9596

This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-cleq 2412  df-clel 2415

This theorem is referenced by:  0cnd  9625  c0ex  9626  1re  9631  00id  9797  mul02lem1  9798  mul02  9800  mul01  9801  addid1  9802  addid2  9805  negcl  9864  subid  9882  subid1  9883  neg0  9909  negid  9910  negsub  9911  subneg  9912  negneg  9913  negeq0  9917  negsubdi  9919  renegcli  9924  mulneg1  10044  msqge0  10124  ixi  10230  muleqadd  10245  div0  10287  ofsubge0  10597  0m0e0  10708  elznn0  10941  ser0  12251  0exp0e1  12263  0exp  12293  sq0  12352  sqeqor  12374  binom2  12375  bcval5  12489  s1co  12904  shftval3  13107  shftidt2  13112  cjne0  13194  sqrt0  13273  abs0  13316  abs00bd  13322  abs2dif  13363  clim0  13537  climz  13580  serclim0  13608  rlimneg  13677  sumrblem  13744  fsumcvg  13745  summolem2a  13748  sumss  13757  fsumss  13758  fsumcvg2  13760  fsumsplit  13773  sumsplit  13796  fsumrelem  13834  fsumrlim  13838  fsumo1  13839  0fallfac  14057  0risefac  14058  binomfallfac  14061  fsumcube  14080  ef0  14112  eftlub  14130  sin0  14170  tan0  14172  divalglem9  14346  sadadd2lem2  14387  sadadd3  14398  bezout  14470  pcmpt2  14790  prmreclem2  14813  4sqlem11  14851  ramcl  14939  odadd1  17414  cnaddablx  17434  cnaddabl  17435  frgpnabllem1  17437  cncrng  18917  cnfld0  18920  cnbl0  21698  cnblcld  21699  cnfldnm  21703  xrge0gsumle  21755  xrge0tsms  21756  cnheibor  21872  csscld  22106  clsocv  22107  cnflduss  22209  cnfldcusp  22210  rrxmvallem  22244  rrxmval  22245  mbfss  22476  mbfmulc2lem  22477  0plef  22504  0pledm  22505  itg1ge0  22518  itg1addlem4  22531  itg2splitlem  22580  itg2addlem  22590  ibl0  22618  iblcnlem  22620  iblss2  22637  itgss3  22646  dvconst  22745  dvcnp2  22748  dvrec  22783  dvexp3  22804  dveflem  22805  dvef  22806  dv11cn  22827  lhop1lem  22839  plyun0  23016  plyeq0lem  23029  coeeulem  23043  coeeu  23044  coef3  23051  dgrle  23062  0dgrb  23065  coefv0  23067  coemulc  23074  coe1termlem  23077  coe1term  23078  dgr0  23081  dgrmulc  23090  dgrcolem2  23093  vieta1lem2  23129  iaa  23143  aareccl  23144  aalioulem3  23152  taylthlem2  23191  psercn  23243  pserdvlem2  23245  abelthlem2  23249  abelthlem3  23250  abelthlem5  23252  abelthlem7  23255  abelth  23258  sin2kpi  23300  cos2kpi  23301  sinkpi  23336  efopn  23465  logtayl  23467  cxpval  23471  0cxp  23473  cxpexp  23475  cxpcl  23481  cxpge0  23490  mulcxplem  23491  mulcxp  23492  cxpmul2  23496  dvsqrt  23544  dvcnsqrt  23546  cxpcn3  23550  abscxpbnd  23555  efrlim  23757  ftalem2  23860  ftalem3  23861  ftalem4  23862  ftalem5  23863  ftalem7  23865  prmorcht  23965  muinv  23982  1sgm2ppw  23988  logfacbnd3  24011  logexprlim  24013  dchrelbas2  24025  dchrmulid2  24040  dchrfi  24043  dchrinv  24049  lgsdir2  24116  lgsdir  24118  dchrvmasumiflem1  24199  dchrvmasumiflem2  24200  rpvmasum2  24210  log2sumbnd  24242  selberg2lem  24248  logdivbnd  24254  ax5seglem8  24809  axlowdimlem6  24820  axlowdimlem13  24827  ex-co  25730  avril1  25742  cnaddablo  25920  cnid  25921  addinv  25922  vc0  26030  vcz  26031  vcoprne  26040  ipasslem8  26320  siilem2  26335  hvmul0  26509  hi01  26581  norm-iii  26625  h1de2ctlem  27040  pjmuli  27174  pjneli  27208  eigre  27320  eigorth  27323  elnlfn  27413  0cnfn  27465  0lnfn  27470  lnopunilem2  27496  xrge0tsmsd  28384  qqh0  28624  qqhcn  28631  eulerpartlemgs2  29036  sgnneg  29196  subfacp1lem6  29693  sinccvglem  30101  abs2sqle  30109  abs2sqlt  30110  tan2h  31641  poimirlem16  31660  poimirlem19  31663  poimirlem31  31675  mblfinlem2  31682  ovoliunnfl  31686  voliunnfl  31688  dvtanlem  31694  ftc1anclem5  31725  cntotbnd  31832  flcidc  35743  dvconstbi  36324  expgrowth  36325  dvradcnv2  36337  binomcxplemdvbinom  36343  binomcxplemnotnn0  36346  negcncfg  37334  ioodvbdlimc1  37381  ioodvbdlimc2  37383  itgsinexplem1  37403  stoweidlem26  37459  stoweidlem36  37470  stoweidlem55  37489  stirlinglem8  37516  fourierdlem103  37645  sqwvfoura  37664  sqwvfourb  37665  nn0sumshdiglemA  39204  nn0sumshdiglemB  39205  nn0sumshdiglem1  39206  sec0  39254