Theorem 0cnd 11207

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℂcc 11108  0cc0 11110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-mulcl 11172  ax-i2m1 11178

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-clel 2811

This theorem is referenced by:  addeq0  11637  mul0or  11854  diveq0  11882  eqneg  11934  un0addcl  12505  un0mulcl  12506  modsumfzodifsn  13909  muldivbinom2  14223  reusq0  15409  clim0c  15451  rlim0  15452  rlim0lt  15453  rlimneg  15593  isercolllem3  15613  sumrblem  15657  summolem2a  15661  sumz  15668  fsumcl  15679  expcnv  15810  ntrivcvgfvn0  15845  ef4p  16056  sadadd2lem2  16391  sadadd2lem  16400  modprm0  16738  iserodd  16768  prmrec  16855  4sqlem10  16880  4sqlem11  16888  frgpnabllem1  19741  fsumcn  24386  cnheibor  24471  evth2  24476  rrxmval  24922  mbfmulc2lem  25164  mbfpos  25168  dvcmulf  25462  dvmptc  25475  dvmptcmul  25481  dvmptfsum  25492  dveflem  25496  dvef  25497  rolle  25507  elply2  25710  plyf  25712  elplyr  25715  elplyd  25716  ply1term  25718  ply0  25722  plyeq0  25725  plyaddlem  25729  plymullem  25730  dgrlem  25743  coeidlem  25751  plyco  25755  coeeq2  25756  coe0  25770  plycj  25791  coecj  25792  plymul0or  25794  dvply1  25797  fta1lem  25820  elqaalem3  25834  tayl0  25874  dvtaylp  25882  taylthlem2  25886  radcnv0  25928  pserdvlem2  25940  pserdv  25941  ptolemy  26006  advlog  26162  advlogexp  26163  efopnlem2  26165  efopn  26166  logtayllem  26167  logtayl  26168  loglesqrt  26266  affineequiv  26328  quad2  26344  dcubic  26351  asinlem  26373  dvatan  26440  leibpilem2  26446  leibpi  26447  rlimcnp  26470  efrlim  26474  emcllem7  26506  dmgmaddn0  26527  lgamgulmlem2  26534  igamf  26555  igamcl  26556  sqff1o  26686  dchrelbasd  26742  dchrsum2  26771  sumdchr2  26773  addsq2reu  26943  addsqnreup  26946  dchrvmasumiflem2  27005  occllem  30556  nlelchi  31314  divnumden2  32024  fprodeq02  32029  ballotlemic  33505  ballotlem1c  33506  signsvfn  33593  circlemeth  33652  elmrsubrn  34511  climlec3  34703  gg-dvcnp2  35174  bj-bary1lem  36191  tan2h  36480  ftc1anclem5  36565  ftc1anclem6  36566  ftc1anclem7  36567  ftc1anclem8  36568  ftc1anc  36569  lcmineqlem7  40900  lcmineqlem12  40905  aks4d1p1p7  40939  aks6d1c2p2  40957  sticksstones10  40971  sticksstones12a  40973  evlsvvval  41135  sn-addlid  41277  remul02  41278  remul01  41280  sn-it0e0  41288  sn-addrid  41293  sn-addid0  41297  sn-mul01  41298  sn-0tie0  41312  sn-mul02  41313  3cubeslem1  41422  pell14qrgt0  41597  expgrowth  43094  binomcxplemnotnn0  43115  ellimcabssub0  44333  0ellimcdiv  44365  clim0cf  44370  cosknegpi  44585  fprodsubrecnncnvlem  44623  fprodaddrecnncnvlem  44625  dvsinax  44629  dvasinbx  44636  dvnmptconst  44657  dvnxpaek  44658  itgiccshift  44696  itgperiod  44697  itgsbtaddcnst  44698  stirlinglem7  44796  dirkertrigeqlem2  44815  fourierdlem59  44881  fourierdlem62  44884  fourierdlem74  44896  fourierdlem75  44897  sqwvfoura  44944  fouriersw  44947  etransclem20  44970  etransclem21  44971  etransclem22  44972  etransclem25  44975  etransclem35  44985  sge0z  45091  ovnhoilem1  45317  vonsn  45407  0nodd  46580  fdivmptf  47227  nn0sumshdiglem2  47308  eenglngeehlnmlem2  47424  itsclc0yqsollem1  47448