Axiom ax-icn 8117

Description: i is a complex number. Axiom for real and complex numbers, justified by Theorem axicn 8073. (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 8024	. 2 class i
2		cc 8020	. 2 class ℂ
3	1, 2	wcel 2200	1 wff i ∈ ℂ

This axiom is referenced by:  0cn  8161  mulrid  8166  cnegexlem2  8345  cnegex  8347  0cnALT  8359  negicn  8370  ine0  8563  ixi  8753  rimul  8755  rereim  8756  apreap  8757  cru  8772  apreim  8773  mulreim  8774  apadd1  8778  apneg  8781  aprcl  8816  aptap  8820  recextlem1  8821  recexaplem2  8822  recexap  8823  crap0  9128  cju  9131  it0e0  9355  2mulicn  9356  iap0  9357  2muliap0  9358  cnref1o  9875  irec  10891  i2  10892  i3  10893  i4  10894  iexpcyc  10896  imval  11401  imre  11402  reim  11403  crre  11408  crim  11409  remim  11411  mulreap  11415  cjreb  11417  recj  11418  reneg  11419  readd  11420  remullem  11422  imcj  11426  imneg  11427  imadd  11428  cjadd  11435  cjneg  11441  imval2  11445  rei  11450  imi  11451  cji  11453  cjreim  11454  cjreim2  11455  cjap  11457  cnrecnv  11461  rennim  11553  absi  11610  absreimsq  11618  absreim  11619  absimle  11635  climcvg1nlem  11900  sinval  12253  cosval  12254  sinf  12255  cosf  12256  tanval2ap  12264  tanval3ap  12265  resinval  12266  recosval  12267  efi4p  12268  resin4p  12269  recos4p  12270  resincl  12271  recoscl  12272  sinneg  12277  cosneg  12278  efival  12283  efmival  12284  efeul  12285  sinadd  12287  cosadd  12288  ef01bndlem  12307  sin01bnd  12308  cos01bnd  12309  absef  12321  absefib  12322  efieq1re  12323  demoivre  12324  demoivreALT  12325  igz  12937  4sqlem17  12970  cnrehmeocntop  15324  sincn  15483  coscn  15484  efhalfpi  15513  ef2kpi  15520  efper  15521  sinperlem  15522  efimpi  15533  2sqlem2  15834  qdencn  16567