Theorem 0cn 11166

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

Assertion

Ref	Expression
0cn	⊢ 0 ∈ ℂ

Proof of Theorem 0cn

Step	Hyp	Ref	Expression
1		ax-i2m1 11136	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 11127	. . . 4 ⊢ i ∈ ℂ
3		mulcl 11152	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 692	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 11126	. . 3 ⊢ 1 ∈ ℂ
6		addcl 11150	. . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
7	4, 5, 6	mp2an 692	. 2 ⊢ ((i · i) + 1) ∈ ℂ
8	1, 7	eqeltrri 2825	1 ⊢ 0 ∈ ℂ

Syntax hints:   ∈ wcel 2109  (class class class)co 7387  ℂcc 11066  0cc0 11068  1c1 11069  ici 11070   + caddc 11071   · cmul 11073

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-mulcl 11130  ax-i2m1 11136

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803

This theorem is referenced by:  0cnd  11167  c0ex  11168  1re  11174  00id  11349  mul02lem1  11350  mul02  11352  mul01  11353  addrid  11354  addlid  11357  negcl  11421  subid  11441  subid1  11442  neg0  11468  negid  11469  negsub  11470  subneg  11471  negneg  11472  negeq0  11476  negsubdi  11478  renegcli  11483  mulneg1  11614  msqge0  11699  ixi  11807  muleqadd  11822  diveq0  11847  div0  11870  div0OLD  11871  ofsubge0  12185  0m0e0  12301  nn0sscn  12447  elznn0  12544  ser0  14019  0exp0e1  14031  0exp  14062  sq0  14157  sqeqor  14181  binom2  14182  bcval5  14283  s1co  14799  shftval3  15042  shftidt2  15047  cjne0  15129  sqrt0  15207  abs0  15251  abs00bd  15257  abs2dif  15299  clim0  15472  climz  15515  serclim0  15543  rlimneg  15613  sumrblem  15677  fsumcvg  15678  summolem2a  15681  sumss  15690  fsumss  15691  fsumcvg2  15693  fsumsplit  15707  sumsplit  15734  fsumrelem  15773  fsumrlim  15777  fsumo1  15778  0fallfac  16003  0risefac  16004  binomfallfac  16007  fsumcube  16026  ef0  16057  eftlub  16077  sin0  16117  tan0  16119  divalglem9  16371  sadadd2lem2  16420  sadadd3  16431  bezout  16513  pcmpt2  16864  4sqlem11  16926  ramcl  17000  4001lem2  17112  odadd1  19778  cnaddablx  19798  cnaddabl  19799  cnaddid  19800  frgpnabllem1  19803  cncrng  21300  cncrngOLD  21301  cnfld0  21304  pzriprnglem5  21395  pzriprnglem6  21396  psdmplcl  22049  cnbl0  24661  cnblcld  24662  cnfldnm  24666  cnn0opn  24675  xrge0gsumle  24722  xrge0tsms  24723  cnheibor  24854  cnlmod  25040  csscld  25149  clsocv  25150  cnflduss  25256  cnfldcusp  25257  rrxmvallem  25304  rrxmval  25305  mbfss  25547  mbfmulc2lem  25548  0plef  25573  0pledm  25574  itg1ge0  25587  itg1addlem4  25600  itg2splitlem  25649  itg2addlem  25659  ibl0  25688  iblcnlem  25690  iblss2  25707  itgss3  25716  dvconst  25818  dvcnp2  25821  dvcnp2OLD  25822  dveflem  25883  dv11cn  25906  lhop1lem  25918  plyun0  26102  plyeq0lem  26115  coeeulem  26129  coeeu  26130  coef3  26137  dgrle  26148  0dgrb  26151  coefv0  26153  coemulc  26160  coe1termlem  26163  coe1term  26164  dgr0  26168  dgrmulc  26177  dgrcolem2  26180  vieta1lem2  26219  iaa  26233  aareccl  26234  aalioulem3  26242  taylthlem2  26282  taylthlem2OLD  26283  psercn  26336  pserdvlem2  26338  abelthlem2  26342  abelthlem3  26343  abelthlem5  26345  abelthlem7  26348  abelth  26351  sin2kpi  26392  cos2kpi  26393  sinkpi  26431  efopn  26567  logtayl  26569  cxpval  26573  0cxp  26575  cxpexp  26577  cxpcl  26583  cxpge0  26592  mulcxplem  26593  mulcxp  26594  cxpmul2  26598  dvsqrt  26651  dvcnsqrt  26653  cxpcn3  26658  abscxpbnd  26663  efrlim  26879  efrlimOLD  26880  ftalem2  26984  ftalem3  26985  ftalem4  26986  ftalem5  26987  ftalem7  26989  prmorcht  27088  muinv  27103  1sgm2ppw  27111  logfacbnd3  27134  logexprlim  27136  dchrelbas2  27148  dchrmullid  27163  dchrfi  27166  dchrinv  27172  lgsdir2  27241  lgsdir  27243  addsqnreup  27354  dchrvmasumiflem1  27412  dchrvmasumiflem2  27413  rpvmasum2  27423  log2sumbnd  27455  selberg2lem  27461  logdivbnd  27467  ax5seglem8  28863  axlowdimlem6  28874  axlowdimlem13  28881  ex-co  30367  avril1  30392  vc0  30503  vcz  30504  cnaddabloOLD  30510  cnidOLD  30511  ipasslem8  30766  siilem2  30781  hvmul0  30953  hi01  31025  norm-iii  31069  h1de2ctlem  31484  pjmuli  31618  pjneli  31652  eigre  31764  eigorth  31767  elnlfn  31857  0cnfn  31909  0lnfn  31914  lnopunilem2  31940  sgnneg  32758  xrge0tsmsd  33002  constrsscn  33730  qqh0  33974  qqhcn  33981  eulerpartlemgs2  34371  breprexpnat  34625  hgt750lem2  34643  subfacp1lem6  35172  sinccvglem  35659  abs2sqle  35667  abs2sqlt  35668  tan2h  37606  poimirlem16  37630  poimirlem19  37633  poimirlem31  37645  mblfinlem2  37652  ovoliunnfl  37656  voliunnfl  37658  ftc1anclem5  37691  cntotbnd  37790  60lcm7e420  41998  lcmineqlem10  42026  3lexlogpow5ineq1  42042  sn-1ne2  42253  0tie0  42303  sn-it0e0  42404  addinvcom  42420  sn-0tie0  42439  fltnltalem  42650  flcidc  43159  dvconstbi  44323  expgrowth  44324  dvradcnv2  44336  binomcxplemdvbinom  44342  binomcxplemnotnn0  44345  xralrple3  45370  negcncfg  45879  ioodvbdlimc1  45931  ioodvbdlimc2  45933  itgsinexplem1  45952  stoweidlem26  46024  stoweidlem36  46034  stoweidlem55  46053  stirlinglem8  46079  fourierdlem103  46207  sqwvfoura  46226  sqwvfourb  46227  ovn0lem  46563  nn0sumshdiglemA  48608  nn0sumshdiglemB  48609  nn0sumshdiglem1  48610  sec0  49749