Theorem 0cnd 8100

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

Syntax hints:   → wi 4   ∈ wcel 2178  ℂcc 7958  0cc0 7960

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2189  ax-1cn 8053  ax-icn 8055  ax-addcl 8056  ax-mulcl 8058  ax-i2m1 8065

This theorem depends on definitions:  df-bi 117  df-cleq 2200  df-clel 2203

This theorem is referenced by:  mulap0r  8723  mulap0  8762  mul0eqap  8778  diveqap0  8790  eqneg  8840  div2subap  8945  prodgt0  8960  un0addcl  9363  un0mulcl  9364  modsumfzodifsn  10578  ser0  10715  ser0f  10716  abs00ap  11488  abs00  11490  abssubne0  11517  mul0inf  11667  clim0c  11712  sumrbdclem  11803  summodclem2a  11807  zsumdc  11810  fsum3  11813  isumz  11815  isumss  11817  fisumss  11818  fsum3cvg2  11820  fsum3ser  11823  fsumcl2lem  11824  fsumcl  11826  fsumadd  11832  fsumsplit  11833  sumsnf  11835  sumsplitdc  11858  fsummulc2  11874  ef0lem  12086  ef4p  12120  tanvalap  12134  modprm0  12692  pcmpt2  12782  4sqlem10  12825  4sqlem11  12839  fsumcncntop  15154  limcimolemlt  15251  dvmptcmulcn  15308  dvmptfsum  15312  dveflem  15313  dvef  15314  plyf  15324  elplyr  15327  elplyd  15328  ply1term  15330  plyaddlem  15336  plymullem  15337  plycolemc  15345  plycn  15349  dvply1  15352  ptolemy  15411  lgsdir2  15625  lgsdir  15627  apdiff  16189  iswomni0  16192