Theorem 0cnd 8267

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

Syntax hints:   → wi 4   ∈ wcel 2203  ℂcc 8125  0cc0 8127

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2214  ax-1cn 8220  ax-icn 8222  ax-addcl 8223  ax-mulcl 8225  ax-i2m1 8232

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

This theorem is referenced by:  mulap0r  8889  mulap0  8928  mul0eqap  8944  diveqap0  8956  eqneg  9006  div2subap  9111  prodgt0  9126  un0addcl  9529  un0mulcl  9530  modsumfzodifsn  10758  ser0  10895  ser0f  10896  abs00ap  11747  abs00  11749  abssubne0  11776  mul0inf  11926  clim0c  11971  sumrbdclem  12063  summodclem2a  12067  zsumdc  12070  fsum3  12073  isumz  12075  isumss  12077  fisumss  12078  fsum3cvg2  12080  fsum3ser  12083  fsumcl2lem  12084  fsumcl  12086  fsumadd  12092  fsumsplit  12093  sumsnf  12095  sumsplitdc  12118  fsummulc2  12134  ef0lem  12346  ef4p  12380  tanvalap  12394  modprm0  12952  pcmpt2  13042  4sqlem10  13085  4sqlem11  13099  fsumcncntop  15432  limcimolemlt  15529  dvmptcmulcn  15586  dvmptfsum  15590  dveflem  15591  dvef  15592  plyf  15602  elplyr  15605  elplyd  15606  ply1term  15608  plyaddlem  15614  plymullem  15615  plycolemc  15623  plycn  15627  dvply1  15630  ptolemy  15689  lgsdir2  15906  lgsdir  15908  apdiff  16832  iswomni0  16836  trimul0or  16845