Axiom ax-icn 8094

Description: _i is a complex number. Axiom for real and complex numbers, justified by Theorem axicn 8050. (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 8001	. 2 class _i
2		cc 7997	. 2 class CC
3	1, 2	wcel 2200	1 wff _i e. CC

This axiom is referenced by:  0cn  8138  mulrid  8143  cnegexlem2  8322  cnegex  8324  0cnALT  8336  negicn  8347  ine0  8540  ixi  8730  rimul  8732  rereim  8733  apreap  8734  cru  8749  apreim  8750  mulreim  8751  apadd1  8755  apneg  8758  aprcl  8793  aptap  8797  recextlem1  8798  recexaplem2  8799  recexap  8800  crap0  9105  cju  9108  it0e0  9332  2mulicn  9333  iap0  9334  2muliap0  9335  cnref1o  9846  irec  10861  i2  10862  i3  10863  i4  10864  iexpcyc  10866  imval  11361  imre  11362  reim  11363  crre  11368  crim  11369  remim  11371  mulreap  11375  cjreb  11377  recj  11378  reneg  11379  readd  11380  remullem  11382  imcj  11386  imneg  11387  imadd  11388  cjadd  11395  cjneg  11401  imval2  11405  rei  11410  imi  11411  cji  11413  cjreim  11414  cjreim2  11415  cjap  11417  cnrecnv  11421  rennim  11513  absi  11570  absreimsq  11578  absreim  11579  absimle  11595  climcvg1nlem  11860  sinval  12213  cosval  12214  sinf  12215  cosf  12216  tanval2ap  12224  tanval3ap  12225  resinval  12226  recosval  12227  efi4p  12228  resin4p  12229  recos4p  12230  resincl  12231  recoscl  12232  sinneg  12237  cosneg  12238  efival  12243  efmival  12244  efeul  12245  sinadd  12247  cosadd  12248  ef01bndlem  12267  sin01bnd  12268  cos01bnd  12269  absef  12281  absefib  12282  efieq1re  12283  demoivre  12284  demoivreALT  12285  igz  12897  4sqlem17  12930  cnrehmeocntop  15284  sincn  15443  coscn  15444  efhalfpi  15473  ef2kpi  15480  efper  15481  sinperlem  15482  efimpi  15493  2sqlem2  15794  qdencn  16395