Theorem 0cnd 9589

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

Syntax hints:   -> wi 4   e. wcel 1802   CCcc 9490   0cc0 9492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-ext 2419  ax-1cn 9550  ax-icn 9551  ax-addcl 9552  ax-mulcl 9554  ax-i2m1 9560

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1598  df-cleq 2433  df-clel 2436

This theorem is referenced by:  mul0or  10192  diveq0  10220  eqneg  10267  un0addcl  10832  un0mulcl  10833  repswcshw  12756  clim0c  13306  rlim0  13307  rlim0lt  13308  rlimneg  13445  isercolllem3  13465  sumrblem  13509  summolem2a  13513  sumz  13520  fsumcl  13531  expcnv  13651  ef4p  13722  sadadd2lem2  13974  sadadd2lem  13983  modprm0  14204  iserodd  14233  prmrec  14314  4sqlem10  14339  4sqlem11  14347  frgpnabllem1  16748  fsumcn  21244  cnheibor  21325  evth2  21330  rrxmval  21702  mbfmulc2lem  21924  mbfpos  21928  dvcmulf  22218  dvmptc  22231  dvmptcmul  22237  dvmptfsum  22246  dveflem  22250  rolle  22261  elply2  22463  plyf  22465  elplyr  22468  elplyd  22469  ply1term  22471  ply0  22475  plyeq0  22478  plyaddlem  22482  plymullem  22483  dgrlem  22496  coeidlem  22504  plyco  22508  coeeq2  22509  coe0  22522  plycj  22543  coecj  22544  plymul0or  22546  dvply1  22549  fta1lem  22572  elqaalem3  22586  tayl0  22626  dvtaylp  22634  taylthlem2  22638  radcnv0  22680  pserdvlem2  22692  pserdv  22693  ptolemy  22758  advlog  22904  advlogexp  22905  efopnlem2  22907  efopn  22908  logtayllem  22909  logtayl  22910  loglesqrt  23001  affineequiv  23026  quad2  23039  dcubic  23046  asinlem  23068  dvatan  23135  leibpilem2  23141  leibpi  23142  rlimcnp  23164  efrlim  23168  emcllem7  23200  sqff1o  23325  dchrelbasd  23383  dchrsum2  23412  sumdchr2  23414  dchrvmasumiflem2  23556  occllem  26090  nlelchi  26849  addeq0  27427  divnumden2  27478  ballotlemic  28315  ballotlem1c  28316  signsvfn  28409  dmgmaddn0  28435  lgamgulmlem2  28442  igamf  28463  igamcl  28464  elmrsubrn  28750  climlec3  28992  ntrivcvgfvn0  29005  tan2h  30019  ftc1anclem5  30066  ftc1anclem6  30067  ftc1anclem7  30068  ftc1anclem8  30069  ftc1anc  30070  pell14qrgt0  30767  expgrowth  31213  ellimcabssub0  31531  0ellimcdiv  31563  clim0cf  31568  cosknegpi  31576  dvsinax  31612  dvasinbx  31621  itgiccshift  31669  itgperiod  31670  itgsbtaddcnst  31671  stirlinglem7  31751  dirkertrigeqlem2  31770  fourierdlem59  31837  fourierdlem62  31840  fourierdlem74  31852  fourierdlem75  31853  sqwvfoura  31900  fouriersw  31903  0nodd  32335  bj-bary1lem  34402