Theorem 0cn 11130

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

Assertion

Ref	Expression
0cn	⊢ 0 ∈ ℂ

Proof of Theorem 0cn

Step	Hyp	Ref	Expression
1		ax-i2m1 11100	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 11091	. . . 4 ⊢ i ∈ ℂ
3		mulcl 11116	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 693	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 11090	. . 3 ⊢ 1 ∈ ℂ
6		addcl 11114	. . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
7	4, 5, 6	mp2an 693	. 2 ⊢ ((i · i) + 1) ∈ ℂ
8	1, 7	eqeltrri 2834	1 ⊢ 0 ∈ ℂ

Syntax hints:   ∈ wcel 2114  (class class class)co 7361  ℂcc 11030  0cc0 11032  1c1 11033  ici 11034   + caddc 11035   · cmul 11037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-mulcl 11094  ax-i2m1 11100

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812

This theorem is referenced by:  0cnd  11131  c0ex  11132  1re  11138  00id  11315  mul02lem1  11316  mul02  11318  mul01  11319  addrid  11320  addlid  11323  negcl  11387  subid  11407  subid1  11408  neg0  11434  negid  11435  negsub  11436  subneg  11437  negneg  11438  negeq0  11442  negsubdi  11444  renegcli  11449  mulneg1  11580  msqge0  11665  ixi  11773  muleqadd  11788  diveq0  11813  div0  11836  div0OLD  11837  ofsubge0  12152  0m0e0  12290  nn0sscn  12436  elznn0  12533  ser0  14010  0exp0e1  14022  0exp  14053  sq0  14148  sqeqor  14172  binom2  14173  bcval5  14274  s1co  14789  shftval3  15032  shftidt2  15037  cjne0  15119  sqrt0  15197  abs0  15241  abs00bd  15247  abs2dif  15289  clim0  15462  climz  15505  serclim0  15533  rlimneg  15603  sumrblem  15667  fsumcvg  15668  summolem2a  15671  sumss  15680  fsumss  15681  fsumcvg2  15683  fsumsplit  15697  sumsplit  15724  fsumrelem  15764  fsumrlim  15768  fsumo1  15769  0fallfac  15996  0risefac  15997  binomfallfac  16000  fsumcube  16019  ef0  16050  eftlub  16070  sin0  16110  tan0  16112  divalglem9  16364  sadadd2lem2  16413  sadadd3  16424  bezout  16506  pcmpt2  16858  4sqlem11  16920  ramcl  16994  4001lem2  17106  odadd1  19817  cnaddablx  19837  cnaddabl  19838  cnaddid  19839  frgpnabllem1  19842  cncrng  21381  cncrngOLD  21382  cnfld0  21385  pzriprnglem5  21478  pzriprnglem6  21479  psdmplcl  22141  cnbl0  24751  cnblcld  24752  cnfldnm  24756  cnn0opn  24765  xrge0gsumle  24812  xrge0tsms  24813  cnheibor  24935  cnlmod  25120  csscld  25229  clsocv  25230  cnflduss  25336  cnfldcusp  25337  rrxmvallem  25384  rrxmval  25385  mbfss  25626  mbfmulc2lem  25627  0plef  25652  0pledm  25653  itg1ge0  25666  itg1addlem4  25679  itg2splitlem  25728  itg2addlem  25738  ibl0  25767  iblcnlem  25769  iblss2  25786  itgss3  25795  dvconst  25897  dvcnp2  25900  dveflem  25959  dv11cn  25981  lhop1lem  25993  plyun0  26175  plyeq0lem  26188  coeeulem  26202  coeeu  26203  coef3  26210  dgrle  26221  0dgrb  26224  coefv0  26226  coemulc  26233  coe1termlem  26236  coe1term  26237  dgr0  26240  dgrmulc  26249  dgrcolem2  26252  vieta1lem2  26291  iaa  26305  aareccl  26306  aalioulem3  26314  taylthlem2  26354  taylthlem2OLD  26355  psercn  26407  pserdvlem2  26409  abelthlem2  26413  abelthlem3  26414  abelthlem5  26416  abelthlem7  26419  abelth  26422  sin2kpi  26463  cos2kpi  26464  sinkpi  26502  efopn  26638  logtayl  26640  cxpval  26644  0cxp  26646  cxpexp  26648  cxpcl  26654  cxpge0  26663  mulcxplem  26664  mulcxp  26665  cxpmul2  26669  dvsqrt  26722  dvcnsqrt  26724  cxpcn3  26728  abscxpbnd  26733  efrlim  26949  efrlimOLD  26950  ftalem2  27054  ftalem3  27055  ftalem4  27056  ftalem5  27057  ftalem7  27059  prmorcht  27158  muinv  27173  1sgm2ppw  27180  logfacbnd3  27203  logexprlim  27205  dchrelbas2  27217  dchrmullid  27232  dchrfi  27235  dchrinv  27241  lgsdir2  27310  lgsdir  27312  addsqnreup  27423  dchrvmasumiflem1  27481  dchrvmasumiflem2  27482  rpvmasum2  27492  log2sumbnd  27524  selberg2lem  27530  logdivbnd  27536  ax5seglem8  29022  axlowdimlem6  29033  axlowdimlem13  29040  ex-co  30526  avril1  30551  vc0  30663  vcz  30664  cnaddabloOLD  30670  cnidOLD  30671  ipasslem8  30926  siilem2  30941  hvmul0  31113  hi01  31185  norm-iii  31229  h1de2ctlem  31644  pjmuli  31778  pjneli  31812  eigre  31924  eigorth  31927  elnlfn  32017  0cnfn  32069  0lnfn  32074  lnopunilem2  32100  sgnneg  32924  xrge0tsmsd  33152  constrsscn  33903  qqh0  34147  qqhcn  34154  eulerpartlemgs2  34543  breprexpnat  34797  hgt750lem2  34815  subfacp1lem6  35386  sinccvglem  35873  abs2sqle  35881  abs2sqlt  35882  tan2h  37950  poimirlem16  37974  poimirlem19  37977  poimirlem31  37989  mblfinlem2  37996  ovoliunnfl  38000  voliunnfl  38002  ftc1anclem5  38035  cntotbnd  38134  60lcm7e420  42466  lcmineqlem10  42494  3lexlogpow5ineq1  42510  sn-1ne2  42720  0tie0  42764  sn-it0e0  42865  addinvcom  42881  sn-0tie0  42913  fltnltalem  43112  flcidc  43619  dvconstbi  44782  expgrowth  44783  dvradcnv2  44795  binomcxplemdvbinom  44801  binomcxplemnotnn0  44804  xralrple3  45824  negcncfg  46330  ioodvbdlimc1  46382  ioodvbdlimc2  46384  itgsinexplem1  46403  stoweidlem26  46475  stoweidlem36  46485  stoweidlem55  46504  stirlinglem8  46530  fourierdlem103  46658  sqwvfoura  46677  sqwvfourb  46678  ovn0lem  47014  nthrucw  47335  nn0sumshdiglemA  49110  nn0sumshdiglemB  49111  nn0sumshdiglem1  49112  sec0  50250