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

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

Detailed syntax breakdown of Axiom ax-icn
StepHypRef Expression
1 ci 7615 . 2 class i
2 cc 7611 . 2 class
31, 2wcel 1480 1 wff i ∈ ℂ
Colors of variables: wff set class
This axiom is referenced by:  0cn  7751  mulid1  7756  cnegexlem2  7931  cnegex  7933  0cnALT  7945  negicn  7956  ine0  8149  ixi  8338  rimul  8340  rereim  8341  apreap  8342  cru  8357  apreim  8358  mulreim  8359  apadd1  8363  apneg  8366  aprcl  8401  recextlem1  8405  recexaplem2  8406  recexap  8407  crap0  8709  cju  8712  it0e0  8934  2mulicn  8935  iap0  8936  2muliap0  8937  cnref1o  9433  irec  10385  i2  10386  i3  10387  i4  10388  iexpcyc  10390  imval  10615  imre  10616  reim  10617  crre  10622  crim  10623  remim  10625  mulreap  10629  cjreb  10631  recj  10632  reneg  10633  readd  10634  remullem  10636  imcj  10640  imneg  10641  imadd  10642  cjadd  10649  cjneg  10655  imval2  10659  rei  10664  imi  10665  cji  10667  cjreim  10668  cjreim2  10669  cjap  10671  cnrecnv  10675  rennim  10767  absi  10824  absreimsq  10832  absreim  10833  absimle  10849  climcvg1nlem  11111  sinval  11398  cosval  11399  sinf  11400  cosf  11401  tanval2ap  11409  tanval3ap  11410  resinval  11411  recosval  11412  efi4p  11413  resin4p  11414  recos4p  11415  resincl  11416  recoscl  11417  sinneg  11422  cosneg  11423  efival  11428  efmival  11429  efeul  11430  sinadd  11432  cosadd  11433  ef01bndlem  11452  sin01bnd  11453  cos01bnd  11454  absef  11465  absefib  11466  efieq1re  11467  demoivre  11468  demoivreALT  11469  cnrehmeocntop  12751  sincn  12847  coscn  12848  efhalfpi  12869  ef2kpi  12876  efper  12877  sinperlem  12878  efimpi  12889  qdencn  13211
  Copyright terms: Public domain W3C validator