Theorem 0cnd 11123

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℂcc 11022  0cc0 11024

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-1cn 11082  ax-icn 11083  ax-addcl 11084  ax-mulcl 11086  ax-i2m1 11092

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2726  df-clel 2809

This theorem is referenced by:  addeq0  11558  mul0or  11775  eqneg  11859  un0addcl  12432  un0mulcl  12433  modsumfzodifsn  13865  muldivbinom2  14184  reusq0  15386  clim0c  15428  rlim0  15429  rlim0lt  15430  rlimneg  15568  isercolllem3  15588  sumrblem  15632  summolem2a  15636  sumz  15643  fsumcl  15654  expcnv  15785  ntrivcvgfvn0  15820  ef4p  16036  sadadd2lem2  16375  sadadd2lem  16384  modprm0  16731  iserodd  16761  prmrec  16848  4sqlem10  16873  4sqlem11  16881  frgpnabllem1  19800  evlsvvval  22046  fsumcn  24815  cnheibor  24908  evth2  24913  rrxmval  25359  mbfmulc2lem  25602  mbfpos  25606  dvcnp2  25875  dvcmulf  25902  dvmptc  25916  dvmptcmul  25922  dvmptfsum  25933  dveflem  25937  dvef  25938  rolle  25948  elply2  26155  plyf  26157  elplyr  26160  elplyd  26161  ply1term  26163  ply0  26167  plyeq0  26170  plyaddlem  26174  plymullem  26175  dgrlem  26188  coeidlem  26196  plyco  26200  coeeq2  26201  coe0  26215  plycj  26237  coecj  26238  plycjOLD  26239  coecjOLD  26240  plymul0or  26242  dvply1  26245  fta1lem  26269  elqaalem3  26283  tayl0  26323  dvtaylp  26332  taylthlem2  26336  taylthlem2OLD  26337  radcnv0  26379  pserdvlem2  26392  pserdv  26393  ptolemy  26459  advlog  26617  advlogexp  26618  efopnlem2  26620  efopn  26621  logtayllem  26622  logtayl  26623  loglesqrt  26725  affineequiv  26787  quad2  26803  dcubic  26810  asinlem  26832  dvatan  26899  leibpilem2  26905  leibpi  26906  rlimcnp  26929  efrlim  26933  efrlimOLD  26934  emcllem7  26966  dmgmaddn0  26987  lgamgulmlem2  26994  igamf  27015  igamcl  27016  sqff1o  27146  dchrelbasd  27204  dchrsum2  27233  sumdchr2  27235  addsq2reu  27405  addsqnreup  27408  dchrvmasumiflem2  27467  occllem  31327  nlelchi  32085  divnumden2  32845  fprodeq02  32853  gsumind  33375  constrrtcc  33841  constrsslem  33847  constraddcl  33868  constrmulcl  33877  cos9thpiminplylem1  33888  cos9thpiminplylem3  33890  cos9thpinconstrlem1  33895  ballotlemic  34613  ballotlem1c  34614  signsvfn  34688  circlemeth  34746  elmrsubrn  35663  climlec3  35877  bj-bary1lem  37454  tan2h  37752  ftc1anclem5  37837  ftc1anclem6  37838  ftc1anclem7  37839  ftc1anclem8  37840  ftc1anc  37841  lcmineqlem7  42228  lcmineqlem12  42233  aks4d1p1p7  42267  aks6d1c2p2  42312  aks6d1c5lem1  42329  aks6d1c5lem2  42331  sticksstones10  42348  sticksstones12a  42350  sn-addlid  42601  remul02  42602  remul01  42604  sn-it0e0  42613  sn-addrid  42618  sn-addid0  42622  sn-mul01  42623  sn-0tie0  42648  sn-mul02  42649  3cubeslem1  42868  pell14qrgt0  43043  expgrowth  44518  binomcxplemnotnn0  44539  ellimcabssub0  45805  0ellimcdiv  45835  clim0cf  45840  cosknegpi  46055  fprodsubrecnncnvlem  46093  fprodaddrecnncnvlem  46095  dvsinax  46099  dvasinbx  46106  dvnmptconst  46127  dvnxpaek  46128  itgiccshift  46166  itgperiod  46167  itgsbtaddcnst  46168  stirlinglem7  46266  dirkertrigeqlem2  46285  fourierdlem59  46351  fourierdlem62  46354  fourierdlem74  46366  fourierdlem75  46367  sqwvfoura  46414  fouriersw  46417  etransclem20  46440  etransclem21  46441  etransclem22  46442  etransclem25  46445  etransclem35  46455  sge0z  46561  ovnhoilem1  46787  vonsn  46877  lambert0  47075  0nodd  48358  fdivmptf  48729  nn0sumshdiglem2  48810  eenglngeehlnmlem2  48926  itsclc0yqsollem1  48950