Theorem 0cnd 8012

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

Syntax hints:   → wi 4   ∈ wcel 2164  ℂcc 7870  0cc0 7872

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2175  ax-1cn 7965  ax-icn 7967  ax-addcl 7968  ax-mulcl 7970  ax-i2m1 7977

This theorem depends on definitions:  df-bi 117  df-cleq 2186  df-clel 2189

This theorem is referenced by:  mulap0r  8634  mulap0  8673  mul0eqap  8689  diveqap0  8701  eqneg  8751  div2subap  8856  prodgt0  8871  un0addcl  9273  un0mulcl  9274  modsumfzodifsn  10467  ser0  10604  ser0f  10605  abs00ap  11206  abs00  11208  abssubne0  11235  mul0inf  11384  clim0c  11429  sumrbdclem  11520  summodclem2a  11524  zsumdc  11527  fsum3  11530  isumz  11532  isumss  11534  fisumss  11535  fsum3cvg2  11537  fsum3ser  11540  fsumcl2lem  11541  fsumcl  11543  fsumadd  11549  fsumsplit  11550  sumsnf  11552  sumsplitdc  11575  fsummulc2  11591  ef0lem  11803  ef4p  11837  tanvalap  11851  modprm0  12392  pcmpt2  12482  4sqlem10  12525  4sqlem11  12539  fsumcncntop  14724  limcimolemlt  14818  dvmptcmulcn  14868  dveflem  14872  dvef  14873  plyf  14883  elplyr  14886  elplyd  14887  ply1term  14889  plyaddlem  14895  plymullem  14896  ptolemy  14959  lgsdir2  15149  lgsdir  15151  apdiff  15538  iswomni0  15541