Axiom ax-icn 8280

Description: i is a complex number. Axiom for real and complex numbers, justified by Theorem axicn 8236. (Contributed by NM, 1-Mar-1995.)

Assertion

Ref	Expression
ax-icn	⊢ i ∈ ℂ

Detailed syntax breakdown of Axiom ax-icn

Step	Hyp	Ref	Expression
1		ci 8187	. 2 class i
2		cc 8183	. 2 class ℂ
3	1, 2	wcel 2209	1 wff i ∈ ℂ

This axiom is used by:  0cn  8324  mulrid  8329  cnegexlem2  8509  cnegex  8511  0cnALT  8523  negicn  8534  ine0  8728  ixi  8919  rimul  8921  rereim  8922  apreap  8923  cru  8938  apreim  8939  mulreim  8940  apadd1  8944  apneg  8947  aprcl  8982  aptap  8986  recextlem1  8987  recexaplem2  8988  recexap  8989  crap0  9296  cju  9299  it0e0  9537  2mulicn  9538  iap0  9539  2muliap0  9540  cnref1o  10067  irec  11096  i2  11097  i3  11098  i4  11099  iexpcyc  11101  imval  11636  imre  11637  reim  11638  crre  11643  crim  11644  remim  11646  mulreap  11650  cjreb  11652  recj  11653  reneg  11654  readd  11655  remullem  11657  imcj  11661  imneg  11662  imadd  11663  cjadd  11670  cjneg  11676  imval2  11680  sq01  11681  rei  11686  imi  11687  cji  11689  cjreim  11690  cjreim2  11691  cjap  11693  cnrecnv  11697  rennim  11789  absi  11846  absreimsq  11854  absreim  11855  absimle  11872  climcvg1nlem  12139  sinval  12493  cosval  12494  sinf  12495  cosf  12496  tanval2ap  12504  tanval3ap  12505  resinval  12506  recosval  12507  efi4p  12508  resin4p  12509  recos4p  12510  resincl  12511  recoscl  12512  sinneg  12517  cosneg  12518  efival  12523  efmival  12524  efeul  12525  sinadd  12527  cosadd  12528  ef01bndlem  12547  sin01bnd  12548  cos01bnd  12549  absef  12561  absefib  12562  efieq1re  12563  demoivre  12564  demoivreALT  12565  igz  13181  4sqlem17  13214  cnrehmeocntop  15853  sincn  16012  coscn  16013  efhalfpi  16043  ef2kpi  16050  efper  16051  sinperlem  16052  efimpi  16063  sineq0re  16093  root1idef  16101  efnthr  16193  2sqlem2  16456  qdencn  17295