Theorem 0cnd 9494

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 9493	. 2 |- 0 e. CC
2	1	a1i 11	1 |- ( ph -> 0 e. CC )

Syntax hints:   -> wi 4   e. wcel 1758   CCcc 9395   0cc0 9397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-ext 2432  ax-1cn 9455  ax-icn 9456  ax-addcl 9457  ax-mulcl 9459  ax-i2m1 9465

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-cleq 2446  df-clel 2449

This theorem is referenced by:  mul0or  10091  diveq0  10119  eqneg  10166  un0addcl  10728  un0mulcl  10729  repswcshw  12568  clim0c  13107  rlim0  13108  rlim0lt  13109  rlimneg  13246  isercolllem3  13266  sumrblem  13310  summolem2a  13314  sumz  13321  fsumcl  13332  expcnv  13448  ef4p  13519  sadadd2lem2  13768  sadadd2lem  13777  modprm0  13995  iserodd  14024  prmrec  14105  4sqlem10  14130  4sqlem11  14138  frgpnabllem1  16476  fsumcn  20588  cnheibor  20669  evth2  20674  mbfmulc2lem  21268  mbfpos  21272  dvcmulf  21562  dvmptc  21575  dvmptcmul  21581  dvmptfsum  21590  dveflem  21594  rolle  21605  elply2  21807  plyf  21809  elplyr  21812  elplyd  21813  ply1term  21815  ply0  21819  plyeq0  21822  plyaddlem  21826  plymullem  21827  dgrlem  21840  coeidlem  21848  plyco  21852  coeeq2  21853  coe0  21866  plycj  21887  coecj  21888  plymul0or  21890  dvply1  21893  fta1lem  21916  elqaalem3  21930  tayl0  21970  dvtaylp  21978  taylthlem2  21982  radcnv0  22024  pserdvlem2  22036  pserdv  22037  ptolemy  22101  advlog  22242  advlogexp  22243  efopnlem2  22245  efopn  22246  logtayllem  22247  logtayl  22248  loglesqr  22339  affineequiv  22364  quad2  22377  dcubic  22384  asinlem  22406  dvatan  22473  leibpilem2  22479  leibpi  22480  rlimcnp  22502  efrlim  22506  emcllem7  22538  sqff1o  22663  dchrelbasd  22721  dchrsum2  22750  sumdchr2  22752  dchrvmasumiflem2  22894  occllem  24885  nlelchi  25644  addeq0  26213  divnumden2  26259  ballotlemic  27056  ballotlem1c  27057  signsvfn  27150  dmgmaddn0  27176  lgamgulmlem2  27183  igamf  27204  igamcl  27205  climlec3  27568  ntrivcvgfvn0  27581  tan2h  28595  ftc1anclem5  28642  ftc1anclem6  28643  ftc1anclem7  28644  ftc1anclem8  28645  ftc1anc  28646  pell14qrgt0  29371  expgrowth  29780  stirlinglem7  30046  bj-bary1lem  32962