Theorem 0cnd 8135

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℂcc 7993  0cc0 7995

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211  ax-1cn 8088  ax-icn 8090  ax-addcl 8091  ax-mulcl 8093  ax-i2m1 8100

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  mulap0r  8758  mulap0  8797  mul0eqap  8813  diveqap0  8825  eqneg  8875  div2subap  8980  prodgt0  8995  un0addcl  9398  un0mulcl  9399  modsumfzodifsn  10613  ser0  10750  ser0f  10751  abs00ap  11568  abs00  11570  abssubne0  11597  mul0inf  11747  clim0c  11792  sumrbdclem  11883  summodclem2a  11887  zsumdc  11890  fsum3  11893  isumz  11895  isumss  11897  fisumss  11898  fsum3cvg2  11900  fsum3ser  11903  fsumcl2lem  11904  fsumcl  11906  fsumadd  11912  fsumsplit  11913  sumsnf  11915  sumsplitdc  11938  fsummulc2  11954  ef0lem  12166  ef4p  12200  tanvalap  12214  modprm0  12772  pcmpt2  12862  4sqlem10  12905  4sqlem11  12919  fsumcncntop  15235  limcimolemlt  15332  dvmptcmulcn  15389  dvmptfsum  15393  dveflem  15394  dvef  15395  plyf  15405  elplyr  15408  elplyd  15409  ply1term  15411  plyaddlem  15417  plymullem  15418  plycolemc  15426  plycn  15430  dvply1  15433  ptolemy  15492  lgsdir2  15706  lgsdir  15708  apdiff  16375  iswomni0  16378