Theorem 0cn 9588

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 9560	. 2 |- ( ( _i x. _i ) + 1 ) = 0
2		ax-icn 9551	. . . 4 |- _i e. CC
3		mulcl 9576	. . . 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 9550	. . 3 |- 1 e. CC
6		addcl 9574	. . 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 2552	1 |- 0 e. CC

Syntax hints:   e. wcel 1767  (class class class)co 6284   CCcc 9490   0cc0 9492   1c1 9493   _ici 9494   + caddc 9495   x. cmul 9497

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-ext 2445  ax-1cn 9550  ax-icn 9551  ax-addcl 9552  ax-mulcl 9554  ax-i2m1 9560

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-cleq 2459  df-clel 2462

This theorem is referenced by:  0cnd  9589  c0ex  9590  1re  9595  00id  9754  mul02lem1  9755  mul02  9757  mul01  9758  addid1  9759  addid2  9762  negcl  9820  subid  9838  subid1  9839  neg0  9865  negid  9866  negsub  9867  subneg  9868  negneg  9869  negeq0  9873  negsubdi  9875  renegcli  9880  mulneg1  9993  msqge0  10074  ixi  10178  muleqadd  10193  div0  10235  ofsubge0  10535  0m0e0  10645  elznn0  10879  ser0  12127  0exp0e1  12139  0exp  12169  sq0  12227  sqeqor  12250  binom2  12251  bcval5  12364  s1co  12762  shftval3  12872  shftidt2  12877  cjne0  12959  sqrt0  13038  abs0  13081  abs00bd  13087  abs2dif  13128  clim0  13292  climz  13335  serclim0  13363  rlimneg  13432  sumrblem  13496  fsumcvg  13497  summolem2a  13500  sumss  13509  fsumss  13510  fsumcvg2  13512  fsumsplit  13525  sumsplit  13546  fsumrelem  13584  fsumrlim  13588  fsumo1  13589  ef0  13688  eftlub  13705  sin0  13745  tan0  13747  divalglem9  13918  sadadd2lem2  13959  sadadd3  13970  bezout  14039  pcmpt2  14271  prmreclem2  14294  4sqlem11  14332  ramcl  14406  odadd1  16657  cnaddablx  16677  cnaddabl  16678  frgpnabllem1  16680  cncrng  18238  cnfld0  18241  cnbl0  21044  cnblcld  21045  cnfldnm  21049  xrge0gsumle  21101  xrge0tsms  21102  cnheibor  21218  csscld  21452  clsocv  21453  cnflduss  21559  cnfldcusp  21560  rrxmvallem  21594  rrxmval  21595  mbfss  21816  mbfmulc2lem  21817  0plef  21842  0pledm  21843  itg1ge0  21856  itg1addlem4  21869  itg2splitlem  21918  itg2addlem  21928  ibl0  21956  iblcnlem  21958  iblss2  21975  itgss3  21984  dvconst  22083  dvcnp2  22086  dvrec  22121  dvexp3  22142  dveflem  22143  dvef  22144  dv11cn  22165  lhop1lem  22177  plyun0  22357  plyeq0lem  22370  coeeulem  22384  coeeu  22385  coef3  22392  dgrle  22403  0dgrb  22406  coefv0  22407  coemulc  22414  coe1termlem  22417  coe1term  22418  dgr0  22421  dgrmulc  22430  dgrcolem2  22433  vieta1lem2  22469  iaa  22483  aareccl  22484  aalioulem3  22492  taylthlem2  22531  psercn  22583  pserdvlem2  22585  abelthlem2  22589  abelthlem3  22590  abelthlem5  22592  abelthlem7  22595  abelth  22598  sin2kpi  22637  cos2kpi  22638  sinkpi  22673  efopn  22795  logtayl  22797  cxpval  22801  0cxp  22803  cxpexp  22805  cxpcl  22811  cxpge0  22820  mulcxplem  22821  mulcxp  22822  cxpmul2  22826  dvsqrt  22874  cxpcn3  22878  abscxpbnd  22883  efrlim  23055  ftalem2  23103  ftalem3  23104  ftalem4  23105  ftalem5  23106  ftalem7  23108  prmorcht  23208  muinv  23225  1sgm2ppw  23231  logfacbnd3  23254  logexprlim  23256  dchrelbas2  23268  dchrmulid2  23283  dchrfi  23286  dchrinv  23292  lgsdir2  23359  lgsdir  23361  dchrvmasumiflem1  23442  dchrvmasumiflem2  23443  rpvmasum2  23453  log2sumbnd  23485  selberg2lem  23491  logdivbnd  23497  ax5seglem8  23943  axlowdimlem6  23954  axlowdimlem13  23961  ex-co  24864  avril1  24875  cnaddablo  25056  cnid  25057  addinv  25058  vc0  25166  vcz  25167  vcoprne  25176  ipasslem8  25456  siilem2  25471  hvmul0  25645  hi01  25717  norm-iii  25761  h1de2ctlem  26177  pjmuli  26311  pjneli  26345  eigre  26458  eigorth  26461  elnlfn  26551  0cnfn  26603  0lnfn  26608  lnopunilem2  26634  xrge0tsmsd  27466  qqh0  27629  qqhcn  27636  eulerpartlemgs2  27987  sgnneg  28147  subfacp1lem6  28297  sinccvglem  28541  abs2sqle  28549  abs2sqlt  28550  0fallfac  28764  0risefac  28765  binomfallfac  28768  fsumcube  29427  tan2h  29652  mblfinlem2  29657  ovoliunnfl  29661  voliunnfl  29663  ftc1anclem5  29699  dvcnsqrt  29706  cntotbnd  29923  flcidc  30756  dvconstbi  30867  expgrowth  30868  ellimcabssub0  31187  0ellimcdiv  31219  clim0cf  31224  negcncfg  31247  dvsinax  31269  dvasinbx  31278  ioodvbdlimc1  31291  ioodvbdlimc2  31293  itgsinexplem1  31299  itgiccshift  31326  itgperiod  31327  itgsbtaddcnst  31328  stoweidlem26  31354  stoweidlem36  31364  stoweidlem55  31383  stirlinglem8  31409  dirkertrigeqlem2  31427  fourierdlem59  31494  fourierdlem74  31509  fourierdlem75  31510  fourierdlem103  31538  sec0  32253