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  10854  ser0  10991  ser0f  10992  resq01  11116  sq01  11682  abs00ap  11850  abs00  11852  abssubne0  11880  mul0inf  12032  clim0c  12077  sumrbdclem  12169  summodclem2a  12173  zsumdc  12176  fsum3  12179  isumz  12181  isumss  12183  fisumss  12184  fsum3cvg2  12186  fsum3ser  12189  fsumcl2lem  12190  fsumcl  12192  fsumadd  12198  fsumsplit  12199  sumsnf  12201  sumsplitdc  12224  fsummulc2  12240  ef0lem  12452  ef4p  12486  tanvalap  12500  modprm0  13062  pcmpt2  13152  4sqlem10  13195  4sqlem11  13209  ballotfilemic  13308  ballotfilem1c  13309  fsumcncntop  15793  limcimolemlt  15890  dvmptcmulcn  15947  dvmptfsum  15951  dveflem  15952  dvef  15953  plyf  15963  elplyr  15966  elplyd  15967  ply1term  15969  plyaddlem  15975  plymullem  15976  plycolemc  15984  plycn  15988  dvply1  15991  ptolemy  16051  prmorcht  16282  lgsdir2  16357  lgsdir  16359  apdiff  17304  iswomni0  17308