Axiom ax-icn 7908

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

This axiom is referenced by:  0cn  7951  mulrid  7956  cnegexlem2  8135  cnegex  8137  0cnALT  8149  negicn  8160  ine0  8353  ixi  8542  rimul  8544  rereim  8545  apreap  8546  cru  8561  apreim  8562  mulreim  8563  apadd1  8567  apneg  8570  aprcl  8605  aptap  8609  recextlem1  8610  recexaplem2  8611  recexap  8612  crap0  8917  cju  8920  it0e0  9142  2mulicn  9143  iap0  9144  2muliap0  9145  cnref1o  9652  irec  10622  i2  10623  i3  10624  i4  10625  iexpcyc  10627  imval  10861  imre  10862  reim  10863  crre  10868  crim  10869  remim  10871  mulreap  10875  cjreb  10877  recj  10878  reneg  10879  readd  10880  remullem  10882  imcj  10886  imneg  10887  imadd  10888  cjadd  10895  cjneg  10901  imval2  10905  rei  10910  imi  10911  cji  10913  cjreim  10914  cjreim2  10915  cjap  10917  cnrecnv  10921  rennim  11013  absi  11070  absreimsq  11078  absreim  11079  absimle  11095  climcvg1nlem  11359  sinval  11712  cosval  11713  sinf  11714  cosf  11715  tanval2ap  11723  tanval3ap  11724  resinval  11725  recosval  11726  efi4p  11727  resin4p  11728  recos4p  11729  resincl  11730  recoscl  11731  sinneg  11736  cosneg  11737  efival  11742  efmival  11743  efeul  11744  sinadd  11746  cosadd  11747  ef01bndlem  11766  sin01bnd  11767  cos01bnd  11768  absef  11779  absefib  11780  efieq1re  11781  demoivre  11782  demoivreALT  11783  igz  12374  cnrehmeocntop  14132  sincn  14229  coscn  14230  efhalfpi  14259  ef2kpi  14266  efper  14267  sinperlem  14268  efimpi  14279  2sqlem2  14501  qdencn  14814