Theorem 0cnd 11189

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

Syntax hints:   → wi 4   ∈ wcel 2106  ℂcc 11090  0cc0 11092

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-1cn 11150  ax-icn 11151  ax-addcl 11152  ax-mulcl 11154  ax-i2m1 11160

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723  df-clel 2809

This theorem is referenced by:  addeq0  11619  mul0or  11836  diveq0  11864  eqneg  11916  un0addcl  12487  un0mulcl  12488  modsumfzodifsn  13891  muldivbinom2  14205  reusq0  15391  clim0c  15433  rlim0  15434  rlim0lt  15435  rlimneg  15575  isercolllem3  15595  sumrblem  15639  summolem2a  15643  sumz  15650  fsumcl  15661  expcnv  15792  ntrivcvgfvn0  15827  ef4p  16038  sadadd2lem2  16373  sadadd2lem  16382  modprm0  16720  iserodd  16750  prmrec  16837  4sqlem10  16862  4sqlem11  16870  frgpnabllem1  19701  fsumcn  24315  cnheibor  24400  evth2  24405  rrxmval  24851  mbfmulc2lem  25093  mbfpos  25097  dvcmulf  25391  dvmptc  25404  dvmptcmul  25410  dvmptfsum  25421  dveflem  25425  dvef  25426  rolle  25436  elply2  25639  plyf  25641  elplyr  25644  elplyd  25645  ply1term  25647  ply0  25651  plyeq0  25654  plyaddlem  25658  plymullem  25659  dgrlem  25672  coeidlem  25680  plyco  25684  coeeq2  25685  coe0  25699  plycj  25720  coecj  25721  plymul0or  25723  dvply1  25726  fta1lem  25749  elqaalem3  25763  tayl0  25803  dvtaylp  25811  taylthlem2  25815  radcnv0  25857  pserdvlem2  25869  pserdv  25870  ptolemy  25935  advlog  26091  advlogexp  26092  efopnlem2  26094  efopn  26095  logtayllem  26096  logtayl  26097  loglesqrt  26193  affineequiv  26255  quad2  26271  dcubic  26278  asinlem  26300  dvatan  26367  leibpilem2  26373  leibpi  26374  rlimcnp  26397  efrlim  26401  emcllem7  26433  dmgmaddn0  26454  lgamgulmlem2  26461  igamf  26482  igamcl  26483  sqff1o  26613  dchrelbasd  26669  dchrsum2  26698  sumdchr2  26700  addsq2reu  26870  addsqnreup  26873  dchrvmasumiflem2  26932  occllem  30419  nlelchi  31177  divnumden2  31895  fprodeq02  31900  ballotlemic  33336  ballotlem1c  33337  signsvfn  33424  circlemeth  33483  elmrsubrn  34342  climlec3  34533  bj-bary1lem  35995  tan2h  36284  ftc1anclem5  36369  ftc1anclem6  36370  ftc1anclem7  36371  ftc1anclem8  36372  ftc1anc  36373  lcmineqlem7  40705  lcmineqlem12  40710  aks4d1p1p7  40744  aks6d1c2p2  40762  sticksstones10  40776  sticksstones12a  40778  sn-addlid  41059  remul02  41060  remul01  41062  sn-it0e0  41070  sn-addrid  41075  sn-addid0  41079  sn-mul01  41080  sn-0tie0  41094  sn-mul02  41095  3cubeslem1  41193  pell14qrgt0  41368  expgrowth  42865  binomcxplemnotnn0  42886  ellimcabssub0  44106  0ellimcdiv  44138  clim0cf  44143  cosknegpi  44358  fprodsubrecnncnvlem  44396  fprodaddrecnncnvlem  44398  dvsinax  44402  dvasinbx  44409  dvnmptconst  44430  dvnxpaek  44431  itgiccshift  44469  itgperiod  44470  itgsbtaddcnst  44471  stirlinglem7  44569  dirkertrigeqlem2  44588  fourierdlem59  44654  fourierdlem62  44657  fourierdlem74  44669  fourierdlem75  44670  sqwvfoura  44717  fouriersw  44720  etransclem20  44743  etransclem21  44744  etransclem22  44745  etransclem25  44748  etransclem35  44758  sge0z  44864  ovnhoilem1  45090  vonsn  45180  0nodd  46352  fdivmptf  46875  nn0sumshdiglem2  46956  eenglngeehlnmlem2  47072  itsclc0yqsollem1  47096