Theorem 0cnd 10369

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

Syntax hints:   → wi 4   ∈ wcel 2106  ℂcc 10270  0cc0 10272

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-9 2115  ax-ext 2753  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-mulcl 10334  ax-i2m1 10340

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824  df-cleq 2769  df-clel 2773

This theorem is referenced by:  addeq0  10798  mul0or  11015  diveq0  11043  eqneg  11095  un0addcl  11677  un0mulcl  11678  modsumfzodifsn  13062  muldivbinom2  13368  clim0c  14646  rlim0  14647  rlim0lt  14648  rlimneg  14785  isercolllem3  14805  sumrblem  14849  summolem2a  14853  sumz  14860  fsumcl  14871  expcnv  15000  ntrivcvgfvn0  15034  ef4p  15245  sadadd2lem2  15578  sadadd2lem  15587  modprm0  15914  iserodd  15944  prmrec  16030  4sqlem10  16055  4sqlem11  16063  frgpnabllem1  18662  fsumcn  23081  cnheibor  23162  evth2  23167  rrxmval  23611  mbfmulc2lem  23851  mbfpos  23855  dvcmulf  24145  dvmptc  24158  dvmptcmul  24164  dvmptfsum  24175  dveflem  24179  rolle  24190  elply2  24389  plyf  24391  elplyr  24394  elplyd  24395  ply1term  24397  ply0  24401  plyeq0  24404  plyaddlem  24408  plymullem  24409  dgrlem  24422  coeidlem  24430  plyco  24434  coeeq2  24435  coe0  24449  plycj  24470  coecj  24471  plymul0or  24473  dvply1  24476  fta1lem  24499  elqaalem3  24513  tayl0  24553  dvtaylp  24561  taylthlem2  24565  radcnv0  24607  pserdvlem2  24619  pserdv  24620  ptolemy  24686  advlog  24837  advlogexp  24838  efopnlem2  24840  efopn  24841  logtayllem  24842  logtayl  24843  loglesqrt  24939  affineequiv  25001  quad2  25017  dcubic  25024  asinlem  25046  dvatan  25113  leibpilem2  25120  leibpi  25121  rlimcnp  25144  efrlim  25148  emcllem7  25180  dmgmaddn0  25201  lgamgulmlem2  25208  igamf  25229  igamcl  25230  sqff1o  25360  dchrelbasd  25416  dchrsum2  25445  sumdchr2  25447  dchrvmasumiflem2  25643  occllem  28734  nlelchi  29492  divnumden2  30128  fprodeq02  30133  ballotlemic  31167  ballotlem1c  31168  signsvfn  31261  circlemeth  31320  elmrsubrn  32016  climlec3  32213  bj-bary1lem  33758  tan2h  34021  ftc1anclem5  34109  ftc1anclem6  34110  ftc1anclem7  34111  ftc1anclem8  34112  ftc1anc  34113  pell14qrgt0  38376  expgrowth  39483  binomcxplemnotnn0  39504  ellimcabssub0  40750  0ellimcdiv  40782  clim0cf  40787  cosknegpi  41001  fprodsubrecnncnvlem  41042  fprodaddrecnncnvlem  41044  dvsinax  41048  dvasinbx  41056  dvnmptconst  41077  dvnxpaek  41078  itgiccshift  41116  itgperiod  41117  itgsbtaddcnst  41118  stirlinglem7  41217  dirkertrigeqlem2  41236  fourierdlem59  41302  fourierdlem62  41305  fourierdlem74  41317  fourierdlem75  41318  sqwvfoura  41365  fouriersw  41368  etransclem20  41391  etransclem21  41392  etransclem22  41393  etransclem25  41396  etransclem35  41406  sge0z  41509  ovnhoilem1  41735  vonsn  41825  0nodd  42818  fdivmptf  43343  nn0sumshdiglem2  43424  eenglngeehlnmlem2  43467  itsclc0yqsollem1  43491