Theorem 0cnd 10634

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 10535  0cc0 10537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-mulcl 10599  ax-i2m1 10605

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814  df-clel 2893

This theorem is referenced by:  addeq0  11063  mul0or  11280  diveq0  11308  eqneg  11360  un0addcl  11931  un0mulcl  11932  modsumfzodifsn  13313  muldivbinom2  13624  reusq0  14822  clim0c  14864  rlim0  14865  rlim0lt  14866  rlimneg  15003  isercolllem3  15023  sumrblem  15068  summolem2a  15072  sumz  15079  fsumcl  15090  expcnv  15219  ntrivcvgfvn0  15255  ef4p  15466  sadadd2lem2  15799  sadadd2lem  15808  modprm0  16142  iserodd  16172  prmrec  16258  4sqlem10  16283  4sqlem11  16291  frgpnabllem1  18993  fsumcn  23478  cnheibor  23559  evth2  23564  rrxmval  24008  mbfmulc2lem  24248  mbfpos  24252  dvcmulf  24542  dvmptc  24555  dvmptcmul  24561  dvmptfsum  24572  dveflem  24576  dvef  24577  rolle  24587  elply2  24786  plyf  24788  elplyr  24791  elplyd  24792  ply1term  24794  ply0  24798  plyeq0  24801  plyaddlem  24805  plymullem  24806  dgrlem  24819  coeidlem  24827  plyco  24831  coeeq2  24832  coe0  24846  plycj  24867  coecj  24868  plymul0or  24870  dvply1  24873  fta1lem  24896  elqaalem3  24910  tayl0  24950  dvtaylp  24958  taylthlem2  24962  radcnv0  25004  pserdvlem2  25016  pserdv  25017  ptolemy  25082  advlog  25237  advlogexp  25238  efopnlem2  25240  efopn  25241  logtayllem  25242  logtayl  25243  loglesqrt  25339  affineequiv  25401  quad2  25417  dcubic  25424  asinlem  25446  dvatan  25513  leibpilem2  25519  leibpi  25520  rlimcnp  25543  efrlim  25547  emcllem7  25579  dmgmaddn0  25600  lgamgulmlem2  25607  igamf  25628  igamcl  25629  sqff1o  25759  dchrelbasd  25815  dchrsum2  25844  sumdchr2  25846  addsq2reu  26016  addsqnreup  26019  dchrvmasumiflem2  26078  occllem  29080  nlelchi  29838  divnumden2  30534  fprodeq02  30539  ballotlemic  31764  ballotlem1c  31765  signsvfn  31852  circlemeth  31911  elmrsubrn  32767  climlec3  32965  bj-bary1lem  34594  tan2h  34899  ftc1anclem5  34986  ftc1anclem6  34987  ftc1anclem7  34988  ftc1anclem8  34989  ftc1anc  34990  sn-addid2  39254  remul02  39255  remul01  39257  3cubeslem1  39301  pell14qrgt0  39476  expgrowth  40687  binomcxplemnotnn0  40708  ellimcabssub0  41918  0ellimcdiv  41950  clim0cf  41955  cosknegpi  42170  fprodsubrecnncnvlem  42211  fprodaddrecnncnvlem  42213  dvsinax  42217  dvasinbx  42225  dvnmptconst  42246  dvnxpaek  42247  itgiccshift  42285  itgperiod  42286  itgsbtaddcnst  42287  stirlinglem7  42385  dirkertrigeqlem2  42404  fourierdlem59  42470  fourierdlem62  42473  fourierdlem74  42485  fourierdlem75  42486  sqwvfoura  42533  fouriersw  42536  etransclem20  42559  etransclem21  42560  etransclem22  42561  etransclem25  42564  etransclem35  42574  sge0z  42677  ovnhoilem1  42903  vonsn  42993  0nodd  44097  fdivmptf  44621  nn0sumshdiglem2  44702  eenglngeehlnmlem2  44745  itsclc0yqsollem1  44769