Theorem 0cnd 11139

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

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

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 11098  ax-icn 11099  ax-addcl 11100  ax-mulcl 11102  ax-i2m1 11108

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  11574  mul0or  11791  eqneg  11875  un0addcl  12448  un0mulcl  12449  modsumfzodifsn  13881  muldivbinom2  14200  reusq0  15402  clim0c  15444  rlim0  15445  rlim0lt  15446  rlimneg  15584  isercolllem3  15604  sumrblem  15648  summolem2a  15652  sumz  15659  fsumcl  15670  expcnv  15801  ntrivcvgfvn0  15836  ef4p  16052  sadadd2lem2  16391  sadadd2lem  16400  modprm0  16747  iserodd  16777  prmrec  16864  4sqlem10  16889  4sqlem11  16897  frgpnabllem1  19819  evlsvvval  22065  fsumcn  24834  cnheibor  24927  evth2  24932  rrxmval  25378  mbfmulc2lem  25621  mbfpos  25625  dvcnp2  25894  dvcmulf  25921  dvmptc  25935  dvmptcmul  25941  dvmptfsum  25952  dveflem  25956  dvef  25957  rolle  25967  elply2  26174  plyf  26176  elplyr  26179  elplyd  26180  ply1term  26182  ply0  26186  plyeq0  26189  plyaddlem  26193  plymullem  26194  dgrlem  26207  coeidlem  26215  plyco  26219  coeeq2  26220  coe0  26234  plycj  26256  coecj  26257  plycjOLD  26258  coecjOLD  26259  plymul0or  26261  dvply1  26264  fta1lem  26288  elqaalem3  26302  tayl0  26342  dvtaylp  26351  taylthlem2  26355  taylthlem2OLD  26356  radcnv0  26398  pserdvlem2  26411  pserdv  26412  ptolemy  26478  advlog  26636  advlogexp  26637  efopnlem2  26639  efopn  26640  logtayllem  26641  logtayl  26642  loglesqrt  26744  affineequiv  26806  quad2  26822  dcubic  26829  asinlem  26851  dvatan  26918  leibpilem2  26924  leibpi  26925  rlimcnp  26948  efrlim  26952  efrlimOLD  26953  emcllem7  26985  dmgmaddn0  27006  lgamgulmlem2  27013  igamf  27034  igamcl  27035  sqff1o  27165  dchrelbasd  27223  dchrsum2  27252  sumdchr2  27254  addsq2reu  27424  addsqnreup  27427  dchrvmasumiflem2  27486  occllem  31397  nlelchi  32155  divnumden2  32913  fprodeq02  32921  gsumind  33444  constrrtcc  33919  constrsslem  33925  constraddcl  33946  constrmulcl  33955  cos9thpiminplylem1  33966  cos9thpiminplylem3  33968  cos9thpinconstrlem1  33973  ballotlemic  34691  ballotlem1c  34692  signsvfn  34766  circlemeth  34824  elmrsubrn  35742  climlec3  35956  bj-bary1lem  37592  tan2h  37892  ftc1anclem5  37977  ftc1anclem6  37978  ftc1anclem7  37979  ftc1anclem8  37980  ftc1anc  37981  lcmineqlem7  42434  lcmineqlem12  42439  aks4d1p1p7  42473  aks6d1c2p2  42518  aks6d1c5lem1  42535  aks6d1c5lem2  42537  sticksstones10  42554  sticksstones12a  42556  sn-addlid  42803  remul02  42804  remul01  42806  sn-it0e0  42815  sn-addrid  42820  sn-addid0  42824  sn-mul01  42825  sn-0tie0  42850  sn-mul02  42851  3cubeslem1  43070  pell14qrgt0  43245  expgrowth  44720  binomcxplemnotnn0  44741  ellimcabssub0  46006  0ellimcdiv  46036  clim0cf  46041  cosknegpi  46256  fprodsubrecnncnvlem  46294  fprodaddrecnncnvlem  46296  dvsinax  46300  dvasinbx  46307  dvnmptconst  46328  dvnxpaek  46329  itgiccshift  46367  itgperiod  46368  itgsbtaddcnst  46369  stirlinglem7  46467  dirkertrigeqlem2  46486  fourierdlem59  46552  fourierdlem62  46555  fourierdlem74  46567  fourierdlem75  46568  sqwvfoura  46615  fouriersw  46618  etransclem20  46641  etransclem21  46642  etransclem22  46643  etransclem25  46646  etransclem35  46656  sge0z  46762  ovnhoilem1  46988  vonsn  47078  lambert0  47276  0nodd  48559  fdivmptf  48930  nn0sumshdiglem2  49011  eenglngeehlnmlem2  49127  itsclc0yqsollem1  49151