Axiom ax-icn 8187

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

This axiom is referenced by:  0cn  8231  mulrid  8236  cnegexlem2  8414  cnegex  8416  0cnALT  8428  negicn  8439  ine0  8632  ixi  8822  rimul  8824  rereim  8825  apreap  8826  cru  8841  apreim  8842  mulreim  8843  apadd1  8847  apneg  8850  aprcl  8885  aptap  8889  recextlem1  8890  recexaplem2  8891  recexap  8892  crap0  9197  cju  9200  it0e0  9424  2mulicn  9425  iap0  9426  2muliap0  9427  cnref1o  9946  irec  10964  i2  10965  i3  10966  i4  10967  iexpcyc  10969  imval  11490  imre  11491  reim  11492  crre  11497  crim  11498  remim  11500  mulreap  11504  cjreb  11506  recj  11507  reneg  11508  readd  11509  remullem  11511  imcj  11515  imneg  11516  imadd  11517  cjadd  11524  cjneg  11530  imval2  11534  rei  11539  imi  11540  cji  11542  cjreim  11543  cjreim2  11544  cjap  11546  cnrecnv  11550  rennim  11642  absi  11699  absreimsq  11707  absreim  11708  absimle  11724  climcvg1nlem  11989  sinval  12343  cosval  12344  sinf  12345  cosf  12346  tanval2ap  12354  tanval3ap  12355  resinval  12356  recosval  12357  efi4p  12358  resin4p  12359  recos4p  12360  resincl  12361  recoscl  12362  sinneg  12367  cosneg  12368  efival  12373  efmival  12374  efeul  12375  sinadd  12377  cosadd  12378  ef01bndlem  12397  sin01bnd  12398  cos01bnd  12399  absef  12411  absefib  12412  efieq1re  12413  demoivre  12414  demoivreALT  12415  igz  13027  4sqlem17  13060  cnrehmeocntop  15421  sincn  15580  coscn  15581  efhalfpi  15610  ef2kpi  15617  efper  15618  sinperlem  15619  efimpi  15630  2sqlem2  15934  qdencn  16755