Theorem 0cnd 9601

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

Syntax hints:   -> wi 4   e. wcel 1767   CCcc 9502   0cc0 9504

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-ext 2445  ax-1cn 9562  ax-icn 9563  ax-addcl 9564  ax-mulcl 9566  ax-i2m1 9572

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-cleq 2459  df-clel 2462

This theorem is referenced by:  mul0or  10201  diveq0  10229  eqneg  10276  un0addcl  10841  un0mulcl  10842  repswcshw  12760  clim0c  13310  rlim0  13311  rlim0lt  13312  rlimneg  13449  isercolllem3  13469  sumrblem  13513  summolem2a  13517  sumz  13524  fsumcl  13535  expcnv  13655  ef4p  13726  sadadd2lem2  13976  sadadd2lem  13985  modprm0  14206  iserodd  14235  prmrec  14316  4sqlem10  14341  4sqlem11  14349  frgpnabllem1  16750  fsumcn  21242  cnheibor  21323  evth2  21328  mbfmulc2lem  21922  mbfpos  21926  dvcmulf  22216  dvmptc  22229  dvmptcmul  22235  dvmptfsum  22244  dveflem  22248  rolle  22259  elply2  22461  plyf  22463  elplyr  22466  elplyd  22467  ply1term  22469  ply0  22473  plyeq0  22476  plyaddlem  22480  plymullem  22481  dgrlem  22494  coeidlem  22502  plyco  22506  coeeq2  22507  coe0  22520  plycj  22541  coecj  22542  plymul0or  22544  dvply1  22547  fta1lem  22570  elqaalem3  22584  tayl0  22624  dvtaylp  22632  taylthlem2  22636  radcnv0  22678  pserdvlem2  22690  pserdv  22691  ptolemy  22755  advlog  22901  advlogexp  22902  efopnlem2  22904  efopn  22905  logtayllem  22906  logtayl  22907  loglesqrt  22998  affineequiv  23023  quad2  23036  dcubic  23043  asinlem  23065  dvatan  23132  leibpilem2  23138  leibpi  23139  rlimcnp  23161  efrlim  23165  emcllem7  23197  sqff1o  23322  dchrelbasd  23380  dchrsum2  23409  sumdchr2  23411  dchrvmasumiflem2  23553  occllem  26044  nlelchi  26803  addeq0  27381  divnumden2  27432  ballotlemic  28270  ballotlem1c  28271  signsvfn  28364  dmgmaddn0  28390  lgamgulmlem2  28397  igamf  28418  igamcl  28419  climlec3  28947  ntrivcvgfvn0  28960  tan2h  29974  ftc1anclem5  30021  ftc1anclem6  30022  ftc1anclem7  30023  ftc1anclem8  30024  ftc1anc  30025  pell14qrgt0  30723  expgrowth  31164  cosknegpi  31528  stirlinglem7  31703  fouriersw  31855  0nodd  32257  bj-bary1lem  34152