Theorem 0cnd 8064

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

Syntax hints:   → wi 4   ∈ wcel 2175  ℂcc 7922  0cc0 7924

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532  ax-17 1548  ax-ial 1556  ax-ext 2186  ax-1cn 8017  ax-icn 8019  ax-addcl 8020  ax-mulcl 8022  ax-i2m1 8029

This theorem depends on definitions:  df-bi 117  df-cleq 2197  df-clel 2200

This theorem is referenced by:  mulap0r  8687  mulap0  8726  mul0eqap  8742  diveqap0  8754  eqneg  8804  div2subap  8909  prodgt0  8924  un0addcl  9327  un0mulcl  9328  modsumfzodifsn  10539  ser0  10676  ser0f  10677  abs00ap  11344  abs00  11346  abssubne0  11373  mul0inf  11523  clim0c  11568  sumrbdclem  11659  summodclem2a  11663  zsumdc  11666  fsum3  11669  isumz  11671  isumss  11673  fisumss  11674  fsum3cvg2  11676  fsum3ser  11679  fsumcl2lem  11680  fsumcl  11682  fsumadd  11688  fsumsplit  11689  sumsnf  11691  sumsplitdc  11714  fsummulc2  11730  ef0lem  11942  ef4p  11976  tanvalap  11990  modprm0  12548  pcmpt2  12638  4sqlem10  12681  4sqlem11  12695  fsumcncntop  15010  limcimolemlt  15107  dvmptcmulcn  15164  dvmptfsum  15168  dveflem  15169  dvef  15170  plyf  15180  elplyr  15183  elplyd  15184  ply1term  15186  plyaddlem  15192  plymullem  15193  plycolemc  15201  plycn  15205  dvply1  15208  ptolemy  15267  lgsdir2  15481  lgsdir  15483  apdiff  15949  iswomni0  15952