Theorem 0cn 10967

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

Assertion

Ref	Expression
0cn	⊢ 0 ∈ ℂ

Proof of Theorem 0cn

Step	Hyp	Ref	Expression
1		ax-i2m1 10939	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 10930	. . . 4 ⊢ i ∈ ℂ
3		mulcl 10955	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 689	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 10929	. . 3 ⊢ 1 ∈ ℂ
6		addcl 10953	. . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
7	4, 5, 6	mp2an 689	. 2 ⊢ ((i · i) + 1) ∈ ℂ
8	1, 7	eqeltrri 2836	1 ⊢ 0 ∈ ℂ

Syntax hints:   ∈ wcel 2106  (class class class)co 7275  ℂcc 10869  0cc0 10871  1c1 10872  ici 10873   + caddc 10874   · cmul 10876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-mulcl 10933  ax-i2m1 10939

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730  df-clel 2816

This theorem is referenced by:  0cnd  10968  c0ex  10969  1re  10975  00id  11150  mul02lem1  11151  mul02  11153  mul01  11154  addid1  11155  addid2  11158  negcl  11221  subid  11240  subid1  11241  neg0  11267  negid  11268  negsub  11269  subneg  11270  negneg  11271  negeq0  11275  negsubdi  11277  renegcli  11282  mulneg1  11411  msqge0  11496  ixi  11604  muleqadd  11619  div0  11663  ofsubge0  11972  0m0e0  12093  nn0sscn  12238  elznn0  12334  ser0  13775  0exp0e1  13787  0exp  13818  sq0  13909  sqeqor  13932  binom2  13933  bcval5  14032  s1co  14546  shftval3  14787  shftidt2  14792  cjne0  14874  sqrt0  14953  abs0  14997  abs00bd  15003  abs2dif  15044  clim0  15215  climz  15258  serclim0  15286  rlimneg  15358  sumrblem  15423  fsumcvg  15424  summolem2a  15427  sumss  15436  fsumss  15437  fsumcvg2  15439  fsumsplit  15453  sumsplit  15480  fsumrelem  15519  fsumrlim  15523  fsumo1  15524  0fallfac  15747  0risefac  15748  binomfallfac  15751  fsumcube  15770  ef0  15800  eftlub  15818  sin0  15858  tan0  15860  divalglem9  16110  sadadd2lem2  16157  sadadd3  16168  bezout  16251  pcmpt2  16594  4sqlem11  16656  ramcl  16730  4001lem2  16843  odadd1  19449  cnaddablx  19469  cnaddabl  19470  cnaddid  19471  frgpnabllem1  19474  cncrng  20619  cnfld0  20622  cnbl0  23937  cnblcld  23938  cnfldnm  23942  xrge0gsumle  23996  xrge0tsms  23997  cnheibor  24118  cnlmod  24303  csscld  24413  clsocv  24414  cnflduss  24520  cnfldcusp  24521  rrxmvallem  24568  rrxmval  24569  mbfss  24810  mbfmulc2lem  24811  0plef  24836  0pledm  24837  itg1ge0  24850  itg1addlem4  24863  itg1addlem4OLD  24864  itg2splitlem  24913  itg2addlem  24923  ibl0  24951  iblcnlem  24953  iblss2  24970  itgss3  24979  dvconst  25081  dvcnp2  25084  dvrec  25119  dvexp3  25142  dveflem  25143  dv11cn  25165  lhop1lem  25177  plyun0  25358  plyeq0lem  25371  coeeulem  25385  coeeu  25386  coef3  25393  dgrle  25404  0dgrb  25407  coefv0  25409  coemulc  25416  coe1termlem  25419  coe1term  25420  dgr0  25423  dgrmulc  25432  dgrcolem2  25435  vieta1lem2  25471  iaa  25485  aareccl  25486  aalioulem3  25494  taylthlem2  25533  psercn  25585  pserdvlem2  25587  abelthlem2  25591  abelthlem3  25592  abelthlem5  25594  abelthlem7  25597  abelth  25600  sin2kpi  25640  cos2kpi  25641  sinkpi  25678  efopn  25813  logtayl  25815  cxpval  25819  0cxp  25821  cxpexp  25823  cxpcl  25829  cxpge0  25838  mulcxplem  25839  mulcxp  25840  cxpmul2  25844  dvsqrt  25895  dvcnsqrt  25897  cxpcn3  25901  abscxpbnd  25906  efrlim  26119  ftalem2  26223  ftalem3  26224  ftalem4  26225  ftalem5  26226  ftalem7  26228  prmorcht  26327  muinv  26342  1sgm2ppw  26348  logfacbnd3  26371  logexprlim  26373  dchrelbas2  26385  dchrmulid2  26400  dchrfi  26403  dchrinv  26409  lgsdir2  26478  lgsdir  26480  addsqnreup  26591  dchrvmasumiflem1  26649  dchrvmasumiflem2  26650  rpvmasum2  26660  log2sumbnd  26692  selberg2lem  26698  logdivbnd  26704  ax5seglem8  27304  axlowdimlem6  27315  axlowdimlem13  27322  ex-co  28802  avril1  28827  vc0  28936  vcz  28937  cnaddabloOLD  28943  cnidOLD  28944  ipasslem8  29199  siilem2  29214  hvmul0  29386  hi01  29458  norm-iii  29502  h1de2ctlem  29917  pjmuli  30051  pjneli  30085  eigre  30197  eigorth  30200  elnlfn  30290  0cnfn  30342  0lnfn  30347  lnopunilem2  30373  xrge0tsmsd  31317  qqh0  31934  qqhcn  31941  eulerpartlemgs2  32347  sgnneg  32507  breprexpnat  32614  hgt750lem2  32632  subfacp1lem6  33147  sinccvglem  33630  abs2sqle  33638  abs2sqlt  33639  tan2h  35769  poimirlem16  35793  poimirlem19  35796  poimirlem31  35808  mblfinlem2  35815  ovoliunnfl  35819  voliunnfl  35821  dvtanlem  35826  ftc1anclem5  35854  cntotbnd  35954  60lcm7e420  40018  lcmineqlem10  40046  3lexlogpow5ineq1  40062  sn-1ne2  40295  sn-it0e0  40397  addinvcom  40413  sn-0tie0  40421  fltnltalem  40499  flcidc  40999  dvconstbi  41952  expgrowth  41953  dvradcnv2  41965  binomcxplemdvbinom  41971  binomcxplemnotnn0  41974  xralrple3  42913  negcncfg  43422  ioodvbdlimc1  43474  ioodvbdlimc2  43476  itgsinexplem1  43495  stoweidlem26  43567  stoweidlem36  43577  stoweidlem55  43596  stirlinglem8  43622  fourierdlem103  43750  sqwvfoura  43769  sqwvfourb  43770  ovn0lem  44103  nn0sumshdiglemA  45965  nn0sumshdiglemB  45966  nn0sumshdiglem1  45967  sec0  46462