Theorem 0cnd 9661

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

Syntax hints:   -> wi 4   e. wcel 1897   CCcc 9562   0cc0 9564

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-ext 2441  ax-1cn 9622  ax-icn 9623  ax-addcl 9624  ax-mulcl 9626  ax-i2m1 9632

This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1674  df-cleq 2454  df-clel 2457

This theorem is referenced by:  mul0or  10279  diveq0  10307  eqneg  10354  un0addcl  10931  un0mulcl  10932  repswcshw  12947  clim0c  13619  rlim0  13620  rlim0lt  13621  rlimneg  13758  isercolllem3  13778  sumrblem  13825  summolem2a  13829  sumz  13836  fsumcl  13847  expcnv  13970  ntrivcvgfvn0  14003  ef4p  14215  sadadd2lem2  14472  sadadd2lem  14481  modprm0  14804  iserodd  14833  prmrec  14914  4sqlem10  14939  4sqlem11  14947  frgpnabllem1  17557  fsumcn  21950  cnheibor  22031  evth2  22036  rrxmval  22407  mbfmulc2lem  22651  mbfpos  22655  dvcmulf  22947  dvmptc  22960  dvmptcmul  22966  dvmptfsum  22975  dveflem  22979  rolle  22990  elply2  23198  plyf  23200  elplyr  23203  elplyd  23204  ply1term  23206  ply0  23210  plyeq0  23213  plyaddlem  23217  plymullem  23218  dgrlem  23231  coeidlem  23239  plyco  23243  coeeq2  23244  coe0  23258  plycj  23279  coecj  23280  plymul0or  23282  dvply1  23285  fta1lem  23308  elqaalem3  23322  elqaalem3OLD  23325  tayl0  23365  dvtaylp  23373  taylthlem2  23377  radcnv0  23419  pserdvlem2  23431  pserdv  23432  ptolemy  23499  advlog  23647  advlogexp  23648  efopnlem2  23650  efopn  23651  logtayllem  23652  logtayl  23653  loglesqrt  23746  affineequiv  23800  quad2  23813  dcubic  23820  asinlem  23842  dvatan  23909  leibpilem2  23915  leibpi  23916  rlimcnp  23939  efrlim  23943  emcllem7  23975  dmgmaddn0  23996  lgamgulmlem2  24003  igamf  24024  igamcl  24025  sqff1o  24157  dchrelbasd  24215  dchrsum2  24244  sumdchr2  24246  dchrvmasumiflem2  24388  occllem  27004  nlelchi  27762  addeq0  28368  divnumden2  28429  ballotlemic  29387  ballotlem1c  29388  ballotlemicOLD  29425  ballotlem1cOLD  29426  signsvfn  29519  elmrsubrn  30206  climlec3  30417  bj-bary1lem  31759  tan2h  31981  ftc1anclem5  32065  ftc1anclem6  32066  ftc1anclem7  32067  ftc1anclem8  32068  ftc1anc  32069  pell14qrgt0  35749  expgrowth  36727  binomcxplemnotnn0  36748  ellimcabssub0  37734  0ellimcdiv  37767  clim0cf  37772  cosknegpi  37781  dvsinax  37820  dvasinbx  37829  dvnmptconst  37853  dvnxpaek  37854  itgiccshift  37894  itgperiod  37895  itgsbtaddcnst  37896  stirlinglem7  37979  dirkertrigeqlem2  37998  fourierdlem59  38066  fourierdlem62  38069  fourierdlem74  38081  fourierdlem75  38082  sqwvfoura  38129  fouriersw  38132  etransclem20  38156  etransclem21  38157  etransclem22  38158  etransclem25  38161  etransclem35  38171  sge0z  38254  ovnhoilem1  38460  0nodd  40082  fdivmptf  40624  nn0sumshdiglem2  40705