Theorem 0cn 9586

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

Assertion

Ref	Expression
0cn	|- 0 e. CC

Proof of Theorem 0cn

Step	Hyp	Ref	Expression
1		ax-i2m1 9558	. 2 |- ( ( _i x. _i ) + 1 ) = 0
2		ax-icn 9549	. . . 4 |- _i e. CC
3		mulcl 9574	. . . 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 9548	. . 3 |- 1 e. CC
6		addcl 9572	. . 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 2526	1 |- 0 e. CC

Syntax hints:   e. wcel 1802  (class class class)co 6277   CCcc 9488   0cc0 9490   1c1 9491   _ici 9492   + caddc 9493   x. cmul 9495

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-ext 2419  ax-1cn 9548  ax-icn 9549  ax-addcl 9550  ax-mulcl 9552  ax-i2m1 9558

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

This theorem is referenced by:  0cnd  9587  c0ex  9588  1re  9593  00id  9753  mul02lem1  9754  mul02  9756  mul01  9757  addid1  9758  addid2  9761  negcl  9820  subid  9838  subid1  9839  neg0  9865  negid  9866  negsub  9867  subneg  9868  negneg  9869  negeq0  9873  negsubdi  9875  renegcli  9880  mulneg1  9994  msqge0  10075  ixi  10179  muleqadd  10194  div0  10236  ofsubge0  10536  0m0e0  10646  elznn0  10880  ser0  12133  0exp0e1  12145  0exp  12175  sq0  12233  sqeqor  12256  binom2  12257  bcval5  12370  s1co  12773  shftval3  12883  shftidt2  12888  cjne0  12970  sqrt0  13049  abs0  13092  abs00bd  13098  abs2dif  13139  clim0  13303  climz  13346  serclim0  13374  rlimneg  13443  sumrblem  13507  fsumcvg  13508  summolem2a  13511  sumss  13520  fsumss  13521  fsumcvg2  13523  fsumsplit  13536  sumsplit  13557  fsumrelem  13595  fsumrlim  13599  fsumo1  13600  ef0  13699  eftlub  13716  sin0  13756  tan0  13758  divalglem9  13931  sadadd2lem2  13972  sadadd3  13983  bezout  14052  pcmpt2  14284  prmreclem2  14307  4sqlem11  14345  ramcl  14419  odadd1  16723  cnaddablx  16743  cnaddabl  16744  frgpnabllem1  16746  cncrng  18307  cnfld0  18310  cnbl0  21147  cnblcld  21148  cnfldnm  21152  xrge0gsumle  21204  xrge0tsms  21205  cnheibor  21321  csscld  21555  clsocv  21556  cnflduss  21662  cnfldcusp  21663  rrxmvallem  21697  rrxmval  21698  mbfss  21919  mbfmulc2lem  21920  0plef  21945  0pledm  21946  itg1ge0  21959  itg1addlem4  21972  itg2splitlem  22021  itg2addlem  22031  ibl0  22059  iblcnlem  22061  iblss2  22078  itgss3  22087  dvconst  22186  dvcnp2  22189  dvrec  22224  dvexp3  22245  dveflem  22246  dvef  22247  dv11cn  22268  lhop1lem  22280  plyun0  22460  plyeq0lem  22473  coeeulem  22487  coeeu  22488  coef3  22495  dgrle  22506  0dgrb  22509  coefv0  22510  coemulc  22517  coe1termlem  22520  coe1term  22521  dgr0  22524  dgrmulc  22533  dgrcolem2  22536  vieta1lem2  22572  iaa  22586  aareccl  22587  aalioulem3  22595  taylthlem2  22634  psercn  22686  pserdvlem2  22688  abelthlem2  22692  abelthlem3  22693  abelthlem5  22695  abelthlem7  22698  abelth  22701  sin2kpi  22741  cos2kpi  22742  sinkpi  22777  efopn  22904  logtayl  22906  cxpval  22910  0cxp  22912  cxpexp  22914  cxpcl  22920  cxpge0  22929  mulcxplem  22930  mulcxp  22931  cxpmul2  22935  dvsqrt  22983  cxpcn3  22987  abscxpbnd  22992  efrlim  23164  ftalem2  23212  ftalem3  23213  ftalem4  23214  ftalem5  23215  ftalem7  23217  prmorcht  23317  muinv  23334  1sgm2ppw  23340  logfacbnd3  23363  logexprlim  23365  dchrelbas2  23377  dchrmulid2  23392  dchrfi  23395  dchrinv  23401  lgsdir2  23468  lgsdir  23470  dchrvmasumiflem1  23551  dchrvmasumiflem2  23552  rpvmasum2  23562  log2sumbnd  23594  selberg2lem  23600  logdivbnd  23606  ax5seglem8  24104  axlowdimlem6  24115  axlowdimlem13  24122  ex-co  25024  avril1  25036  cnaddablo  25217  cnid  25218  addinv  25219  vc0  25327  vcz  25328  vcoprne  25337  ipasslem8  25617  siilem2  25632  hvmul0  25806  hi01  25878  norm-iii  25922  h1de2ctlem  26338  pjmuli  26472  pjneli  26506  eigre  26619  eigorth  26622  elnlfn  26712  0cnfn  26764  0lnfn  26769  lnopunilem2  26795  xrge0tsmsd  27641  qqh0  27831  qqhcn  27838  eulerpartlemgs2  28185  sgnneg  28345  subfacp1lem6  28495  sinccvglem  28904  abs2sqle  28912  abs2sqlt  28913  0fallfac  29127  0risefac  29128  binomfallfac  29131  fsumcube  29790  tan2h  30015  mblfinlem2  30020  ovoliunnfl  30024  voliunnfl  30026  ftc1anclem5  30062  dvcnsqrt  30069  cntotbnd  30260  flcidc  31092  dvconstbi  31208  expgrowth  31209  negcncfg  31586  ioodvbdlimc1  31630  ioodvbdlimc2  31632  itgsinexplem1  31638  stoweidlem26  31693  stoweidlem36  31703  stoweidlem55  31722  stirlinglem8  31748  fourierdlem103  31877  sqwvfoura  31896  sqwvfourb  31897  sec0  32864