Theorem 0cnd 11131

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 11030  0cc0 11032

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-mulcl 11094  ax-i2m1 11100

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812

This theorem is referenced by:  addeq0  11567  mul0or  11784  eqneg  11869  un0addcl  12464  un0mulcl  12465  modsumfzodifsn  13900  muldivbinom2  14219  reusq0  15421  clim0c  15463  rlim0  15464  rlim0lt  15465  rlimneg  15603  isercolllem3  15623  sumrblem  15667  summolem2a  15671  sumz  15678  fsumcl  15689  expcnv  15823  ntrivcvgfvn0  15858  ef4p  16074  sadadd2lem2  16413  sadadd2lem  16422  modprm0  16770  iserodd  16800  prmrec  16887  4sqlem10  16912  4sqlem11  16920  frgpnabllem1  19842  evlsvvval  22084  fsumcn  24850  cnheibor  24935  evth2  24940  rrxmval  25385  mbfmulc2lem  25627  mbfpos  25631  dvcnp2  25900  dvcmulf  25925  dvmptc  25938  dvmptcmul  25944  dvmptfsum  25955  dveflem  25959  dvef  25960  rolle  25970  elply2  26174  plyf  26176  elplyr  26179  elplyd  26180  ply1term  26182  ply0  26186  plyeq0  26189  plyaddlem  26193  plymullem  26194  dgrlem  26207  coeidlem  26215  plyco  26219  coeeq2  26220  coe0  26234  plycj  26255  coecj  26256  plycjOLD  26257  coecjOLD  26258  plymul0or  26260  dvply1  26263  fta1lem  26287  elqaalem3  26301  tayl0  26341  dvtaylp  26350  taylthlem2  26354  taylthlem2OLD  26355  radcnv0  26397  pserdvlem2  26409  pserdv  26410  ptolemy  26476  advlog  26634  advlogexp  26635  efopnlem2  26637  efopn  26638  logtayllem  26639  logtayl  26640  loglesqrt  26741  affineequiv  26803  quad2  26819  dcubic  26826  asinlem  26848  dvatan  26915  leibpilem2  26921  leibpi  26922  rlimcnp  26945  efrlim  26949  efrlimOLD  26950  emcllem7  26982  dmgmaddn0  27003  lgamgulmlem2  27010  igamf  27031  igamcl  27032  sqff1o  27162  dchrelbasd  27219  dchrsum2  27248  sumdchr2  27250  addsq2reu  27420  addsqnreup  27423  dchrvmasumiflem2  27482  occllem  31392  nlelchi  32150  divnumden2  32907  fprodeq02  32915  gsumind  33423  constrrtcc  33898  constrsslem  33904  constraddcl  33925  constrmulcl  33934  cos9thpiminplylem1  33945  cos9thpiminplylem3  33947  cos9thpinconstrlem1  33952  ballotlemic  34670  ballotlem1c  34671  signsvfn  34745  circlemeth  34803  elmrsubrn  35721  climlec3  35935  bj-bary1lem  37643  tan2h  37950  ftc1anclem5  38035  ftc1anclem6  38036  ftc1anclem7  38037  ftc1anclem8  38038  ftc1anc  38039  lcmineqlem7  42491  lcmineqlem12  42496  aks4d1p1p7  42530  aks6d1c2p2  42575  aks6d1c5lem1  42592  aks6d1c5lem2  42594  sticksstones10  42611  sticksstones12a  42613  sn-addlid  42853  remul02  42854  remul01  42856  sn-it0e0  42865  sn-addrid  42870  sn-addid0  42874  sn-mul01  42875  sn-0tie0  42913  sn-mul02  42914  3cubeslem1  43133  pell14qrgt0  43308  expgrowth  44783  binomcxplemnotnn0  44804  ellimcabssub0  46068  0ellimcdiv  46098  clim0cf  46103  cosknegpi  46318  fprodsubrecnncnvlem  46356  fprodaddrecnncnvlem  46358  dvsinax  46362  dvasinbx  46369  dvnmptconst  46390  dvnxpaek  46391  itgiccshift  46429  itgperiod  46430  itgsbtaddcnst  46431  stirlinglem7  46529  dirkertrigeqlem2  46548  fourierdlem59  46614  fourierdlem62  46617  fourierdlem74  46629  fourierdlem75  46630  sqwvfoura  46677  fouriersw  46680  etransclem20  46703  etransclem21  46704  etransclem22  46705  etransclem25  46708  etransclem35  46718  sge0z  46824  ovnhoilem1  47050  vonsn  47140  lambert0  47350  0nodd  48661  fdivmptf  49032  nn0sumshdiglem2  49113  eenglngeehlnmlem2  49229  itsclc0yqsollem1  49253