Theorem 0cnd 10705

Description: Zero is a complex number, deduction form. (Contributed by David A. Wheeler, 8-Dec-2018.)

Assertion

Ref	Expression
0cnd	⊢ (𝜑 → 0 ∈ ℂ)

Proof of Theorem 0cnd

Step	Hyp	Ref	Expression
1		0cn 10704	. 2 ⊢ 0 ∈ ℂ
2	1	a1i 11	1 ⊢ (𝜑 → 0 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2113  ℂcc 10606  0cc0 10608

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710  ax-1cn 10666  ax-icn 10667  ax-addcl 10668  ax-mulcl 10670  ax-i2m1 10676

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787  df-cleq 2730  df-clel 2811

This theorem is referenced by:  addeq0  11134  mul0or  11351  diveq0  11379  eqneg  11431  un0addcl  12002  un0mulcl  12003  modsumfzodifsn  13396  muldivbinom2  13708  reusq0  14905  clim0c  14947  rlim0  14948  rlim0lt  14949  rlimneg  15089  isercolllem3  15109  sumrblem  15154  summolem2a  15158  sumz  15165  fsumcl  15176  expcnv  15305  ntrivcvgfvn0  15340  ef4p  15551  sadadd2lem2  15886  sadadd2lem  15895  modprm0  16235  iserodd  16265  prmrec  16351  4sqlem10  16376  4sqlem11  16384  frgpnabllem1  19105  fsumcn  23615  cnheibor  23700  evth2  23705  rrxmval  24150  mbfmulc2lem  24392  mbfpos  24396  dvcmulf  24689  dvmptc  24702  dvmptcmul  24708  dvmptfsum  24719  dveflem  24723  dvef  24724  rolle  24734  elply2  24937  plyf  24939  elplyr  24942  elplyd  24943  ply1term  24945  ply0  24949  plyeq0  24952  plyaddlem  24956  plymullem  24957  dgrlem  24970  coeidlem  24978  plyco  24982  coeeq2  24983  coe0  24997  plycj  25018  coecj  25019  plymul0or  25021  dvply1  25024  fta1lem  25047  elqaalem3  25061  tayl0  25101  dvtaylp  25109  taylthlem2  25113  radcnv0  25155  pserdvlem2  25167  pserdv  25168  ptolemy  25233  advlog  25389  advlogexp  25390  efopnlem2  25392  efopn  25393  logtayllem  25394  logtayl  25395  loglesqrt  25491  affineequiv  25553  quad2  25569  dcubic  25576  asinlem  25598  dvatan  25665  leibpilem2  25671  leibpi  25672  rlimcnp  25695  efrlim  25699  emcllem7  25731  dmgmaddn0  25752  lgamgulmlem2  25759  igamf  25780  igamcl  25781  sqff1o  25911  dchrelbasd  25967  dchrsum2  25996  sumdchr2  25998  addsq2reu  26168  addsqnreup  26171  dchrvmasumiflem2  26230  occllem  29230  nlelchi  29988  divnumden2  30699  fprodeq02  30704  ballotlemic  32035  ballotlem1c  32036  signsvfn  32123  circlemeth  32182  elmrsubrn  33045  climlec3  33262  bj-bary1lem  35090  tan2h  35381  ftc1anclem5  35466  ftc1anclem6  35467  ftc1anclem7  35468  ftc1anclem8  35469  ftc1anc  35470  lcmineqlem7  39652  lcmineqlem12  39657  aks4d1p1p7  39690  sn-addid2  39948  remul02  39949  remul01  39951  sn-it0e0  39958  sn-addid1  39963  sn-addid0  39967  sn-mul01  39968  sn-0tie0  39982  sn-mul02  39983  3cubeslem1  40062  pell14qrgt0  40237  expgrowth  41475  binomcxplemnotnn0  41496  ellimcabssub0  42684  0ellimcdiv  42716  clim0cf  42721  cosknegpi  42936  fprodsubrecnncnvlem  42974  fprodaddrecnncnvlem  42976  dvsinax  42980  dvasinbx  42987  dvnmptconst  43008  dvnxpaek  43009  itgiccshift  43047  itgperiod  43048  itgsbtaddcnst  43049  stirlinglem7  43147  dirkertrigeqlem2  43166  fourierdlem59  43232  fourierdlem62  43235  fourierdlem74  43247  fourierdlem75  43248  sqwvfoura  43295  fouriersw  43298  etransclem20  43321  etransclem21  43322  etransclem22  43323  etransclem25  43326  etransclem35  43336  sge0z  43439  ovnhoilem1  43665  vonsn  43755  0nodd  44882  fdivmptf  45405  nn0sumshdiglem2  45486  eenglngeehlnmlem2  45602  itsclc0yqsollem1  45626