Theorem 0cnd 8319

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

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   CCcc 8177   0cc0 8179

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220  ax-1cn 8272  ax-icn 8274  ax-addcl 8275  ax-mulcl 8277  ax-i2m1 8284

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  addeq0  8703  mulap0r  8943  mulap0  8982  msq0  8997  mul0eqap  9000  diveqap0  9012  eqneg  9062  div2subap  9167  prodgt0  9182  un0addcl  9596  un0mulcl  9597  modsumfzodifsn  10833  ser0  10970  ser0f  10971  resq01  11095  sq01  11660  abs00ap  11828  abs00  11830  abssubne0  11857  mul0inf  12007  clim0c  12052  sumrbdclem  12144  summodclem2a  12148  zsumdc  12151  fsum3  12154  isumz  12156  isumss  12158  fisumss  12159  fsum3cvg2  12161  fsum3ser  12164  fsumcl2lem  12165  fsumcl  12167  fsumadd  12173  fsumsplit  12174  sumsnf  12176  sumsplitdc  12199  fsummulc2  12215  ef0lem  12427  ef4p  12461  tanvalap  12475  modprm0  13033  pcmpt2  13123  4sqlem10  13166  4sqlem11  13180  ballotfilemic  13250  ballotfilem1c  13251  fsumcncntop  15668  limcimolemlt  15765  dvmptcmulcn  15822  dvmptfsum  15826  dveflem  15827  dvef  15828  plyf  15838  elplyr  15841  elplyd  15842  ply1term  15844  plyaddlem  15850  plymullem  15851  plycolemc  15859  plycn  15863  dvply1  15866  ptolemy  15925  lgsdir2  16152  lgsdir  16154  apdiff  17097  iswomni0  17101