Axiom ax-icn 8020

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

Assertion

Ref	Expression
ax-icn	|- _i e. CC

Detailed syntax breakdown of Axiom ax-icn

Step	Hyp	Ref	Expression
1		ci 7927	. 2 class _i
2		cc 7923	. 2 class CC
3	1, 2	wcel 2176	1 wff _i e. CC

This axiom is referenced by:  0cn  8064  mulrid  8069  cnegexlem2  8248  cnegex  8250  0cnALT  8262  negicn  8273  ine0  8466  ixi  8656  rimul  8658  rereim  8659  apreap  8660  cru  8675  apreim  8676  mulreim  8677  apadd1  8681  apneg  8684  aprcl  8719  aptap  8723  recextlem1  8724  recexaplem2  8725  recexap  8726  crap0  9031  cju  9034  it0e0  9258  2mulicn  9259  iap0  9260  2muliap0  9261  cnref1o  9772  irec  10784  i2  10785  i3  10786  i4  10787  iexpcyc  10789  imval  11161  imre  11162  reim  11163  crre  11168  crim  11169  remim  11171  mulreap  11175  cjreb  11177  recj  11178  reneg  11179  readd  11180  remullem  11182  imcj  11186  imneg  11187  imadd  11188  cjadd  11195  cjneg  11201  imval2  11205  rei  11210  imi  11211  cji  11213  cjreim  11214  cjreim2  11215  cjap  11217  cnrecnv  11221  rennim  11313  absi  11370  absreimsq  11378  absreim  11379  absimle  11395  climcvg1nlem  11660  sinval  12013  cosval  12014  sinf  12015  cosf  12016  tanval2ap  12024  tanval3ap  12025  resinval  12026  recosval  12027  efi4p  12028  resin4p  12029  recos4p  12030  resincl  12031  recoscl  12032  sinneg  12037  cosneg  12038  efival  12043  efmival  12044  efeul  12045  sinadd  12047  cosadd  12048  ef01bndlem  12067  sin01bnd  12068  cos01bnd  12069  absef  12081  absefib  12082  efieq1re  12083  demoivre  12084  demoivreALT  12085  igz  12697  4sqlem17  12730  cnrehmeocntop  15082  sincn  15241  coscn  15242  efhalfpi  15271  ef2kpi  15278  efper  15279  sinperlem  15280  efimpi  15291  2sqlem2  15592  qdencn  15966