ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  0cnd GIF version

Theorem 0cnd 7928
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
StepHypRef Expression
1 0cn 7927 . 2 0 ∈ ℂ
21a1i 9 1 (𝜑 → 0 ∈ ℂ)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 2148  cc 7787  0cc0 7789
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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159  ax-1cn 7882  ax-icn 7884  ax-addcl 7885  ax-mulcl 7887  ax-i2m1 7894
This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173
This theorem is referenced by:  mulap0r  8549  mulap0  8587  mul0eqap  8603  diveqap0  8615  eqneg  8665  div2subap  8770  prodgt0  8785  un0addcl  9185  un0mulcl  9186  modsumfzodifsn  10369  ser0  10487  ser0f  10488  abs00ap  11042  abs00  11044  abssubne0  11071  mul0inf  11220  clim0c  11265  sumrbdclem  11356  summodclem2a  11360  zsumdc  11363  fsum3  11366  isumz  11368  isumss  11370  fisumss  11371  fsum3cvg2  11373  fsum3ser  11376  fsumcl2lem  11377  fsumcl  11379  fsumadd  11385  fsumsplit  11386  sumsnf  11388  sumsplitdc  11411  fsummulc2  11427  ef0lem  11639  ef4p  11673  tanvalap  11687  modprm0  12224  pcmpt2  12312  4sqlem10  12355  fsumcncntop  13689  limcimolemlt  13766  dvmptcmulcn  13816  dveflem  13820  dvef  13821  ptolemy  13878  lgsdir2  14067  lgsdir  14069  apdiff  14419  iswomni0  14422
  Copyright terms: Public domain W3C validator