Axiom ax-icn 8105

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

This axiom is referenced by:  0cn  8149  mulrid  8154  cnegexlem2  8333  cnegex  8335  0cnALT  8347  negicn  8358  ine0  8551  ixi  8741  rimul  8743  rereim  8744  apreap  8745  cru  8760  apreim  8761  mulreim  8762  apadd1  8766  apneg  8769  aprcl  8804  aptap  8808  recextlem1  8809  recexaplem2  8810  recexap  8811  crap0  9116  cju  9119  it0e0  9343  2mulicn  9344  iap0  9345  2muliap0  9346  cnref1o  9858  irec  10873  i2  10874  i3  10875  i4  10876  iexpcyc  10878  imval  11377  imre  11378  reim  11379  crre  11384  crim  11385  remim  11387  mulreap  11391  cjreb  11393  recj  11394  reneg  11395  readd  11396  remullem  11398  imcj  11402  imneg  11403  imadd  11404  cjadd  11411  cjneg  11417  imval2  11421  rei  11426  imi  11427  cji  11429  cjreim  11430  cjreim2  11431  cjap  11433  cnrecnv  11437  rennim  11529  absi  11586  absreimsq  11594  absreim  11595  absimle  11611  climcvg1nlem  11876  sinval  12229  cosval  12230  sinf  12231  cosf  12232  tanval2ap  12240  tanval3ap  12241  resinval  12242  recosval  12243  efi4p  12244  resin4p  12245  recos4p  12246  resincl  12247  recoscl  12248  sinneg  12253  cosneg  12254  efival  12259  efmival  12260  efeul  12261  sinadd  12263  cosadd  12264  ef01bndlem  12283  sin01bnd  12284  cos01bnd  12285  absef  12297  absefib  12298  efieq1re  12299  demoivre  12300  demoivreALT  12301  igz  12913  4sqlem17  12946  cnrehmeocntop  15300  sincn  15459  coscn  15460  efhalfpi  15489  ef2kpi  15496  efper  15497  sinperlem  15498  efimpi  15509  2sqlem2  15810  qdencn  16483