Theorem 0cnd 8150

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

Syntax hints:   -> wi 4   e. wcel 2200   CCcc 8008   0cc0 8010

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211  ax-1cn 8103  ax-icn 8105  ax-addcl 8106  ax-mulcl 8108  ax-i2m1 8115

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  mulap0r  8773  mulap0  8812  mul0eqap  8828  diveqap0  8840  eqneg  8890  div2subap  8995  prodgt0  9010  un0addcl  9413  un0mulcl  9414  modsumfzodifsn  10630  ser0  10767  ser0f  10768  abs00ap  11589  abs00  11591  abssubne0  11618  mul0inf  11768  clim0c  11813  sumrbdclem  11904  summodclem2a  11908  zsumdc  11911  fsum3  11914  isumz  11916  isumss  11918  fisumss  11919  fsum3cvg2  11921  fsum3ser  11924  fsumcl2lem  11925  fsumcl  11927  fsumadd  11933  fsumsplit  11934  sumsnf  11936  sumsplitdc  11959  fsummulc2  11975  ef0lem  12187  ef4p  12221  tanvalap  12235  modprm0  12793  pcmpt2  12883  4sqlem10  12926  4sqlem11  12940  fsumcncntop  15257  limcimolemlt  15354  dvmptcmulcn  15411  dvmptfsum  15415  dveflem  15416  dvef  15417  plyf  15427  elplyr  15430  elplyd  15431  ply1term  15433  plyaddlem  15439  plymullem  15440  plycolemc  15448  plycn  15452  dvply1  15455  ptolemy  15514  lgsdir2  15728  lgsdir  15730  apdiff  16504  iswomni0  16507