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  35610  sinccvglem  36097  abs2sqle  36105  abs2sqlt  36106  tan2h  38185  poimirlem16  38209  poimirlem19  38212  poimirlem31  38224  mblfinlem2  38231  ovoliunnfl  38235  voliunnfl  38237  ftc1anclem5  38270  cntotbnd  38369  60lcm7e420  42701  lcmineqlem10  42729  3lexlogpow5ineq1  42745  25or6to4  42897  sn-1ne2  42956  0tie0  43000  sn-it0e0  43101  addinvcom  43117  sn-0tie0  43149  fltnltalem  43320  flcidc  43823  dvconstbi  44970  expgrowth  44971  dvradcnv2  44983  binomcxplemdvbinom  44989  binomcxplemnotnn0  44992  xralrple3  46015  negcncfg  46521  ioodvbdlimc1  46573  ioodvbdlimc2  46575  itgsinexplem1  46594  stoweidlem26  46666  stoweidlem36  46676  stoweidlem55  46695  stirlinglem8  46721  fourierdlem103  46849  sqwvfoura  46868  sqwvfourb  46869  ovn0lem  47205  nthrucw  47528  nn0sumshdiglemA  49318  nn0sumshdiglemB  49319  nn0sumshdiglem1  49320  sec0  50457