Theorem 0cnd 9912

Description: 0 is a complex number, deductive form. (Contributed by David A. Wheeler, 8-Dec-2018.)

Assertion

Ref	Expression
0cnd	⊢ (𝜑 → 0 ∈ ℂ)

Proof of Theorem 0cnd

Step	Hyp	Ref	Expression
1		0cn 9911	. 2 ⊢ 0 ∈ ℂ
2	1	a1i 11	1 ⊢ (𝜑 → 0 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 1977  ℂcc 9813  0cc0 9815

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-ext 2590  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-mulcl 9877  ax-i2m1 9883

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-cleq 2603  df-clel 2606

This theorem is referenced by:  mul0or  10546  diveq0  10574  eqneg  10624  un0addcl  11203  un0mulcl  11204  modsumfzodifsn  12605  muldivbinom2  12909  repswcshw  13409  clim0c  14086  rlim0  14087  rlim0lt  14088  rlimneg  14225  isercolllem3  14245  sumrblem  14289  summolem2a  14293  sumz  14300  fsumcl  14311  expcnv  14435  ntrivcvgfvn0  14470  ef4p  14682  sadadd2lem2  15010  sadadd2lem  15019  modprm0  15348  iserodd  15378  prmrec  15464  4sqlem10  15489  4sqlem11  15497  frgpnabllem1  18099  fsumcn  22481  cnheibor  22562  evth2  22567  rrxmval  22996  mbfmulc2lem  23220  mbfpos  23224  dvcmulf  23514  dvmptc  23527  dvmptcmul  23533  dvmptfsum  23542  dveflem  23546  rolle  23557  elply2  23756  plyf  23758  elplyr  23761  elplyd  23762  ply1term  23764  ply0  23768  plyeq0  23771  plyaddlem  23775  plymullem  23776  dgrlem  23789  coeidlem  23797  plyco  23801  coeeq2  23802  coe0  23816  plycj  23837  coecj  23838  plymul0or  23840  dvply1  23843  fta1lem  23866  elqaalem3  23880  tayl0  23920  dvtaylp  23928  taylthlem2  23932  radcnv0  23974  pserdvlem2  23986  pserdv  23987  ptolemy  24052  advlog  24200  advlogexp  24201  efopnlem2  24203  efopn  24204  logtayllem  24205  logtayl  24206  loglesqrt  24299  affineequiv  24353  quad2  24366  dcubic  24373  asinlem  24395  dvatan  24462  leibpilem2  24468  leibpi  24469  rlimcnp  24492  efrlim  24496  emcllem7  24528  dmgmaddn0  24549  lgamgulmlem2  24556  igamf  24577  igamcl  24578  sqff1o  24708  dchrelbasd  24764  dchrsum2  24793  sumdchr2  24795  dchrvmasumiflem2  24991  occllem  27546  nlelchi  28304  addeq0  28898  divnumden2  28951  ballotlemic  29895  ballotlem1c  29896  signsvfn  29985  elmrsubrn  30671  climlec3  30872  bj-bary1lem  32337  tan2h  32571  ftc1anclem5  32659  ftc1anclem6  32660  ftc1anclem7  32661  ftc1anclem8  32662  ftc1anc  32663  pell14qrgt0  36441  expgrowth  37556  binomcxplemnotnn0  37577  ellimcabssub0  38684  0ellimcdiv  38716  clim0cf  38721  cosknegpi  38752  fprodsubrecnncnvlem  38794  fprodaddrecnncnvlem  38796  dvsinax  38801  dvasinbx  38810  dvnmptconst  38831  dvnxpaek  38832  itgiccshift  38872  itgperiod  38873  itgsbtaddcnst  38874  stirlinglem7  38973  dirkertrigeqlem2  38992  fourierdlem59  39058  fourierdlem62  39061  fourierdlem74  39073  fourierdlem75  39074  sqwvfoura  39121  fouriersw  39124  etransclem20  39147  etransclem21  39148  etransclem22  39149  etransclem25  39152  etransclem35  39162  sge0z  39268  ovnhoilem1  39491  vonsn  39582  0nodd  41600  fdivmptf  42133  nn0sumshdiglem2  42214