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

Theorem 0cnd 7771
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 7770 . 2 0 ∈ ℂ
21a1i 9 1 (𝜑 → 0 ∈ ℂ)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1480  cc 7630  0cc0 7632
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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2121  ax-1cn 7725  ax-icn 7727  ax-addcl 7728  ax-mulcl 7730  ax-i2m1 7737
This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135
This theorem is referenced by:  mulap0r  8389  mulap0  8427  mul0eqap  8443  diveqap0  8454  eqneg  8504  div2subap  8608  prodgt0  8622  un0addcl  9022  un0mulcl  9023  modsumfzodifsn  10181  ser0  10299  ser0f  10300  abs00ap  10846  abs00  10848  abssubne0  10875  mul0inf  11024  clim0c  11067  sumrbdclem  11158  summodclem2a  11162  zsumdc  11165  fsum3  11168  isumz  11170  isumss  11172  fisumss  11173  fsum3cvg2  11175  fsum3ser  11178  fsumcl2lem  11179  fsumcl  11181  fsumadd  11187  fsumsplit  11188  sumsnf  11190  sumsplitdc  11213  fsummulc2  11229  ef0lem  11378  ef4p  11412  tanvalap  11426  fsumcncntop  12739  limcimolemlt  12816  dvmptcmulcn  12866  dveflem  12870  dvef  12871  ptolemy  12927  apdiff  13302
  Copyright terms: Public domain W3C validator