Theorem 0cnd 8319

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

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

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 8272  ax-icn 8274  ax-addcl 8275  ax-mulcl 8277  ax-i2m1 8284

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

This theorem is used by:  addeq0  8704  mulap0r  8945  mulap0  8984  msq0  8999  mul0eqap  9002  diveqap0  9014  eqneg  9064  div2subap  9169  prodgt0  9184  un0addcl  9600  un0mulcl  9601  modsumfzodifsn  10846  ser0  10983  ser0f  10984  resq01  11108  sq01  11674  abs00ap  11842  abs00  11844  abssubne0  11872  mul0inf  12023  clim0c  12068  sumrbdclem  12160  summodclem2a  12164  zsumdc  12167  fsum3  12170  isumz  12172  isumss  12174  fisumss  12175  fsum3cvg2  12177  fsum3ser  12180  fsumcl2lem  12181  fsumcl  12183  fsumadd  12189  fsumsplit  12190  sumsnf  12192  sumsplitdc  12215  fsummulc2  12231  ef0lem  12443  ef4p  12477  tanvalap  12491  modprm0  13053  pcmpt2  13143  4sqlem10  13186  4sqlem11  13200  ballotfilemic  13299  ballotfilem1c  13300  fsumcncntop  15717  limcimolemlt  15814  dvmptcmulcn  15871  dvmptfsum  15875  dveflem  15876  dvef  15877  plyf  15887  elplyr  15890  elplyd  15891  ply1term  15893  plyaddlem  15899  plymullem  15900  plycolemc  15908  plycn  15912  dvply1  15915  ptolemy  15975  lgsdir2  16250  lgsdir  16252  apdiff  17195  iswomni0  17199