Theorem 0cn 9399

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

Assertion

Ref	Expression
0cn	|- 0 e. CC

Proof of Theorem 0cn

Step	Hyp	Ref	Expression
1		ax-i2m1 9371	. 2 |- ( ( _i x. _i ) + 1 ) = 0
2		ax-icn 9362	. . . 4 |- _i e. CC
3		mulcl 9387	. . . 4 |- ( ( _i e. CC /\ _i e. CC ) -> ( _i x. _i ) e. CC )
4	2, 2, 3	mp2an 672	. . 3 |- ( _i x. _i ) e. CC
5		ax-1cn 9361	. . 3 |- 1 e. CC
6		addcl 9385	. . 3 |- ( ( ( _i x. _i ) e. CC /\ 1 e. CC ) -> ( ( _i x. _i ) + 1 ) e. CC )
7	4, 5, 6	mp2an 672	. 2 |- ( ( _i x. _i ) + 1 ) e. CC
8	1, 7	eqeltrri 2514	1 |- 0 e. CC

Syntax hints:   e. wcel 1756  (class class class)co 6112   CCcc 9301   0cc0 9303   1c1 9304   _ici 9305   + caddc 9306   x. cmul 9308

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2423  ax-1cn 9361  ax-icn 9362  ax-addcl 9363  ax-mulcl 9365  ax-i2m1 9371

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-cleq 2436  df-clel 2439

This theorem is referenced by:  0cnd  9400  c0ex  9401  1re  9406  00id  9565  mul02lem1  9566  mul02  9568  mul01  9569  addid1  9570  addid2  9573  negcl  9631  subid  9649  subid1  9650  neg0  9676  negid  9677  negsub  9678  subneg  9679  negneg  9680  negeq0  9684  negsubdi  9686  renegcli  9691  mulneg1  9802  msqge0  9882  ixi  9986  muleqadd  10001  div0  10043  ofsubge0  10342  0m0e0  10452  elznn0  10682  ser0  11879  0exp0e1  11891  0exp  11920  sq0  11978  sqeqor  12001  binom2  12002  bcval5  12115  s1co  12482  shftval3  12586  shftidt2  12591  cjne0  12673  sqr0  12752  abs0  12795  abs00bd  12801  abs2dif  12841  clim0  13005  climz  13048  serclim0  13076  rlimneg  13145  sumrblem  13209  fsumcvg  13210  summolem2a  13213  sumss  13222  fsumss  13223  fsumcvg2  13225  fsumsplit  13237  sumsplit  13256  fsumrelem  13291  fsumrlim  13295  fsumo1  13296  ef0  13397  eftlub  13414  sin0  13454  tan0  13456  divalglem9  13626  sadadd2lem2  13667  sadadd3  13678  bezout  13747  pcmpt2  13976  prmreclem2  13999  4sqlem11  14037  ramcl  14111  odadd1  16351  cnaddablx  16369  cnaddabl  16370  frgpnabllem1  16372  cncrng  17859  cnfld0  17862  cnbl0  20375  cnblcld  20376  cnfldnm  20380  xrge0gsumle  20432  xrge0tsms  20433  cnheibor  20549  csscld  20783  clsocv  20784  cnflduss  20890  cnfldcusp  20891  rrxmvallem  20925  rrxmval  20926  mbfss  21146  mbfmulc2lem  21147  0plef  21172  0pledm  21173  itg1ge0  21186  itg1addlem4  21199  itg2splitlem  21248  itg2addlem  21258  ibl0  21286  iblcnlem  21288  iblss2  21305  itgss3  21314  dvconst  21413  dvcnp2  21416  dvrec  21451  dvexp3  21472  dveflem  21473  dvef  21474  dv11cn  21495  lhop1lem  21507  plyun0  21687  plyeq0lem  21700  coeeulem  21714  coeeu  21715  coef3  21722  dgrle  21733  0dgrb  21736  coefv0  21737  coemulc  21744  coe1termlem  21747  coe1term  21748  dgr0  21751  dgrmulc  21760  dgrcolem2  21763  vieta1lem2  21799  iaa  21813  aareccl  21814  aalioulem3  21822  taylthlem2  21861  psercn  21913  pserdvlem2  21915  abelthlem2  21919  abelthlem3  21920  abelthlem5  21922  abelthlem7  21925  abelth  21928  sin2kpi  21967  cos2kpi  21968  sinkpi  22003  efopn  22125  logtayl  22127  cxpval  22131  0cxp  22133  cxpexp  22135  cxpcl  22141  cxpge0  22150  mulcxplem  22151  mulcxp  22152  cxpmul2  22156  dvsqr  22204  cxpcn3  22208  abscxpbnd  22213  efrlim  22385  ftalem2  22433  ftalem3  22434  ftalem4  22435  ftalem5  22436  ftalem7  22438  prmorcht  22538  muinv  22555  1sgm2ppw  22561  logfacbnd3  22584  logexprlim  22586  dchrelbas2  22598  dchrmulid2  22613  dchrfi  22616  dchrinv  22622  lgsdir2  22689  lgsdir  22691  dchrvmasumiflem1  22772  dchrvmasumiflem2  22773  rpvmasum2  22783  log2sumbnd  22815  selberg2lem  22821  logdivbnd  22827  ax5seglem8  23204  axlowdimlem6  23215  axlowdimlem13  23222  ex-co  23667  avril1  23678  cnaddablo  23859  cnid  23860  addinv  23861  vc0  23969  vcz  23970  vcoprne  23979  ipasslem8  24259  siilem2  24274  hvmul0  24448  hi01  24520  norm-iii  24564  h1de2ctlem  24980  pjmuli  25114  pjneli  25148  eigre  25261  eigorth  25264  elnlfn  25354  0cnfn  25406  0lnfn  25411  lnopunilem2  25437  xrge0tsmsd  26275  qqh0  26435  qqhcn  26442  eulerpartlemgs2  26785  sgnneg  26945  subfacp1lem6  27095  sinccvglem  27339  abs2sqle  27347  abs2sqlt  27348  0fallfac  27562  0risefac  27563  binomfallfac  27566  fsumcube  28225  tan2h  28450  mblfinlem2  28455  ovoliunnfl  28459  voliunnfl  28461  ftc1anclem5  28497  dvcnsqr  28504  cntotbnd  28721  flcidc  29557  dvconstbi  29634  expgrowth  29635  itgsinexplem1  29820  stoweidlem26  29847  stoweidlem36  29857  stoweidlem55  29876  stirlinglem8  29902  sec0  31191