Theorem 0cn 10070

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

Assertion

Ref	Expression
0cn	⊢ 0 ∈ ℂ

Proof of Theorem 0cn

Step	Hyp	Ref	Expression
1		ax-i2m1 10042	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 10033	. . . 4 ⊢ i ∈ ℂ
3		mulcl 10058	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 708	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 10032	. . 3 ⊢ 1 ∈ ℂ
6		addcl 10056	. . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
7	4, 5, 6	mp2an 708	. 2 ⊢ ((i · i) + 1) ∈ ℂ
8	1, 7	eqeltrri 2727	1 ⊢ 0 ∈ ℂ

Syntax hints:   ∈ wcel 2030  (class class class)co 6690  ℂcc 9972  0cc0 9974  1c1 9975  ici 9976   + caddc 9977   · cmul 9979

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-mulcl 10036  ax-i2m1 10042

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644  df-clel 2647

This theorem is referenced by:  0cnd  10071  c0ex  10072  1re  10077  00id  10249  mul02lem1  10250  mul02  10252  mul01  10253  addid1  10254  addid2  10257  negcl  10319  subid  10338  subid1  10339  neg0  10365  negid  10366  negsub  10367  subneg  10368  negneg  10369  negeq0  10373  negsubdi  10375  renegcli  10380  mulneg1  10504  msqge0  10587  ixi  10694  muleqadd  10709  div0  10753  ofsubge0  11057  0m0e0  11168  elznn0  11430  ser0  12893  0exp0e1  12905  0exp  12935  sq0  12995  sqeqor  13018  binom2  13019  bcval5  13145  s1co  13625  shftval3  13860  shftidt2  13865  cjne0  13947  sqrt0  14026  abs0  14069  abs00bd  14075  abs2dif  14116  clim0  14281  climz  14324  serclim0  14352  rlimneg  14421  sumrblem  14486  fsumcvg  14487  summolem2a  14490  sumss  14499  fsumss  14500  fsumcvg2  14502  fsumsplit  14515  sumsplit  14543  fsumrelem  14583  fsumrlim  14587  fsumo1  14588  0fallfac  14812  0risefac  14813  binomfallfac  14816  fsumcube  14835  ef0  14865  eftlub  14883  sin0  14923  tan0  14925  divalglem9  15171  sadadd2lem2  15219  sadadd3  15230  bezout  15307  pcmpt2  15644  4sqlem11  15706  ramcl  15780  4001lem2  15896  odadd1  18297  cnaddablx  18317  cnaddabl  18318  cnaddid  18319  frgpnabllem1  18322  cncrng  19815  cnfld0  19818  cnbl0  22624  cnblcld  22625  cnfldnm  22629  xrge0gsumle  22683  xrge0tsms  22684  cnheibor  22801  cnlmod  22986  csscld  23094  clsocv  23095  cnflduss  23198  cnfldcusp  23199  rrxmvallem  23233  rrxmval  23234  mbfss  23458  mbfmulc2lem  23459  0plef  23484  0pledm  23485  itg1ge0  23498  itg1addlem4  23511  itg2splitlem  23560  itg2addlem  23570  ibl0  23598  iblcnlem  23600  iblss2  23617  itgss3  23626  dvconst  23725  dvcnp2  23728  dvrec  23763  dvexp3  23786  dveflem  23787  dvef  23788  dv11cn  23809  lhop1lem  23821  plyun0  23998  plyeq0lem  24011  coeeulem  24025  coeeu  24026  coef3  24033  dgrle  24044  0dgrb  24047  coefv0  24049  coemulc  24056  coe1termlem  24059  coe1term  24060  dgr0  24063  dgrmulc  24072  dgrcolem2  24075  vieta1lem2  24111  iaa  24125  aareccl  24126  aalioulem3  24134  taylthlem2  24173  psercn  24225  pserdvlem2  24227  abelthlem2  24231  abelthlem3  24232  abelthlem5  24234  abelthlem7  24237  abelth  24240  sin2kpi  24280  cos2kpi  24281  sinkpi  24316  efopn  24449  logtayl  24451  cxpval  24455  0cxp  24457  cxpexp  24459  cxpcl  24465  cxpge0  24474  mulcxplem  24475  mulcxp  24476  cxpmul2  24480  dvsqrt  24528  dvcnsqrt  24530  cxpcn3  24534  abscxpbnd  24539  efrlim  24741  ftalem2  24845  ftalem3  24846  ftalem4  24847  ftalem5  24848  ftalem7  24850  prmorcht  24949  muinv  24964  1sgm2ppw  24970  logfacbnd3  24993  logexprlim  24995  dchrelbas2  25007  dchrmulid2  25022  dchrfi  25025  dchrinv  25031  lgsdir2  25100  lgsdir  25102  dchrvmasumiflem1  25235  dchrvmasumiflem2  25236  rpvmasum2  25246  log2sumbnd  25278  selberg2lem  25284  logdivbnd  25290  ax5seglem8  25861  axlowdimlem6  25872  axlowdimlem13  25879  ex-co  27425  avril1  27449  vc0  27557  vcz  27558  cnaddabloOLD  27564  cnidOLD  27565  ipasslem8  27820  siilem2  27835  hvmul0  28009  hi01  28081  norm-iii  28125  h1de2ctlem  28542  pjmuli  28676  pjneli  28710  eigre  28822  eigorth  28825  elnlfn  28915  0cnfn  28967  0lnfn  28972  lnopunilem2  28998  xrge0tsmsd  29913  qqh0  30156  qqhcn  30163  eulerpartlemgs2  30570  sgnneg  30730  breprexpnat  30840  hgt750lem2  30858  subfacp1lem6  31293  sinccvglem  31692  abs2sqle  31700  abs2sqlt  31701  tan2h  33531  poimirlem16  33555  poimirlem19  33558  poimirlem31  33570  mblfinlem2  33577  ovoliunnfl  33581  voliunnfl  33583  dvtanlem  33589  ftc1anclem5  33619  cntotbnd  33725  flcidc  38061  dvconstbi  38850  expgrowth  38851  dvradcnv2  38863  binomcxplemdvbinom  38869  binomcxplemnotnn0  38872  xralrple3  39903  negcncfg  40412  ioodvbdlimc1  40466  ioodvbdlimc2  40468  itgsinexplem1  40487  stoweidlem26  40561  stoweidlem36  40571  stoweidlem55  40590  stirlinglem8  40616  fourierdlem103  40744  sqwvfoura  40763  sqwvfourb  40764  ovn0lem  41100  nn0sumshdiglemA  42738  nn0sumshdiglemB  42739  nn0sumshdiglem1  42740  sec0  42829