Theorem 0cnd 9375

Description: 0 is a complex number, deductive form. (Contributed by David A. Wheeler, 8-Dec-2018.)

Assertion

Ref	Expression
0cnd	|- ( ph -> 0 e. CC )

Proof of Theorem 0cnd

Step	Hyp	Ref	Expression
1		0cn 9374	. 2 |- 0 e. CC
2	1	a1i 11	1 |- ( ph -> 0 e. CC )

Syntax hints:   -> wi 4   e. wcel 1761   CCcc 9276   0cc0 9278

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-12 1797  ax-ext 2422  ax-1cn 9336  ax-icn 9337  ax-addcl 9338  ax-mulcl 9340  ax-i2m1 9346

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-cleq 2434  df-clel 2437

This theorem is referenced by:  mul0or  9972  diveq0  10000  eqneg  10047  un0addcl  10609  un0mulcl  10610  repswcshw  12442  clim0c  12981  rlim0  12982  rlim0lt  12983  rlimneg  13120  isercolllem3  13140  sumrblem  13184  summolem2a  13188  sumz  13195  fsumcl  13206  expcnv  13322  ef4p  13393  sadadd2lem2  13642  sadadd2lem  13651  modprm0  13869  iserodd  13898  prmrec  13979  4sqlem10  14004  4sqlem11  14012  frgpnabllem1  16344  fsumcn  20346  cnheibor  20427  evth2  20432  mbfmulc2lem  21025  mbfpos  21029  dvcmulf  21319  dvmptc  21332  dvmptcmul  21338  dvmptfsum  21347  dveflem  21351  rolle  21362  elply2  21607  plyf  21609  elplyr  21612  elplyd  21613  ply1term  21615  ply0  21619  plyeq0  21622  plyaddlem  21626  plymullem  21627  dgrlem  21640  coeidlem  21648  plyco  21652  coeeq2  21653  coe0  21666  plycj  21687  coecj  21688  plymul0or  21690  dvply1  21693  fta1lem  21716  elqaalem3  21730  tayl0  21770  dvtaylp  21778  taylthlem2  21782  radcnv0  21824  pserdvlem2  21836  pserdv  21837  ptolemy  21901  advlog  22042  advlogexp  22043  efopnlem2  22045  efopn  22046  logtayllem  22047  logtayl  22048  loglesqr  22139  affineequiv  22164  quad2  22177  dcubic  22184  asinlem  22206  dvatan  22273  leibpilem2  22279  leibpi  22280  rlimcnp  22302  efrlim  22306  emcllem7  22338  sqff1o  22463  dchrelbasd  22521  dchrsum2  22550  sumdchr2  22552  dchrvmasumiflem2  22694  occllem  24625  nlelchi  25384  addeq0  25954  divnumden2  26004  ballotlemic  26803  ballotlem1c  26804  signsvfn  26897  dmgmaddn0  26923  lgamgulmlem2  26930  igamf  26951  igamcl  26952  climlec3  27314  ntrivcvgfvn0  27327  tan2h  28333  ftc1anclem5  28380  ftc1anclem6  28381  ftc1anclem7  28382  ftc1anclem8  28383  ftc1anc  28384  pell14qrgt0  29109  expgrowth  29518  stirlinglem7  29784  bj-bary1lem  32289