Theorem 0cn 11206

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

Assertion

Ref	Expression
0cn	⊢ 0 ∈ ℂ

Proof of Theorem 0cn

Step	Hyp	Ref	Expression
1		ax-i2m1 11178	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 11169	. . . 4 ⊢ i ∈ ℂ
3		mulcl 11194	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 691	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 11168	. . 3 ⊢ 1 ∈ ℂ
6		addcl 11192	. . 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 7409  ℂcc 11108  0cc0 11110  1c1 11111  ici 11112   + caddc 11113   · cmul 11115

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 11168  ax-icn 11169  ax-addcl 11170  ax-mulcl 11172  ax-i2m1 11178

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  11207  c0ex  11208  1re  11214  00id  11389  mul02lem1  11390  mul02  11392  mul01  11393  addrid  11394  addlid  11397  negcl  11460  subid  11479  subid1  11480  neg0  11506  negid  11507  negsub  11508  subneg  11509  negneg  11510  negeq0  11514  negsubdi  11516  renegcli  11521  mulneg1  11650  msqge0  11735  ixi  11843  muleqadd  11858  div0  11902  ofsubge0  12211  0m0e0  12332  nn0sscn  12477  elznn0  12573  ser0  14020  0exp0e1  14032  0exp  14063  sq0  14156  sqeqor  14180  binom2  14181  bcval5  14278  s1co  14784  shftval3  15023  shftidt2  15028  cjne0  15110  sqrt0  15188  abs0  15232  abs00bd  15238  abs2dif  15279  clim0  15450  climz  15493  serclim0  15521  rlimneg  15593  sumrblem  15657  fsumcvg  15658  summolem2a  15661  sumss  15670  fsumss  15671  fsumcvg2  15673  fsumsplit  15687  sumsplit  15714  fsumrelem  15753  fsumrlim  15757  fsumo1  15758  0fallfac  15981  0risefac  15982  binomfallfac  15985  fsumcube  16004  ef0  16034  eftlub  16052  sin0  16092  tan0  16094  divalglem9  16344  sadadd2lem2  16391  sadadd3  16402  bezout  16485  pcmpt2  16826  4sqlem11  16888  ramcl  16962  4001lem2  17075  odadd1  19716  cnaddablx  19736  cnaddabl  19737  cnaddid  19738  frgpnabllem1  19741  cncrng  20966  cnfld0  20969  cnbl0  24290  cnblcld  24291  cnfldnm  24295  xrge0gsumle  24349  xrge0tsms  24350  cnheibor  24471  cnlmod  24656  csscld  24766  clsocv  24767  cnflduss  24873  cnfldcusp  24874  rrxmvallem  24921  rrxmval  24922  mbfss  25163  mbfmulc2lem  25164  0plef  25189  0pledm  25190  itg1ge0  25203  itg1addlem4  25216  itg1addlem4OLD  25217  itg2splitlem  25266  itg2addlem  25276  ibl0  25304  iblcnlem  25306  iblss2  25323  itgss3  25332  dvconst  25434  dvcnp2  25437  dvrec  25472  dvexp3  25495  dveflem  25496  dv11cn  25518  lhop1lem  25530  plyun0  25711  plyeq0lem  25724  coeeulem  25738  coeeu  25739  coef3  25746  dgrle  25757  0dgrb  25760  coefv0  25762  coemulc  25769  coe1termlem  25772  coe1term  25773  dgr0  25776  dgrmulc  25785  dgrcolem2  25788  vieta1lem2  25824  iaa  25838  aareccl  25839  aalioulem3  25847  taylthlem2  25886  psercn  25938  pserdvlem2  25940  abelthlem2  25944  abelthlem3  25945  abelthlem5  25947  abelthlem7  25950  abelth  25953  sin2kpi  25993  cos2kpi  25994  sinkpi  26031  efopn  26166  logtayl  26168  cxpval  26172  0cxp  26174  cxpexp  26176  cxpcl  26182  cxpge0  26191  mulcxplem  26192  mulcxp  26193  cxpmul2  26197  dvsqrt  26250  dvcnsqrt  26252  cxpcn3  26256  abscxpbnd  26261  efrlim  26474  ftalem2  26578  ftalem3  26579  ftalem4  26580  ftalem5  26581  ftalem7  26583  prmorcht  26682  muinv  26697  1sgm2ppw  26703  logfacbnd3  26726  logexprlim  26728  dchrelbas2  26740  dchrmullid  26755  dchrfi  26758  dchrinv  26764  lgsdir2  26833  lgsdir  26835  addsqnreup  26946  dchrvmasumiflem1  27004  dchrvmasumiflem2  27005  rpvmasum2  27015  log2sumbnd  27047  selberg2lem  27053  logdivbnd  27059  ax5seglem8  28194  axlowdimlem6  28205  axlowdimlem13  28212  ex-co  29691  avril1  29716  vc0  29827  vcz  29828  cnaddabloOLD  29834  cnidOLD  29835  ipasslem8  30090  siilem2  30105  hvmul0  30277  hi01  30349  norm-iii  30393  h1de2ctlem  30808  pjmuli  30942  pjneli  30976  eigre  31088  eigorth  31091  elnlfn  31181  0cnfn  31233  0lnfn  31238  lnopunilem2  31264  xrge0tsmsd  32209  qqh0  32964  qqhcn  32971  eulerpartlemgs2  33379  sgnneg  33539  breprexpnat  33646  hgt750lem2  33664  subfacp1lem6  34176  sinccvglem  34657  abs2sqle  34665  abs2sqlt  34666  gg-dvcnp2  35174  tan2h  36480  poimirlem16  36504  poimirlem19  36507  poimirlem31  36519  mblfinlem2  36526  ovoliunnfl  36530  voliunnfl  36532  dvtanlem  36537  ftc1anclem5  36565  cntotbnd  36664  60lcm7e420  40875  lcmineqlem10  40903  3lexlogpow5ineq1  40919  sn-1ne2  41179  sn-it0e0  41288  addinvcom  41304  sn-0tie0  41312  fltnltalem  41404  flcidc  41916  dvconstbi  43093  expgrowth  43094  dvradcnv2  43106  binomcxplemdvbinom  43112  binomcxplemnotnn0  43115  xralrple3  44084  negcncfg  44597  ioodvbdlimc1  44649  ioodvbdlimc2  44651  itgsinexplem1  44670  stoweidlem26  44742  stoweidlem36  44752  stoweidlem55  44771  stirlinglem8  44797  fourierdlem103  44925  sqwvfoura  44944  sqwvfourb  44945  ovn0lem  45281  pzriprnglem5  46809  pzriprnglem6  46810  nn0sumshdiglemA  47305  nn0sumshdiglemB  47306  nn0sumshdiglem1  47307  sec0  47805