Theorem 0cnd 11309

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ℂcc 11208  0cc0 11210

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-1cn 11268  ax-icn 11269  ax-addcl 11270  ax-mulcl 11272  ax-i2m1 11278

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2755  df-clel 2838

This theorem is used by:  addeq0  11749  mul0or  11966  eqneg  12047  un0addcl  12649  un0mulcl  12650  modsumfzodifsn  14097  muldivbinom2  14417  reusq0  15644  clim0c  15686  rlim0  15687  rlim0lt  15688  rlimneg  15826  isercolllem3  15846  sumrblem  15889  summolem2a  15893  sumz  15900  fsumcl  15911  expcnv  16045  ntrivcvgfvn0  16080  ef4p  16293  sadadd2lem2  16632  sadadd2lem  16641  modprm0  16995  iserodd  17025  prmrec  17112  4sqlem10  17137  4sqlem11  17145  frgpnabllem1  20099  evlsvvval  22414  fsumcn  25203  cnheibor  25288  evth2  25293  rrxmval  25738  mbfmulc2lem  25980  mbfpos  25984  dvcnp2  26252  dvcmulf  26277  dvmptc  26290  dvmptcmul  26296  dvmptfsum  26307  dveflem  26311  dvef  26312  rolle  26322  elply2  26526  plyf  26528  elplyr  26531  elplyd  26532  ply1term  26534  ply0  26538  plyeq0  26542  plyaddlem  26546  plymullem  26547  dgrlem  26560  coeidlem  26568  plyco  26572  coeeq2  26573  coe0  26587  plycj  26608  coecj  26609  plymul0or  26611  dvply1  26617  fta1lem  26640  elqaalem3  26656  tayl0  26701  dvtaylp  26709  taylthlem2  26713  radcnv0  26755  pserdvlem2  26767  pserdv  26768  ptolemy  26837  advlog  26994  advlogexp  26995  efopnlem2  26997  efopn  26998  logtayllem  26999  logtayl  27000  loglesqrt  27101  affineequiv  27163  quad2  27179  dcubic  27186  asinlem  27208  dvatan  27275  leibpilem2  27281  leibpi  27282  rlimcnp  27305  efrlim  27309  emcllem7  27341  dmgmaddn0  27362  lgamgulmlem2  27369  igamf  27390  igamcl  27391  sqff1o  27521  dchrelbasd  27578  dchrsum2  27607  sumdchr2  27609  addsq2reu  27779  addsqnreup  27782  dchrvmasumiflem2  27841  occllem  31917  nlelchi  32675  divnumden2  33460  fprodeq02  33468  gsumind  33959  constrrtcc  34420  constrsslem  34426  constraddcl  34447  constrmulcl  34456  cos9thpiminplylem1  34467  cos9thpiminplylem3  34469  cos9thpinconstrlem1  34474  ballotlemic  35192  ballotlem1c  35193  signsvfn  35264  circlemeth  35322  elmrsubrn  36406  climlec3  36626  bj-bary1lem  38371  tan2h  38675  ftc1anclem5  38755  ftc1anclem6  38756  ftc1anclem7  38757  ftc1anclem8  38758  ftc1anc  38759  lcmineqlem7  43225  lcmineqlem12  43230  aks4d1p1p7  43264  aks6d1c2p2  43309  aks6d1c5lem1  43326  aks6d1c5lem2  43328  sticksstones10  43345  sticksstones12a  43347  sn-addlid  43595  remul02  43596  remul01  43598  sn-it0e0  43607  sn-addrid  43612  sn-addid0  43616  sn-mul01  43617  sn-0tie0  43655  sn-mul02  43656  3cubeslem1  43834  pell14qrgt0  44006  expgrowth  45459  binomcxplemnotnn0  45480  ellimcabssub0  46768  0ellimcdiv  46798  clim0cf  46803  cosknegpi  47018  fprodsubrecnncnvlem  47056  fprodaddrecnncnvlem  47058  dvsinax  47062  dvasinbx  47069  dvnmptconst  47090  dvnxpaek  47091  itgiccshift  47129  itgperiod  47130  itgsbtaddcnst  47131  stirlinglem7  47229  dirkertrigeqlem2  47248  fourierdlem59  47314  fourierdlem62  47317  fourierdlem74  47329  fourierdlem75  47330  sqwvfoura  47377  fouriersw  47380  etransclem20  47403  etransclem21  47404  etransclem22  47405  etransclem25  47408  etransclem35  47418  sge0z  47524  ovnhoilem1  47750  vonsn  47840  sqrtnnaa  48052  sqrtnzqaa  48053  lambert0  48076  0nodd  49406  fdivmptf  49792  nn0sumshdiglem2  49873  eenglngeehlnmlem2  49990  itsclc0yqsollem1  50013