Theorem 0cnd 8067

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

Syntax hints:   -> wi 4   e. wcel 2176   CCcc 7925   0cc0 7927

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-ext 2187  ax-1cn 8020  ax-icn 8022  ax-addcl 8023  ax-mulcl 8025  ax-i2m1 8032

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-clel 2201

This theorem is referenced by:  mulap0r  8690  mulap0  8729  mul0eqap  8745  diveqap0  8757  eqneg  8807  div2subap  8912  prodgt0  8927  un0addcl  9330  un0mulcl  9331  modsumfzodifsn  10543  ser0  10680  ser0f  10681  abs00ap  11406  abs00  11408  abssubne0  11435  mul0inf  11585  clim0c  11630  sumrbdclem  11721  summodclem2a  11725  zsumdc  11728  fsum3  11731  isumz  11733  isumss  11735  fisumss  11736  fsum3cvg2  11738  fsum3ser  11741  fsumcl2lem  11742  fsumcl  11744  fsumadd  11750  fsumsplit  11751  sumsnf  11753  sumsplitdc  11776  fsummulc2  11792  ef0lem  12004  ef4p  12038  tanvalap  12052  modprm0  12610  pcmpt2  12700  4sqlem10  12743  4sqlem11  12757  fsumcncntop  15072  limcimolemlt  15169  dvmptcmulcn  15226  dvmptfsum  15230  dveflem  15231  dvef  15232  plyf  15242  elplyr  15245  elplyd  15246  ply1term  15248  plyaddlem  15254  plymullem  15255  plycolemc  15263  plycn  15267  dvply1  15270  ptolemy  15329  lgsdir2  15543  lgsdir  15545  apdiff  16024  iswomni0  16027