Theorem 0cnd 7479

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

Syntax hints:   -> wi 4   e. wcel 1438   CCcc 7346   0cc0 7348

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-17 1464  ax-ial 1472  ax-ext 2070  ax-1cn 7436  ax-icn 7438  ax-addcl 7439  ax-mulcl 7441  ax-i2m1 7448

This theorem depends on definitions:  df-bi 115  df-cleq 2081  df-clel 2084

This theorem is referenced by:  mulap0r  8090  mulap0  8121  diveqap0  8147  eqneg  8197  div2subap  8300  prodgt0  8311  un0addcl  8704  un0mulcl  8705  modsumfzodifsn  9799  iser0  9943  iser0f  9944  ser0  9945  ser0f  9946  abs00ap  10491  abssubne0  10520  clim0c  10670  isumrblem  10761  isummolem2a  10767  zisum  10770  fisum  10774  fsum3  10775  isumz  10777  isumss  10779  fisumss  10780  fisumcvg2  10782  fsum3cvg2  10783  fisumser  10786  fsumcl2lem  10788  fsumcl  10790  fsumadd  10796  fsumsplit  10797  sumsnf  10799  sumsplitdc  10822  fsummulc2  10838  ef0lem  10946  ef4p  10980  tanvalap  10995