Theorem 0cn 10790

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

Assertion

Ref	Expression
0cn	⊢ 0 ∈ ℂ

Proof of Theorem 0cn

Step	Hyp	Ref	Expression
1		ax-i2m1 10762	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 10753	. . . 4 ⊢ i ∈ ℂ
3		mulcl 10778	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 692	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 10752	. . 3 ⊢ 1 ∈ ℂ
6		addcl 10776	. . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
7	4, 5, 6	mp2an 692	. 2 ⊢ ((i · i) + 1) ∈ ℂ
8	1, 7	eqeltrri 2828	1 ⊢ 0 ∈ ℂ

Syntax hints:   ∈ wcel 2112  (class class class)co 7191  ℂcc 10692  0cc0 10694  1c1 10695  ici 10696   + caddc 10697   · cmul 10699

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708  ax-1cn 10752  ax-icn 10753  ax-addcl 10754  ax-mulcl 10756  ax-i2m1 10762

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2728  df-clel 2809

This theorem is referenced by:  0cnd  10791  c0ex  10792  1re  10798  00id  10972  mul02lem1  10973  mul02  10975  mul01  10976  addid1  10977  addid2  10980  negcl  11043  subid  11062  subid1  11063  neg0  11089  negid  11090  negsub  11091  subneg  11092  negneg  11093  negeq0  11097  negsubdi  11099  renegcli  11104  mulneg1  11233  msqge0  11318  ixi  11426  muleqadd  11441  div0  11485  ofsubge0  11794  0m0e0  11915  nn0sscn  12060  elznn0  12156  ser0  13593  0exp0e1  13605  0exp  13635  sq0  13726  sqeqor  13749  binom2  13750  bcval5  13849  s1co  14363  shftval3  14604  shftidt2  14609  cjne0  14691  sqrt0  14770  abs0  14814  abs00bd  14820  abs2dif  14861  clim0  15032  climz  15075  serclim0  15103  rlimneg  15175  sumrblem  15240  fsumcvg  15241  summolem2a  15244  sumss  15253  fsumss  15254  fsumcvg2  15256  fsumsplit  15269  sumsplit  15295  fsumrelem  15334  fsumrlim  15338  fsumo1  15339  0fallfac  15562  0risefac  15563  binomfallfac  15566  fsumcube  15585  ef0  15615  eftlub  15633  sin0  15673  tan0  15675  divalglem9  15925  sadadd2lem2  15972  sadadd3  15983  bezout  16066  pcmpt2  16409  4sqlem11  16471  ramcl  16545  4001lem2  16658  odadd1  19187  cnaddablx  19207  cnaddabl  19208  cnaddid  19209  frgpnabllem1  19212  cncrng  20338  cnfld0  20341  cnbl0  23625  cnblcld  23626  cnfldnm  23630  xrge0gsumle  23684  xrge0tsms  23685  cnheibor  23806  cnlmod  23991  csscld  24100  clsocv  24101  cnflduss  24207  cnfldcusp  24208  rrxmvallem  24255  rrxmval  24256  mbfss  24497  mbfmulc2lem  24498  0plef  24523  0pledm  24524  itg1ge0  24537  itg1addlem4  24550  itg1addlem4OLD  24551  itg2splitlem  24600  itg2addlem  24610  ibl0  24638  iblcnlem  24640  iblss2  24657  itgss3  24666  dvconst  24768  dvcnp2  24771  dvrec  24806  dvexp3  24829  dveflem  24830  dv11cn  24852  lhop1lem  24864  plyun0  25045  plyeq0lem  25058  coeeulem  25072  coeeu  25073  coef3  25080  dgrle  25091  0dgrb  25094  coefv0  25096  coemulc  25103  coe1termlem  25106  coe1term  25107  dgr0  25110  dgrmulc  25119  dgrcolem2  25122  vieta1lem2  25158  iaa  25172  aareccl  25173  aalioulem3  25181  taylthlem2  25220  psercn  25272  pserdvlem2  25274  abelthlem2  25278  abelthlem3  25279  abelthlem5  25281  abelthlem7  25284  abelth  25287  sin2kpi  25327  cos2kpi  25328  sinkpi  25365  efopn  25500  logtayl  25502  cxpval  25506  0cxp  25508  cxpexp  25510  cxpcl  25516  cxpge0  25525  mulcxplem  25526  mulcxp  25527  cxpmul2  25531  dvsqrt  25582  dvcnsqrt  25584  cxpcn3  25588  abscxpbnd  25593  efrlim  25806  ftalem2  25910  ftalem3  25911  ftalem4  25912  ftalem5  25913  ftalem7  25915  prmorcht  26014  muinv  26029  1sgm2ppw  26035  logfacbnd3  26058  logexprlim  26060  dchrelbas2  26072  dchrmulid2  26087  dchrfi  26090  dchrinv  26096  lgsdir2  26165  lgsdir  26167  addsqnreup  26278  dchrvmasumiflem1  26336  dchrvmasumiflem2  26337  rpvmasum2  26347  log2sumbnd  26379  selberg2lem  26385  logdivbnd  26391  ax5seglem8  26981  axlowdimlem6  26992  axlowdimlem13  26999  ex-co  28475  avril1  28500  vc0  28609  vcz  28610  cnaddabloOLD  28616  cnidOLD  28617  ipasslem8  28872  siilem2  28887  hvmul0  29059  hi01  29131  norm-iii  29175  h1de2ctlem  29590  pjmuli  29724  pjneli  29758  eigre  29870  eigorth  29873  elnlfn  29963  0cnfn  30015  0lnfn  30020  lnopunilem2  30046  xrge0tsmsd  30990  qqh0  31600  qqhcn  31607  eulerpartlemgs2  32013  sgnneg  32173  breprexpnat  32280  hgt750lem2  32298  subfacp1lem6  32814  sinccvglem  33297  abs2sqle  33305  abs2sqlt  33306  tan2h  35455  poimirlem16  35479  poimirlem19  35482  poimirlem31  35494  mblfinlem2  35501  ovoliunnfl  35505  voliunnfl  35507  dvtanlem  35512  ftc1anclem5  35540  cntotbnd  35640  60lcm7e420  39701  lcmineqlem10  39729  3lexlogpow5ineq1  39745  sn-1ne2  39943  sn-it0e0  40046  addinvcom  40062  sn-0tie0  40070  fltnltalem  40143  flcidc  40643  dvconstbi  41566  expgrowth  41567  dvradcnv2  41579  binomcxplemdvbinom  41585  binomcxplemnotnn0  41588  xralrple3  42527  negcncfg  43040  ioodvbdlimc1  43092  ioodvbdlimc2  43094  itgsinexplem1  43113  stoweidlem26  43185  stoweidlem36  43195  stoweidlem55  43214  stirlinglem8  43240  fourierdlem103  43368  sqwvfoura  43387  sqwvfourb  43388  ovn0lem  43721  nn0sumshdiglemA  45581  nn0sumshdiglemB  45582  nn0sumshdiglem1  45583  sec0  46076