Theorem 0cn 11127

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

Assertion

Ref	Expression
0cn	⊢ 0 ∈ ℂ

Proof of Theorem 0cn

Step	Hyp	Ref	Expression
1		ax-i2m1 11097	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 11088	. . . 4 ⊢ i ∈ ℂ
3		mulcl 11113	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 698	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 11087	. . 3 ⊢ 1 ∈ ℂ
6		addcl 11111	. . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
7	4, 5, 6	mp2an 698	. 2 ⊢ ((i · i) + 1) ∈ ℂ
8	1, 7	eqeltrri 2836	1 ⊢ 0 ∈ ℂ

Syntax hints:   ∈ wcel 2119  (class class class)co 7356  ℂcc 11027  0cc0 11029  1c1 11030  ici 11031   + caddc 11032   · cmul 11034

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-mulcl 11091  ax-i2m1 11097

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-clel 2814

This theorem is referenced by:  0cnd  11128  c0ex  11129  1re  11135  00id  11312  mul02lem1  11313  mul02  11315  mul01  11316  addrid  11317  addlid  11320  negcl  11384  subid  11404  subid1  11405  neg0  11431  negid  11432  negsub  11433  subneg  11434  negneg  11435  negeq0  11439  negsubdi  11441  renegcli  11446  mulneg1  11577  msqge0  11662  ixi  11770  muleqadd  11785  diveq0  11810  div0  11833  div0OLD  11834  ofsubge0  12149  0m0e0  12287  nn0sscn  12433  elznn0  12530  ser0  14007  0exp0e1  14019  0exp  14050  sq0  14145  sqeqor  14169  binom2  14170  bcval5  14271  s1co  14786  shftval3  15029  shftidt2  15034  cjne0  15116  sqrt0  15194  abs0  15238  abs00bd  15244  abs2dif  15286  clim0  15459  climz  15502  serclim0  15530  rlimneg  15600  sumrblem  15664  fsumcvg  15665  summolem2a  15668  sumss  15677  fsumss  15678  fsumcvg2  15680  fsumsplit  15694  sumsplit  15721  fsumrelem  15761  fsumrlim  15765  fsumo1  15766  0fallfac  15993  0risefac  15994  binomfallfac  15997  fsumcube  16016  ef0  16047  eftlub  16067  sin0  16107  tan0  16109  divalglem9  16361  sadadd2lem2  16410  sadadd3  16421  bezout  16503  pcmpt2  16855  4sqlem11  16917  ramcl  16991  4001lem2  17103  odadd1  19814  cnaddablx  19834  cnaddabl  19835  cnaddid  19836  frgpnabllem1  19839  cncrng  21368  cnfld0  21371  pzriprnglem5  21460  pzriprnglem6  21461  psdmplcl  22150  cnbl0  24756  cnblcld  24757  cnfldnm  24761  cnn0opn  24770  xrge0gsumle  24817  xrge0tsms  24818  cnheibor  24940  cnlmod  25125  csscld  25234  clsocv  25235  cnflduss  25341  cnfldcusp  25342  rrxmvallem  25389  rrxmval  25390  mbfss  25631  mbfmulc2lem  25632  0plef  25657  0pledm  25658  itg1ge0  25671  itg1addlem4  25684  itg2splitlem  25733  itg2addlem  25743  ibl0  25772  iblcnlem  25774  iblss2  25791  itgss3  25800  dvconst  25902  dvcnp2  25905  dveflem  25964  dv11cn  25986  lhop1lem  25998  plyun0  26180  plyeq0lem  26193  coeeulem  26207  coeeu  26208  coef3  26215  dgrle  26226  0dgrb  26229  coefv0  26231  coemulc  26238  coe1termlem  26241  coe1term  26242  dgr0  26245  dgrmulc  26254  dgrcolem2  26257  vieta1lem2  26295  iaa  26309  aareccl  26310  aalioulem3  26318  taylthlem2  26357  psercn  26409  pserdvlem2  26411  abelthlem2  26415  abelthlem3  26416  abelthlem5  26418  abelthlem7  26421  abelth  26424  sin2kpi  26465  cos2kpi  26466  sinkpi  26504  efopn  26640  logtayl  26642  cxpval  26646  0cxp  26648  cxpexp  26650  cxpcl  26656  cxpge0  26665  mulcxplem  26666  mulcxp  26667  cxpmul2  26671  dvsqrt  26724  dvcnsqrt  26726  cxpcn3  26730  abscxpbnd  26735  efrlim  26951  ftalem2  27055  ftalem3  27056  ftalem4  27057  ftalem5  27058  ftalem7  27060  prmorcht  27159  muinv  27174  1sgm2ppw  27181  logfacbnd3  27204  logexprlim  27206  dchrelbas2  27218  dchrmullid  27233  dchrfi  27236  dchrinv  27242  lgsdir2  27311  lgsdir  27313  addsqnreup  27424  dchrvmasumiflem1  27482  dchrvmasumiflem2  27483  rpvmasum2  27493  log2sumbnd  27525  selberg2lem  27531  logdivbnd  27537  ax5seglem8  29023  axlowdimlem6  29034  axlowdimlem13  29041  ex-co  30526  avril1  30551  vc0  30663  vcz  30664  cnaddabloOLD  30670  cnidOLD  30671  ipasslem8  30926  siilem2  30941  hvmul0  31113  hi01  31185  norm-iii  31229  h1de2ctlem  31644  pjmuli  31778  pjneli  31812  eigre  31924  eigorth  31927  elnlfn  32017  0cnfn  32069  0lnfn  32074  lnopunilem2  32100  sgnneg  32925  xrge0tsmsd  33154  constrsscn  33924  qqh0  34168  qqhcn  34175  eulerpartlemgs2  34564  breprexpnat  34818  hgt750lem2  34836  subfacp1lem6  35413  sinccvglem  35900  abs2sqle  35908  abs2sqlt  35909  tan2h  37979  poimirlem16  38003  poimirlem19  38006  poimirlem31  38018  mblfinlem2  38025  ovoliunnfl  38029  voliunnfl  38031  ftc1anclem5  38064  cntotbnd  38163  60lcm7e420  42495  lcmineqlem10  42523  3lexlogpow5ineq1  42539  sn-1ne2  42748  0tie0  42792  sn-it0e0  42893  addinvcom  42909  sn-0tie0  42941  fltnltalem  43112  flcidc  43615  dvconstbi  44778  expgrowth  44779  dvradcnv2  44791  binomcxplemdvbinom  44797  binomcxplemnotnn0  44800  xralrple3  45818  negcncfg  46324  ioodvbdlimc1  46376  ioodvbdlimc2  46378  itgsinexplem1  46397  stoweidlem26  46469  stoweidlem36  46479  stoweidlem55  46498  stirlinglem8  46524  fourierdlem103  46652  sqwvfoura  46671  sqwvfourb  46672  ovn0lem  47008  nthrucw  47331  nn0sumshdiglemA  49110  nn0sumshdiglemB  49111  nn0sumshdiglem1  49112  sec0  50250