Theorem 0cnd 11251

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

Syntax hints:   → wi 4   ∈ wcel 2105  ℂcc 11150  0cc0 11152

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-mulcl 11214  ax-i2m1 11220

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

This theorem is referenced by:  addeq0  11683  mul0or  11900  eqneg  11984  un0addcl  12556  un0mulcl  12557  modsumfzodifsn  13981  muldivbinom2  14298  reusq0  15497  clim0c  15539  rlim0  15540  rlim0lt  15541  rlimneg  15679  isercolllem3  15699  sumrblem  15743  summolem2a  15747  sumz  15754  fsumcl  15765  expcnv  15896  ntrivcvgfvn0  15931  ef4p  16145  sadadd2lem2  16483  sadadd2lem  16492  modprm0  16838  iserodd  16868  prmrec  16955  4sqlem10  16980  4sqlem11  16988  frgpnabllem1  19905  fsumcn  24907  cnheibor  25000  evth2  25005  rrxmval  25452  mbfmulc2lem  25695  mbfpos  25699  dvcnp2  25969  dvcmulf  25996  dvmptc  26010  dvmptcmul  26016  dvmptfsum  26027  dveflem  26031  dvef  26032  rolle  26042  elply2  26249  plyf  26251  elplyr  26254  elplyd  26255  ply1term  26257  ply0  26261  plyeq0  26264  plyaddlem  26268  plymullem  26269  dgrlem  26282  coeidlem  26290  plyco  26294  coeeq2  26295  coe0  26309  plycj  26331  coecj  26332  plycjOLD  26333  coecjOLD  26334  plymul0or  26336  dvply1  26339  fta1lem  26363  elqaalem3  26377  tayl0  26417  dvtaylp  26426  taylthlem2  26430  taylthlem2OLD  26431  radcnv0  26473  pserdvlem2  26486  pserdv  26487  ptolemy  26552  advlog  26710  advlogexp  26711  efopnlem2  26713  efopn  26714  logtayllem  26715  logtayl  26716  loglesqrt  26818  affineequiv  26880  quad2  26896  dcubic  26903  asinlem  26925  dvatan  26992  leibpilem2  26998  leibpi  26999  rlimcnp  27022  efrlim  27026  efrlimOLD  27027  emcllem7  27059  dmgmaddn0  27080  lgamgulmlem2  27087  igamf  27108  igamcl  27109  sqff1o  27239  dchrelbasd  27297  dchrsum2  27326  sumdchr2  27328  addsq2reu  27498  addsqnreup  27501  dchrvmasumiflem2  27560  occllem  31331  nlelchi  32089  divnumden2  32821  fprodeq02  32829  constrrtcc  33740  constrsslem  33745  ballotlemic  34487  ballotlem1c  34488  signsvfn  34575  circlemeth  34633  elmrsubrn  35504  climlec3  35713  bj-bary1lem  37292  tan2h  37598  ftc1anclem5  37683  ftc1anclem6  37684  ftc1anclem7  37685  ftc1anclem8  37686  ftc1anc  37687  lcmineqlem7  42016  lcmineqlem12  42021  aks4d1p1p7  42055  aks6d1c2p2  42100  aks6d1c5lem1  42117  aks6d1c5lem2  42119  sticksstones10  42136  sticksstones12a  42138  sn-addlid  42410  remul02  42411  remul01  42413  sn-it0e0  42421  sn-addrid  42426  sn-addid0  42430  sn-mul01  42431  sn-0tie0  42445  sn-mul02  42446  evlsvvval  42549  3cubeslem1  42671  pell14qrgt0  42846  expgrowth  44330  binomcxplemnotnn0  44351  ellimcabssub0  45572  0ellimcdiv  45604  clim0cf  45609  cosknegpi  45824  fprodsubrecnncnvlem  45862  fprodaddrecnncnvlem  45864  dvsinax  45868  dvasinbx  45875  dvnmptconst  45896  dvnxpaek  45897  itgiccshift  45935  itgperiod  45936  itgsbtaddcnst  45937  stirlinglem7  46035  dirkertrigeqlem2  46054  fourierdlem59  46120  fourierdlem62  46123  fourierdlem74  46135  fourierdlem75  46136  sqwvfoura  46183  fouriersw  46186  etransclem20  46209  etransclem21  46210  etransclem22  46211  etransclem25  46214  etransclem35  46224  sge0z  46330  ovnhoilem1  46556  vonsn  46646  0nodd  48013  fdivmptf  48390  nn0sumshdiglem2  48471  eenglngeehlnmlem2  48587  itsclc0yqsollem1  48611