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  10068  irec  11097  i2  11098  i3  11099  i4  11100  iexpcyc  11102  imval  11637  imre  11638  reim  11639  crre  11644  crim  11645  remim  11647  mulreap  11651  cjreb  11653  recj  11654  reneg  11655  readd  11656  remullem  11658  imcj  11662  imneg  11663  imadd  11664  cjadd  11671  cjneg  11677  imval2  11681  sq01  11682  rei  11687  imi  11688  cji  11690  cjreim  11691  cjreim2  11692  cjap  11694  cnrecnv  11698  rennim  11790  absi  11847  absreimsq  11855  absreim  11856  absimle  11873  climcvg1nlem  12140  sinval  12494  cosval  12495  sinf  12496  cosf  12497  tanval2ap  12505  tanval3ap  12506  resinval  12507  recosval  12508  efi4p  12509  resin4p  12510  recos4p  12511  resincl  12512  recoscl  12513  sinneg  12518  cosneg  12519  efival  12524  efmival  12525  efeul  12526  sinadd  12528  cosadd  12529  ef01bndlem  12548  sin01bnd  12549  cos01bnd  12550  absef  12562  absefib  12563  efieq1re  12564  demoivre  12565  demoivreALT  12566  igz  13182  4sqlem17  13215  cnrehmeocntop  15836  sincn  15995  coscn  15996  efhalfpi  16026  ef2kpi  16033  efper  16034  sinperlem  16035  efimpi  16046  sineq0re  16076  root1idef  16084  efnthr  16176  2sqlem2  16439  qdencn  17278