Theorem 0cn 11104

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

Assertion

Ref	Expression
0cn	⊢ 0 ∈ ℂ

Proof of Theorem 0cn

Step	Hyp	Ref	Expression
1		ax-i2m1 11074	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 11065	. . . 4 ⊢ i ∈ ℂ
3		mulcl 11090	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 692	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 11064	. . 3 ⊢ 1 ∈ ℂ
6		addcl 11088	. . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
7	4, 5, 6	mp2an 692	. 2 ⊢ ((i · i) + 1) ∈ ℂ
8	1, 7	eqeltrri 2828	1 ⊢ 0 ∈ ℂ

Syntax hints:   ∈ wcel 2111  (class class class)co 7346  ℂcc 11004  0cc0 11006  1c1 11007  ici 11008   + caddc 11009   · cmul 11011

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-1cn 11064  ax-icn 11065  ax-addcl 11066  ax-mulcl 11068  ax-i2m1 11074

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-clel 2806

This theorem is referenced by:  0cnd  11105  c0ex  11106  1re  11112  00id  11288  mul02lem1  11289  mul02  11291  mul01  11292  addrid  11293  addlid  11296  negcl  11360  subid  11380  subid1  11381  neg0  11407  negid  11408  negsub  11409  subneg  11410  negneg  11411  negeq0  11415  negsubdi  11417  renegcli  11422  mulneg1  11553  msqge0  11638  ixi  11746  muleqadd  11761  diveq0  11786  div0  11809  div0OLD  11810  ofsubge0  12124  0m0e0  12240  nn0sscn  12386  elznn0  12483  ser0  13961  0exp0e1  13973  0exp  14004  sq0  14099  sqeqor  14123  binom2  14124  bcval5  14225  s1co  14740  shftval3  14983  shftidt2  14988  cjne0  15070  sqrt0  15148  abs0  15192  abs00bd  15198  abs2dif  15240  clim0  15413  climz  15456  serclim0  15484  rlimneg  15554  sumrblem  15618  fsumcvg  15619  summolem2a  15622  sumss  15631  fsumss  15632  fsumcvg2  15634  fsumsplit  15648  sumsplit  15675  fsumrelem  15714  fsumrlim  15718  fsumo1  15719  0fallfac  15944  0risefac  15945  binomfallfac  15948  fsumcube  15967  ef0  15998  eftlub  16018  sin0  16058  tan0  16060  divalglem9  16312  sadadd2lem2  16361  sadadd3  16372  bezout  16454  pcmpt2  16805  4sqlem11  16867  ramcl  16941  4001lem2  17053  odadd1  19760  cnaddablx  19780  cnaddabl  19781  cnaddid  19782  frgpnabllem1  19785  cncrng  21325  cncrngOLD  21326  cnfld0  21329  pzriprnglem5  21422  pzriprnglem6  21423  psdmplcl  22077  cnbl0  24688  cnblcld  24689  cnfldnm  24693  cnn0opn  24702  xrge0gsumle  24749  xrge0tsms  24750  cnheibor  24881  cnlmod  25067  csscld  25176  clsocv  25177  cnflduss  25283  cnfldcusp  25284  rrxmvallem  25331  rrxmval  25332  mbfss  25574  mbfmulc2lem  25575  0plef  25600  0pledm  25601  itg1ge0  25614  itg1addlem4  25627  itg2splitlem  25676  itg2addlem  25686  ibl0  25715  iblcnlem  25717  iblss2  25734  itgss3  25743  dvconst  25845  dvcnp2  25848  dvcnp2OLD  25849  dveflem  25910  dv11cn  25933  lhop1lem  25945  plyun0  26129  plyeq0lem  26142  coeeulem  26156  coeeu  26157  coef3  26164  dgrle  26175  0dgrb  26178  coefv0  26180  coemulc  26187  coe1termlem  26190  coe1term  26191  dgr0  26195  dgrmulc  26204  dgrcolem2  26207  vieta1lem2  26246  iaa  26260  aareccl  26261  aalioulem3  26269  taylthlem2  26309  taylthlem2OLD  26310  psercn  26363  pserdvlem2  26365  abelthlem2  26369  abelthlem3  26370  abelthlem5  26372  abelthlem7  26375  abelth  26378  sin2kpi  26419  cos2kpi  26420  sinkpi  26458  efopn  26594  logtayl  26596  cxpval  26600  0cxp  26602  cxpexp  26604  cxpcl  26610  cxpge0  26619  mulcxplem  26620  mulcxp  26621  cxpmul2  26625  dvsqrt  26678  dvcnsqrt  26680  cxpcn3  26685  abscxpbnd  26690  efrlim  26906  efrlimOLD  26907  ftalem2  27011  ftalem3  27012  ftalem4  27013  ftalem5  27014  ftalem7  27016  prmorcht  27115  muinv  27130  1sgm2ppw  27138  logfacbnd3  27161  logexprlim  27163  dchrelbas2  27175  dchrmullid  27190  dchrfi  27193  dchrinv  27199  lgsdir2  27268  lgsdir  27270  addsqnreup  27381  dchrvmasumiflem1  27439  dchrvmasumiflem2  27440  rpvmasum2  27450  log2sumbnd  27482  selberg2lem  27488  logdivbnd  27494  ax5seglem8  28914  axlowdimlem6  28925  axlowdimlem13  28932  ex-co  30418  avril1  30443  vc0  30554  vcz  30555  cnaddabloOLD  30561  cnidOLD  30562  ipasslem8  30817  siilem2  30832  hvmul0  31004  hi01  31076  norm-iii  31120  h1de2ctlem  31535  pjmuli  31669  pjneli  31703  eigre  31815  eigorth  31818  elnlfn  31908  0cnfn  31960  0lnfn  31965  lnopunilem2  31991  sgnneg  32816  xrge0tsmsd  33042  constrsscn  33753  qqh0  33997  qqhcn  34004  eulerpartlemgs2  34393  breprexpnat  34647  hgt750lem2  34665  subfacp1lem6  35229  sinccvglem  35716  abs2sqle  35724  abs2sqlt  35725  tan2h  37660  poimirlem16  37684  poimirlem19  37687  poimirlem31  37699  mblfinlem2  37706  ovoliunnfl  37710  voliunnfl  37712  ftc1anclem5  37745  cntotbnd  37844  60lcm7e420  42051  lcmineqlem10  42079  3lexlogpow5ineq1  42095  sn-1ne2  42306  0tie0  42356  sn-it0e0  42457  addinvcom  42473  sn-0tie0  42492  fltnltalem  42703  flcidc  43211  dvconstbi  44375  expgrowth  44376  dvradcnv2  44388  binomcxplemdvbinom  44394  binomcxplemnotnn0  44397  xralrple3  45420  negcncfg  45927  ioodvbdlimc1  45979  ioodvbdlimc2  45981  itgsinexplem1  46000  stoweidlem26  46072  stoweidlem36  46082  stoweidlem55  46101  stirlinglem8  46127  fourierdlem103  46255  sqwvfoura  46274  sqwvfourb  46275  ovn0lem  46611  nn0sumshdiglemA  48659  nn0sumshdiglemB  48660  nn0sumshdiglem1  48661  sec0  49800