Axiom ax-icn 7848

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

This axiom is referenced by:  0cn  7891  mulid1  7896  cnegexlem2  8074  cnegex  8076  0cnALT  8088  negicn  8099  ine0  8292  ixi  8481  rimul  8483  rereim  8484  apreap  8485  cru  8500  apreim  8501  mulreim  8502  apadd1  8506  apneg  8509  aprcl  8544  recextlem1  8548  recexaplem2  8549  recexap  8550  crap0  8853  cju  8856  it0e0  9078  2mulicn  9079  iap0  9080  2muliap0  9081  cnref1o  9588  irec  10554  i2  10555  i3  10556  i4  10557  iexpcyc  10559  imval  10792  imre  10793  reim  10794  crre  10799  crim  10800  remim  10802  mulreap  10806  cjreb  10808  recj  10809  reneg  10810  readd  10811  remullem  10813  imcj  10817  imneg  10818  imadd  10819  cjadd  10826  cjneg  10832  imval2  10836  rei  10841  imi  10842  cji  10844  cjreim  10845  cjreim2  10846  cjap  10848  cnrecnv  10852  rennim  10944  absi  11001  absreimsq  11009  absreim  11010  absimle  11026  climcvg1nlem  11290  sinval  11643  cosval  11644  sinf  11645  cosf  11646  tanval2ap  11654  tanval3ap  11655  resinval  11656  recosval  11657  efi4p  11658  resin4p  11659  recos4p  11660  resincl  11661  recoscl  11662  sinneg  11667  cosneg  11668  efival  11673  efmival  11674  efeul  11675  sinadd  11677  cosadd  11678  ef01bndlem  11697  sin01bnd  11698  cos01bnd  11699  absef  11710  absefib  11711  efieq1re  11712  demoivre  11713  demoivreALT  11714  igz  12304  cnrehmeocntop  13243  sincn  13340  coscn  13341  efhalfpi  13370  ef2kpi  13377  efper  13378  sinperlem  13379  efimpi  13390  2sqlem2  13601  qdencn  13916