Theorem 0cnd 11174

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 11073  0cc0 11075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-mulcl 11137  ax-i2m1 11143

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-clel 2804

This theorem is referenced by:  addeq0  11608  mul0or  11825  eqneg  11909  un0addcl  12482  un0mulcl  12483  modsumfzodifsn  13916  muldivbinom2  14235  reusq0  15438  clim0c  15480  rlim0  15481  rlim0lt  15482  rlimneg  15620  isercolllem3  15640  sumrblem  15684  summolem2a  15688  sumz  15695  fsumcl  15706  expcnv  15837  ntrivcvgfvn0  15872  ef4p  16088  sadadd2lem2  16427  sadadd2lem  16436  modprm0  16783  iserodd  16813  prmrec  16900  4sqlem10  16925  4sqlem11  16933  frgpnabllem1  19810  fsumcn  24768  cnheibor  24861  evth2  24866  rrxmval  25312  mbfmulc2lem  25555  mbfpos  25559  dvcnp2  25828  dvcmulf  25855  dvmptc  25869  dvmptcmul  25875  dvmptfsum  25886  dveflem  25890  dvef  25891  rolle  25901  elply2  26108  plyf  26110  elplyr  26113  elplyd  26114  ply1term  26116  ply0  26120  plyeq0  26123  plyaddlem  26127  plymullem  26128  dgrlem  26141  coeidlem  26149  plyco  26153  coeeq2  26154  coe0  26168  plycj  26190  coecj  26191  plycjOLD  26192  coecjOLD  26193  plymul0or  26195  dvply1  26198  fta1lem  26222  elqaalem3  26236  tayl0  26276  dvtaylp  26285  taylthlem2  26289  taylthlem2OLD  26290  radcnv0  26332  pserdvlem2  26345  pserdv  26346  ptolemy  26412  advlog  26570  advlogexp  26571  efopnlem2  26573  efopn  26574  logtayllem  26575  logtayl  26576  loglesqrt  26678  affineequiv  26740  quad2  26756  dcubic  26763  asinlem  26785  dvatan  26852  leibpilem2  26858  leibpi  26859  rlimcnp  26882  efrlim  26886  efrlimOLD  26887  emcllem7  26919  dmgmaddn0  26940  lgamgulmlem2  26947  igamf  26968  igamcl  26969  sqff1o  27099  dchrelbasd  27157  dchrsum2  27186  sumdchr2  27188  addsq2reu  27358  addsqnreup  27361  dchrvmasumiflem2  27420  occllem  31239  nlelchi  31997  divnumden2  32747  fprodeq02  32755  constrrtcc  33732  constrsslem  33738  constraddcl  33759  constrmulcl  33768  cos9thpiminplylem1  33779  cos9thpiminplylem3  33781  cos9thpinconstrlem1  33786  ballotlemic  34505  ballotlem1c  34506  signsvfn  34580  circlemeth  34638  elmrsubrn  35514  climlec3  35728  bj-bary1lem  37305  tan2h  37613  ftc1anclem5  37698  ftc1anclem6  37699  ftc1anclem7  37700  ftc1anclem8  37701  ftc1anc  37702  lcmineqlem7  42030  lcmineqlem12  42035  aks4d1p1p7  42069  aks6d1c2p2  42114  aks6d1c5lem1  42131  aks6d1c5lem2  42133  sticksstones10  42150  sticksstones12a  42152  sn-addlid  42399  remul02  42400  remul01  42402  sn-it0e0  42411  sn-addrid  42416  sn-addid0  42420  sn-mul01  42421  sn-0tie0  42446  sn-mul02  42447  evlsvvval  42558  3cubeslem1  42679  pell14qrgt0  42854  expgrowth  44331  binomcxplemnotnn0  44352  ellimcabssub0  45622  0ellimcdiv  45654  clim0cf  45659  cosknegpi  45874  fprodsubrecnncnvlem  45912  fprodaddrecnncnvlem  45914  dvsinax  45918  dvasinbx  45925  dvnmptconst  45946  dvnxpaek  45947  itgiccshift  45985  itgperiod  45986  itgsbtaddcnst  45987  stirlinglem7  46085  dirkertrigeqlem2  46104  fourierdlem59  46170  fourierdlem62  46173  fourierdlem74  46185  fourierdlem75  46186  sqwvfoura  46233  fouriersw  46236  etransclem20  46259  etransclem21  46260  etransclem22  46261  etransclem25  46264  etransclem35  46274  sge0z  46380  ovnhoilem1  46606  vonsn  46696  lambert0  46895  0nodd  48162  fdivmptf  48534  nn0sumshdiglem2  48615  eenglngeehlnmlem2  48731  itsclc0yqsollem1  48755