Theorem 0cnd 8172

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

Syntax hints:   -> wi 4   e. wcel 2202   CCcc 8030   0cc0 8032

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213  ax-1cn 8125  ax-icn 8127  ax-addcl 8128  ax-mulcl 8130  ax-i2m1 8137

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227

This theorem is referenced by:  mulap0r  8795  mulap0  8834  mul0eqap  8850  diveqap0  8862  eqneg  8912  div2subap  9017  prodgt0  9032  un0addcl  9435  un0mulcl  9436  modsumfzodifsn  10659  ser0  10796  ser0f  10797  abs00ap  11640  abs00  11642  abssubne0  11669  mul0inf  11819  clim0c  11864  sumrbdclem  11956  summodclem2a  11960  zsumdc  11963  fsum3  11966  isumz  11968  isumss  11970  fisumss  11971  fsum3cvg2  11973  fsum3ser  11976  fsumcl2lem  11977  fsumcl  11979  fsumadd  11985  fsumsplit  11986  sumsnf  11988  sumsplitdc  12011  fsummulc2  12027  ef0lem  12239  ef4p  12273  tanvalap  12287  modprm0  12845  pcmpt2  12935  4sqlem10  12978  4sqlem11  12992  fsumcncntop  15310  limcimolemlt  15407  dvmptcmulcn  15464  dvmptfsum  15468  dveflem  15469  dvef  15470  plyf  15480  elplyr  15483  elplyd  15484  ply1term  15486  plyaddlem  15492  plymullem  15493  plycolemc  15501  plycn  15505  dvply1  15508  ptolemy  15567  lgsdir2  15781  lgsdir  15783  apdiff  16703  iswomni0  16707