Theorem 0cn 9635

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

Assertion

Ref	Expression
0cn	|- 0 e. CC

Proof of Theorem 0cn

Step	Hyp	Ref	Expression
1		ax-i2m1 9607	. 2 |- ( ( _i x. _i ) + 1 ) = 0
2		ax-icn 9598	. . . 4 |- _i e. CC
3		mulcl 9623	. . . 4 |- ( ( _i e. CC /\ _i e. CC ) -> ( _i x. _i ) e. CC )
4	2, 2, 3	mp2an 678	. . 3 |- ( _i x. _i ) e. CC
5		ax-1cn 9597	. . 3 |- 1 e. CC
6		addcl 9621	. . 3 |- ( ( ( _i x. _i ) e. CC /\ 1 e. CC ) -> ( ( _i x. _i ) + 1 ) e. CC )
7	4, 5, 6	mp2an 678	. 2 |- ( ( _i x. _i ) + 1 ) e. CC
8	1, 7	eqeltrri 2526	1 |- 0 e. CC

Syntax hints:   e. wcel 1887  (class class class)co 6290   CCcc 9537   0cc0 9539   1c1 9540   _ici 9541   + caddc 9542   x. cmul 9544

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-ext 2431  ax-1cn 9597  ax-icn 9598  ax-addcl 9599  ax-mulcl 9601  ax-i2m1 9607

This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1664  df-cleq 2444  df-clel 2447

This theorem is referenced by:  0cnd  9636  c0ex  9637  1re  9642  00id  9808  mul02lem1  9809  mul02  9811  mul01  9812  addid1  9813  addid2  9816  negcl  9875  subid  9893  subid1  9894  neg0  9920  negid  9921  negsub  9922  subneg  9923  negneg  9924  negeq0  9928  negsubdi  9930  renegcli  9935  mulneg1  10055  msqge0  10135  ixi  10241  muleqadd  10256  div0  10298  ofsubge0  10608  0m0e0  10719  elznn0  10952  ser0  12265  0exp0e1  12277  0exp  12307  sq0  12366  sqeqor  12388  binom2  12389  bcval5  12503  s1co  12930  shftval3  13139  shftidt2  13144  cjne0  13226  sqrt0  13305  abs0  13348  abs00bd  13354  abs2dif  13395  clim0  13570  climz  13613  serclim0  13641  rlimneg  13710  sumrblem  13777  fsumcvg  13778  summolem2a  13781  sumss  13790  fsumss  13791  fsumcvg2  13793  fsumsplit  13806  sumsplit  13829  fsumrelem  13867  fsumrlim  13871  fsumo1  13872  0fallfac  14090  0risefac  14091  binomfallfac  14094  fsumcube  14113  ef0  14145  eftlub  14163  sin0  14203  tan0  14205  divalglem9  14381  divalglem9OLD  14382  sadadd2lem2  14424  sadadd3  14435  bezout  14510  pcmpt2  14838  prmreclem2  14861  4sqlem11  14899  ramcl  14987  odadd1  17486  cnaddablx  17506  cnaddabl  17507  frgpnabllem1  17509  cncrng  18989  cnfld0  18992  cnbl0  21794  cnblcld  21795  cnfldnm  21799  xrge0gsumle  21851  xrge0tsms  21852  cnheibor  21983  csscld  22220  clsocv  22221  cnflduss  22323  cnfldcusp  22324  rrxmvallem  22358  rrxmval  22359  mbfss  22602  mbfmulc2lem  22603  0plef  22630  0pledm  22631  itg1ge0  22644  itg1addlem4  22657  itg2splitlem  22706  itg2addlem  22716  ibl0  22744  iblcnlem  22746  iblss2  22763  itgss3  22772  dvconst  22871  dvcnp2  22874  dvrec  22909  dvexp3  22930  dveflem  22931  dvef  22932  dv11cn  22953  lhop1lem  22965  plyun0  23151  plyeq0lem  23164  coeeulem  23178  coeeu  23179  coef3  23186  dgrle  23197  0dgrb  23200  coefv0  23202  coemulc  23209  coe1termlem  23212  coe1term  23213  dgr0  23216  dgrmulc  23225  dgrcolem2  23228  vieta1lem2  23264  iaa  23281  aareccl  23282  aalioulem3  23290  taylthlem2  23329  psercn  23381  pserdvlem2  23383  abelthlem2  23387  abelthlem3  23388  abelthlem5  23390  abelthlem7  23393  abelth  23396  sin2kpi  23438  cos2kpi  23439  sinkpi  23474  efopn  23603  logtayl  23605  cxpval  23609  0cxp  23611  cxpexp  23613  cxpcl  23619  cxpge0  23628  mulcxplem  23629  mulcxp  23630  cxpmul2  23634  dvsqrt  23682  dvcnsqrt  23684  cxpcn3  23688  abscxpbnd  23693  efrlim  23895  ftalem2  23998  ftalem3  23999  ftalem4  24000  ftalem5  24001  ftalem4OLD  24002  ftalem5OLD  24003  ftalem7  24005  prmorcht  24105  muinv  24122  1sgm2ppw  24128  logfacbnd3  24151  logexprlim  24153  dchrelbas2  24165  dchrmulid2  24180  dchrfi  24183  dchrinv  24189  lgsdir2  24256  lgsdir  24258  dchrvmasumiflem1  24339  dchrvmasumiflem2  24340  rpvmasum2  24350  log2sumbnd  24382  selberg2lem  24388  logdivbnd  24394  ax5seglem8  24966  axlowdimlem6  24977  axlowdimlem13  24984  ex-co  25888  avril1  25900  cnaddablo  26078  cnid  26079  addinv  26080  vc0  26188  vcz  26189  vcoprne  26198  ipasslem8  26478  siilem2  26493  hvmul0  26677  hi01  26749  norm-iii  26793  h1de2ctlem  27208  pjmuli  27342  pjneli  27376  eigre  27488  eigorth  27491  elnlfn  27581  0cnfn  27633  0lnfn  27638  lnopunilem2  27664  xrge0tsmsd  28548  qqh0  28788  qqhcn  28795  eulerpartlemgs2  29213  sgnneg  29411  subfacp1lem6  29908  sinccvglem  30316  abs2sqle  30324  abs2sqlt  30325  tan2h  31937  poimirlem16  31956  poimirlem19  31959  poimirlem31  31971  mblfinlem2  31978  ovoliunnfl  31982  voliunnfl  31984  dvtanlem  31990  ftc1anclem5  32021  cntotbnd  32128  flcidc  36040  dvconstbi  36683  expgrowth  36684  dvradcnv2  36696  binomcxplemdvbinom  36702  binomcxplemnotnn0  36705  negcncfg  37758  ioodvbdlimc1  37807  ioodvbdlimc2  37810  itgsinexplem1  37830  stoweidlem26  37886  stoweidlem36  37897  stoweidlem55  37916  stirlinglem8  37943  fourierdlem103  38073  sqwvfoura  38092  sqwvfourb  38093  ovn0lem  38387  nn0sumshdiglemA  40483  nn0sumshdiglemB  40484  nn0sumshdiglem1  40485  sec0  40533