Theorem 0cnd 11128

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

Syntax hints:   → wi 4   ∈ wcel 2119  ℂcc 11027  0cc0 11029

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-mulcl 11091  ax-i2m1 11097

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-clel 2814

This theorem is referenced by:  addeq0  11564  mul0or  11781  eqneg  11866  un0addcl  12461  un0mulcl  12462  modsumfzodifsn  13897  muldivbinom2  14216  reusq0  15418  clim0c  15460  rlim0  15461  rlim0lt  15462  rlimneg  15600  isercolllem3  15620  sumrblem  15664  summolem2a  15668  sumz  15675  fsumcl  15686  expcnv  15820  ntrivcvgfvn0  15855  ef4p  16071  sadadd2lem2  16410  sadadd2lem  16419  modprm0  16767  iserodd  16797  prmrec  16884  4sqlem10  16909  4sqlem11  16917  frgpnabllem1  19839  evlsvvval  22069  fsumcn  24855  cnheibor  24940  evth2  24945  rrxmval  25390  mbfmulc2lem  25632  mbfpos  25636  dvcnp2  25905  dvcmulf  25930  dvmptc  25943  dvmptcmul  25949  dvmptfsum  25960  dveflem  25964  dvef  25965  rolle  25975  elply2  26179  plyf  26181  elplyr  26184  elplyd  26185  ply1term  26187  ply0  26191  plyeq0  26194  plyaddlem  26198  plymullem  26199  dgrlem  26212  coeidlem  26220  plyco  26224  coeeq2  26225  coe0  26239  plycj  26260  coecj  26261  plycjOLD  26262  coecjOLD  26263  plymul0or  26265  dvply1  26268  fta1lem  26291  elqaalem3  26305  tayl0  26345  dvtaylp  26353  taylthlem2  26357  radcnv0  26399  pserdvlem2  26411  pserdv  26412  ptolemy  26478  advlog  26636  advlogexp  26637  efopnlem2  26639  efopn  26640  logtayllem  26641  logtayl  26642  loglesqrt  26743  affineequiv  26805  quad2  26821  dcubic  26828  asinlem  26850  dvatan  26917  leibpilem2  26923  leibpi  26924  rlimcnp  26947  efrlim  26951  emcllem7  26983  dmgmaddn0  27004  lgamgulmlem2  27011  igamf  27032  igamcl  27033  sqff1o  27163  dchrelbasd  27220  dchrsum2  27249  sumdchr2  27251  addsq2reu  27421  addsqnreup  27424  dchrvmasumiflem2  27483  occllem  31392  nlelchi  32150  divnumden2  32908  fprodeq02  32916  gsumind  33428  constrrtcc  33919  constrsslem  33925  constraddcl  33946  constrmulcl  33955  cos9thpiminplylem1  33966  cos9thpiminplylem3  33968  cos9thpinconstrlem1  33973  ballotlemic  34691  ballotlem1c  34692  signsvfn  34766  circlemeth  34824  elmrsubrn  35748  climlec3  35962  bj-bary1lem  37670  tan2h  37979  ftc1anclem5  38064  ftc1anclem6  38065  ftc1anclem7  38066  ftc1anclem8  38067  ftc1anc  38068  lcmineqlem7  42520  lcmineqlem12  42525  aks4d1p1p7  42559  aks6d1c2p2  42604  aks6d1c5lem1  42621  aks6d1c5lem2  42623  sticksstones10  42640  sticksstones12a  42642  sn-addlid  42881  remul02  42882  remul01  42884  sn-it0e0  42893  sn-addrid  42898  sn-addid0  42902  sn-mul01  42903  sn-0tie0  42941  sn-mul02  42942  3cubeslem1  43133  pell14qrgt0  43304  expgrowth  44779  binomcxplemnotnn0  44800  ellimcabssub0  46062  0ellimcdiv  46092  clim0cf  46097  cosknegpi  46312  fprodsubrecnncnvlem  46350  fprodaddrecnncnvlem  46352  dvsinax  46356  dvasinbx  46363  dvnmptconst  46384  dvnxpaek  46385  itgiccshift  46423  itgperiod  46424  itgsbtaddcnst  46425  stirlinglem7  46523  dirkertrigeqlem2  46542  fourierdlem59  46608  fourierdlem62  46611  fourierdlem74  46623  fourierdlem75  46624  sqwvfoura  46671  fouriersw  46674  etransclem20  46697  etransclem21  46698  etransclem22  46699  etransclem25  46702  etransclem35  46712  sge0z  46818  ovnhoilem1  47044  vonsn  47134  lambert0  47350  0nodd  48661  fdivmptf  49032  nn0sumshdiglem2  49113  eenglngeehlnmlem2  49229  itsclc0yqsollem1  49253