Axiom ax-icn 8055

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

This axiom is referenced by:  0cn  8099  mulrid  8104  cnegexlem2  8283  cnegex  8285  0cnALT  8297  negicn  8308  ine0  8501  ixi  8691  rimul  8693  rereim  8694  apreap  8695  cru  8710  apreim  8711  mulreim  8712  apadd1  8716  apneg  8719  aprcl  8754  aptap  8758  recextlem1  8759  recexaplem2  8760  recexap  8761  crap0  9066  cju  9069  it0e0  9293  2mulicn  9294  iap0  9295  2muliap0  9296  cnref1o  9807  irec  10821  i2  10822  i3  10823  i4  10824  iexpcyc  10826  imval  11276  imre  11277  reim  11278  crre  11283  crim  11284  remim  11286  mulreap  11290  cjreb  11292  recj  11293  reneg  11294  readd  11295  remullem  11297  imcj  11301  imneg  11302  imadd  11303  cjadd  11310  cjneg  11316  imval2  11320  rei  11325  imi  11326  cji  11328  cjreim  11329  cjreim2  11330  cjap  11332  cnrecnv  11336  rennim  11428  absi  11485  absreimsq  11493  absreim  11494  absimle  11510  climcvg1nlem  11775  sinval  12128  cosval  12129  sinf  12130  cosf  12131  tanval2ap  12139  tanval3ap  12140  resinval  12141  recosval  12142  efi4p  12143  resin4p  12144  recos4p  12145  resincl  12146  recoscl  12147  sinneg  12152  cosneg  12153  efival  12158  efmival  12159  efeul  12160  sinadd  12162  cosadd  12163  ef01bndlem  12182  sin01bnd  12183  cos01bnd  12184  absef  12196  absefib  12197  efieq1re  12198  demoivre  12199  demoivreALT  12200  igz  12812  4sqlem17  12845  cnrehmeocntop  15197  sincn  15356  coscn  15357  efhalfpi  15386  ef2kpi  15393  efper  15394  sinperlem  15395  efimpi  15406  2sqlem2  15707  qdencn  16168