Theorem 0cn 9040

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

Assertion

Ref	Expression
0cn	|- 0 e. CC

Proof of Theorem 0cn

Step	Hyp	Ref	Expression
1		ax-i2m1 9014	. 2 |- ( ( _i x. _i ) + 1 ) = 0
2		ax-icn 9005	. . . 4 |- _i e. CC
3		mulcl 9030	. . . 4 |- ( ( _i e. CC /\ _i e. CC ) -> ( _i x. _i ) e. CC )
4	2, 2, 3	mp2an 654	. . 3 |- ( _i x. _i ) e. CC
5		ax-1cn 9004	. . 3 |- 1 e. CC
6		addcl 9028	. . 3 |- ( ( ( _i x. _i ) e. CC /\ 1 e. CC ) -> ( ( _i x. _i ) + 1 ) e. CC )
7	4, 5, 6	mp2an 654	. 2 |- ( ( _i x. _i ) + 1 ) e. CC
8	1, 7	eqeltrri 2475	1 |- 0 e. CC

Syntax hints:   e. wcel 1721  (class class class)co 6040   CCcc 8944   0cc0 8946   1c1 8947   _ici 8948   + caddc 8949   x. cmul 8951

This theorem is referenced by:  c0ex  9041  1re  9046  00id  9197  mul02lem1  9198  mul02  9200  mul01  9201  addid1  9202  addid2  9205  negcl  9262  subid  9277  subid1  9278  neg0  9303  negid  9304  negsub  9305  subneg  9306  negneg  9307  negeq0  9311  negsubdi  9313  renegcli  9318  mulneg1  9426  msqge0  9505  ixi  9607  mul0or  9618  muleqadd  9622  diveq0  9644  div0  9662  eqneg  9690  ofsubge0  9955  un0addcl  10209  un0mulcl  10210  elznn0  10252  ser0  11330  0exp  11370  sq0  11428  sqeqor  11450  binom2  11451  discr  11471  faclbnd  11536  faclbnd3  11538  faclbnd4lem3  11541  facubnd  11546  bcval5  11564  revs1  11752  s1co  11757  shftval3  11846  shftidt2  11851  cjne0  11923  sqr0  12002  abs0  12045  abs00bd  12051  abs2dif  12091  clim0  12255  clim0c  12256  rlim0  12257  rlim0lt  12258  climz  12298  serclim0  12326  rlimneg  12395  isercolllem3  12415  sumrblem  12460  fsumcvg  12461  summolem2a  12464  zsum  12467  sumz  12471  sumss  12473  fsumss  12474  fsumcvg2  12476  fsumcl  12482  fsumsplit  12488  sumsplit  12507  fsumparts  12540  fsumrelem  12541  fsumrlim  12545  fsumo1  12546  binom  12564  arisum2  12595  expcnv  12598  ef0lem  12636  ef0  12648  eftlub  12665  ef4p  12669  sin0  12705  tan0  12707  divalglem9  12876  sadadd2lem2  12917  sadadd2lem  12926  sadadd3  12928  bezout  12997  phiprmpw  13120  iserodd  13164  pcmpt2  13217  prmreclem2  13240  prmreclem4  13242  prmrec  13245  4sqlem10  13270  4sqlem11  13278  ramcl  13352  odadd1  15418  cnaddablx  15436  cnaddabl  15437  frgpnabllem1  15439  cncrng  16677  cnfld0  16680  cnbl0  18761  cnblcld  18762  cnfldnm  18766  xrge0gsumle  18817  xrge0tsms  18818  fsumcn  18853  cnheibor  18933  evth2  18938  csscld  19156  clsocv  19157  cnflduss  19263  cnfldcusp  19264  ovolicc1  19365  mbfss  19491  mbfmulc2lem  19492  0plef  19517  0pledm  19518  itg1ge0  19531  itg1addlem4  19544  itg2splitlem  19593  itg2addlem  19603  ibl0  19631  iblcnlem  19633  itgrevallem1  19639  iblss2  19650  itgss3  19659  dvconst  19756  dvcnp2  19759  dvcmulf  19784  dvrec  19794  dvmptc  19797  dvmptcmul  19803  dvmptfsum  19812  dvexp3  19815  dveflem  19816  dvef  19817  rolle  19827  dv11cn  19838  lhop1lem  19850  elply2  20068  plyun0  20069  plyf  20070  elplyr  20073  elplyd  20074  ply1term  20076  ply0  20080  plyeq0lem  20082  plyeq0  20083  plyaddlem  20087  plymullem  20088  coeeulem  20096  coeeu  20097  dgrlem  20101  coef3  20104  coeidlem  20109  plyco  20113  coeeq2  20114  dgrle  20115  0dgrb  20118  coefv0  20119  coemulc  20126  coe0  20127  coe1termlem  20129  coe1term  20130  dgr0  20133  dgrmulc  20142  dgrcolem2  20145  plycj  20148  coecj  20149  plymul0or  20151  dvply1  20154  plydiveu  20168  fta1lem  20177  vieta1lem2  20181  elqaalem3  20191  iaa  20195  aareccl  20196  aalioulem3  20204  tayl0  20231  dvtaylp  20239  taylthlem2  20243  radcnv0  20285  psercn  20295  pserdvlem2  20297  pserdv  20298  abelthlem2  20301  abelthlem3  20302  abelthlem5  20304  abelthlem7  20307  abelth  20310  pilem2  20321  sin2kpi  20344  cos2kpi  20345  ptolemy  20357  sinkpi  20380  advlog  20498  advlogexp  20499  efopnlem2  20501  efopn  20502  logtayllem  20503  logtayl  20504  cxpval  20508  0cxp  20510  cxpexp  20512  cxpcl  20518  cxpge0  20527  mulcxplem  20528  mulcxp  20529  cxpmul2  20533  dvsqr  20581  cxpcn3  20585  abscxpbnd  20590  loglesqr  20595  affineequiv  20620  quad2  20632  dcubic  20639  asinlem  20661  dvatan  20728  leibpilem2  20734  leibpi  20735  efrlim  20761  emcllem7  20793  harmonicbnd3  20799  ftalem2  20809  ftalem3  20810  ftalem4  20811  ftalem5  20812  ftalem7  20814  prmorcht  20914  sqff1o  20918  musum  20929  muinv  20931  1sgm2ppw  20937  logfacbnd3  20960  logexprlim  20962  dchrelbas2  20974  dchrelbasd  20976  dchrmulid2  20989  dchrfi  20992  dchrinv  20998  dchrsum2  21005  sumdchr2  21007  bposlem1  21021  bposlem2  21022  lgsdir2  21065  lgsdir  21067  rplogsumlem2  21132  dchrvmasumiflem1  21148  dchrvmasumiflem2  21149  rpvmasum2  21159  log2sumbnd  21191  selberg2lem  21197  logdivbnd  21203  pntrsumo1  21212  pntrlog2bndlem4  21227  pntrlog2bndlem5  21228  pntleml  21258  ex-co  21699  avril1  21710  cnaddablo  21891  cnid  21892  addinv  21893  vc0  22001  vcz  22002  vcoprne  22011  ipasslem8  22291  siilem2  22306  hvmul0  22479  hi01  22551  norm-iii  22595  occllem  22758  h1de2ctlem  23010  pjmuli  23144  pjneli  23178  eigre  23291  eigorth  23294  elnlfn  23384  0cnfn  23436  0lnfn  23441  lnopeq0i  23463  lnopunilem2  23467  nlelchi  23517  addeq0  24067  divnumden2  24114  xrge0tsmsd  24176  qqh0  24321  qqhcn  24328  ballotlemfval0  24706  ballotlem4  24709  ballotlemi1  24713  ballotlemic  24717  ballotlem1c  24718  dmgmaddn0  24760  lgamgulmlem2  24767  igamf  24788  igamcl  24789  subfacp1lem6  24824  sinccvglem  25062  abs2sqle  25073  abs2sqlt  25074  climlec3  25167  ntrivcvgfvn0  25180  0fallfac  25304  0risefac  25305  binomfallfac  25308  ax5seglem8  25779  axlowdimlem6  25790  axlowdimlem13  25797  fsumcube  26010  mblfinlem  26143  ovoliunnfl  26147  voliunnfl  26149  itg2addnclem  26155  itg2addnclem3  26157  dvreacos  26180  cntotbnd  26395  pell14qrgt0  26812  acongeq  26938  mpaaeu  27223  flcidc  27247  dvconstbi  27419  expgrowth  27420  itgsinexplem1  27615  stoweidlem26  27642  stoweidlem36  27652  stoweidlem55  27671  stirlinglem7  27696  stirlinglem8  27697  swrdccatin12lem3b  28022  swrdccat3a  28030  swrdccat3b  28031  sec0  28217

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2385  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-mulcl 9008  ax-i2m1 9014

This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-cleq 2397  df-clel 2400