Theorem 0cn 11198

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 11168	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 11159	. . . 4 ⊢ i ∈ ℂ
3		mulcl 11184	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 704	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 11158	. . 3 ⊢ 1 ∈ ℂ
6		addcl 11182	. . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
7	4, 5, 6	mp2an 704	. 2 ⊢ ((i · i) + 1) ∈ ℂ
8	1, 7	eqeltrri 2866	1 ⊢ 0 ∈ ℂ

Syntax hints:   ∈ wcel 2149  (class class class)co 7411  ℂcc 11098  0cc0 11100  1c1 11101  ici 11102   + caddc 11103   · cmul 11105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-1cn 11158  ax-icn 11159  ax-addcl 11160  ax-mulcl 11162  ax-i2m1 11168

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-clel 2844

This theorem is referenced by:  0cnd  11199  c0ex  11200  1re  11208  00id  11385  mul02lem1  11386  mul02  11388  mul01  11389  addrid  11390  addlid  11393  negcl  11457  subid  11477  subid1  11478  neg0  11504  negid  11505  negsub  11506  subneg  11507  negneg  11508  negeq0  11512  negsubdi  11514  renegcli  11519  mulneg1  11650  msqge0  11735  ixi  11843  muleqadd  11858  diveq0  11882  div0  11903  ofsubge0  12217  0m0e0  12359  nn0sscn  12509  elznn0  12606  ser0  14090  0exp0e1  14102  0exp  14133  sq0  14228  sqeqor  14252  binom2  14253  bcval5  14354  s1co  14870  shftval3  15113  shftidt2  15118  sgnneg  15137  cjne0  15214  sqrt0  15292  abs0  15336  abs00bd  15342  abs2dif  15384  clim0  15557  climz  15600  serclim0  15628  rlimneg  15698  sumrblem  15762  fsumcvg  15763  summolem2a  15766  sumss  15775  fsumss  15776  fsumcvg2  15778  fsumsplit  15792  sumsplit  15819  fsumrelem  15859  fsumrlim  15863  fsumo1  15864  0fallfac  16091  0risefac  16092  binomfallfac  16095  fsumcube  16114  ef0  16145  eftlub  16165  sin0  16205  tan0  16207  divalglem9  16459  sadadd2lem2  16508  sadadd3  16519  bezout  16601  pcmpt2  16953  4sqlem11  17015  ramcl  17089  4001lem2  17202  odadd1  19918  cnaddablx  19938  cnaddabl  19939  cnaddid  19940  frgpnabllem1  19943  cncrng  21512  cnfld0  21515  pzriprnglem5  21604  pzriprnglem6  21605  psdmplcl  22294  cnbl0  24899  cnblcld  24900  cnfldnm  24904  cnn0opn  24913  xrge0gsumle  24960  xrge0tsms  24961  cnheibor  25083  cnlmod  25268  csscld  25377  clsocv  25378  cnflduss  25484  cnfldcusp  25485  rrxmvallem  25532  rrxmval  25533  mbfss  25774  mbfmulc2lem  25775  0plef  25800  0pledm  25801  itg1ge0  25814  itg1addlem4  25827  itg2splitlem  25876  itg2addlem  25886  ibl0  25915  iblcnlem  25917  iblss2  25934  itgss3  25943  dvconst  26045  dvcnp2  26048  dveflem  26107  dv11cn  26129  lhop1lem  26141  plyun0  26323  plyeq0lem  26336  coeeulem  26350  coeeu  26351  coef3  26358  dgrle  26369  0dgrb  26372  coefv0  26374  coemulc  26381  coe1termlem  26384  coe1term  26385  dgr0  26388  dgrmulc  26397  dgrcolem2  26400  vieta1lem2  26441  iaa  26455  aareccl  26456  aalioulem3  26464  taylthlem2  26503  psercn  26555  pserdvlem2  26557  abelthlem2  26561  abelthlem3  26562  abelthlem5  26564  abelthlem7  26567  abelth  26570  sin2kpi  26614  cos2kpi  26615  sinkpi  26653  efopn  26789  logtayl  26791  cxpval  26795  0cxp  26797  cxpexp  26799  cxpcl  26805  cxpge0  26814  mulcxplem  26815  mulcxp  26816  cxpmul2  26820  dvsqrt  26873  dvcnsqrt  26875  cxpcn3  26879  abscxpbnd  26884  efrlim  27100  ftalem2  27204  ftalem3  27205  ftalem4  27206  ftalem5  27207  ftalem7  27209  prmorcht  27308  muinv  27323  1sgm2ppw  27330  logfacbnd3  27353  logexprlim  27355  dchrelbas2  27367  dchrmullid  27382  dchrfi  27385  dchrinv  27391  lgsdir2  27460  lgsdir  27462  addsqnreup  27573  dchrvmasumiflem1  27631  dchrvmasumiflem2  27632  rpvmasum2  27642  log2sumbnd  27674  selberg2lem  27680  logdivbnd  27686  ax5seglem8  29227  axlowdimlem6  29238  axlowdimlem13  29245  ex-co  30730  avril1  30755  vc0  30867  vcz  30868  cnaddabloOLD  30874  cnidOLD  30875  ipasslem8  31130  siilem2  31145  hvmul0  31317  hi01  31389  norm-iii  31433  h1de2ctlem  31848  pjmuli  31982  pjneli  32016  eigre  32128  eigorth  32131  elnlfn  32221  0cnfn  32273  0lnfn  32278  lnopunilem2  32304  xrge0tsmsd  33334  constrsscn  34075  qqh0  34319  qqhcn  34326  eulerpartlemgs2  34715  breprexpnat  34966  hgt750lem2  34984  subfacp1lem6  35576  sinccvglem  36063  abs2sqle  36071  abs2sqlt  36072  tan2h  38151  poimirlem16  38175  poimirlem19  38178  poimirlem31  38190  mblfinlem2  38197  ovoliunnfl  38201  voliunnfl  38203  ftc1anclem5  38236  cntotbnd  38335  60lcm7e420  42667  lcmineqlem10  42695  3lexlogpow5ineq1  42711  25or6to4  42863  sn-1ne2  42922  0tie0  42966  sn-it0e0  43067  addinvcom  43083  sn-0tie0  43115  fltnltalem  43286  flcidc  43789  dvconstbi  44936  expgrowth  44937  dvradcnv2  44949  binomcxplemdvbinom  44955  binomcxplemnotnn0  44958  xralrple3  45981  negcncfg  46487  ioodvbdlimc1  46539  ioodvbdlimc2  46541  itgsinexplem1  46560  stoweidlem26  46632  stoweidlem36  46642  stoweidlem55  46661  stirlinglem8  46687  fourierdlem103  46815  sqwvfoura  46834  sqwvfourb  46835  ovn0lem  47171  nthrucw  47494  nn0sumshdiglemA  49284  nn0sumshdiglemB  49285  nn0sumshdiglem1  49286  sec0  50423