Theorem 0cnd 11137

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 11036  0cc0 11038

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-mulcl 11100  ax-i2m1 11106

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812

This theorem is referenced by:  addeq0  11572  mul0or  11789  eqneg  11873  un0addcl  12446  un0mulcl  12447  modsumfzodifsn  13879  muldivbinom2  14198  reusq0  15400  clim0c  15442  rlim0  15443  rlim0lt  15444  rlimneg  15582  isercolllem3  15602  sumrblem  15646  summolem2a  15650  sumz  15657  fsumcl  15668  expcnv  15799  ntrivcvgfvn0  15834  ef4p  16050  sadadd2lem2  16389  sadadd2lem  16398  modprm0  16745  iserodd  16775  prmrec  16862  4sqlem10  16887  4sqlem11  16895  frgpnabllem1  19817  evlsvvval  22063  fsumcn  24832  cnheibor  24925  evth2  24930  rrxmval  25376  mbfmulc2lem  25619  mbfpos  25623  dvcnp2  25892  dvcmulf  25919  dvmptc  25933  dvmptcmul  25939  dvmptfsum  25950  dveflem  25954  dvef  25955  rolle  25965  elply2  26172  plyf  26174  elplyr  26177  elplyd  26178  ply1term  26180  ply0  26184  plyeq0  26187  plyaddlem  26191  plymullem  26192  dgrlem  26205  coeidlem  26213  plyco  26217  coeeq2  26218  coe0  26232  plycj  26254  coecj  26255  plycjOLD  26256  coecjOLD  26257  plymul0or  26259  dvply1  26262  fta1lem  26286  elqaalem3  26300  tayl0  26340  dvtaylp  26349  taylthlem2  26353  taylthlem2OLD  26354  radcnv0  26396  pserdvlem2  26409  pserdv  26410  ptolemy  26476  advlog  26634  advlogexp  26635  efopnlem2  26637  efopn  26638  logtayllem  26639  logtayl  26640  loglesqrt  26742  affineequiv  26804  quad2  26820  dcubic  26827  asinlem  26849  dvatan  26916  leibpilem2  26922  leibpi  26923  rlimcnp  26946  efrlim  26950  efrlimOLD  26951  emcllem7  26983  dmgmaddn0  27004  lgamgulmlem2  27011  igamf  27032  igamcl  27033  sqff1o  27163  dchrelbasd  27221  dchrsum2  27250  sumdchr2  27252  addsq2reu  27422  addsqnreup  27425  dchrvmasumiflem2  27484  occllem  31395  nlelchi  32153  divnumden2  32911  fprodeq02  32919  gsumind  33442  constrrtcc  33917  constrsslem  33923  constraddcl  33944  constrmulcl  33953  cos9thpiminplylem1  33964  cos9thpiminplylem3  33966  cos9thpinconstrlem1  33971  ballotlemic  34689  ballotlem1c  34690  signsvfn  34764  circlemeth  34822  elmrsubrn  35740  climlec3  35954  bj-bary1lem  37569  tan2h  37867  ftc1anclem5  37952  ftc1anclem6  37953  ftc1anclem7  37954  ftc1anclem8  37955  ftc1anc  37956  lcmineqlem7  42409  lcmineqlem12  42414  aks4d1p1p7  42448  aks6d1c2p2  42493  aks6d1c5lem1  42510  aks6d1c5lem2  42512  sticksstones10  42529  sticksstones12a  42531  sn-addlid  42778  remul02  42779  remul01  42781  sn-it0e0  42790  sn-addrid  42795  sn-addid0  42799  sn-mul01  42800  sn-0tie0  42825  sn-mul02  42826  3cubeslem1  43045  pell14qrgt0  43220  expgrowth  44695  binomcxplemnotnn0  44716  ellimcabssub0  45981  0ellimcdiv  46011  clim0cf  46016  cosknegpi  46231  fprodsubrecnncnvlem  46269  fprodaddrecnncnvlem  46271  dvsinax  46275  dvasinbx  46282  dvnmptconst  46303  dvnxpaek  46304  itgiccshift  46342  itgperiod  46343  itgsbtaddcnst  46344  stirlinglem7  46442  dirkertrigeqlem2  46461  fourierdlem59  46527  fourierdlem62  46530  fourierdlem74  46542  fourierdlem75  46543  sqwvfoura  46590  fouriersw  46593  etransclem20  46616  etransclem21  46617  etransclem22  46618  etransclem25  46621  etransclem35  46631  sge0z  46737  ovnhoilem1  46963  vonsn  47053  lambert0  47251  0nodd  48534  fdivmptf  48905  nn0sumshdiglem2  48986  eenglngeehlnmlem2  49102  itsclc0yqsollem1  49126