Theorem 0cnd 8038

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

Syntax hints:   → wi 4   ∈ wcel 2167  ℂcc 7896  0cc0 7898

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178  ax-1cn 7991  ax-icn 7993  ax-addcl 7994  ax-mulcl 7996  ax-i2m1 8003

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

This theorem is referenced by:  mulap0r  8661  mulap0  8700  mul0eqap  8716  diveqap0  8728  eqneg  8778  div2subap  8883  prodgt0  8898  un0addcl  9301  un0mulcl  9302  modsumfzodifsn  10507  ser0  10644  ser0f  10645  abs00ap  11246  abs00  11248  abssubne0  11275  mul0inf  11425  clim0c  11470  sumrbdclem  11561  summodclem2a  11565  zsumdc  11568  fsum3  11571  isumz  11573  isumss  11575  fisumss  11576  fsum3cvg2  11578  fsum3ser  11581  fsumcl2lem  11582  fsumcl  11584  fsumadd  11590  fsumsplit  11591  sumsnf  11593  sumsplitdc  11616  fsummulc2  11632  ef0lem  11844  ef4p  11878  tanvalap  11892  modprm0  12450  pcmpt2  12540  4sqlem10  12583  4sqlem11  12597  fsumcncntop  14911  limcimolemlt  15008  dvmptcmulcn  15065  dvmptfsum  15069  dveflem  15070  dvef  15071  plyf  15081  elplyr  15084  elplyd  15085  ply1term  15087  plyaddlem  15093  plymullem  15094  plycolemc  15102  plycn  15106  dvply1  15109  ptolemy  15168  lgsdir2  15382  lgsdir  15384  apdiff  15805  iswomni0  15808