Theorem 0cnd 11157

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

Syntax hints:   → wi 4   ∈ wcel 2106  ℂcc 11058  0cc0 11060

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-1cn 11118  ax-icn 11119  ax-addcl 11120  ax-mulcl 11122  ax-i2m1 11128

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723  df-clel 2809

This theorem is referenced by:  addeq0  11587  mul0or  11804  diveq0  11832  eqneg  11884  un0addcl  12455  un0mulcl  12456  modsumfzodifsn  13859  muldivbinom2  14173  reusq0  15359  clim0c  15401  rlim0  15402  rlim0lt  15403  rlimneg  15543  isercolllem3  15563  sumrblem  15607  summolem2a  15611  sumz  15618  fsumcl  15629  expcnv  15760  ntrivcvgfvn0  15795  ef4p  16006  sadadd2lem2  16341  sadadd2lem  16350  modprm0  16688  iserodd  16718  prmrec  16805  4sqlem10  16830  4sqlem11  16838  frgpnabllem1  19665  fsumcn  24270  cnheibor  24355  evth2  24360  rrxmval  24806  mbfmulc2lem  25048  mbfpos  25052  dvcmulf  25346  dvmptc  25359  dvmptcmul  25365  dvmptfsum  25376  dveflem  25380  dvef  25381  rolle  25391  elply2  25594  plyf  25596  elplyr  25599  elplyd  25600  ply1term  25602  ply0  25606  plyeq0  25609  plyaddlem  25613  plymullem  25614  dgrlem  25627  coeidlem  25635  plyco  25639  coeeq2  25640  coe0  25654  plycj  25675  coecj  25676  plymul0or  25678  dvply1  25681  fta1lem  25704  elqaalem3  25718  tayl0  25758  dvtaylp  25766  taylthlem2  25770  radcnv0  25812  pserdvlem2  25824  pserdv  25825  ptolemy  25890  advlog  26046  advlogexp  26047  efopnlem2  26049  efopn  26050  logtayllem  26051  logtayl  26052  loglesqrt  26148  affineequiv  26210  quad2  26226  dcubic  26233  asinlem  26255  dvatan  26322  leibpilem2  26328  leibpi  26329  rlimcnp  26352  efrlim  26356  emcllem7  26388  dmgmaddn0  26409  lgamgulmlem2  26416  igamf  26437  igamcl  26438  sqff1o  26568  dchrelbasd  26624  dchrsum2  26653  sumdchr2  26655  addsq2reu  26825  addsqnreup  26828  dchrvmasumiflem2  26887  occllem  30308  nlelchi  31066  divnumden2  31784  fprodeq02  31789  ballotlemic  33195  ballotlem1c  33196  signsvfn  33283  circlemeth  33342  elmrsubrn  34201  climlec3  34392  bj-bary1lem  35854  tan2h  36143  ftc1anclem5  36228  ftc1anclem6  36229  ftc1anclem7  36230  ftc1anclem8  36231  ftc1anc  36232  lcmineqlem7  40565  lcmineqlem12  40570  aks4d1p1p7  40604  aks6d1c2p2  40622  sticksstones10  40636  sticksstones12a  40638  sn-addlid  40931  remul02  40932  remul01  40934  sn-it0e0  40942  sn-addrid  40947  sn-addid0  40951  sn-mul01  40952  sn-0tie0  40966  sn-mul02  40967  3cubeslem1  41065  pell14qrgt0  41240  expgrowth  42737  binomcxplemnotnn0  42758  ellimcabssub0  43978  0ellimcdiv  44010  clim0cf  44015  cosknegpi  44230  fprodsubrecnncnvlem  44268  fprodaddrecnncnvlem  44270  dvsinax  44274  dvasinbx  44281  dvnmptconst  44302  dvnxpaek  44303  itgiccshift  44341  itgperiod  44342  itgsbtaddcnst  44343  stirlinglem7  44441  dirkertrigeqlem2  44460  fourierdlem59  44526  fourierdlem62  44529  fourierdlem74  44541  fourierdlem75  44542  sqwvfoura  44589  fouriersw  44592  etransclem20  44615  etransclem21  44616  etransclem22  44617  etransclem25  44620  etransclem35  44630  sge0z  44736  ovnhoilem1  44962  vonsn  45052  0nodd  46224  fdivmptf  46747  nn0sumshdiglem2  46828  eenglngeehlnmlem2  46944  itsclc0yqsollem1  46968