Theorem 0cnd 7783

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

Syntax hints:   -> wi 4   e. wcel 1481   CCcc 7642   0cc0 7644

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 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515  ax-ext 2122  ax-1cn 7737  ax-icn 7739  ax-addcl 7740  ax-mulcl 7742  ax-i2m1 7749

This theorem depends on definitions:  df-bi 116  df-cleq 2133  df-clel 2136

This theorem is referenced by:  mulap0r  8401  mulap0  8439  mul0eqap  8455  diveqap0  8466  eqneg  8516  div2subap  8620  prodgt0  8634  un0addcl  9034  un0mulcl  9035  modsumfzodifsn  10200  ser0  10318  ser0f  10319  abs00ap  10866  abs00  10868  abssubne0  10895  mul0inf  11044  clim0c  11087  sumrbdclem  11178  summodclem2a  11182  zsumdc  11185  fsum3  11188  isumz  11190  isumss  11192  fisumss  11193  fsum3cvg2  11195  fsum3ser  11198  fsumcl2lem  11199  fsumcl  11201  fsumadd  11207  fsumsplit  11208  sumsnf  11210  sumsplitdc  11233  fsummulc2  11249  ef0lem  11403  ef4p  11437  tanvalap  11451  fsumcncntop  12764  limcimolemlt  12841  dvmptcmulcn  12891  dveflem  12895  dvef  12896  ptolemy  12953  apdiff  13416