Theorem 0cnd 7872

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

Syntax hints:   -> wi 4   e. wcel 2128   CCcc 7731   0cc0 7733

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-4 1490  ax-17 1506  ax-ial 1514  ax-ext 2139  ax-1cn 7826  ax-icn 7828  ax-addcl 7829  ax-mulcl 7831  ax-i2m1 7838

This theorem depends on definitions:  df-bi 116  df-cleq 2150  df-clel 2153

This theorem is referenced by:  mulap0r  8491  mulap0  8529  mul0eqap  8545  diveqap0  8556  eqneg  8606  div2subap  8710  prodgt0  8724  un0addcl  9124  un0mulcl  9125  modsumfzodifsn  10299  ser0  10417  ser0f  10418  abs00ap  10966  abs00  10968  abssubne0  10995  mul0inf  11144  clim0c  11187  sumrbdclem  11278  summodclem2a  11282  zsumdc  11285  fsum3  11288  isumz  11290  isumss  11292  fisumss  11293  fsum3cvg2  11295  fsum3ser  11298  fsumcl2lem  11299  fsumcl  11301  fsumadd  11307  fsumsplit  11308  sumsnf  11310  sumsplitdc  11333  fsummulc2  11349  ef0lem  11561  ef4p  11595  tanvalap  11609  modprm0  12133  fsumcncntop  12998  limcimolemlt  13075  dvmptcmulcn  13125  dveflem  13129  dvef  13130  ptolemy  13187  apdiff  13661  iswomni0  13664