Theorem 0cnd 11105

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

Syntax hints:   → wi 4   ∈ wcel 2111  ℂcc 11004  0cc0 11006

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-1cn 11064  ax-icn 11065  ax-addcl 11066  ax-mulcl 11068  ax-i2m1 11074

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-clel 2806

This theorem is referenced by:  addeq0  11540  mul0or  11757  eqneg  11841  un0addcl  12414  un0mulcl  12415  modsumfzodifsn  13851  muldivbinom2  14170  reusq0  15372  clim0c  15414  rlim0  15415  rlim0lt  15416  rlimneg  15554  isercolllem3  15574  sumrblem  15618  summolem2a  15622  sumz  15629  fsumcl  15640  expcnv  15771  ntrivcvgfvn0  15806  ef4p  16022  sadadd2lem2  16361  sadadd2lem  16370  modprm0  16717  iserodd  16747  prmrec  16834  4sqlem10  16859  4sqlem11  16867  frgpnabllem1  19785  fsumcn  24788  cnheibor  24881  evth2  24886  rrxmval  25332  mbfmulc2lem  25575  mbfpos  25579  dvcnp2  25848  dvcmulf  25875  dvmptc  25889  dvmptcmul  25895  dvmptfsum  25906  dveflem  25910  dvef  25911  rolle  25921  elply2  26128  plyf  26130  elplyr  26133  elplyd  26134  ply1term  26136  ply0  26140  plyeq0  26143  plyaddlem  26147  plymullem  26148  dgrlem  26161  coeidlem  26169  plyco  26173  coeeq2  26174  coe0  26188  plycj  26210  coecj  26211  plycjOLD  26212  coecjOLD  26213  plymul0or  26215  dvply1  26218  fta1lem  26242  elqaalem3  26256  tayl0  26296  dvtaylp  26305  taylthlem2  26309  taylthlem2OLD  26310  radcnv0  26352  pserdvlem2  26365  pserdv  26366  ptolemy  26432  advlog  26590  advlogexp  26591  efopnlem2  26593  efopn  26594  logtayllem  26595  logtayl  26596  loglesqrt  26698  affineequiv  26760  quad2  26776  dcubic  26783  asinlem  26805  dvatan  26872  leibpilem2  26878  leibpi  26879  rlimcnp  26902  efrlim  26906  efrlimOLD  26907  emcllem7  26939  dmgmaddn0  26960  lgamgulmlem2  26967  igamf  26988  igamcl  26989  sqff1o  27119  dchrelbasd  27177  dchrsum2  27206  sumdchr2  27208  addsq2reu  27378  addsqnreup  27381  dchrvmasumiflem2  27440  occllem  31283  nlelchi  32041  divnumden2  32798  fprodeq02  32806  gsumind  33310  constrrtcc  33748  constrsslem  33754  constraddcl  33775  constrmulcl  33784  cos9thpiminplylem1  33795  cos9thpiminplylem3  33797  cos9thpinconstrlem1  33802  ballotlemic  34520  ballotlem1c  34521  signsvfn  34595  circlemeth  34653  elmrsubrn  35564  climlec3  35778  bj-bary1lem  37354  tan2h  37662  ftc1anclem5  37747  ftc1anclem6  37748  ftc1anclem7  37749  ftc1anclem8  37750  ftc1anc  37751  lcmineqlem7  42138  lcmineqlem12  42143  aks4d1p1p7  42177  aks6d1c2p2  42222  aks6d1c5lem1  42239  aks6d1c5lem2  42241  sticksstones10  42258  sticksstones12a  42260  sn-addlid  42507  remul02  42508  remul01  42510  sn-it0e0  42519  sn-addrid  42524  sn-addid0  42528  sn-mul01  42529  sn-0tie0  42554  sn-mul02  42555  evlsvvval  42666  3cubeslem1  42787  pell14qrgt0  42962  expgrowth  44438  binomcxplemnotnn0  44459  ellimcabssub0  45727  0ellimcdiv  45757  clim0cf  45762  cosknegpi  45977  fprodsubrecnncnvlem  46015  fprodaddrecnncnvlem  46017  dvsinax  46021  dvasinbx  46028  dvnmptconst  46049  dvnxpaek  46050  itgiccshift  46088  itgperiod  46089  itgsbtaddcnst  46090  stirlinglem7  46188  dirkertrigeqlem2  46207  fourierdlem59  46273  fourierdlem62  46276  fourierdlem74  46288  fourierdlem75  46289  sqwvfoura  46336  fouriersw  46339  etransclem20  46362  etransclem21  46363  etransclem22  46364  etransclem25  46367  etransclem35  46377  sge0z  46483  ovnhoilem1  46709  vonsn  46799  lambert0  46997  0nodd  48280  fdivmptf  48652  nn0sumshdiglem2  48733  eenglngeehlnmlem2  48849  itsclc0yqsollem1  48873