Axiom ax-icn 7974

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

This axiom is referenced by:  0cn  8018  mulrid  8023  cnegexlem2  8202  cnegex  8204  0cnALT  8216  negicn  8227  ine0  8420  ixi  8610  rimul  8612  rereim  8613  apreap  8614  cru  8629  apreim  8630  mulreim  8631  apadd1  8635  apneg  8638  aprcl  8673  aptap  8677  recextlem1  8678  recexaplem2  8679  recexap  8680  crap0  8985  cju  8988  it0e0  9212  2mulicn  9213  iap0  9214  2muliap0  9215  cnref1o  9725  irec  10731  i2  10732  i3  10733  i4  10734  iexpcyc  10736  imval  11015  imre  11016  reim  11017  crre  11022  crim  11023  remim  11025  mulreap  11029  cjreb  11031  recj  11032  reneg  11033  readd  11034  remullem  11036  imcj  11040  imneg  11041  imadd  11042  cjadd  11049  cjneg  11055  imval2  11059  rei  11064  imi  11065  cji  11067  cjreim  11068  cjreim2  11069  cjap  11071  cnrecnv  11075  rennim  11167  absi  11224  absreimsq  11232  absreim  11233  absimle  11249  climcvg1nlem  11514  sinval  11867  cosval  11868  sinf  11869  cosf  11870  tanval2ap  11878  tanval3ap  11879  resinval  11880  recosval  11881  efi4p  11882  resin4p  11883  recos4p  11884  resincl  11885  recoscl  11886  sinneg  11891  cosneg  11892  efival  11897  efmival  11898  efeul  11899  sinadd  11901  cosadd  11902  ef01bndlem  11921  sin01bnd  11922  cos01bnd  11923  absef  11935  absefib  11936  efieq1re  11937  demoivre  11938  demoivreALT  11939  igz  12543  4sqlem17  12576  cnrehmeocntop  14846  sincn  15005  coscn  15006  efhalfpi  15035  ef2kpi  15042  efper  15043  sinperlem  15044  efimpi  15055  2sqlem2  15356  qdencn  15671