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

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

Detailed syntax breakdown of Axiom ax-icn
StepHypRef Expression
1 ci 7590 . 2 class i
2 cc 7586 . 2 class
31, 2wcel 1465 1 wff i ∈ ℂ
Colors of variables: wff set class
This axiom is referenced by:  0cn  7726  mulid1  7731  cnegexlem2  7906  cnegex  7908  0cnALT  7920  negicn  7931  ine0  8124  ixi  8312  rimul  8314  rereim  8315  apreap  8316  cru  8331  apreim  8332  mulreim  8333  apadd1  8337  apneg  8340  aprcl  8375  recextlem1  8379  recexaplem2  8380  recexap  8381  crap0  8680  cju  8683  it0e0  8899  2mulicn  8900  iap0  8901  2muliap0  8902  cnref1o  9396  irec  10347  i2  10348  i3  10349  i4  10350  iexpcyc  10352  imval  10577  imre  10578  reim  10579  crre  10584  crim  10585  remim  10587  mulreap  10591  cjreb  10593  recj  10594  reneg  10595  readd  10596  remullem  10598  imcj  10602  imneg  10603  imadd  10604  cjadd  10611  cjneg  10617  imval2  10621  rei  10626  imi  10627  cji  10629  cjreim  10630  cjreim2  10631  cjap  10633  cnrecnv  10637  rennim  10729  absi  10786  absreimsq  10794  absreim  10795  absimle  10811  climcvg1nlem  11073  sinval  11323  cosval  11324  sinf  11325  cosf  11326  tanval2ap  11334  tanval3ap  11335  resinval  11336  recosval  11337  efi4p  11338  resin4p  11339  recos4p  11340  resincl  11341  recoscl  11342  sinneg  11347  cosneg  11348  efival  11353  efmival  11354  efeul  11355  sinadd  11357  cosadd  11358  ef01bndlem  11377  sin01bnd  11378  cos01bnd  11379  absef  11390  absefib  11391  efieq1re  11392  demoivre  11393  demoivreALT  11394  cnrehmeocntop  12673  sincn  12769  coscn  12770  efhalfpi  12791  ef2kpi  12798  efper  12799  sinperlem  12800  efimpi  12811  qdencn  13118
  Copyright terms: Public domain W3C validator