Theorem 0cnd 8036

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

Syntax hints:   -> wi 4   e. wcel 2167   CCcc 7894   0cc0 7896

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178  ax-1cn 7989  ax-icn 7991  ax-addcl 7992  ax-mulcl 7994  ax-i2m1 8001

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-clel 2192

This theorem is referenced by:  mulap0r  8659  mulap0  8698  mul0eqap  8714  diveqap0  8726  eqneg  8776  div2subap  8881  prodgt0  8896  un0addcl  9299  un0mulcl  9300  modsumfzodifsn  10505  ser0  10642  ser0f  10643  abs00ap  11244  abs00  11246  abssubne0  11273  mul0inf  11423  clim0c  11468  sumrbdclem  11559  summodclem2a  11563  zsumdc  11566  fsum3  11569  isumz  11571  isumss  11573  fisumss  11574  fsum3cvg2  11576  fsum3ser  11579  fsumcl2lem  11580  fsumcl  11582  fsumadd  11588  fsumsplit  11589  sumsnf  11591  sumsplitdc  11614  fsummulc2  11630  ef0lem  11842  ef4p  11876  tanvalap  11890  modprm0  12448  pcmpt2  12538  4sqlem10  12581  4sqlem11  12595  fsumcncntop  14887  limcimolemlt  14984  dvmptcmulcn  15041  dvmptfsum  15045  dveflem  15046  dvef  15047  plyf  15057  elplyr  15060  elplyd  15061  ply1term  15063  plyaddlem  15069  plymullem  15070  plycolemc  15078  plycn  15082  dvply1  15085  ptolemy  15144  lgsdir2  15358  lgsdir  15360  apdiff  15779  iswomni0  15782