Theorem 0cn 11173

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

Assertion

Ref	Expression
0cn	⊢ 0 ∈ ℂ

Proof of Theorem 0cn

Step	Hyp	Ref	Expression
1		ax-i2m1 11143	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 11134	. . . 4 ⊢ i ∈ ℂ
3		mulcl 11159	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 692	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 11133	. . 3 ⊢ 1 ∈ ℂ
6		addcl 11157	. . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
7	4, 5, 6	mp2an 692	. 2 ⊢ ((i · i) + 1) ∈ ℂ
8	1, 7	eqeltrri 2826	1 ⊢ 0 ∈ ℂ

Syntax hints:   ∈ wcel 2109  (class class class)co 7390  ℂcc 11073  0cc0 11075  1c1 11076  ici 11077   + caddc 11078   · cmul 11080

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 2702  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-mulcl 11137  ax-i2m1 11143

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

This theorem is referenced by:  0cnd  11174  c0ex  11175  1re  11181  00id  11356  mul02lem1  11357  mul02  11359  mul01  11360  addrid  11361  addlid  11364  negcl  11428  subid  11448  subid1  11449  neg0  11475  negid  11476  negsub  11477  subneg  11478  negneg  11479  negeq0  11483  negsubdi  11485  renegcli  11490  mulneg1  11621  msqge0  11706  ixi  11814  muleqadd  11829  diveq0  11854  div0  11877  div0OLD  11878  ofsubge0  12192  0m0e0  12308  nn0sscn  12454  elznn0  12551  ser0  14026  0exp0e1  14038  0exp  14069  sq0  14164  sqeqor  14188  binom2  14189  bcval5  14290  s1co  14806  shftval3  15049  shftidt2  15054  cjne0  15136  sqrt0  15214  abs0  15258  abs00bd  15264  abs2dif  15306  clim0  15479  climz  15522  serclim0  15550  rlimneg  15620  sumrblem  15684  fsumcvg  15685  summolem2a  15688  sumss  15697  fsumss  15698  fsumcvg2  15700  fsumsplit  15714  sumsplit  15741  fsumrelem  15780  fsumrlim  15784  fsumo1  15785  0fallfac  16010  0risefac  16011  binomfallfac  16014  fsumcube  16033  ef0  16064  eftlub  16084  sin0  16124  tan0  16126  divalglem9  16378  sadadd2lem2  16427  sadadd3  16438  bezout  16520  pcmpt2  16871  4sqlem11  16933  ramcl  17007  4001lem2  17119  odadd1  19785  cnaddablx  19805  cnaddabl  19806  cnaddid  19807  frgpnabllem1  19810  cncrng  21307  cncrngOLD  21308  cnfld0  21311  pzriprnglem5  21402  pzriprnglem6  21403  psdmplcl  22056  cnbl0  24668  cnblcld  24669  cnfldnm  24673  cnn0opn  24682  xrge0gsumle  24729  xrge0tsms  24730  cnheibor  24861  cnlmod  25047  csscld  25156  clsocv  25157  cnflduss  25263  cnfldcusp  25264  rrxmvallem  25311  rrxmval  25312  mbfss  25554  mbfmulc2lem  25555  0plef  25580  0pledm  25581  itg1ge0  25594  itg1addlem4  25607  itg2splitlem  25656  itg2addlem  25666  ibl0  25695  iblcnlem  25697  iblss2  25714  itgss3  25723  dvconst  25825  dvcnp2  25828  dvcnp2OLD  25829  dveflem  25890  dv11cn  25913  lhop1lem  25925  plyun0  26109  plyeq0lem  26122  coeeulem  26136  coeeu  26137  coef3  26144  dgrle  26155  0dgrb  26158  coefv0  26160  coemulc  26167  coe1termlem  26170  coe1term  26171  dgr0  26175  dgrmulc  26184  dgrcolem2  26187  vieta1lem2  26226  iaa  26240  aareccl  26241  aalioulem3  26249  taylthlem2  26289  taylthlem2OLD  26290  psercn  26343  pserdvlem2  26345  abelthlem2  26349  abelthlem3  26350  abelthlem5  26352  abelthlem7  26355  abelth  26358  sin2kpi  26399  cos2kpi  26400  sinkpi  26438  efopn  26574  logtayl  26576  cxpval  26580  0cxp  26582  cxpexp  26584  cxpcl  26590  cxpge0  26599  mulcxplem  26600  mulcxp  26601  cxpmul2  26605  dvsqrt  26658  dvcnsqrt  26660  cxpcn3  26665  abscxpbnd  26670  efrlim  26886  efrlimOLD  26887  ftalem2  26991  ftalem3  26992  ftalem4  26993  ftalem5  26994  ftalem7  26996  prmorcht  27095  muinv  27110  1sgm2ppw  27118  logfacbnd3  27141  logexprlim  27143  dchrelbas2  27155  dchrmullid  27170  dchrfi  27173  dchrinv  27179  lgsdir2  27248  lgsdir  27250  addsqnreup  27361  dchrvmasumiflem1  27419  dchrvmasumiflem2  27420  rpvmasum2  27430  log2sumbnd  27462  selberg2lem  27468  logdivbnd  27474  ax5seglem8  28870  axlowdimlem6  28881  axlowdimlem13  28888  ex-co  30374  avril1  30399  vc0  30510  vcz  30511  cnaddabloOLD  30517  cnidOLD  30518  ipasslem8  30773  siilem2  30788  hvmul0  30960  hi01  31032  norm-iii  31076  h1de2ctlem  31491  pjmuli  31625  pjneli  31659  eigre  31771  eigorth  31774  elnlfn  31864  0cnfn  31916  0lnfn  31921  lnopunilem2  31947  sgnneg  32765  xrge0tsmsd  33009  constrsscn  33737  qqh0  33981  qqhcn  33988  eulerpartlemgs2  34378  breprexpnat  34632  hgt750lem2  34650  subfacp1lem6  35179  sinccvglem  35666  abs2sqle  35674  abs2sqlt  35675  tan2h  37613  poimirlem16  37637  poimirlem19  37640  poimirlem31  37652  mblfinlem2  37659  ovoliunnfl  37663  voliunnfl  37665  ftc1anclem5  37698  cntotbnd  37797  60lcm7e420  42005  lcmineqlem10  42033  3lexlogpow5ineq1  42049  sn-1ne2  42260  0tie0  42310  sn-it0e0  42411  addinvcom  42427  sn-0tie0  42446  fltnltalem  42657  flcidc  43166  dvconstbi  44330  expgrowth  44331  dvradcnv2  44343  binomcxplemdvbinom  44349  binomcxplemnotnn0  44352  xralrple3  45377  negcncfg  45886  ioodvbdlimc1  45938  ioodvbdlimc2  45940  itgsinexplem1  45959  stoweidlem26  46031  stoweidlem36  46041  stoweidlem55  46060  stirlinglem8  46086  fourierdlem103  46214  sqwvfoura  46233  sqwvfourb  46234  ovn0lem  46570  nn0sumshdiglemA  48612  nn0sumshdiglemB  48613  nn0sumshdiglem1  48614  sec0  49753