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

Theorem 0cnd 7727
Description: 0 is a complex number, deductive form. (Contributed by David A. Wheeler, 8-Dec-2018.)
Assertion
Ref Expression
0cnd  |-  ( ph  ->  0  e.  CC )

Proof of Theorem 0cnd
StepHypRef Expression
1 0cn 7726 . 2  |-  0  e.  CC
21a1i 9 1  |-  ( ph  ->  0  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1465   CCcc 7586   0cc0 7588
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1408  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-4 1472  ax-17 1491  ax-ial 1499  ax-ext 2099  ax-1cn 7681  ax-icn 7683  ax-addcl 7684  ax-mulcl 7686  ax-i2m1 7693
This theorem depends on definitions:  df-bi 116  df-cleq 2110  df-clel 2113
This theorem is referenced by:  mulap0r  8344  mulap0  8382  mul0eqap  8398  diveqap0  8409  eqneg  8459  div2subap  8563  prodgt0  8574  un0addcl  8968  un0mulcl  8969  modsumfzodifsn  10124  ser0  10242  ser0f  10243  abs00ap  10789  abs00  10791  abssubne0  10818  mul0inf  10967  clim0c  11010  sumrbdclem  11100  summodclem2a  11105  zsumdc  11108  fsum3  11111  isumz  11113  isumss  11115  fisumss  11116  fsum3cvg2  11118  fsum3ser  11121  fsumcl2lem  11122  fsumcl  11124  fsumadd  11130  fsumsplit  11131  sumsnf  11133  sumsplitdc  11156  fsummulc2  11172  ef0lem  11280  ef4p  11314  tanvalap  11329  fsumcncntop  12636  limcimolemlt  12713  dvmptcmulcn  12763  dveflem  12766  dvef  12767  ptolemy  12816
  Copyright terms: Public domain W3C validator