Theorem 0cnd 11137

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 11036  0cc0 11038

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 2708  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-mulcl 11100  ax-i2m1 11106

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

This theorem is referenced by:  addeq0  11573  mul0or  11790  eqneg  11875  un0addcl  12470  un0mulcl  12471  modsumfzodifsn  13906  muldivbinom2  14225  reusq0  15427  clim0c  15469  rlim0  15470  rlim0lt  15471  rlimneg  15609  isercolllem3  15629  sumrblem  15673  summolem2a  15677  sumz  15684  fsumcl  15695  expcnv  15829  ntrivcvgfvn0  15864  ef4p  16080  sadadd2lem2  16419  sadadd2lem  16428  modprm0  16776  iserodd  16806  prmrec  16893  4sqlem10  16918  4sqlem11  16926  frgpnabllem1  19848  evlsvvval  22071  fsumcn  24837  cnheibor  24922  evth2  24927  rrxmval  25372  mbfmulc2lem  25614  mbfpos  25618  dvcnp2  25887  dvcmulf  25912  dvmptc  25925  dvmptcmul  25931  dvmptfsum  25942  dveflem  25946  dvef  25947  rolle  25957  elply2  26161  plyf  26163  elplyr  26166  elplyd  26167  ply1term  26169  ply0  26173  plyeq0  26176  plyaddlem  26180  plymullem  26181  dgrlem  26194  coeidlem  26202  plyco  26206  coeeq2  26207  coe0  26221  plycj  26242  coecj  26243  plycjOLD  26244  coecjOLD  26245  plymul0or  26247  dvply1  26250  fta1lem  26273  elqaalem3  26287  tayl0  26327  dvtaylp  26335  taylthlem2  26339  radcnv0  26381  pserdvlem2  26393  pserdv  26394  ptolemy  26460  advlog  26618  advlogexp  26619  efopnlem2  26621  efopn  26622  logtayllem  26623  logtayl  26624  loglesqrt  26725  affineequiv  26787  quad2  26803  dcubic  26810  asinlem  26832  dvatan  26899  leibpilem2  26905  leibpi  26906  rlimcnp  26929  efrlim  26933  emcllem7  26965  dmgmaddn0  26986  lgamgulmlem2  26993  igamf  27014  igamcl  27015  sqff1o  27145  dchrelbasd  27202  dchrsum2  27231  sumdchr2  27233  addsq2reu  27403  addsqnreup  27406  dchrvmasumiflem2  27465  occllem  31374  nlelchi  32132  divnumden2  32889  fprodeq02  32897  gsumind  33405  constrrtcc  33879  constrsslem  33885  constraddcl  33906  constrmulcl  33915  cos9thpiminplylem1  33926  cos9thpiminplylem3  33928  cos9thpinconstrlem1  33933  ballotlemic  34651  ballotlem1c  34652  signsvfn  34726  circlemeth  34784  elmrsubrn  35702  climlec3  35916  bj-bary1lem  37624  tan2h  37933  ftc1anclem5  38018  ftc1anclem6  38019  ftc1anclem7  38020  ftc1anclem8  38021  ftc1anc  38022  lcmineqlem7  42474  lcmineqlem12  42479  aks4d1p1p7  42513  aks6d1c2p2  42558  aks6d1c5lem1  42575  aks6d1c5lem2  42577  sticksstones10  42594  sticksstones12a  42596  sn-addlid  42836  remul02  42837  remul01  42839  sn-it0e0  42848  sn-addrid  42853  sn-addid0  42857  sn-mul01  42858  sn-0tie0  42896  sn-mul02  42897  3cubeslem1  43116  pell14qrgt0  43287  expgrowth  44762  binomcxplemnotnn0  44783  ellimcabssub0  46047  0ellimcdiv  46077  clim0cf  46082  cosknegpi  46297  fprodsubrecnncnvlem  46335  fprodaddrecnncnvlem  46337  dvsinax  46341  dvasinbx  46348  dvnmptconst  46369  dvnxpaek  46370  itgiccshift  46408  itgperiod  46409  itgsbtaddcnst  46410  stirlinglem7  46508  dirkertrigeqlem2  46527  fourierdlem59  46593  fourierdlem62  46596  fourierdlem74  46608  fourierdlem75  46609  sqwvfoura  46656  fouriersw  46659  etransclem20  46682  etransclem21  46683  etransclem22  46684  etransclem25  46687  etransclem35  46697  sge0z  46803  ovnhoilem1  47029  vonsn  47119  lambert0  47335  0nodd  48646  fdivmptf  49017  nn0sumshdiglem2  49098  eenglngeehlnmlem2  49214  itsclc0yqsollem1  49238