Theorem 0cn 11136

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

Assertion

Ref	Expression
0cn	⊢ 0 ∈ ℂ

Proof of Theorem 0cn

Step	Hyp	Ref	Expression
1		ax-i2m1 11106	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 11097	. . . 4 ⊢ i ∈ ℂ
3		mulcl 11122	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 693	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 11096	. . 3 ⊢ 1 ∈ ℂ
6		addcl 11120	. . 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 7368  ℂcc 11036  0cc0 11038  1c1 11039  ici 11040   + caddc 11041   · cmul 11043

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 11096  ax-icn 11097  ax-addcl 11098  ax-mulcl 11100  ax-i2m1 11106

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  11137  c0ex  11138  1re  11144  00id  11320  mul02lem1  11321  mul02  11323  mul01  11324  addrid  11325  addlid  11328  negcl  11392  subid  11412  subid1  11413  neg0  11439  negid  11440  negsub  11441  subneg  11442  negneg  11443  negeq0  11447  negsubdi  11449  renegcli  11454  mulneg1  11585  msqge0  11670  ixi  11778  muleqadd  11793  diveq0  11818  div0  11841  div0OLD  11842  ofsubge0  12156  0m0e0  12272  nn0sscn  12418  elznn0  12515  ser0  13989  0exp0e1  14001  0exp  14032  sq0  14127  sqeqor  14151  binom2  14152  bcval5  14253  s1co  14768  shftval3  15011  shftidt2  15016  cjne0  15098  sqrt0  15176  abs0  15220  abs00bd  15226  abs2dif  15268  clim0  15441  climz  15484  serclim0  15512  rlimneg  15582  sumrblem  15646  fsumcvg  15647  summolem2a  15650  sumss  15659  fsumss  15660  fsumcvg2  15662  fsumsplit  15676  sumsplit  15703  fsumrelem  15742  fsumrlim  15746  fsumo1  15747  0fallfac  15972  0risefac  15973  binomfallfac  15976  fsumcube  15995  ef0  16026  eftlub  16046  sin0  16086  tan0  16088  divalglem9  16340  sadadd2lem2  16389  sadadd3  16400  bezout  16482  pcmpt2  16833  4sqlem11  16895  ramcl  16969  4001lem2  17081  odadd1  19789  cnaddablx  19809  cnaddabl  19810  cnaddid  19811  frgpnabllem1  19814  cncrng  21355  cncrngOLD  21356  cnfld0  21359  pzriprnglem5  21452  pzriprnglem6  21453  psdmplcl  22117  cnbl0  24729  cnblcld  24730  cnfldnm  24734  cnn0opn  24743  xrge0gsumle  24790  xrge0tsms  24791  cnheibor  24922  cnlmod  25108  csscld  25217  clsocv  25218  cnflduss  25324  cnfldcusp  25325  rrxmvallem  25372  rrxmval  25373  mbfss  25615  mbfmulc2lem  25616  0plef  25641  0pledm  25642  itg1ge0  25655  itg1addlem4  25668  itg2splitlem  25717  itg2addlem  25727  ibl0  25756  iblcnlem  25758  iblss2  25775  itgss3  25784  dvconst  25886  dvcnp2  25889  dvcnp2OLD  25890  dveflem  25951  dv11cn  25974  lhop1lem  25986  plyun0  26170  plyeq0lem  26183  coeeulem  26197  coeeu  26198  coef3  26205  dgrle  26216  0dgrb  26219  coefv0  26221  coemulc  26228  coe1termlem  26231  coe1term  26232  dgr0  26236  dgrmulc  26245  dgrcolem2  26248  vieta1lem2  26287  iaa  26301  aareccl  26302  aalioulem3  26310  taylthlem2  26350  taylthlem2OLD  26351  psercn  26404  pserdvlem2  26406  abelthlem2  26410  abelthlem3  26411  abelthlem5  26413  abelthlem7  26416  abelth  26419  sin2kpi  26460  cos2kpi  26461  sinkpi  26499  efopn  26635  logtayl  26637  cxpval  26641  0cxp  26643  cxpexp  26645  cxpcl  26651  cxpge0  26660  mulcxplem  26661  mulcxp  26662  cxpmul2  26666  dvsqrt  26719  dvcnsqrt  26721  cxpcn3  26726  abscxpbnd  26731  efrlim  26947  efrlimOLD  26948  ftalem2  27052  ftalem3  27053  ftalem4  27054  ftalem5  27055  ftalem7  27057  prmorcht  27156  muinv  27171  1sgm2ppw  27179  logfacbnd3  27202  logexprlim  27204  dchrelbas2  27216  dchrmullid  27231  dchrfi  27234  dchrinv  27240  lgsdir2  27309  lgsdir  27311  addsqnreup  27422  dchrvmasumiflem1  27480  dchrvmasumiflem2  27481  rpvmasum2  27491  log2sumbnd  27523  selberg2lem  27529  logdivbnd  27535  ax5seglem8  29021  axlowdimlem6  29032  axlowdimlem13  29039  ex-co  30525  avril1  30550  vc0  30662  vcz  30663  cnaddabloOLD  30669  cnidOLD  30670  ipasslem8  30925  siilem2  30940  hvmul0  31112  hi01  31184  norm-iii  31228  h1de2ctlem  31643  pjmuli  31777  pjneli  31811  eigre  31923  eigorth  31926  elnlfn  32016  0cnfn  32068  0lnfn  32073  lnopunilem2  32099  sgnneg  32925  xrge0tsmsd  33167  constrsscn  33918  qqh0  34162  qqhcn  34169  eulerpartlemgs2  34558  breprexpnat  34812  hgt750lem2  34830  subfacp1lem6  35401  sinccvglem  35888  abs2sqle  35896  abs2sqlt  35897  tan2h  37863  poimirlem16  37887  poimirlem19  37890  poimirlem31  37902  mblfinlem2  37909  ovoliunnfl  37913  voliunnfl  37915  ftc1anclem5  37948  cntotbnd  38047  60lcm7e420  42380  lcmineqlem10  42408  3lexlogpow5ineq1  42424  sn-1ne2  42635  0tie0  42685  sn-it0e0  42786  addinvcom  42802  sn-0tie0  42821  fltnltalem  43020  flcidc  43527  dvconstbi  44690  expgrowth  44691  dvradcnv2  44703  binomcxplemdvbinom  44709  binomcxplemnotnn0  44712  xralrple3  45732  negcncfg  46239  ioodvbdlimc1  46291  ioodvbdlimc2  46293  itgsinexplem1  46312  stoweidlem26  46384  stoweidlem36  46394  stoweidlem55  46413  stirlinglem8  46439  fourierdlem103  46567  sqwvfoura  46586  sqwvfourb  46587  ovn0lem  46923  nthrucw  47244  nn0sumshdiglemA  48979  nn0sumshdiglemB  48980  nn0sumshdiglem1  48981  sec0  50119