Theorem 0cn 9365

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

Assertion

Ref	Expression
0cn	|- 0 e. CC

Proof of Theorem 0cn

Step	Hyp	Ref	Expression
1		ax-i2m1 9337	. 2 |- ( ( _i x. _i ) + 1 ) = 0
2		ax-icn 9328	. . . 4 |- _i e. CC
3		mulcl 9353	. . . 4 |- ( ( _i e. CC /\ _i e. CC ) -> ( _i x. _i ) e. CC )
4	2, 2, 3	mp2an 665	. . 3 |- ( _i x. _i ) e. CC
5		ax-1cn 9327	. . 3 |- 1 e. CC
6		addcl 9351	. . 3 |- ( ( ( _i x. _i ) e. CC /\ 1 e. CC ) -> ( ( _i x. _i ) + 1 ) e. CC )
7	4, 5, 6	mp2an 665	. 2 |- ( ( _i x. _i ) + 1 ) e. CC
8	1, 7	eqeltrri 2504	1 |- 0 e. CC

Syntax hints:   e. wcel 1755  (class class class)co 6080   CCcc 9267   0cc0 9269   1c1 9270   _ici 9271   + caddc 9272   x. cmul 9274

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791  ax-ext 2414  ax-1cn 9327  ax-icn 9328  ax-addcl 9329  ax-mulcl 9331  ax-i2m1 9337

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-cleq 2426  df-clel 2429

This theorem is referenced by:  0cnd  9366  c0ex  9367  1re  9372  00id  9531  mul02lem1  9532  mul02  9534  mul01  9535  addid1  9536  addid2  9539  negcl  9597  subid  9615  subid1  9616  neg0  9642  negid  9643  negsub  9644  subneg  9645  negneg  9646  negeq0  9650  negsubdi  9652  renegcli  9657  mulneg1  9768  msqge0  9848  ixi  9952  muleqadd  9967  div0  10009  ofsubge0  10308  0m0e0  10418  elznn0  10648  ser0  11841  0exp0e1  11853  0exp  11882  sq0  11940  sqeqor  11963  binom2  11964  bcval5  12077  s1co  12444  shftval3  12548  shftidt2  12553  cjne0  12635  sqr0  12714  abs0  12757  abs00bd  12763  abs2dif  12803  clim0  12967  climz  13010  serclim0  13038  rlimneg  13107  sumrblem  13171  fsumcvg  13172  summolem2a  13175  sumss  13184  fsumss  13185  fsumcvg2  13187  fsumsplit  13199  sumsplit  13218  fsumrelem  13252  fsumrlim  13256  fsumo1  13257  ef0  13358  eftlub  13375  sin0  13415  tan0  13417  divalglem9  13587  sadadd2lem2  13628  sadadd3  13639  bezout  13708  pcmpt2  13937  prmreclem2  13960  4sqlem11  13998  ramcl  14072  odadd1  16309  cnaddablx  16327  cnaddabl  16328  frgpnabllem1  16330  cncrng  17680  cnfld0  17683  cnbl0  20194  cnblcld  20195  cnfldnm  20199  xrge0gsumle  20251  xrge0tsms  20252  cnheibor  20368  csscld  20602  clsocv  20603  cnflduss  20709  cnfldcusp  20710  rrxmvallem  20744  rrxmval  20745  mbfss  20965  mbfmulc2lem  20966  0plef  20991  0pledm  20992  itg1ge0  21005  itg1addlem4  21018  itg2splitlem  21067  itg2addlem  21077  ibl0  21105  iblcnlem  21107  iblss2  21124  itgss3  21133  dvconst  21232  dvcnp2  21235  dvrec  21270  dvexp3  21291  dveflem  21292  dvef  21293  dv11cn  21314  lhop1lem  21326  plyun0  21549  plyeq0lem  21562  coeeulem  21576  coeeu  21577  coef3  21584  dgrle  21595  0dgrb  21598  coefv0  21599  coemulc  21606  coe1termlem  21609  coe1term  21610  dgr0  21613  dgrmulc  21622  dgrcolem2  21625  vieta1lem2  21661  iaa  21675  aareccl  21676  aalioulem3  21684  taylthlem2  21723  psercn  21775  pserdvlem2  21777  abelthlem2  21781  abelthlem3  21782  abelthlem5  21784  abelthlem7  21787  abelth  21790  sin2kpi  21829  cos2kpi  21830  sinkpi  21865  efopn  21987  logtayl  21989  cxpval  21993  0cxp  21995  cxpexp  21997  cxpcl  22003  cxpge0  22012  mulcxplem  22013  mulcxp  22014  cxpmul2  22018  dvsqr  22066  cxpcn3  22070  abscxpbnd  22075  efrlim  22247  ftalem2  22295  ftalem3  22296  ftalem4  22297  ftalem5  22298  ftalem7  22300  prmorcht  22400  muinv  22417  1sgm2ppw  22423  logfacbnd3  22446  logexprlim  22448  dchrelbas2  22460  dchrmulid2  22475  dchrfi  22478  dchrinv  22484  lgsdir2  22551  lgsdir  22553  dchrvmasumiflem1  22634  dchrvmasumiflem2  22635  rpvmasum2  22645  log2sumbnd  22677  selberg2lem  22683  logdivbnd  22689  ax5seglem8  23004  axlowdimlem6  23015  axlowdimlem13  23022  ex-co  23467  avril1  23478  cnaddablo  23659  cnid  23660  addinv  23661  vc0  23769  vcz  23770  vcoprne  23779  ipasslem8  24059  siilem2  24074  hvmul0  24248  hi01  24320  norm-iii  24364  h1de2ctlem  24780  pjmuli  24914  pjneli  24948  eigre  25061  eigorth  25064  elnlfn  25154  0cnfn  25206  0lnfn  25211  lnopunilem2  25237  xrge0tsmsd  26105  qqh0  26266  qqhcn  26273  eulerpartlemgs2  26610  sgnneg  26770  subfacp1lem6  26920  sinccvglem  27163  abs2sqle  27171  abs2sqlt  27172  0fallfac  27386  0risefac  27387  binomfallfac  27390  fsumcube  28049  tan2h  28265  mblfinlem2  28270  ovoliunnfl  28274  voliunnfl  28276  ftc1anclem5  28312  dvcnsqr  28319  cntotbnd  28536  flcidc  29373  dvconstbi  29450  expgrowth  29451  itgsinexplem1  29637  stoweidlem26  29664  stoweidlem36  29674  stoweidlem55  29693  stirlinglem8  29719  sec0  30801