Theorem 0cnd 10636

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 10635	. 2 ⊢ 0 ∈ ℂ
2	1	a1i 11	1 ⊢ (𝜑 → 0 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 10537  0cc0 10539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795  ax-1cn 10597  ax-icn 10598  ax-addcl 10599  ax-mulcl 10601  ax-i2m1 10607

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2816  df-clel 2895

This theorem is referenced by:  addeq0  11065  mul0or  11282  diveq0  11310  eqneg  11362  un0addcl  11933  un0mulcl  11934  modsumfzodifsn  13315  muldivbinom2  13626  reusq0  14824  clim0c  14866  rlim0  14867  rlim0lt  14868  rlimneg  15005  isercolllem3  15025  sumrblem  15070  summolem2a  15074  sumz  15081  fsumcl  15092  expcnv  15221  ntrivcvgfvn0  15257  ef4p  15468  sadadd2lem2  15801  sadadd2lem  15810  modprm0  16144  iserodd  16174  prmrec  16260  4sqlem10  16285  4sqlem11  16293  frgpnabllem1  18995  fsumcn  23480  cnheibor  23561  evth2  23566  rrxmval  24010  mbfmulc2lem  24250  mbfpos  24254  dvcmulf  24544  dvmptc  24557  dvmptcmul  24563  dvmptfsum  24574  dveflem  24578  dvef  24579  rolle  24589  elply2  24788  plyf  24790  elplyr  24793  elplyd  24794  ply1term  24796  ply0  24800  plyeq0  24803  plyaddlem  24807  plymullem  24808  dgrlem  24821  coeidlem  24829  plyco  24833  coeeq2  24834  coe0  24848  plycj  24869  coecj  24870  plymul0or  24872  dvply1  24875  fta1lem  24898  elqaalem3  24912  tayl0  24952  dvtaylp  24960  taylthlem2  24964  radcnv0  25006  pserdvlem2  25018  pserdv  25019  ptolemy  25084  advlog  25239  advlogexp  25240  efopnlem2  25242  efopn  25243  logtayllem  25244  logtayl  25245  loglesqrt  25341  affineequiv  25403  quad2  25419  dcubic  25426  asinlem  25448  dvatan  25515  leibpilem2  25521  leibpi  25522  rlimcnp  25545  efrlim  25549  emcllem7  25581  dmgmaddn0  25602  lgamgulmlem2  25609  igamf  25630  igamcl  25631  sqff1o  25761  dchrelbasd  25817  dchrsum2  25846  sumdchr2  25848  addsq2reu  26018  addsqnreup  26021  dchrvmasumiflem2  26080  occllem  29082  nlelchi  29840  divnumden2  30536  fprodeq02  30541  ballotlemic  31766  ballotlem1c  31767  signsvfn  31854  circlemeth  31913  elmrsubrn  32769  climlec3  32967  bj-bary1lem  34593  tan2h  34886  ftc1anclem5  34973  ftc1anclem6  34974  ftc1anclem7  34975  ftc1anclem8  34976  ftc1anc  34977  sn-addid2  39241  remul02  39242  remul01  39244  3cubeslem1  39288  pell14qrgt0  39463  expgrowth  40674  binomcxplemnotnn0  40695  ellimcabssub0  41905  0ellimcdiv  41937  clim0cf  41942  cosknegpi  42157  fprodsubrecnncnvlem  42198  fprodaddrecnncnvlem  42200  dvsinax  42204  dvasinbx  42212  dvnmptconst  42233  dvnxpaek  42234  itgiccshift  42272  itgperiod  42273  itgsbtaddcnst  42274  stirlinglem7  42372  dirkertrigeqlem2  42391  fourierdlem59  42457  fourierdlem62  42460  fourierdlem74  42472  fourierdlem75  42473  sqwvfoura  42520  fouriersw  42523  etransclem20  42546  etransclem21  42547  etransclem22  42548  etransclem25  42551  etransclem35  42561  sge0z  42664  ovnhoilem1  42890  vonsn  42980  0nodd  44084  fdivmptf  44608  nn0sumshdiglem2  44689  eenglngeehlnmlem2  44732  itsclc0yqsollem1  44756