Theorem 0cnd 11299

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℂcc 11198  0cc0 11200

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-mulcl 11262  ax-i2m1 11268

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-clel 2836

This theorem is used by:  addeq0  11739  mul0or  11956  eqneg  12037  un0addcl  12639  un0mulcl  12640  modsumfzodifsn  14087  muldivbinom2  14407  reusq0  15632  clim0c  15674  rlim0  15675  rlim0lt  15676  rlimneg  15814  isercolllem3  15834  sumrblem  15877  summolem2a  15881  sumz  15888  fsumcl  15899  expcnv  16033  ntrivcvgfvn0  16068  ef4p  16281  sadadd2lem2  16620  sadadd2lem  16629  modprm0  16983  iserodd  17013  prmrec  17100  4sqlem10  17125  4sqlem11  17133  frgpnabllem1  20087  evlsvvval  22402  fsumcn  25191  cnheibor  25276  evth2  25281  rrxmval  25726  mbfmulc2lem  25968  mbfpos  25972  dvcnp2  26240  dvcmulf  26265  dvmptc  26278  dvmptcmul  26284  dvmptfsum  26295  dveflem  26299  dvef  26300  rolle  26310  elply2  26514  plyf  26516  elplyr  26519  elplyd  26520  ply1term  26522  ply0  26526  plyeq0  26530  plyaddlem  26534  plymullem  26535  dgrlem  26548  coeidlem  26556  plyco  26560  coeeq2  26561  coe0  26575  plycj  26596  coecj  26597  plymul0or  26599  dvply1  26605  fta1lem  26628  elqaalem3  26644  tayl0  26689  dvtaylp  26697  taylthlem2  26701  radcnv0  26743  pserdvlem2  26755  pserdv  26756  ptolemy  26825  advlog  26982  advlogexp  26983  efopnlem2  26985  efopn  26986  logtayllem  26987  logtayl  26988  loglesqrt  27089  affineequiv  27151  quad2  27167  dcubic  27174  asinlem  27196  dvatan  27263  leibpilem2  27269  leibpi  27270  rlimcnp  27293  efrlim  27297  emcllem7  27329  dmgmaddn0  27350  lgamgulmlem2  27357  igamf  27378  igamcl  27379  sqff1o  27509  dchrelbasd  27566  dchrsum2  27595  sumdchr2  27597  addsq2reu  27767  addsqnreup  27770  dchrvmasumiflem2  27829  occllem  31905  nlelchi  32663  divnumden2  33407  fprodeq02  33415  gsumind  33906  constrrtcc  34367  constrsslem  34373  constraddcl  34394  constrmulcl  34403  cos9thpiminplylem1  34414  cos9thpiminplylem3  34416  cos9thpinconstrlem1  34421  ballotlemic  35139  ballotlem1c  35140  signsvfn  35211  circlemeth  35269  elmrsubrn  36285  climlec3  36499  bj-bary1lem  38231  tan2h  38535  ftc1anclem5  38615  ftc1anclem6  38616  ftc1anclem7  38617  ftc1anclem8  38618  ftc1anc  38619  lcmineqlem7  43085  lcmineqlem12  43090  aks4d1p1p7  43124  aks6d1c2p2  43169  aks6d1c5lem1  43186  aks6d1c5lem2  43188  sticksstones10  43205  sticksstones12a  43207  sn-addlid  43455  remul02  43456  remul01  43458  sn-it0e0  43467  sn-addrid  43472  sn-addid0  43476  sn-mul01  43477  sn-0tie0  43515  sn-mul02  43516  3cubeslem1  43694  pell14qrgt0  43865  expgrowth  45318  binomcxplemnotnn0  45339  ellimcabssub0  46628  0ellimcdiv  46658  clim0cf  46663  cosknegpi  46878  fprodsubrecnncnvlem  46916  fprodaddrecnncnvlem  46918  dvsinax  46922  dvasinbx  46929  dvnmptconst  46950  dvnxpaek  46951  itgiccshift  46989  itgperiod  46990  itgsbtaddcnst  46991  stirlinglem7  47089  dirkertrigeqlem2  47108  fourierdlem59  47174  fourierdlem62  47177  fourierdlem74  47189  fourierdlem75  47190  sqwvfoura  47237  fouriersw  47240  etransclem20  47263  etransclem21  47264  etransclem22  47265  etransclem25  47268  etransclem35  47278  sge0z  47384  ovnhoilem1  47610  vonsn  47700  sqrtnnaa  47912  sqrtnzqaa  47913  lambert0  47936  0nodd  49266  fdivmptf  49652  nn0sumshdiglem2  49733  eenglngeehlnmlem2  49849  itsclc0yqsollem1  49873