Theorem 0cnd 11143

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 11042  0cc0 11044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-mulcl 11106  ax-i2m1 11112

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803

This theorem is referenced by:  addeq0  11577  mul0or  11794  eqneg  11878  un0addcl  12451  un0mulcl  12452  modsumfzodifsn  13885  muldivbinom2  14204  reusq0  15407  clim0c  15449  rlim0  15450  rlim0lt  15451  rlimneg  15589  isercolllem3  15609  sumrblem  15653  summolem2a  15657  sumz  15664  fsumcl  15675  expcnv  15806  ntrivcvgfvn0  15841  ef4p  16057  sadadd2lem2  16396  sadadd2lem  16405  modprm0  16752  iserodd  16782  prmrec  16869  4sqlem10  16894  4sqlem11  16902  frgpnabllem1  19787  fsumcn  24794  cnheibor  24887  evth2  24892  rrxmval  25338  mbfmulc2lem  25581  mbfpos  25585  dvcnp2  25854  dvcmulf  25881  dvmptc  25895  dvmptcmul  25901  dvmptfsum  25912  dveflem  25916  dvef  25917  rolle  25927  elply2  26134  plyf  26136  elplyr  26139  elplyd  26140  ply1term  26142  ply0  26146  plyeq0  26149  plyaddlem  26153  plymullem  26154  dgrlem  26167  coeidlem  26175  plyco  26179  coeeq2  26180  coe0  26194  plycj  26216  coecj  26217  plycjOLD  26218  coecjOLD  26219  plymul0or  26221  dvply1  26224  fta1lem  26248  elqaalem3  26262  tayl0  26302  dvtaylp  26311  taylthlem2  26315  taylthlem2OLD  26316  radcnv0  26358  pserdvlem2  26371  pserdv  26372  ptolemy  26438  advlog  26596  advlogexp  26597  efopnlem2  26599  efopn  26600  logtayllem  26601  logtayl  26602  loglesqrt  26704  affineequiv  26766  quad2  26782  dcubic  26789  asinlem  26811  dvatan  26878  leibpilem2  26884  leibpi  26885  rlimcnp  26908  efrlim  26912  efrlimOLD  26913  emcllem7  26945  dmgmaddn0  26966  lgamgulmlem2  26973  igamf  26994  igamcl  26995  sqff1o  27125  dchrelbasd  27183  dchrsum2  27212  sumdchr2  27214  addsq2reu  27384  addsqnreup  27387  dchrvmasumiflem2  27446  occllem  31282  nlelchi  32040  divnumden2  32790  fprodeq02  32798  constrrtcc  33718  constrsslem  33724  constraddcl  33745  constrmulcl  33754  cos9thpiminplylem1  33765  cos9thpiminplylem3  33767  cos9thpinconstrlem1  33772  ballotlemic  34491  ballotlem1c  34492  signsvfn  34566  circlemeth  34624  elmrsubrn  35500  climlec3  35714  bj-bary1lem  37291  tan2h  37599  ftc1anclem5  37684  ftc1anclem6  37685  ftc1anclem7  37686  ftc1anclem8  37687  ftc1anc  37688  lcmineqlem7  42016  lcmineqlem12  42021  aks4d1p1p7  42055  aks6d1c2p2  42100  aks6d1c5lem1  42117  aks6d1c5lem2  42119  sticksstones10  42136  sticksstones12a  42138  sn-addlid  42385  remul02  42386  remul01  42388  sn-it0e0  42397  sn-addrid  42402  sn-addid0  42406  sn-mul01  42407  sn-0tie0  42432  sn-mul02  42433  evlsvvval  42544  3cubeslem1  42665  pell14qrgt0  42840  expgrowth  44317  binomcxplemnotnn0  44338  ellimcabssub0  45608  0ellimcdiv  45640  clim0cf  45645  cosknegpi  45860  fprodsubrecnncnvlem  45898  fprodaddrecnncnvlem  45900  dvsinax  45904  dvasinbx  45911  dvnmptconst  45932  dvnxpaek  45933  itgiccshift  45971  itgperiod  45972  itgsbtaddcnst  45973  stirlinglem7  46071  dirkertrigeqlem2  46090  fourierdlem59  46156  fourierdlem62  46159  fourierdlem74  46171  fourierdlem75  46172  sqwvfoura  46219  fouriersw  46222  etransclem20  46245  etransclem21  46246  etransclem22  46247  etransclem25  46250  etransclem35  46260  sge0z  46366  ovnhoilem1  46592  vonsn  46682  lambert0  46881  0nodd  48151  fdivmptf  48523  nn0sumshdiglem2  48604  eenglngeehlnmlem2  48720  itsclc0yqsollem1  48744