Theorem 0cn 9577

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

Assertion

Ref	Expression
0cn	|- 0 e. CC

Proof of Theorem 0cn

Step	Hyp	Ref	Expression
1		ax-i2m1 9549	. 2 |- ( ( _i x. _i ) + 1 ) = 0
2		ax-icn 9540	. . . 4 |- _i e. CC
3		mulcl 9565	. . . 4 |- ( ( _i e. CC /\ _i e. CC ) -> ( _i x. _i ) e. CC )
4	2, 2, 3	mp2an 670	. . 3 |- ( _i x. _i ) e. CC
5		ax-1cn 9539	. . 3 |- 1 e. CC
6		addcl 9563	. . 3 |- ( ( ( _i x. _i ) e. CC /\ 1 e. CC ) -> ( ( _i x. _i ) + 1 ) e. CC )
7	4, 5, 6	mp2an 670	. 2 |- ( ( _i x. _i ) + 1 ) e. CC
8	1, 7	eqeltrri 2539	1 |- 0 e. CC

Syntax hints:   e. wcel 1823  (class class class)co 6270   CCcc 9479   0cc0 9481   1c1 9482   _ici 9483   + caddc 9484   x. cmul 9486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-ext 2432  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-mulcl 9543  ax-i2m1 9549

This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1618  df-cleq 2446  df-clel 2449

This theorem is referenced by:  0cnd  9578  c0ex  9579  1re  9584  00id  9744  mul02lem1  9745  mul02  9747  mul01  9748  addid1  9749  addid2  9752  negcl  9811  subid  9829  subid1  9830  neg0  9856  negid  9857  negsub  9858  subneg  9859  negneg  9860  negeq0  9864  negsubdi  9866  renegcli  9871  mulneg1  9989  msqge0  10070  ixi  10174  muleqadd  10189  div0  10231  ofsubge0  10530  0m0e0  10641  elznn0  10875  ser0  12141  0exp0e1  12153  0exp  12183  sq0  12241  sqeqor  12264  binom2  12265  bcval5  12378  s1co  12790  shftval3  12991  shftidt2  12996  cjne0  13078  sqrt0  13157  abs0  13200  abs00bd  13206  abs2dif  13247  clim0  13411  climz  13454  serclim0  13482  rlimneg  13551  sumrblem  13615  fsumcvg  13616  summolem2a  13619  sumss  13628  fsumss  13629  fsumcvg2  13631  fsumsplit  13644  sumsplit  13665  fsumrelem  13703  fsumrlim  13707  fsumo1  13708  ef0  13908  eftlub  13926  sin0  13966  tan0  13968  divalglem9  14143  sadadd2lem2  14184  sadadd3  14195  bezout  14264  pcmpt2  14496  prmreclem2  14519  4sqlem11  14557  ramcl  14631  odadd1  17053  cnaddablx  17073  cnaddabl  17074  frgpnabllem1  17076  cncrng  18634  cnfld0  18637  cnbl0  21447  cnblcld  21448  cnfldnm  21452  xrge0gsumle  21504  xrge0tsms  21505  cnheibor  21621  csscld  21855  clsocv  21856  cnflduss  21962  cnfldcusp  21963  rrxmvallem  21997  rrxmval  21998  mbfss  22219  mbfmulc2lem  22220  0plef  22245  0pledm  22246  itg1ge0  22259  itg1addlem4  22272  itg2splitlem  22321  itg2addlem  22331  ibl0  22359  iblcnlem  22361  iblss2  22378  itgss3  22387  dvconst  22486  dvcnp2  22489  dvrec  22524  dvexp3  22545  dveflem  22546  dvef  22547  dv11cn  22568  lhop1lem  22580  plyun0  22760  plyeq0lem  22773  coeeulem  22787  coeeu  22788  coef3  22795  dgrle  22806  0dgrb  22809  coefv0  22811  coemulc  22818  coe1termlem  22821  coe1term  22822  dgr0  22825  dgrmulc  22834  dgrcolem2  22837  vieta1lem2  22873  iaa  22887  aareccl  22888  aalioulem3  22896  taylthlem2  22935  psercn  22987  pserdvlem2  22989  abelthlem2  22993  abelthlem3  22994  abelthlem5  22996  abelthlem7  22999  abelth  23002  sin2kpi  23042  cos2kpi  23043  sinkpi  23078  efopn  23207  logtayl  23209  cxpval  23213  0cxp  23215  cxpexp  23217  cxpcl  23223  cxpge0  23232  mulcxplem  23233  mulcxp  23234  cxpmul2  23238  dvsqrt  23286  cxpcn3  23290  abscxpbnd  23295  efrlim  23497  ftalem2  23545  ftalem3  23546  ftalem4  23547  ftalem5  23548  ftalem7  23550  prmorcht  23650  muinv  23667  1sgm2ppw  23673  logfacbnd3  23696  logexprlim  23698  dchrelbas2  23710  dchrmulid2  23725  dchrfi  23728  dchrinv  23734  lgsdir2  23801  lgsdir  23803  dchrvmasumiflem1  23884  dchrvmasumiflem2  23885  rpvmasum2  23895  log2sumbnd  23927  selberg2lem  23933  logdivbnd  23939  ax5seglem8  24441  axlowdimlem6  24452  axlowdimlem13  24459  ex-co  25361  avril1  25373  cnaddablo  25550  cnid  25551  addinv  25552  vc0  25660  vcz  25661  vcoprne  25670  ipasslem8  25950  siilem2  25965  hvmul0  26139  hi01  26211  norm-iii  26255  h1de2ctlem  26671  pjmuli  26805  pjneli  26839  eigre  26952  eigorth  26955  elnlfn  27045  0cnfn  27097  0lnfn  27102  lnopunilem2  27128  xrge0tsmsd  28010  qqh0  28199  qqhcn  28206  eulerpartlemgs2  28583  sgnneg  28743  subfacp1lem6  28893  sinccvglem  29302  abs2sqle  29310  abs2sqlt  29311  0fallfac  29400  0risefac  29401  binomfallfac  29404  fsumcube  30050  tan2h  30287  mblfinlem2  30292  ovoliunnfl  30296  voliunnfl  30298  ftc1anclem5  30334  dvcnsqrt  30341  cntotbnd  30532  flcidc  31364  dvconstbi  31480  expgrowth  31481  dvradcnv2  31493  binomcxplemdvbinom  31499  binomcxplemnotnn0  31502  negcncfg  31922  ioodvbdlimc1  31969  ioodvbdlimc2  31971  itgsinexplem1  31991  stoweidlem26  32047  stoweidlem36  32057  stoweidlem55  32076  stirlinglem8  32102  fourierdlem103  32231  sqwvfoura  32250  sqwvfourb  32251  nn0sumshdiglemA  33494  nn0sumshdiglemB  33495  nn0sumshdiglem1  33496  sec0  33544