Theorem 0cn 11203

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

Assertion

Ref	Expression
0cn	⊢ 0 ∈ ℂ

Proof of Theorem 0cn

Step	Hyp	Ref	Expression
1		ax-i2m1 11175	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 11166	. . . 4 ⊢ i ∈ ℂ
3		mulcl 11191	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 691	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 11165	. . 3 ⊢ 1 ∈ ℂ
6		addcl 11189	. . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
7	4, 5, 6	mp2an 691	. 2 ⊢ ((i · i) + 1) ∈ ℂ
8	1, 7	eqeltrri 2831	1 ⊢ 0 ∈ ℂ

Syntax hints:   ∈ wcel 2107  (class class class)co 7406  ℂcc 11105  0cc0 11107  1c1 11108  ici 11109   + caddc 11110   · cmul 11112

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-mulcl 11169  ax-i2m1 11175

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-clel 2811

This theorem is referenced by:  0cnd  11204  c0ex  11205  1re  11211  00id  11386  mul02lem1  11387  mul02  11389  mul01  11390  addrid  11391  addlid  11394  negcl  11457  subid  11476  subid1  11477  neg0  11503  negid  11504  negsub  11505  subneg  11506  negneg  11507  negeq0  11511  negsubdi  11513  renegcli  11518  mulneg1  11647  msqge0  11732  ixi  11840  muleqadd  11855  div0  11899  ofsubge0  12208  0m0e0  12329  nn0sscn  12474  elznn0  12570  ser0  14017  0exp0e1  14029  0exp  14060  sq0  14153  sqeqor  14177  binom2  14178  bcval5  14275  s1co  14781  shftval3  15020  shftidt2  15025  cjne0  15107  sqrt0  15185  abs0  15229  abs00bd  15235  abs2dif  15276  clim0  15447  climz  15490  serclim0  15518  rlimneg  15590  sumrblem  15654  fsumcvg  15655  summolem2a  15658  sumss  15667  fsumss  15668  fsumcvg2  15670  fsumsplit  15684  sumsplit  15711  fsumrelem  15750  fsumrlim  15754  fsumo1  15755  0fallfac  15978  0risefac  15979  binomfallfac  15982  fsumcube  16001  ef0  16031  eftlub  16049  sin0  16089  tan0  16091  divalglem9  16341  sadadd2lem2  16388  sadadd3  16399  bezout  16482  pcmpt2  16823  4sqlem11  16885  ramcl  16959  4001lem2  17072  odadd1  19711  cnaddablx  19731  cnaddabl  19732  cnaddid  19733  frgpnabllem1  19736  cncrng  20959  cnfld0  20962  cnbl0  24282  cnblcld  24283  cnfldnm  24287  xrge0gsumle  24341  xrge0tsms  24342  cnheibor  24463  cnlmod  24648  csscld  24758  clsocv  24759  cnflduss  24865  cnfldcusp  24866  rrxmvallem  24913  rrxmval  24914  mbfss  25155  mbfmulc2lem  25156  0plef  25181  0pledm  25182  itg1ge0  25195  itg1addlem4  25208  itg1addlem4OLD  25209  itg2splitlem  25258  itg2addlem  25268  ibl0  25296  iblcnlem  25298  iblss2  25315  itgss3  25324  dvconst  25426  dvcnp2  25429  dvrec  25464  dvexp3  25487  dveflem  25488  dv11cn  25510  lhop1lem  25522  plyun0  25703  plyeq0lem  25716  coeeulem  25730  coeeu  25731  coef3  25738  dgrle  25749  0dgrb  25752  coefv0  25754  coemulc  25761  coe1termlem  25764  coe1term  25765  dgr0  25768  dgrmulc  25777  dgrcolem2  25780  vieta1lem2  25816  iaa  25830  aareccl  25831  aalioulem3  25839  taylthlem2  25878  psercn  25930  pserdvlem2  25932  abelthlem2  25936  abelthlem3  25937  abelthlem5  25939  abelthlem7  25942  abelth  25945  sin2kpi  25985  cos2kpi  25986  sinkpi  26023  efopn  26158  logtayl  26160  cxpval  26164  0cxp  26166  cxpexp  26168  cxpcl  26174  cxpge0  26183  mulcxplem  26184  mulcxp  26185  cxpmul2  26189  dvsqrt  26240  dvcnsqrt  26242  cxpcn3  26246  abscxpbnd  26251  efrlim  26464  ftalem2  26568  ftalem3  26569  ftalem4  26570  ftalem5  26571  ftalem7  26573  prmorcht  26672  muinv  26687  1sgm2ppw  26693  logfacbnd3  26716  logexprlim  26718  dchrelbas2  26730  dchrmullid  26745  dchrfi  26748  dchrinv  26754  lgsdir2  26823  lgsdir  26825  addsqnreup  26936  dchrvmasumiflem1  26994  dchrvmasumiflem2  26995  rpvmasum2  27005  log2sumbnd  27037  selberg2lem  27043  logdivbnd  27049  ax5seglem8  28184  axlowdimlem6  28195  axlowdimlem13  28202  ex-co  29681  avril1  29706  vc0  29815  vcz  29816  cnaddabloOLD  29822  cnidOLD  29823  ipasslem8  30078  siilem2  30093  hvmul0  30265  hi01  30337  norm-iii  30381  h1de2ctlem  30796  pjmuli  30930  pjneli  30964  eigre  31076  eigorth  31079  elnlfn  31169  0cnfn  31221  0lnfn  31226  lnopunilem2  31252  xrge0tsmsd  32197  qqh0  32953  qqhcn  32960  eulerpartlemgs2  33368  sgnneg  33528  breprexpnat  33635  hgt750lem2  33653  subfacp1lem6  34165  sinccvglem  34646  abs2sqle  34654  abs2sqlt  34655  gg-dvcnp2  35163  tan2h  36469  poimirlem16  36493  poimirlem19  36496  poimirlem31  36508  mblfinlem2  36515  ovoliunnfl  36519  voliunnfl  36521  dvtanlem  36526  ftc1anclem5  36554  cntotbnd  36653  60lcm7e420  40864  lcmineqlem10  40892  3lexlogpow5ineq1  40908  sn-1ne2  41177  sn-it0e0  41285  addinvcom  41301  sn-0tie0  41309  fltnltalem  41401  flcidc  41902  dvconstbi  43079  expgrowth  43080  dvradcnv2  43092  binomcxplemdvbinom  43098  binomcxplemnotnn0  43101  xralrple3  44071  negcncfg  44584  ioodvbdlimc1  44636  ioodvbdlimc2  44638  itgsinexplem1  44657  stoweidlem26  44729  stoweidlem36  44739  stoweidlem55  44758  stirlinglem8  44784  fourierdlem103  44912  sqwvfoura  44931  sqwvfourb  44932  ovn0lem  45268  nn0sumshdiglemA  47259  nn0sumshdiglemB  47260  nn0sumshdiglem1  47261  sec0  47759