Theorem 0cn 9888

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

Assertion

Ref	Expression
0cn	⊢ 0 ∈ ℂ

Proof of Theorem 0cn

Step	Hyp	Ref	Expression
1		ax-i2m1 9860	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 9851	. . . 4 ⊢ i ∈ ℂ
3		mulcl 9876	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 703	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 9850	. . 3 ⊢ 1 ∈ ℂ
6		addcl 9874	. . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
7	4, 5, 6	mp2an 703	. 2 ⊢ ((i · i) + 1) ∈ ℂ
8	1, 7	eqeltrri 2684	1 ⊢ 0 ∈ ℂ

Syntax hints:   ∈ wcel 1976  (class class class)co 6526  ℂcc 9790  0cc0 9792  1c1 9793  ici 9794   + caddc 9795   · cmul 9797

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-ext 2589  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-mulcl 9854  ax-i2m1 9860

This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-cleq 2602  df-clel 2605

This theorem is referenced by:  0cnd  9889  c0ex  9890  1re  9895  00id  10062  mul02lem1  10063  mul02  10065  mul01  10066  addid1  10067  addid2  10070  negcl  10132  subid  10151  subid1  10152  neg0  10178  negid  10179  negsub  10180  subneg  10181  negneg  10182  negeq0  10186  negsubdi  10188  renegcli  10193  mulneg1  10317  msqge0  10400  ixi  10507  muleqadd  10522  div0  10566  ofsubge0  10868  0m0e0  10979  elznn0  11227  ser0  12672  0exp0e1  12684  0exp  12714  sq0  12774  sqeqor  12797  binom2  12798  bcval5  12924  s1co  13378  shftval3  13612  shftidt2  13617  cjne0  13699  sqrt0  13778  abs0  13821  abs00bd  13827  abs2dif  13868  clim0  14033  climz  14076  serclim0  14104  rlimneg  14173  sumrblem  14237  fsumcvg  14238  summolem2a  14241  sumss  14250  fsumss  14251  fsumcvg2  14253  fsumsplit  14266  sumsplit  14289  fsumrelem  14328  fsumrlim  14332  fsumo1  14333  0fallfac  14555  0risefac  14556  binomfallfac  14559  fsumcube  14578  ef0  14608  eftlub  14626  sin0  14666  tan0  14668  divalglem9  14910  sadadd2lem2  14958  sadadd3  14969  bezout  15046  pcmpt2  15383  4sqlem11  15445  ramcl  15519  4001lem2  15635  odadd1  18022  cnaddablx  18042  cnaddabl  18043  cnaddid  18044  frgpnabllem1  18047  cncrng  19534  cnfld0  19537  cnbl0  22334  cnblcld  22335  cnfldnm  22339  xrge0gsumle  22391  xrge0tsms  22392  cnheibor  22509  cnlmod  22695  csscld  22800  clsocv  22801  cnflduss  22904  cnfldcusp  22905  rrxmvallem  22939  rrxmval  22940  mbfss  23163  mbfmulc2lem  23164  0plef  23189  0pledm  23190  itg1ge0  23203  itg1addlem4  23216  itg2splitlem  23265  itg2addlem  23275  ibl0  23303  iblcnlem  23305  iblss2  23322  itgss3  23331  dvconst  23430  dvcnp2  23433  dvrec  23468  dvexp3  23489  dveflem  23490  dvef  23491  dv11cn  23512  lhop1lem  23524  plyun0  23701  plyeq0lem  23714  coeeulem  23728  coeeu  23729  coef3  23736  dgrle  23747  0dgrb  23750  coefv0  23752  coemulc  23759  coe1termlem  23762  coe1term  23763  dgr0  23766  dgrmulc  23775  dgrcolem2  23778  vieta1lem2  23814  iaa  23828  aareccl  23829  aalioulem3  23837  taylthlem2  23876  psercn  23928  pserdvlem2  23930  abelthlem2  23934  abelthlem3  23935  abelthlem5  23937  abelthlem7  23940  abelth  23943  sin2kpi  23983  cos2kpi  23984  sinkpi  24019  efopn  24148  logtayl  24150  cxpval  24154  0cxp  24156  cxpexp  24158  cxpcl  24164  cxpge0  24173  mulcxplem  24174  mulcxp  24175  cxpmul2  24179  dvsqrt  24227  dvcnsqrt  24229  cxpcn3  24233  abscxpbnd  24238  efrlim  24440  ftalem2  24544  ftalem3  24545  ftalem4  24546  ftalem5  24547  ftalem7  24549  prmorcht  24648  muinv  24663  1sgm2ppw  24669  logfacbnd3  24692  logexprlim  24694  dchrelbas2  24706  dchrmulid2  24721  dchrfi  24724  dchrinv  24730  lgsdir2  24799  lgsdir  24801  dchrvmasumiflem1  24934  dchrvmasumiflem2  24935  rpvmasum2  24945  log2sumbnd  24977  selberg2lem  24983  logdivbnd  24989  ax5seglem8  25561  axlowdimlem6  25572  axlowdimlem13  25579  ex-co  26480  avril1  26504  vc0  26606  vcz  26607  cnaddabloOLD  26613  cnidOLD  26614  ipasslem8  26869  siilem2  26884  hvmul0  27058  hi01  27130  norm-iii  27174  h1de2ctlem  27591  pjmuli  27725  pjneli  27759  eigre  27871  eigorth  27874  elnlfn  27964  0cnfn  28016  0lnfn  28021  lnopunilem2  28047  xrge0tsmsd  28909  qqh0  29149  qqhcn  29156  eulerpartlemgs2  29562  sgnneg  29722  subfacp1lem6  30214  sinccvglem  30613  abs2sqle  30621  abs2sqlt  30622  tan2h  32354  poimirlem16  32378  poimirlem19  32381  poimirlem31  32393  mblfinlem2  32400  ovoliunnfl  32404  voliunnfl  32406  dvtanlem  32412  ftc1anclem5  32442  cntotbnd  32548  flcidc  36546  dvconstbi  37338  expgrowth  37339  dvradcnv2  37351  binomcxplemdvbinom  37357  binomcxplemnotnn0  37360  xralrple3  38314  negcncfg  38549  ioodvbdlimc1  38606  ioodvbdlimc2  38608  itgsinexplem1  38628  stoweidlem26  38702  stoweidlem36  38712  stoweidlem55  38731  stirlinglem8  38757  fourierdlem103  38885  sqwvfoura  38904  sqwvfourb  38905  ovn0lem  39238  nn0sumshdiglemA  42192  nn0sumshdiglemB  42193  nn0sumshdiglem1  42194  sec0  42242