Theorem 0cnd 10623

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

Syntax hints:   → wi 4   ∈ wcel 2111  ℂcc 10524  0cc0 10526

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-mulcl 10588  ax-i2m1 10594

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870

This theorem is referenced by:  addeq0  11052  mul0or  11269  diveq0  11297  eqneg  11349  un0addcl  11918  un0mulcl  11919  modsumfzodifsn  13307  muldivbinom2  13619  reusq0  14814  clim0c  14856  rlim0  14857  rlim0lt  14858  rlimneg  14995  isercolllem3  15015  sumrblem  15060  summolem2a  15064  sumz  15071  fsumcl  15082  expcnv  15211  ntrivcvgfvn0  15247  ef4p  15458  sadadd2lem2  15789  sadadd2lem  15798  modprm0  16132  iserodd  16162  prmrec  16248  4sqlem10  16273  4sqlem11  16281  frgpnabllem1  18986  fsumcn  23475  cnheibor  23560  evth2  23565  rrxmval  24009  mbfmulc2lem  24251  mbfpos  24255  dvcmulf  24548  dvmptc  24561  dvmptcmul  24567  dvmptfsum  24578  dveflem  24582  dvef  24583  rolle  24593  elply2  24793  plyf  24795  elplyr  24798  elplyd  24799  ply1term  24801  ply0  24805  plyeq0  24808  plyaddlem  24812  plymullem  24813  dgrlem  24826  coeidlem  24834  plyco  24838  coeeq2  24839  coe0  24853  plycj  24874  coecj  24875  plymul0or  24877  dvply1  24880  fta1lem  24903  elqaalem3  24917  tayl0  24957  dvtaylp  24965  taylthlem2  24969  radcnv0  25011  pserdvlem2  25023  pserdv  25024  ptolemy  25089  advlog  25245  advlogexp  25246  efopnlem2  25248  efopn  25249  logtayllem  25250  logtayl  25251  loglesqrt  25347  affineequiv  25409  quad2  25425  dcubic  25432  asinlem  25454  dvatan  25521  leibpilem2  25527  leibpi  25528  rlimcnp  25551  efrlim  25555  emcllem7  25587  dmgmaddn0  25608  lgamgulmlem2  25615  igamf  25636  igamcl  25637  sqff1o  25767  dchrelbasd  25823  dchrsum2  25852  sumdchr2  25854  addsq2reu  26024  addsqnreup  26027  dchrvmasumiflem2  26086  occllem  29086  nlelchi  29844  divnumden2  30560  fprodeq02  30565  ballotlemic  31874  ballotlem1c  31875  signsvfn  31962  circlemeth  32021  elmrsubrn  32880  climlec3  33078  bj-bary1lem  34724  tan2h  35049  ftc1anclem5  35134  ftc1anclem6  35135  ftc1anclem7  35136  ftc1anclem8  35137  ftc1anc  35138  lcmineqlem7  39323  lcmineqlem12  39328  sn-addid2  39542  remul02  39543  remul01  39545  sn-it0e0  39552  sn-addid1  39557  sn-addid0  39561  sn-mul01  39562  sn-0tie0  39576  sn-mul02  39577  3cubeslem1  39625  pell14qrgt0  39800  expgrowth  41039  binomcxplemnotnn0  41060  ellimcabssub0  42259  0ellimcdiv  42291  clim0cf  42296  cosknegpi  42511  fprodsubrecnncnvlem  42549  fprodaddrecnncnvlem  42551  dvsinax  42555  dvasinbx  42562  dvnmptconst  42583  dvnxpaek  42584  itgiccshift  42622  itgperiod  42623  itgsbtaddcnst  42624  stirlinglem7  42722  dirkertrigeqlem2  42741  fourierdlem59  42807  fourierdlem62  42810  fourierdlem74  42822  fourierdlem75  42823  sqwvfoura  42870  fouriersw  42873  etransclem20  42896  etransclem21  42897  etransclem22  42898  etransclem25  42901  etransclem35  42911  sge0z  43014  ovnhoilem1  43240  vonsn  43330  0nodd  44430  fdivmptf  44955  nn0sumshdiglem2  45036  eenglngeehlnmlem2  45152  itsclc0yqsollem1  45176