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

Axiom ax-icn 7387
Description:  _i is a complex number. Axiom for real and complex numbers, justified by theorem axicn 7347. (Contributed by NM, 1-Mar-1995.)
Assertion
Ref Expression
ax-icn  |-  _i  e.  CC

Detailed syntax breakdown of Axiom ax-icn
StepHypRef Expression
1 ci 7299 . 2  class  _i
2 cc 7295 . 2  class  CC
31, 2wcel 1436 1  wff  _i  e.  CC
Colors of variables: wff set class
This axiom is referenced by:  0cn  7427  mulid1  7432  cnegexlem2  7605  cnegex  7607  0cnALT  7619  negicn  7630  ine0  7819  ixi  8004  rimul  8006  rereim  8007  apreap  8008  cru  8023  apreim  8024  mulreim  8025  apadd1  8029  apneg  8032  recextlem1  8062  recexaplem2  8063  recexap  8064  crap0  8356  cju  8359  it0e0  8573  2mulicn  8574  iap0  8575  2muliap0  8576  cnref1o  9068  irec  9955  i2  9956  i3  9957  i4  9958  iexpcyc  9960  imval  10183  imre  10184  reim  10185  crre  10190  crim  10191  remim  10193  mulreap  10197  cjreb  10199  recj  10200  reneg  10201  readd  10202  remullem  10204  imcj  10208  imneg  10209  imadd  10210  cjadd  10217  cjneg  10223  imval2  10227  rei  10232  imi  10233  cji  10235  cjreim  10236  cjreim2  10237  cjap  10239  cnrecnv  10243  rennim  10334  absi  10391  absreimsq  10399  absreim  10400  absimle  10416  climcvg1nlem  10633  qdencn  11384
  Copyright terms: Public domain W3C validator