Axiom ax-icn 7991

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

This axiom is referenced by:  0cn  8035  mulrid  8040  cnegexlem2  8219  cnegex  8221  0cnALT  8233  negicn  8244  ine0  8437  ixi  8627  rimul  8629  rereim  8630  apreap  8631  cru  8646  apreim  8647  mulreim  8648  apadd1  8652  apneg  8655  aprcl  8690  aptap  8694  recextlem1  8695  recexaplem2  8696  recexap  8697  crap0  9002  cju  9005  it0e0  9229  2mulicn  9230  iap0  9231  2muliap0  9232  cnref1o  9742  irec  10748  i2  10749  i3  10750  i4  10751  iexpcyc  10753  imval  11032  imre  11033  reim  11034  crre  11039  crim  11040  remim  11042  mulreap  11046  cjreb  11048  recj  11049  reneg  11050  readd  11051  remullem  11053  imcj  11057  imneg  11058  imadd  11059  cjadd  11066  cjneg  11072  imval2  11076  rei  11081  imi  11082  cji  11084  cjreim  11085  cjreim2  11086  cjap  11088  cnrecnv  11092  rennim  11184  absi  11241  absreimsq  11249  absreim  11250  absimle  11266  climcvg1nlem  11531  sinval  11884  cosval  11885  sinf  11886  cosf  11887  tanval2ap  11895  tanval3ap  11896  resinval  11897  recosval  11898  efi4p  11899  resin4p  11900  recos4p  11901  resincl  11902  recoscl  11903  sinneg  11908  cosneg  11909  efival  11914  efmival  11915  efeul  11916  sinadd  11918  cosadd  11919  ef01bndlem  11938  sin01bnd  11939  cos01bnd  11940  absef  11952  absefib  11953  efieq1re  11954  demoivre  11955  demoivreALT  11956  igz  12568  4sqlem17  12601  cnrehmeocntop  14930  sincn  15089  coscn  15090  efhalfpi  15119  ef2kpi  15126  efper  15127  sinperlem  15128  efimpi  15139  2sqlem2  15440  qdencn  15758