Axiom ax-icn 7901

Description: i is a complex number. Axiom for real and complex numbers, justified by Theorem axicn 7857. (Contributed by NM, 1-Mar-1995.)

Assertion

Ref	Expression
ax-icn	⊢ i ∈ ℂ

Detailed syntax breakdown of Axiom ax-icn

Step	Hyp	Ref	Expression
1		ci 7808	. 2 class i
2		cc 7804	. 2 class ℂ
3	1, 2	wcel 2148	1 wff i ∈ ℂ

This axiom is referenced by:  0cn  7944  mulrid  7949  cnegexlem2  8127  cnegex  8129  0cnALT  8141  negicn  8152  ine0  8345  ixi  8534  rimul  8536  rereim  8537  apreap  8538  cru  8553  apreim  8554  mulreim  8555  apadd1  8559  apneg  8562  aprcl  8597  aptap  8601  recextlem1  8602  recexaplem2  8603  recexap  8604  crap0  8909  cju  8912  it0e0  9134  2mulicn  9135  iap0  9136  2muliap0  9137  cnref1o  9644  irec  10612  i2  10613  i3  10614  i4  10615  iexpcyc  10617  imval  10850  imre  10851  reim  10852  crre  10857  crim  10858  remim  10860  mulreap  10864  cjreb  10866  recj  10867  reneg  10868  readd  10869  remullem  10871  imcj  10875  imneg  10876  imadd  10877  cjadd  10884  cjneg  10890  imval2  10894  rei  10899  imi  10900  cji  10902  cjreim  10903  cjreim2  10904  cjap  10906  cnrecnv  10910  rennim  11002  absi  11059  absreimsq  11067  absreim  11068  absimle  11084  climcvg1nlem  11348  sinval  11701  cosval  11702  sinf  11703  cosf  11704  tanval2ap  11712  tanval3ap  11713  resinval  11714  recosval  11715  efi4p  11716  resin4p  11717  recos4p  11718  resincl  11719  recoscl  11720  sinneg  11725  cosneg  11726  efival  11731  efmival  11732  efeul  11733  sinadd  11735  cosadd  11736  ef01bndlem  11755  sin01bnd  11756  cos01bnd  11757  absef  11768  absefib  11769  efieq1re  11770  demoivre  11771  demoivreALT  11772  igz  12362  cnrehmeocntop  13875  sincn  13972  coscn  13973  efhalfpi  14002  ef2kpi  14009  efper  14010  sinperlem  14011  efimpi  14022  2sqlem2  14233  qdencn  14546