Theorem 0cn 10427

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

Assertion

Ref	Expression
0cn	⊢ 0 ∈ ℂ

Proof of Theorem 0cn

Step	Hyp	Ref	Expression
1		ax-i2m1 10399	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 10390	. . . 4 ⊢ i ∈ ℂ
3		mulcl 10415	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 679	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 10389	. . 3 ⊢ 1 ∈ ℂ
6		addcl 10413	. . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
7	4, 5, 6	mp2an 679	. 2 ⊢ ((i · i) + 1) ∈ ℂ
8	1, 7	eqeltrri 2860	1 ⊢ 0 ∈ ℂ

Syntax hints:   ∈ wcel 2048  (class class class)co 6974  ℂcc 10329  0cc0 10331  1c1 10332  ici 10333   + caddc 10334   · cmul 10336

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-ext 2747  ax-1cn 10389  ax-icn 10390  ax-addcl 10391  ax-mulcl 10393  ax-i2m1 10399

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-cleq 2768  df-clel 2843

This theorem is referenced by:  0cnd  10428  c0ex  10429  1re  10435  00id  10611  mul02lem1  10612  mul02  10614  mul01  10615  addid1  10616  addid2  10619  negcl  10682  subid  10702  subid1  10703  neg0  10729  negid  10730  negsub  10731  subneg  10732  negneg  10733  negeq0  10737  negsubdi  10739  renegcli  10744  mulneg1  10873  msqge0  10958  ixi  11066  muleqadd  11081  div0  11125  ofsubge0  11434  0m0e0  11564  nn0sscn  11709  elznn0  11805  ser0  13234  0exp0e1  13246  0exp  13276  sq0  13367  sqeqor  13390  binom2  13391  bcval5  13490  s1co  14051  shftval3  14290  shftidt2  14295  cjne0  14377  sqrt0  14456  abs0  14500  abs00bd  14506  abs2dif  14547  clim0  14718  climz  14761  serclim0  14789  rlimneg  14858  sumrblem  14922  fsumcvg  14923  summolem2a  14926  sumss  14935  fsumss  14936  fsumcvg2  14938  fsumsplit  14951  sumsplit  14977  fsumrelem  15016  fsumrlim  15020  fsumo1  15021  0fallfac  15245  0risefac  15246  binomfallfac  15249  fsumcube  15268  ef0  15298  eftlub  15316  sin0  15356  tan0  15358  divalglem9  15606  sadadd2lem2  15653  sadadd3  15664  bezout  15741  pcmpt2  16079  4sqlem11  16141  ramcl  16215  4001lem2  16325  odadd1  18718  cnaddablx  18738  cnaddabl  18739  cnaddid  18740  frgpnabllem1  18743  cncrng  20262  cnfld0  20265  cnbl0  23079  cnblcld  23080  cnfldnm  23084  xrge0gsumle  23138  xrge0tsms  23139  cnheibor  23256  cnlmod  23441  csscld  23549  clsocv  23550  cnflduss  23656  cnfldcusp  23657  rrxmvallem  23704  rrxmval  23705  mbfss  23944  mbfmulc2lem  23945  0plef  23970  0pledm  23971  itg1ge0  23984  itg1addlem4  23997  itg2splitlem  24046  itg2addlem  24056  ibl0  24084  iblcnlem  24086  iblss2  24103  itgss3  24112  dvconst  24211  dvcnp2  24214  dvrec  24249  dvexp3  24272  dveflem  24273  dv11cn  24295  lhop1lem  24307  plyun0  24484  plyeq0lem  24497  coeeulem  24511  coeeu  24512  coef3  24519  dgrle  24530  0dgrb  24533  coefv0  24535  coemulc  24542  coe1termlem  24545  coe1term  24546  dgr0  24549  dgrmulc  24558  dgrcolem2  24561  vieta1lem2  24597  iaa  24611  aareccl  24612  aalioulem3  24620  taylthlem2  24659  psercn  24711  pserdvlem2  24713  abelthlem2  24717  abelthlem3  24718  abelthlem5  24720  abelthlem7  24723  abelth  24726  sin2kpi  24766  cos2kpi  24767  sinkpi  24804  efopn  24936  logtayl  24938  cxpval  24942  0cxp  24944  cxpexp  24946  cxpcl  24952  cxpge0  24961  mulcxplem  24962  mulcxp  24963  cxpmul2  24967  dvsqrt  25018  dvcnsqrt  25020  cxpcn3  25024  abscxpbnd  25029  efrlim  25243  ftalem2  25347  ftalem3  25348  ftalem4  25349  ftalem5  25350  ftalem7  25352  prmorcht  25451  muinv  25466  1sgm2ppw  25472  logfacbnd3  25495  logexprlim  25497  dchrelbas2  25509  dchrmulid2  25524  dchrfi  25527  dchrinv  25533  lgsdir2  25602  lgsdir  25604  addsqnreup  25715  dchrvmasumiflem1  25773  dchrvmasumiflem2  25774  rpvmasum2  25784  log2sumbnd  25816  selberg2lem  25822  logdivbnd  25828  ax5seglem8  26419  axlowdimlem6  26430  axlowdimlem13  26437  ex-co  27989  avril1  28013  vc0  28122  vcz  28123  cnaddabloOLD  28129  cnidOLD  28130  ipasslem8  28385  siilem2  28400  hvmul0  28574  hi01  28646  norm-iii  28690  h1de2ctlem  29107  pjmuli  29241  pjneli  29275  eigre  29387  eigorth  29390  elnlfn  29480  0cnfn  29532  0lnfn  29537  lnopunilem2  29563  xrge0tsmsd  30521  qqh0  30860  qqhcn  30867  eulerpartlemgs2  31274  sgnneg  31435  breprexpnat  31544  hgt750lem2  31562  subfacp1lem6  32007  sinccvglem  32405  abs2sqle  32413  abs2sqlt  32414  tan2h  34303  poimirlem16  34327  poimirlem19  34330  poimirlem31  34342  mblfinlem2  34349  ovoliunnfl  34353  voliunnfl  34355  dvtanlem  34360  ftc1anclem5  34390  cntotbnd  34494  fltnltalem  38659  flcidc  39148  dvconstbi  40059  expgrowth  40060  dvradcnv2  40072  binomcxplemdvbinom  40078  binomcxplemnotnn0  40081  xralrple3  41050  negcncfg  41573  ioodvbdlimc1  41627  ioodvbdlimc2  41629  itgsinexplem1  41648  stoweidlem26  41721  stoweidlem36  41731  stoweidlem55  41750  stirlinglem8  41776  fourierdlem103  41904  sqwvfoura  41923  sqwvfourb  41924  ovn0lem  42257  nn0sumshdiglemA  44021  nn0sumshdiglemB  44022  nn0sumshdiglem1  44023  sec0  44200