Theorem 0cnd 11283

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℂcc 11182  0cc0 11184

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-mulcl 11246  ax-i2m1 11252

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-clel 2819

This theorem is referenced by:  addeq0  11713  mul0or  11930  eqneg  12014  un0addcl  12586  un0mulcl  12587  modsumfzodifsn  13995  muldivbinom2  14312  reusq0  15511  clim0c  15553  rlim0  15554  rlim0lt  15555  rlimneg  15695  isercolllem3  15715  sumrblem  15759  summolem2a  15763  sumz  15770  fsumcl  15781  expcnv  15912  ntrivcvgfvn0  15947  ef4p  16161  sadadd2lem2  16496  sadadd2lem  16505  modprm0  16852  iserodd  16882  prmrec  16969  4sqlem10  16994  4sqlem11  17002  frgpnabllem1  19915  fsumcn  24913  cnheibor  25006  evth2  25011  rrxmval  25458  mbfmulc2lem  25701  mbfpos  25705  dvcnp2  25975  dvcmulf  26002  dvmptc  26016  dvmptcmul  26022  dvmptfsum  26033  dveflem  26037  dvef  26038  rolle  26048  elply2  26255  plyf  26257  elplyr  26260  elplyd  26261  ply1term  26263  ply0  26267  plyeq0  26270  plyaddlem  26274  plymullem  26275  dgrlem  26288  coeidlem  26296  plyco  26300  coeeq2  26301  coe0  26315  plycj  26337  coecj  26338  plymul0or  26340  dvply1  26343  fta1lem  26367  elqaalem3  26381  tayl0  26421  dvtaylp  26430  taylthlem2  26434  taylthlem2OLD  26435  radcnv0  26477  pserdvlem2  26490  pserdv  26491  ptolemy  26556  advlog  26714  advlogexp  26715  efopnlem2  26717  efopn  26718  logtayllem  26719  logtayl  26720  loglesqrt  26822  affineequiv  26884  quad2  26900  dcubic  26907  asinlem  26929  dvatan  26996  leibpilem2  27002  leibpi  27003  rlimcnp  27026  efrlim  27030  efrlimOLD  27031  emcllem7  27063  dmgmaddn0  27084  lgamgulmlem2  27091  igamf  27112  igamcl  27113  sqff1o  27243  dchrelbasd  27301  dchrsum2  27330  sumdchr2  27332  addsq2reu  27502  addsqnreup  27505  dchrvmasumiflem2  27564  occllem  31335  nlelchi  32093  divnumden2  32819  fprodeq02  32827  constrrtcc  33726  constrsslem  33731  ballotlemic  34471  ballotlem1c  34472  signsvfn  34559  circlemeth  34617  elmrsubrn  35488  climlec3  35696  bj-bary1lem  37276  tan2h  37572  ftc1anclem5  37657  ftc1anclem6  37658  ftc1anclem7  37659  ftc1anclem8  37660  ftc1anc  37661  lcmineqlem7  41992  lcmineqlem12  41997  aks4d1p1p7  42031  aks6d1c2p2  42076  aks6d1c5lem1  42093  aks6d1c5lem2  42095  sticksstones10  42112  sticksstones12a  42114  sn-addlid  42380  remul02  42381  remul01  42383  sn-it0e0  42391  sn-addrid  42396  sn-addid0  42400  sn-mul01  42401  sn-0tie0  42415  sn-mul02  42416  evlsvvval  42518  3cubeslem1  42640  pell14qrgt0  42815  expgrowth  44304  binomcxplemnotnn0  44325  ellimcabssub0  45538  0ellimcdiv  45570  clim0cf  45575  cosknegpi  45790  fprodsubrecnncnvlem  45828  fprodaddrecnncnvlem  45830  dvsinax  45834  dvasinbx  45841  dvnmptconst  45862  dvnxpaek  45863  itgiccshift  45901  itgperiod  45902  itgsbtaddcnst  45903  stirlinglem7  46001  dirkertrigeqlem2  46020  fourierdlem59  46086  fourierdlem62  46089  fourierdlem74  46101  fourierdlem75  46102  sqwvfoura  46149  fouriersw  46152  etransclem20  46175  etransclem21  46176  etransclem22  46177  etransclem25  46180  etransclem35  46190  sge0z  46296  ovnhoilem1  46522  vonsn  46612  0nodd  47893  fdivmptf  48275  nn0sumshdiglem2  48356  eenglngeehlnmlem2  48472  itsclc0yqsollem1  48496