Theorem 0cn 10032

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

Assertion

Ref	Expression
0cn	|- 0 e. CC

Proof of Theorem 0cn

Step	Hyp	Ref	Expression
1		ax-i2m1 10004	. 2 |- ( ( _i x. _i ) + 1 ) = 0
2		ax-icn 9995	. . . 4 |- _i e. CC
3		mulcl 10020	. . . 4 |- ( ( _i e. CC /\ _i e. CC ) -> ( _i x. _i ) e. CC )
4	2, 2, 3	mp2an 708	. . 3 |- ( _i x. _i ) e. CC
5		ax-1cn 9994	. . 3 |- 1 e. CC
6		addcl 10018	. . 3 |- ( ( ( _i x. _i ) e. CC /\ 1 e. CC ) -> ( ( _i x. _i ) + 1 ) e. CC )
7	4, 5, 6	mp2an 708	. 2 |- ( ( _i x. _i ) + 1 ) e. CC
8	1, 7	eqeltrri 2698	1 |- 0 e. CC

Syntax hints:   e. wcel 1990  (class class class)co 6650   CCcc 9934   0cc0 9936   1c1 9937   _ici 9938   + caddc 9939   x. cmul 9941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-mulcl 9998  ax-i2m1 10004

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-clel 2618

This theorem is referenced by:  0cnd  10033  c0ex  10034  1re  10039  00id  10211  mul02lem1  10212  mul02  10214  mul01  10215  addid1  10216  addid2  10219  negcl  10281  subid  10300  subid1  10301  neg0  10327  negid  10328  negsub  10329  subneg  10330  negneg  10331  negeq0  10335  negsubdi  10337  renegcli  10342  mulneg1  10466  msqge0  10549  ixi  10656  muleqadd  10671  div0  10715  ofsubge0  11019  0m0e0  11130  elznn0  11392  ser0  12853  0exp0e1  12865  0exp  12895  sq0  12955  sqeqor  12978  binom2  12979  bcval5  13105  s1co  13579  shftval3  13816  shftidt2  13821  cjne0  13903  sqrt0  13982  abs0  14025  abs00bd  14031  abs2dif  14072  clim0  14237  climz  14280  serclim0  14308  rlimneg  14377  sumrblem  14442  fsumcvg  14443  summolem2a  14446  sumss  14455  fsumss  14456  fsumcvg2  14458  fsumsplit  14471  sumsplit  14499  fsumrelem  14539  fsumrlim  14543  fsumo1  14544  0fallfac  14768  0risefac  14769  binomfallfac  14772  fsumcube  14791  ef0  14821  eftlub  14839  sin0  14879  tan0  14881  divalglem9  15124  sadadd2lem2  15172  sadadd3  15183  bezout  15260  pcmpt2  15597  4sqlem11  15659  ramcl  15733  4001lem2  15849  odadd1  18251  cnaddablx  18271  cnaddabl  18272  cnaddid  18273  frgpnabllem1  18276  cncrng  19767  cnfld0  19770  cnbl0  22577  cnblcld  22578  cnfldnm  22582  xrge0gsumle  22636  xrge0tsms  22637  cnheibor  22754  cnlmod  22940  csscld  23048  clsocv  23049  cnflduss  23152  cnfldcusp  23153  rrxmvallem  23187  rrxmval  23188  mbfss  23413  mbfmulc2lem  23414  0plef  23439  0pledm  23440  itg1ge0  23453  itg1addlem4  23466  itg2splitlem  23515  itg2addlem  23525  ibl0  23553  iblcnlem  23555  iblss2  23572  itgss3  23581  dvconst  23680  dvcnp2  23683  dvrec  23718  dvexp3  23741  dveflem  23742  dvef  23743  dv11cn  23764  lhop1lem  23776  plyun0  23953  plyeq0lem  23966  coeeulem  23980  coeeu  23981  coef3  23988  dgrle  23999  0dgrb  24002  coefv0  24004  coemulc  24011  coe1termlem  24014  coe1term  24015  dgr0  24018  dgrmulc  24027  dgrcolem2  24030  vieta1lem2  24066  iaa  24080  aareccl  24081  aalioulem3  24089  taylthlem2  24128  psercn  24180  pserdvlem2  24182  abelthlem2  24186  abelthlem3  24187  abelthlem5  24189  abelthlem7  24192  abelth  24195  sin2kpi  24235  cos2kpi  24236  sinkpi  24271  efopn  24404  logtayl  24406  cxpval  24410  0cxp  24412  cxpexp  24414  cxpcl  24420  cxpge0  24429  mulcxplem  24430  mulcxp  24431  cxpmul2  24435  dvsqrt  24483  dvcnsqrt  24485  cxpcn3  24489  abscxpbnd  24494  efrlim  24696  ftalem2  24800  ftalem3  24801  ftalem4  24802  ftalem5  24803  ftalem7  24805  prmorcht  24904  muinv  24919  1sgm2ppw  24925  logfacbnd3  24948  logexprlim  24950  dchrelbas2  24962  dchrmulid2  24977  dchrfi  24980  dchrinv  24986  lgsdir2  25055  lgsdir  25057  dchrvmasumiflem1  25190  dchrvmasumiflem2  25191  rpvmasum2  25201  log2sumbnd  25233  selberg2lem  25239  logdivbnd  25245  ax5seglem8  25816  axlowdimlem6  25827  axlowdimlem13  25834  ex-co  27295  avril1  27319  vc0  27429  vcz  27430  cnaddabloOLD  27436  cnidOLD  27437  ipasslem8  27692  siilem2  27707  hvmul0  27881  hi01  27953  norm-iii  27997  h1de2ctlem  28414  pjmuli  28548  pjneli  28582  eigre  28694  eigorth  28697  elnlfn  28787  0cnfn  28839  0lnfn  28844  lnopunilem2  28870  xrge0tsmsd  29785  qqh0  30028  qqhcn  30035  eulerpartlemgs2  30442  sgnneg  30602  breprexpnat  30712  hgt750lem2  30730  subfacp1lem6  31167  sinccvglem  31566  abs2sqle  31574  abs2sqlt  31575  tan2h  33401  poimirlem16  33425  poimirlem19  33428  poimirlem31  33440  mblfinlem2  33447  ovoliunnfl  33451  voliunnfl  33453  dvtanlem  33459  ftc1anclem5  33489  cntotbnd  33595  flcidc  37744  dvconstbi  38533  expgrowth  38534  dvradcnv2  38546  binomcxplemdvbinom  38552  binomcxplemnotnn0  38555  xralrple3  39590  negcncfg  40094  ioodvbdlimc1  40148  ioodvbdlimc2  40150  itgsinexplem1  40169  stoweidlem26  40243  stoweidlem36  40253  stoweidlem55  40272  stirlinglem8  40298  fourierdlem103  40426  sqwvfoura  40445  sqwvfourb  40446  ovn0lem  40779  nn0sumshdiglemA  42413  nn0sumshdiglemB  42414  nn0sumshdiglem1  42415  sec0  42501