Axiom ax-icn 7905

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

This axiom is referenced by:  0cn  7948  mulrid  7953  cnegexlem2  8131  cnegex  8133  0cnALT  8145  negicn  8156  ine0  8349  ixi  8538  rimul  8540  rereim  8541  apreap  8542  cru  8557  apreim  8558  mulreim  8559  apadd1  8563  apneg  8566  aprcl  8601  aptap  8605  recextlem1  8606  recexaplem2  8607  recexap  8608  crap0  8913  cju  8916  it0e0  9138  2mulicn  9139  iap0  9140  2muliap0  9141  cnref1o  9648  irec  10616  i2  10617  i3  10618  i4  10619  iexpcyc  10621  imval  10854  imre  10855  reim  10856  crre  10861  crim  10862  remim  10864  mulreap  10868  cjreb  10870  recj  10871  reneg  10872  readd  10873  remullem  10875  imcj  10879  imneg  10880  imadd  10881  cjadd  10888  cjneg  10894  imval2  10898  rei  10903  imi  10904  cji  10906  cjreim  10907  cjreim2  10908  cjap  10910  cnrecnv  10914  rennim  11006  absi  11063  absreimsq  11071  absreim  11072  absimle  11088  climcvg1nlem  11352  sinval  11705  cosval  11706  sinf  11707  cosf  11708  tanval2ap  11716  tanval3ap  11717  resinval  11718  recosval  11719  efi4p  11720  resin4p  11721  recos4p  11722  resincl  11723  recoscl  11724  sinneg  11729  cosneg  11730  efival  11735  efmival  11736  efeul  11737  sinadd  11739  cosadd  11740  ef01bndlem  11759  sin01bnd  11760  cos01bnd  11761  absef  11772  absefib  11773  efieq1re  11774  demoivre  11775  demoivreALT  11776  igz  12366  cnrehmeocntop  13986  sincn  14083  coscn  14084  efhalfpi  14113  ef2kpi  14120  efper  14121  sinperlem  14122  efimpi  14133  2sqlem2  14344  qdencn  14657