Theorem 0cn 11095

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

Assertion

Ref	Expression
0cn	⊢ 0 ∈ ℂ

Proof of Theorem 0cn

Step	Hyp	Ref	Expression
1		ax-i2m1 11065	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 11056	. . . 4 ⊢ i ∈ ℂ
3		mulcl 11081	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 692	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 11055	. . 3 ⊢ 1 ∈ ℂ
6		addcl 11079	. . 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 7340  ℂcc 10995  0cc0 10997  1c1 10998  ici 10999   + caddc 11000   · cmul 11002

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 11055  ax-icn 11056  ax-addcl 11057  ax-mulcl 11059  ax-i2m1 11065

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  11096  c0ex  11097  1re  11103  00id  11279  mul02lem1  11280  mul02  11282  mul01  11283  addrid  11284  addlid  11287  negcl  11351  subid  11371  subid1  11372  neg0  11398  negid  11399  negsub  11400  subneg  11401  negneg  11402  negeq0  11406  negsubdi  11408  renegcli  11413  mulneg1  11544  msqge0  11629  ixi  11737  muleqadd  11752  diveq0  11777  div0  11800  div0OLD  11801  ofsubge0  12115  0m0e0  12231  nn0sscn  12377  elznn0  12474  ser0  13949  0exp0e1  13961  0exp  13992  sq0  14087  sqeqor  14111  binom2  14112  bcval5  14213  s1co  14727  shftval3  14970  shftidt2  14975  cjne0  15057  sqrt0  15135  abs0  15179  abs00bd  15185  abs2dif  15227  clim0  15400  climz  15443  serclim0  15471  rlimneg  15541  sumrblem  15605  fsumcvg  15606  summolem2a  15609  sumss  15618  fsumss  15619  fsumcvg2  15621  fsumsplit  15635  sumsplit  15662  fsumrelem  15701  fsumrlim  15705  fsumo1  15706  0fallfac  15931  0risefac  15932  binomfallfac  15935  fsumcube  15954  ef0  15985  eftlub  16005  sin0  16045  tan0  16047  divalglem9  16299  sadadd2lem2  16348  sadadd3  16359  bezout  16441  pcmpt2  16792  4sqlem11  16854  ramcl  16928  4001lem2  17040  odadd1  19714  cnaddablx  19734  cnaddabl  19735  cnaddid  19736  frgpnabllem1  19739  cncrng  21279  cncrngOLD  21280  cnfld0  21283  pzriprnglem5  21376  pzriprnglem6  21377  psdmplcl  22031  cnbl0  24642  cnblcld  24643  cnfldnm  24647  cnn0opn  24656  xrge0gsumle  24703  xrge0tsms  24704  cnheibor  24835  cnlmod  25021  csscld  25130  clsocv  25131  cnflduss  25237  cnfldcusp  25238  rrxmvallem  25285  rrxmval  25286  mbfss  25528  mbfmulc2lem  25529  0plef  25554  0pledm  25555  itg1ge0  25568  itg1addlem4  25581  itg2splitlem  25630  itg2addlem  25640  ibl0  25669  iblcnlem  25671  iblss2  25688  itgss3  25697  dvconst  25799  dvcnp2  25802  dvcnp2OLD  25803  dveflem  25864  dv11cn  25887  lhop1lem  25899  plyun0  26083  plyeq0lem  26096  coeeulem  26110  coeeu  26111  coef3  26118  dgrle  26129  0dgrb  26132  coefv0  26134  coemulc  26141  coe1termlem  26144  coe1term  26145  dgr0  26149  dgrmulc  26158  dgrcolem2  26161  vieta1lem2  26200  iaa  26214  aareccl  26215  aalioulem3  26223  taylthlem2  26263  taylthlem2OLD  26264  psercn  26317  pserdvlem2  26319  abelthlem2  26323  abelthlem3  26324  abelthlem5  26326  abelthlem7  26329  abelth  26332  sin2kpi  26373  cos2kpi  26374  sinkpi  26412  efopn  26548  logtayl  26550  cxpval  26554  0cxp  26556  cxpexp  26558  cxpcl  26564  cxpge0  26573  mulcxplem  26574  mulcxp  26575  cxpmul2  26579  dvsqrt  26632  dvcnsqrt  26634  cxpcn3  26639  abscxpbnd  26644  efrlim  26860  efrlimOLD  26861  ftalem2  26965  ftalem3  26966  ftalem4  26967  ftalem5  26968  ftalem7  26970  prmorcht  27069  muinv  27084  1sgm2ppw  27092  logfacbnd3  27115  logexprlim  27117  dchrelbas2  27129  dchrmullid  27144  dchrfi  27147  dchrinv  27153  lgsdir2  27222  lgsdir  27224  addsqnreup  27335  dchrvmasumiflem1  27393  dchrvmasumiflem2  27394  rpvmasum2  27404  log2sumbnd  27436  selberg2lem  27442  logdivbnd  27448  ax5seglem8  28868  axlowdimlem6  28879  axlowdimlem13  28886  ex-co  30369  avril1  30394  vc0  30505  vcz  30506  cnaddabloOLD  30512  cnidOLD  30513  ipasslem8  30768  siilem2  30783  hvmul0  30955  hi01  31027  norm-iii  31071  h1de2ctlem  31486  pjmuli  31620  pjneli  31654  eigre  31766  eigorth  31769  elnlfn  31859  0cnfn  31911  0lnfn  31916  lnopunilem2  31942  sgnneg  32771  xrge0tsmsd  33010  constrsscn  33721  qqh0  33965  qqhcn  33972  eulerpartlemgs2  34361  breprexpnat  34615  hgt750lem2  34633  subfacp1lem6  35175  sinccvglem  35662  abs2sqle  35670  abs2sqlt  35671  tan2h  37609  poimirlem16  37633  poimirlem19  37636  poimirlem31  37648  mblfinlem2  37655  ovoliunnfl  37659  voliunnfl  37661  ftc1anclem5  37694  cntotbnd  37793  60lcm7e420  42000  lcmineqlem10  42028  3lexlogpow5ineq1  42044  sn-1ne2  42255  0tie0  42305  sn-it0e0  42406  addinvcom  42422  sn-0tie0  42441  fltnltalem  42652  flcidc  43160  dvconstbi  44324  expgrowth  44325  dvradcnv2  44337  binomcxplemdvbinom  44343  binomcxplemnotnn0  44346  xralrple3  45369  negcncfg  45876  ioodvbdlimc1  45928  ioodvbdlimc2  45930  itgsinexplem1  45949  stoweidlem26  46021  stoweidlem36  46031  stoweidlem55  46050  stirlinglem8  46076  fourierdlem103  46204  sqwvfoura  46223  sqwvfourb  46224  ovn0lem  46560  nn0sumshdiglemA  48618  nn0sumshdiglemB  48619  nn0sumshdiglem1  48620  sec0  49759