Theorem 0cnd 8150

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℂcc 8008  0cc0 8010

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211  ax-1cn 8103  ax-icn 8105  ax-addcl 8106  ax-mulcl 8108  ax-i2m1 8115

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  mulap0r  8773  mulap0  8812  mul0eqap  8828  diveqap0  8840  eqneg  8890  div2subap  8995  prodgt0  9010  un0addcl  9413  un0mulcl  9414  modsumfzodifsn  10630  ser0  10767  ser0f  10768  abs00ap  11588  abs00  11590  abssubne0  11617  mul0inf  11767  clim0c  11812  sumrbdclem  11903  summodclem2a  11907  zsumdc  11910  fsum3  11913  isumz  11915  isumss  11917  fisumss  11918  fsum3cvg2  11920  fsum3ser  11923  fsumcl2lem  11924  fsumcl  11926  fsumadd  11932  fsumsplit  11933  sumsnf  11935  sumsplitdc  11958  fsummulc2  11974  ef0lem  12186  ef4p  12220  tanvalap  12234  modprm0  12792  pcmpt2  12882  4sqlem10  12925  4sqlem11  12939  fsumcncntop  15256  limcimolemlt  15353  dvmptcmulcn  15410  dvmptfsum  15414  dveflem  15415  dvef  15416  plyf  15426  elplyr  15429  elplyd  15430  ply1term  15432  plyaddlem  15438  plymullem  15439  plycolemc  15447  plycn  15451  dvply1  15454  ptolemy  15513  lgsdir2  15727  lgsdir  15729  apdiff  16476  iswomni0  16479