Theorem 0cn 11171

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

Assertion

Ref	Expression
0cn	⊢ 0 ∈ ℂ

Proof of Theorem 0cn

Step	Hyp	Ref	Expression
1		ax-i2m1 11141	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 11132	. . . 4 ⊢ i ∈ ℂ
3		mulcl 11157	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 702	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 11131	. . 3 ⊢ 1 ∈ ℂ
6		addcl 11155	. . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
7	4, 5, 6	mp2an 702	. 2 ⊢ ((i · i) + 1) ∈ ℂ
8	1, 7	eqeltrri 2859	1 ⊢ 0 ∈ ℂ

Syntax hints:   ∈ wcel 2142  (class class class)co 7396  ℂcc 11071  0cc0 11073  1c1 11074  ici 11075   + caddc 11076   · cmul 11078

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-1cn 11131  ax-icn 11132  ax-addcl 11133  ax-mulcl 11135  ax-i2m1 11141

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754  df-clel 2837

This theorem is referenced by:  0cnd  11172  c0ex  11173  1re  11181  00id  11358  mul02lem1  11359  mul02  11361  mul01  11362  addrid  11363  addlid  11366  negcl  11430  subid  11450  subid1  11451  neg0  11477  negid  11478  negsub  11479  subneg  11480  negneg  11481  negeq0  11485  negsubdi  11487  renegcli  11492  mulneg1  11623  msqge0  11708  ixi  11816  muleqadd  11831  diveq0  11855  div0  11878  div0OLD  11879  ofsubge0  12194  0m0e0  12336  nn0sscn  12486  elznn0  12583  ser0  14067  0exp0e1  14079  0exp  14110  sq0  14205  sqeqor  14229  binom2  14230  bcval5  14331  s1co  14846  shftval3  15089  shftidt2  15094  sgnneg  15113  cjne0  15190  sqrt0  15268  abs0  15312  abs00bd  15318  abs2dif  15360  clim0  15533  climz  15576  serclim0  15604  rlimneg  15674  sumrblem  15738  fsumcvg  15739  summolem2a  15742  sumss  15751  fsumss  15752  fsumcvg2  15754  fsumsplit  15768  sumsplit  15795  fsumrelem  15835  fsumrlim  15839  fsumo1  15840  0fallfac  16067  0risefac  16068  binomfallfac  16071  fsumcube  16090  ef0  16121  eftlub  16141  sin0  16181  tan0  16183  divalglem9  16435  sadadd2lem2  16484  sadadd3  16495  bezout  16577  pcmpt2  16929  4sqlem11  16991  ramcl  17065  4001lem2  17178  odadd1  19888  cnaddablx  19908  cnaddabl  19909  cnaddid  19910  frgpnabllem1  19913  cncrng  21445  cnfld0  21448  pzriprnglem5  21537  pzriprnglem6  21538  psdmplcl  22227  cnbl0  24833  cnblcld  24834  cnfldnm  24838  cnn0opn  24847  xrge0gsumle  24894  xrge0tsms  24895  cnheibor  25017  cnlmod  25202  csscld  25311  clsocv  25312  cnflduss  25418  cnfldcusp  25419  rrxmvallem  25466  rrxmval  25467  mbfss  25708  mbfmulc2lem  25709  0plef  25734  0pledm  25735  itg1ge0  25748  itg1addlem4  25761  itg2splitlem  25810  itg2addlem  25820  ibl0  25849  iblcnlem  25851  iblss2  25868  itgss3  25877  dvconst  25979  dvcnp2  25982  dveflem  26041  dv11cn  26063  lhop1lem  26075  plyun0  26257  plyeq0lem  26270  coeeulem  26284  coeeu  26285  coef3  26292  dgrle  26303  0dgrb  26306  coefv0  26308  coemulc  26315  coe1termlem  26318  coe1term  26319  dgr0  26322  dgrmulc  26331  dgrcolem2  26334  vieta1lem2  26375  iaa  26389  aareccl  26390  aalioulem3  26398  taylthlem2  26437  psercn  26489  pserdvlem2  26491  abelthlem2  26495  abelthlem3  26496  abelthlem5  26498  abelthlem7  26501  abelth  26504  sin2kpi  26548  cos2kpi  26549  sinkpi  26587  efopn  26723  logtayl  26725  cxpval  26729  0cxp  26731  cxpexp  26733  cxpcl  26739  cxpge0  26748  mulcxplem  26749  mulcxp  26750  cxpmul2  26754  dvsqrt  26807  dvcnsqrt  26809  cxpcn3  26813  abscxpbnd  26818  efrlim  27034  ftalem2  27138  ftalem3  27139  ftalem4  27140  ftalem5  27141  ftalem7  27143  prmorcht  27242  muinv  27257  1sgm2ppw  27264  logfacbnd3  27287  logexprlim  27289  dchrelbas2  27301  dchrmullid  27316  dchrfi  27319  dchrinv  27325  lgsdir2  27394  lgsdir  27396  addsqnreup  27507  dchrvmasumiflem1  27565  dchrvmasumiflem2  27566  rpvmasum2  27576  log2sumbnd  27608  selberg2lem  27614  logdivbnd  27620  ax5seglem8  29137  axlowdimlem6  29148  axlowdimlem13  29155  ex-co  30640  avril1  30665  vc0  30777  vcz  30778  cnaddabloOLD  30784  cnidOLD  30785  ipasslem8  31040  siilem2  31055  hvmul0  31227  hi01  31299  norm-iii  31343  h1de2ctlem  31758  pjmuli  31892  pjneli  31926  eigre  32038  eigorth  32041  elnlfn  32131  0cnfn  32183  0lnfn  32188  lnopunilem2  32214  xrge0tsmsd  33253  constrsscn  34037  qqh0  34281  qqhcn  34288  eulerpartlemgs2  34677  breprexpnat  34928  hgt750lem2  34946  subfacp1lem6  35535  sinccvglem  36022  abs2sqle  36030  abs2sqlt  36031  tan2h  38111  poimirlem16  38135  poimirlem19  38138  poimirlem31  38150  mblfinlem2  38157  ovoliunnfl  38161  voliunnfl  38163  ftc1anclem5  38196  cntotbnd  38295  60lcm7e420  42627  lcmineqlem10  42655  3lexlogpow5ineq1  42671  sn-1ne2  42880  0tie0  42924  sn-it0e0  43025  addinvcom  43041  sn-0tie0  43073  fltnltalem  43244  flcidc  43747  dvconstbi  44910  expgrowth  44911  dvradcnv2  44923  binomcxplemdvbinom  44929  binomcxplemnotnn0  44932  xralrple3  45949  negcncfg  46455  ioodvbdlimc1  46507  ioodvbdlimc2  46509  itgsinexplem1  46528  stoweidlem26  46600  stoweidlem36  46610  stoweidlem55  46629  stirlinglem8  46655  fourierdlem103  46783  sqwvfoura  46802  sqwvfourb  46803  ovn0lem  47139  nthrucw  47462  nn0sumshdiglemA  49241  nn0sumshdiglemB  49242  nn0sumshdiglem1  49243  sec0  50381