Theorem 0cnd 11199

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

Syntax hints:   → wi 4   ∈ wcel 2149  ℂcc 11098  0cc0 11100

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-1cn 11158  ax-icn 11159  ax-addcl 11160  ax-mulcl 11162  ax-i2m1 11168

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-clel 2844

This theorem is referenced by:  addeq0  11637  mul0or  11854  eqneg  11935  un0addcl  12537  un0mulcl  12538  modsumfzodifsn  13980  muldivbinom2  14299  reusq0  15516  clim0c  15558  rlim0  15559  rlim0lt  15560  rlimneg  15698  isercolllem3  15718  sumrblem  15762  summolem2a  15766  sumz  15773  fsumcl  15784  expcnv  15918  ntrivcvgfvn0  15953  ef4p  16169  sadadd2lem2  16508  sadadd2lem  16517  modprm0  16865  iserodd  16895  prmrec  16982  4sqlem10  17007  4sqlem11  17015  frgpnabllem1  19943  evlsvvval  22213  fsumcn  24998  cnheibor  25083  evth2  25088  rrxmval  25533  mbfmulc2lem  25775  mbfpos  25779  dvcnp2  26048  dvcmulf  26073  dvmptc  26086  dvmptcmul  26092  dvmptfsum  26103  dveflem  26107  dvef  26108  rolle  26118  elply2  26322  plyf  26324  elplyr  26327  elplyd  26328  ply1term  26330  ply0  26334  plyeq0  26337  plyaddlem  26341  plymullem  26342  dgrlem  26355  coeidlem  26363  plyco  26367  coeeq2  26368  coe0  26382  plycj  26403  coecj  26404  plycjOLD  26405  coecjOLD  26406  plymul0or  26408  dvply1  26414  fta1lem  26437  elqaalem3  26451  tayl0  26491  dvtaylp  26499  taylthlem2  26503  radcnv0  26545  pserdvlem2  26557  pserdv  26558  ptolemy  26627  advlog  26785  advlogexp  26786  efopnlem2  26788  efopn  26789  logtayllem  26790  logtayl  26791  loglesqrt  26892  affineequiv  26954  quad2  26970  dcubic  26977  asinlem  26999  dvatan  27066  leibpilem2  27072  leibpi  27073  rlimcnp  27096  efrlim  27100  emcllem7  27132  dmgmaddn0  27153  lgamgulmlem2  27160  igamf  27181  igamcl  27182  sqff1o  27312  dchrelbasd  27369  dchrsum2  27398  sumdchr2  27400  addsq2reu  27570  addsqnreup  27573  dchrvmasumiflem2  27632  occllem  31596  nlelchi  32354  divnumden2  33101  fprodeq02  33109  gsumind  33608  constrrtcc  34070  constrsslem  34076  constraddcl  34097  constrmulcl  34106  cos9thpiminplylem1  34117  cos9thpiminplylem3  34119  cos9thpinconstrlem1  34124  ballotlemic  34842  ballotlem1c  34843  signsvfn  34914  circlemeth  34972  elmrsubrn  35911  climlec3  36125  bj-bary1lem  37842  tan2h  38151  ftc1anclem5  38236  ftc1anclem6  38237  ftc1anclem7  38238  ftc1anclem8  38239  ftc1anc  38240  lcmineqlem7  42692  lcmineqlem12  42697  aks4d1p1p7  42731  aks6d1c2p2  42776  aks6d1c5lem1  42793  aks6d1c5lem2  42795  sticksstones10  42812  sticksstones12a  42814  sn-addlid  43055  remul02  43056  remul01  43058  sn-it0e0  43067  sn-addrid  43072  sn-addid0  43076  sn-mul01  43077  sn-0tie0  43115  sn-mul02  43116  3cubeslem1  43307  pell14qrgt0  43478  expgrowth  44937  binomcxplemnotnn0  44958  ellimcabssub0  46225  0ellimcdiv  46255  clim0cf  46260  cosknegpi  46475  fprodsubrecnncnvlem  46513  fprodaddrecnncnvlem  46515  dvsinax  46519  dvasinbx  46526  dvnmptconst  46547  dvnxpaek  46548  itgiccshift  46586  itgperiod  46587  itgsbtaddcnst  46588  stirlinglem7  46686  dirkertrigeqlem2  46705  fourierdlem59  46771  fourierdlem62  46774  fourierdlem74  46786  fourierdlem75  46787  sqwvfoura  46834  fouriersw  46837  etransclem20  46860  etransclem21  46861  etransclem22  46862  etransclem25  46865  etransclem35  46875  sge0z  46981  ovnhoilem1  47207  vonsn  47297  lambert0  47513  0nodd  48824  fdivmptf  49206  nn0sumshdiglem2  49287  eenglngeehlnmlem2  49403  itsclc0yqsollem1  49427