Theorem 0cnd 10968

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

Syntax hints:   → wi 4   ∈ wcel 2106  ℂcc 10869  0cc0 10871

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-mulcl 10933  ax-i2m1 10939

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730  df-clel 2816

This theorem is referenced by:  addeq0  11398  mul0or  11615  diveq0  11643  eqneg  11695  un0addcl  12266  un0mulcl  12267  modsumfzodifsn  13664  muldivbinom2  13977  reusq0  15174  clim0c  15216  rlim0  15217  rlim0lt  15218  rlimneg  15358  isercolllem3  15378  sumrblem  15423  summolem2a  15427  sumz  15434  fsumcl  15445  expcnv  15576  ntrivcvgfvn0  15611  ef4p  15822  sadadd2lem2  16157  sadadd2lem  16166  modprm0  16506  iserodd  16536  prmrec  16623  4sqlem10  16648  4sqlem11  16656  frgpnabllem1  19474  fsumcn  24033  cnheibor  24118  evth2  24123  rrxmval  24569  mbfmulc2lem  24811  mbfpos  24815  dvcmulf  25109  dvmptc  25122  dvmptcmul  25128  dvmptfsum  25139  dveflem  25143  dvef  25144  rolle  25154  elply2  25357  plyf  25359  elplyr  25362  elplyd  25363  ply1term  25365  ply0  25369  plyeq0  25372  plyaddlem  25376  plymullem  25377  dgrlem  25390  coeidlem  25398  plyco  25402  coeeq2  25403  coe0  25417  plycj  25438  coecj  25439  plymul0or  25441  dvply1  25444  fta1lem  25467  elqaalem3  25481  tayl0  25521  dvtaylp  25529  taylthlem2  25533  radcnv0  25575  pserdvlem2  25587  pserdv  25588  ptolemy  25653  advlog  25809  advlogexp  25810  efopnlem2  25812  efopn  25813  logtayllem  25814  logtayl  25815  loglesqrt  25911  affineequiv  25973  quad2  25989  dcubic  25996  asinlem  26018  dvatan  26085  leibpilem2  26091  leibpi  26092  rlimcnp  26115  efrlim  26119  emcllem7  26151  dmgmaddn0  26172  lgamgulmlem2  26179  igamf  26200  igamcl  26201  sqff1o  26331  dchrelbasd  26387  dchrsum2  26416  sumdchr2  26418  addsq2reu  26588  addsqnreup  26591  dchrvmasumiflem2  26650  occllem  29665  nlelchi  30423  divnumden2  31132  fprodeq02  31137  ballotlemic  32473  ballotlem1c  32474  signsvfn  32561  circlemeth  32620  elmrsubrn  33482  climlec3  33699  bj-bary1lem  35481  tan2h  35769  ftc1anclem5  35854  ftc1anclem6  35855  ftc1anclem7  35856  ftc1anclem8  35857  ftc1anc  35858  lcmineqlem7  40043  lcmineqlem12  40048  aks4d1p1p7  40082  sticksstones10  40111  sticksstones12a  40113  sn-addid2  40387  remul02  40388  remul01  40390  sn-it0e0  40397  sn-addid1  40402  sn-addid0  40406  sn-mul01  40407  sn-0tie0  40421  sn-mul02  40422  3cubeslem1  40506  pell14qrgt0  40681  expgrowth  41953  binomcxplemnotnn0  41974  ellimcabssub0  43158  0ellimcdiv  43190  clim0cf  43195  cosknegpi  43410  fprodsubrecnncnvlem  43448  fprodaddrecnncnvlem  43450  dvsinax  43454  dvasinbx  43461  dvnmptconst  43482  dvnxpaek  43483  itgiccshift  43521  itgperiod  43522  itgsbtaddcnst  43523  stirlinglem7  43621  dirkertrigeqlem2  43640  fourierdlem59  43706  fourierdlem62  43709  fourierdlem74  43721  fourierdlem75  43722  sqwvfoura  43769  fouriersw  43772  etransclem20  43795  etransclem21  43796  etransclem22  43797  etransclem25  43800  etransclem35  43810  sge0z  43913  ovnhoilem1  44139  vonsn  44229  0nodd  45364  fdivmptf  45887  nn0sumshdiglem2  45968  eenglngeehlnmlem2  46084  itsclc0yqsollem1  46108