Theorem 0cnd 8014

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

Syntax hints:   → wi 4   ∈ wcel 2164  ℂcc 7872  0cc0 7874

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2175  ax-1cn 7967  ax-icn 7969  ax-addcl 7970  ax-mulcl 7972  ax-i2m1 7979

This theorem depends on definitions:  df-bi 117  df-cleq 2186  df-clel 2189

This theorem is referenced by:  mulap0r  8636  mulap0  8675  mul0eqap  8691  diveqap0  8703  eqneg  8753  div2subap  8858  prodgt0  8873  un0addcl  9276  un0mulcl  9277  modsumfzodifsn  10470  ser0  10607  ser0f  10608  abs00ap  11209  abs00  11211  abssubne0  11238  mul0inf  11387  clim0c  11432  sumrbdclem  11523  summodclem2a  11527  zsumdc  11530  fsum3  11533  isumz  11535  isumss  11537  fisumss  11538  fsum3cvg2  11540  fsum3ser  11543  fsumcl2lem  11544  fsumcl  11546  fsumadd  11552  fsumsplit  11553  sumsnf  11555  sumsplitdc  11578  fsummulc2  11594  ef0lem  11806  ef4p  11840  tanvalap  11854  modprm0  12395  pcmpt2  12485  4sqlem10  12528  4sqlem11  12542  fsumcncntop  14746  limcimolemlt  14843  dvmptcmulcn  14900  dvmptfsum  14904  dveflem  14905  dvef  14906  plyf  14916  elplyr  14919  elplyd  14920  ply1term  14922  plyaddlem  14928  plymullem  14929  plycolemc  14936  plycn  14940  dvply1  14943  ptolemy  15000  lgsdir2  15190  lgsdir  15192  apdiff  15608  iswomni0  15611