Theorem 0cnd 7963

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

Syntax hints:   -> wi 4   e. wcel 2158   CCcc 7822   0cc0 7824

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 1457  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-4 1520  ax-17 1536  ax-ial 1544  ax-ext 2169  ax-1cn 7917  ax-icn 7919  ax-addcl 7920  ax-mulcl 7922  ax-i2m1 7929

This theorem depends on definitions:  df-bi 117  df-cleq 2180  df-clel 2183

This theorem is referenced by:  mulap0r  8585  mulap0  8624  mul0eqap  8640  diveqap0  8652  eqneg  8702  div2subap  8807  prodgt0  8822  un0addcl  9222  un0mulcl  9223  modsumfzodifsn  10409  ser0  10527  ser0f  10528  abs00ap  11084  abs00  11086  abssubne0  11113  mul0inf  11262  clim0c  11307  sumrbdclem  11398  summodclem2a  11402  zsumdc  11405  fsum3  11408  isumz  11410  isumss  11412  fisumss  11413  fsum3cvg2  11415  fsum3ser  11418  fsumcl2lem  11419  fsumcl  11421  fsumadd  11427  fsumsplit  11428  sumsnf  11430  sumsplitdc  11453  fsummulc2  11469  ef0lem  11681  ef4p  11715  tanvalap  11729  modprm0  12267  pcmpt2  12355  4sqlem10  12398  fsumcncntop  14327  limcimolemlt  14404  dvmptcmulcn  14454  dveflem  14458  dvef  14459  ptolemy  14516  lgsdir2  14705  lgsdir  14707  apdiff  15068  iswomni0  15071