Theorem 0cnd 8325

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

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

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 8278  ax-icn 8280  ax-addcl 8281  ax-mulcl 8283  ax-i2m1 8290

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

This theorem is used by:  addeq0  8710  mulap0r  8951  mulap0  8990  msq0  9005  mul0eqap  9008  diveqap0  9020  eqneg  9070  div2subap  9175  prodgt0  9190  un0addcl  9607  un0mulcl  9608  modsumfzodifsn  10853  ser0  10990  ser0f  10991  resq01  11115  sq01  11681  abs00ap  11849  abs00  11851  abssubne0  11879  mul0inf  12031  clim0c  12076  sumrbdclem  12168  summodclem2a  12172  zsumdc  12175  fsum3  12178  isumz  12180  isumss  12182  fisumss  12183  fsum3cvg2  12185  fsum3ser  12188  fsumcl2lem  12189  fsumcl  12191  fsumadd  12197  fsumsplit  12198  sumsnf  12200  sumsplitdc  12223  fsummulc2  12239  ef0lem  12451  ef4p  12485  tanvalap  12499  modprm0  13061  pcmpt2  13151  4sqlem10  13194  4sqlem11  13208  ballotfilemic  13307  ballotfilem1c  13308  fsumcncntop  15810  limcimolemlt  15907  dvmptcmulcn  15964  dvmptfsum  15968  dveflem  15969  dvef  15970  plyf  15980  elplyr  15983  elplyd  15984  ply1term  15986  plyaddlem  15992  plymullem  15993  plycolemc  16001  plycn  16005  dvply1  16008  ptolemy  16068  prmorcht  16299  lgsdir2  16374  lgsdir  16376  apdiff  17321  iswomni0  17325