Theorem 0cnd 10899

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℂcc 10800  0cc0 10802

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-mulcl 10864  ax-i2m1 10870

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-clel 2817

This theorem is referenced by:  addeq0  11328  mul0or  11545  diveq0  11573  eqneg  11625  un0addcl  12196  un0mulcl  12197  modsumfzodifsn  13592  muldivbinom2  13905  reusq0  15102  clim0c  15144  rlim0  15145  rlim0lt  15146  rlimneg  15286  isercolllem3  15306  sumrblem  15351  summolem2a  15355  sumz  15362  fsumcl  15373  expcnv  15504  ntrivcvgfvn0  15539  ef4p  15750  sadadd2lem2  16085  sadadd2lem  16094  modprm0  16434  iserodd  16464  prmrec  16551  4sqlem10  16576  4sqlem11  16584  frgpnabllem1  19389  fsumcn  23939  cnheibor  24024  evth2  24029  rrxmval  24474  mbfmulc2lem  24716  mbfpos  24720  dvcmulf  25014  dvmptc  25027  dvmptcmul  25033  dvmptfsum  25044  dveflem  25048  dvef  25049  rolle  25059  elply2  25262  plyf  25264  elplyr  25267  elplyd  25268  ply1term  25270  ply0  25274  plyeq0  25277  plyaddlem  25281  plymullem  25282  dgrlem  25295  coeidlem  25303  plyco  25307  coeeq2  25308  coe0  25322  plycj  25343  coecj  25344  plymul0or  25346  dvply1  25349  fta1lem  25372  elqaalem3  25386  tayl0  25426  dvtaylp  25434  taylthlem2  25438  radcnv0  25480  pserdvlem2  25492  pserdv  25493  ptolemy  25558  advlog  25714  advlogexp  25715  efopnlem2  25717  efopn  25718  logtayllem  25719  logtayl  25720  loglesqrt  25816  affineequiv  25878  quad2  25894  dcubic  25901  asinlem  25923  dvatan  25990  leibpilem2  25996  leibpi  25997  rlimcnp  26020  efrlim  26024  emcllem7  26056  dmgmaddn0  26077  lgamgulmlem2  26084  igamf  26105  igamcl  26106  sqff1o  26236  dchrelbasd  26292  dchrsum2  26321  sumdchr2  26323  addsq2reu  26493  addsqnreup  26496  dchrvmasumiflem2  26555  occllem  29566  nlelchi  30324  divnumden2  31034  fprodeq02  31039  ballotlemic  32373  ballotlem1c  32374  signsvfn  32461  circlemeth  32520  elmrsubrn  33382  climlec3  33605  bj-bary1lem  35408  tan2h  35696  ftc1anclem5  35781  ftc1anclem6  35782  ftc1anclem7  35783  ftc1anclem8  35784  ftc1anc  35785  lcmineqlem7  39971  lcmineqlem12  39976  aks4d1p1p7  40010  sticksstones10  40039  sticksstones12a  40041  sn-addid2  40308  remul02  40309  remul01  40311  sn-it0e0  40318  sn-addid1  40323  sn-addid0  40327  sn-mul01  40328  sn-0tie0  40342  sn-mul02  40343  3cubeslem1  40422  pell14qrgt0  40597  expgrowth  41842  binomcxplemnotnn0  41863  ellimcabssub0  43048  0ellimcdiv  43080  clim0cf  43085  cosknegpi  43300  fprodsubrecnncnvlem  43338  fprodaddrecnncnvlem  43340  dvsinax  43344  dvasinbx  43351  dvnmptconst  43372  dvnxpaek  43373  itgiccshift  43411  itgperiod  43412  itgsbtaddcnst  43413  stirlinglem7  43511  dirkertrigeqlem2  43530  fourierdlem59  43596  fourierdlem62  43599  fourierdlem74  43611  fourierdlem75  43612  sqwvfoura  43659  fouriersw  43662  etransclem20  43685  etransclem21  43686  etransclem22  43687  etransclem25  43690  etransclem35  43700  sge0z  43803  ovnhoilem1  44029  vonsn  44119  0nodd  45252  fdivmptf  45775  nn0sumshdiglem2  45856  eenglngeehlnmlem2  45972  itsclc0yqsollem1  45996