ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax-icn GIF version

Axiom ax-icn 6979
Description: i is a complex number. Axiom for real and complex numbers, justified by theorem axicn 6939. (Contributed by NM, 1-Mar-1995.)
Assertion
Ref Expression
ax-icn i ∈ ℂ

Detailed syntax breakdown of Axiom ax-icn
StepHypRef Expression
1 ci 6891 . 2 class i
2 cc 6887 . 2 class
31, 2wcel 1393 1 wff i ∈ ℂ
Colors of variables: wff set class
This axiom is referenced by:  0cn  7019  mulid1  7024  cnegexlem2  7187  cnegex  7189  0cnALT  7201  negicn  7212  ine0  7391  ixi  7574  rimul  7576  rereim  7577  apreap  7578  cru  7593  apreim  7594  mulreim  7595  apadd1  7599  apneg  7602  recextlem1  7632  recexaplem2  7633  recexap  7634  crap0  7910  cju  7913  it0e0  8146  2mulicn  8147  iap0  8148  2muliap0  8149  cnref1o  8582  irec  9352  i2  9353  i3  9354  i4  9355  imval  9450  imre  9451  reim  9452  crre  9457  crim  9458  remim  9460  mulreap  9464  cjreb  9466  recj  9467  reneg  9468  readd  9469  remullem  9471  imcj  9475  imneg  9476  imadd  9477  cjadd  9484  cjneg  9490  imval2  9494  rei  9499  imi  9500  cji  9502  cjreim  9503  cjreim2  9504  cjap  9506  cnrecnv  9510  rennim  9600  absi  9657  absreimsq  9665  absreim  9666  absimle  9680  climcvg1nlem  9868  qdencn  10124
  Copyright terms: Public domain W3C validator