Theorem 0cnd 11167

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 11066  0cc0 11068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-mulcl 11130  ax-i2m1 11136

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803

This theorem is referenced by:  addeq0  11601  mul0or  11818  eqneg  11902  un0addcl  12475  un0mulcl  12476  modsumfzodifsn  13909  muldivbinom2  14228  reusq0  15431  clim0c  15473  rlim0  15474  rlim0lt  15475  rlimneg  15613  isercolllem3  15633  sumrblem  15677  summolem2a  15681  sumz  15688  fsumcl  15699  expcnv  15830  ntrivcvgfvn0  15865  ef4p  16081  sadadd2lem2  16420  sadadd2lem  16429  modprm0  16776  iserodd  16806  prmrec  16893  4sqlem10  16918  4sqlem11  16926  frgpnabllem1  19803  fsumcn  24761  cnheibor  24854  evth2  24859  rrxmval  25305  mbfmulc2lem  25548  mbfpos  25552  dvcnp2  25821  dvcmulf  25848  dvmptc  25862  dvmptcmul  25868  dvmptfsum  25879  dveflem  25883  dvef  25884  rolle  25894  elply2  26101  plyf  26103  elplyr  26106  elplyd  26107  ply1term  26109  ply0  26113  plyeq0  26116  plyaddlem  26120  plymullem  26121  dgrlem  26134  coeidlem  26142  plyco  26146  coeeq2  26147  coe0  26161  plycj  26183  coecj  26184  plycjOLD  26185  coecjOLD  26186  plymul0or  26188  dvply1  26191  fta1lem  26215  elqaalem3  26229  tayl0  26269  dvtaylp  26278  taylthlem2  26282  taylthlem2OLD  26283  radcnv0  26325  pserdvlem2  26338  pserdv  26339  ptolemy  26405  advlog  26563  advlogexp  26564  efopnlem2  26566  efopn  26567  logtayllem  26568  logtayl  26569  loglesqrt  26671  affineequiv  26733  quad2  26749  dcubic  26756  asinlem  26778  dvatan  26845  leibpilem2  26851  leibpi  26852  rlimcnp  26875  efrlim  26879  efrlimOLD  26880  emcllem7  26912  dmgmaddn0  26933  lgamgulmlem2  26940  igamf  26961  igamcl  26962  sqff1o  27092  dchrelbasd  27150  dchrsum2  27179  sumdchr2  27181  addsq2reu  27351  addsqnreup  27354  dchrvmasumiflem2  27413  occllem  31232  nlelchi  31990  divnumden2  32740  fprodeq02  32748  constrrtcc  33725  constrsslem  33731  constraddcl  33752  constrmulcl  33761  cos9thpiminplylem1  33772  cos9thpiminplylem3  33774  cos9thpinconstrlem1  33779  ballotlemic  34498  ballotlem1c  34499  signsvfn  34573  circlemeth  34631  elmrsubrn  35507  climlec3  35721  bj-bary1lem  37298  tan2h  37606  ftc1anclem5  37691  ftc1anclem6  37692  ftc1anclem7  37693  ftc1anclem8  37694  ftc1anc  37695  lcmineqlem7  42023  lcmineqlem12  42028  aks4d1p1p7  42062  aks6d1c2p2  42107  aks6d1c5lem1  42124  aks6d1c5lem2  42126  sticksstones10  42143  sticksstones12a  42145  sn-addlid  42392  remul02  42393  remul01  42395  sn-it0e0  42404  sn-addrid  42409  sn-addid0  42413  sn-mul01  42414  sn-0tie0  42439  sn-mul02  42440  evlsvvval  42551  3cubeslem1  42672  pell14qrgt0  42847  expgrowth  44324  binomcxplemnotnn0  44345  ellimcabssub0  45615  0ellimcdiv  45647  clim0cf  45652  cosknegpi  45867  fprodsubrecnncnvlem  45905  fprodaddrecnncnvlem  45907  dvsinax  45911  dvasinbx  45918  dvnmptconst  45939  dvnxpaek  45940  itgiccshift  45978  itgperiod  45979  itgsbtaddcnst  45980  stirlinglem7  46078  dirkertrigeqlem2  46097  fourierdlem59  46163  fourierdlem62  46166  fourierdlem74  46178  fourierdlem75  46179  sqwvfoura  46226  fouriersw  46229  etransclem20  46252  etransclem21  46253  etransclem22  46254  etransclem25  46257  etransclem35  46267  sge0z  46373  ovnhoilem1  46599  vonsn  46689  lambert0  46888  0nodd  48158  fdivmptf  48530  nn0sumshdiglem2  48611  eenglngeehlnmlem2  48727  itsclc0yqsollem1  48751