Theorem 0cn 11215

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

Assertion

Ref	Expression
0cn	⊢ 0 ∈ ℂ

Proof of Theorem 0cn

Step	Hyp	Ref	Expression
1		ax-i2m1 11185	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 11176	. . . 4 ⊢ i ∈ ℂ
3		mulcl 11201	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 705	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 11175	. . 3 ⊢ 1 ∈ ℂ
6		addcl 11199	. . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
7	4, 5, 6	mp2an 705	. 2 ⊢ ((i · i) + 1) ∈ ℂ
8	1, 7	eqeltrri 2862	1 ⊢ 0 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2146  (class class class)co 7419  ℂcc 11115  0cc0 11117  1c1 11118  ici 11119   + caddc 11120   · cmul 11122

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-1cn 11175  ax-icn 11176  ax-addcl 11177  ax-mulcl 11179  ax-i2m1 11185

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-clel 2840

This theorem is used by:  0cnd  11216  c0ex  11217  1re  11225  00id  11402  mul02lem1  11403  mul02  11405  mul01  11406  addrid  11407  addlid  11410  negcl  11474  subid  11494  subid1  11495  neg0  11521  negid  11522  negsub  11523  subneg  11524  negneg  11525  negeq0  11529  negsubdi  11531  renegcli  11536  mulneg1  11667  msqge0  11752  ixi  11860  muleqadd  11875  diveq0  11899  div0  11920  ofsubge0  12234  0m0e0  12376  nn0sscn  12526  elznn0  12623  ser0  14110  0exp0e1  14122  0exp  14153  sq0  14248  sqeqor  14272  binom2  14273  bcval5  14374  s1co  14896  shftval3  15139  shftidt2  15144  sgnneg  15163  cjne0  15240  sqrt0  15318  abs0  15362  abs00bd  15368  abs2dif  15410  clim0  15583  climz  15626  serclim0  15654  rlimneg  15724  sumrblem  15787  fsumcvg  15788  summolem2a  15791  sumss  15800  fsumss  15801  fsumcvg2  15803  fsumsplit  15817  sumsplit  15844  fsumrelem  15884  fsumrlim  15888  fsumo1  15889  0fallfac  16115  0risefac  16116  binomfallfac  16119  fsumcube  16138  ef0  16169  eftlub  16189  sin0  16229  tan0  16231  divalglem9  16483  sadadd2lem2  16532  sadadd3  16543  bezout  16625  pcmpt2  16977  4sqlem11  17039  ramcl  17113  4001lem2  17226  odadd1  19964  cnaddablx  19984  cnaddabl  19985  cnaddid  19986  frgpnabllem1  19989  cncrng  21595  cnfld0  21598  pzriprnglem5  21687  pzriprnglem6  21688  psdmplcl  22377  cnbl0  24983  cnblcld  24984  cnfldnm  24988  cnn0opn  24997  xrge0gsumle  25044  xrge0tsms  25045  cnheibor  25167  cnlmod  25352  csscld  25461  clsocv  25462  cnflduss  25568  cnfldcusp  25569  rrxmvallem  25616  rrxmval  25617  mbfss  25858  mbfmulc2lem  25859  0plef  25884  0pledm  25885  itg1ge0  25898  itg1addlem4  25911  itg2splitlem  25960  itg2addlem  25970  ibl0  25999  iblcnlem  26001  iblss2  26018  itgss3  26027  dvconst  26129  dvcnp2  26132  dveflem  26191  dv11cn  26213  lhop1lem  26225  plyun0  26407  plyeq0lem  26420  coeeulem  26434  coeeu  26435  coef3  26442  dgrle  26453  0dgrb  26456  coefv0  26458  coemulc  26465  coe1termlem  26468  coe1term  26469  dgr0  26472  dgrmulc  26481  dgrcolem2  26484  vieta1lem2  26525  iaa  26541  aareccl  26542  aalioulem3  26550  taylthlem2  26590  psercn  26642  pserdvlem2  26644  abelthlem2  26648  abelthlem3  26649  abelthlem5  26651  abelthlem7  26654  abelth  26657  sin2kpi  26701  cos2kpi  26702  sinkpi  26740  efopn  26876  logtayl  26878  cxpval  26882  0cxp  26884  cxpexp  26886  cxpcl  26892  cxpge0  26901  mulcxplem  26902  mulcxp  26903  cxpmul2  26907  dvsqrt  26960  dvcnsqrt  26962  cxpcn3  26966  abscxpbnd  26971  efrlim  27187  ftalem2  27291  ftalem3  27292  ftalem4  27293  ftalem5  27294  ftalem7  27296  prmorcht  27395  muinv  27410  1sgm2ppw  27417  logfacbnd3  27440  logexprlim  27442  dchrelbas2  27454  dchrmullid  27469  dchrfi  27472  dchrinv  27478  lgsdir2  27547  lgsdir  27549  addsqnreup  27660  dchrvmasumiflem1  27718  dchrvmasumiflem2  27719  rpvmasum2  27729  log2sumbnd  27761  selberg2lem  27767  logdivbnd  27773  ax5seglem8  29343  axlowdimlem6  29354  axlowdimlem13  29361  ex-co  30862  avril1  30887  vc0  30999  vcz  31000  cnaddabloOLD  31006  cnidOLD  31007  ipasslem8  31262  siilem2  31277  hvmul0  31449  hi01  31521  norm-iii  31565  h1de2ctlem  31980  pjmuli  32114  pjneli  32148  eigre  32260  eigorth  32263  elnlfn  32353  0cnfn  32405  0lnfn  32410  lnopunilem2  32436  xrge0tsmsd  33459  constrsscn  34196  qqh0  34440  qqhcn  34447  eulerpartlemgs2  34837  breprexpnat  35088  hgt750lem2  35106  subfacp1lem6  35716  sinccvglem  36203  abs2sqle  36211  abs2sqlt  36212  tan2h  38322  poimirlem16  38346  poimirlem19  38349  poimirlem31  38361  mblfinlem2  38368  ovoliunnfl  38372  voliunnfl  38374  ftc1anclem5  38407  cntotbnd  38507  60lcm7e420  42837  lcmineqlem10  42865  3lexlogpow5ineq1  42881  25or6to4  43033  sn-1ne2  43092  0tie0  43136  sn-it0e0  43237  addinvcom  43253  sn-0tie0  43285  fltnltalem  43454  flcidc  43957  dvconstbi  45104  expgrowth  45105  dvradcnv2  45117  binomcxplemdvbinom  45123  binomcxplemnotnn0  45126  xralrple3  46149  negcncfg  46655  ioodvbdlimc1  46707  ioodvbdlimc2  46709  itgsinexplem1  46728  stoweidlem26  46800  stoweidlem36  46810  stoweidlem55  46829  stirlinglem8  46855  fourierdlem103  46983  sqwvfoura  47002  sqwvfourb  47003  ovn0lem  47339  sqrtnnaa  47664  sqrtnzqaa  47665  nn0sumshdiglemA  49458  nn0sumshdiglemB  49459  nn0sumshdiglem1  49460  sec0  50597