Theorem 0cnd 8232

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

Syntax hints:   -> wi 4   e. wcel 2202   CCcc 8090   0cc0 8092

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2213  ax-1cn 8185  ax-icn 8187  ax-addcl 8188  ax-mulcl 8190  ax-i2m1 8197

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

This theorem is referenced by:  mulap0r  8854  mulap0  8893  mul0eqap  8909  diveqap0  8921  eqneg  8971  div2subap  9076  prodgt0  9091  un0addcl  9494  un0mulcl  9495  modsumfzodifsn  10721  ser0  10858  ser0f  10859  abs00ap  11702  abs00  11704  abssubne0  11731  mul0inf  11881  clim0c  11926  sumrbdclem  12018  summodclem2a  12022  zsumdc  12025  fsum3  12028  isumz  12030  isumss  12032  fisumss  12033  fsum3cvg2  12035  fsum3ser  12038  fsumcl2lem  12039  fsumcl  12041  fsumadd  12047  fsumsplit  12048  sumsnf  12050  sumsplitdc  12073  fsummulc2  12089  ef0lem  12301  ef4p  12335  tanvalap  12349  modprm0  12907  pcmpt2  12997  4sqlem10  13040  4sqlem11  13054  fsumcncntop  15378  limcimolemlt  15475  dvmptcmulcn  15532  dvmptfsum  15536  dveflem  15537  dvef  15538  plyf  15548  elplyr  15551  elplyd  15552  ply1term  15554  plyaddlem  15560  plymullem  15561  plycolemc  15569  plycn  15573  dvply1  15576  ptolemy  15635  lgsdir2  15852  lgsdir  15854  apdiff  16780  iswomni0  16784