Theorem 0cnd 8320

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  ℂcc 8178  0cc0 8180

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220  ax-1cn 8273  ax-icn 8275  ax-addcl 8276  ax-mulcl 8278  ax-i2m1 8285

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  addeq0  8705  mulap0r  8946  mulap0  8985  msq0  9000  mul0eqap  9003  diveqap0  9015  eqneg  9065  div2subap  9170  prodgt0  9185  un0addcl  9601  un0mulcl  9602  modsumfzodifsn  10848  ser0  10985  ser0f  10986  resq01  11110  sq01  11676  abs00ap  11844  abs00  11846  abssubne0  11874  mul0inf  12026  clim0c  12071  sumrbdclem  12163  summodclem2a  12167  zsumdc  12170  fsum3  12173  isumz  12175  isumss  12177  fisumss  12178  fsum3cvg2  12180  fsum3ser  12183  fsumcl2lem  12184  fsumcl  12186  fsumadd  12192  fsumsplit  12193  sumsnf  12195  sumsplitdc  12218  fsummulc2  12234  ef0lem  12446  ef4p  12480  tanvalap  12494  modprm0  13056  pcmpt2  13146  4sqlem10  13189  4sqlem11  13203  ballotfilemic  13302  ballotfilem1c  13303  fsumcncntop  15759  limcimolemlt  15856  dvmptcmulcn  15913  dvmptfsum  15917  dveflem  15918  dvef  15919  plyf  15929  elplyr  15932  elplyd  15933  ply1term  15935  plyaddlem  15941  plymullem  15942  plycolemc  15950  plycn  15954  dvply1  15957  ptolemy  16017  prmorcht  16243  lgsdir2  16318  lgsdir  16320  apdiff  17264  iswomni0  17268