Axiom ax-icn 7844

Description: i is a complex number. Axiom for real and complex numbers, justified by Theorem axicn 7800. (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 7751	. 2 class i
2		cc 7747	. 2 class ℂ
3	1, 2	wcel 2136	1 wff i ∈ ℂ

This axiom is referenced by:  0cn  7887  mulid1  7892  cnegexlem2  8070  cnegex  8072  0cnALT  8084  negicn  8095  ine0  8288  ixi  8477  rimul  8479  rereim  8480  apreap  8481  cru  8496  apreim  8497  mulreim  8498  apadd1  8502  apneg  8505  aprcl  8540  recextlem1  8544  recexaplem2  8545  recexap  8546  crap0  8849  cju  8852  it0e0  9074  2mulicn  9075  iap0  9076  2muliap0  9077  cnref1o  9584  irec  10550  i2  10551  i3  10552  i4  10553  iexpcyc  10555  imval  10788  imre  10789  reim  10790  crre  10795  crim  10796  remim  10798  mulreap  10802  cjreb  10804  recj  10805  reneg  10806  readd  10807  remullem  10809  imcj  10813  imneg  10814  imadd  10815  cjadd  10822  cjneg  10828  imval2  10832  rei  10837  imi  10838  cji  10840  cjreim  10841  cjreim2  10842  cjap  10844  cnrecnv  10848  rennim  10940  absi  10997  absreimsq  11005  absreim  11006  absimle  11022  climcvg1nlem  11286  sinval  11639  cosval  11640  sinf  11641  cosf  11642  tanval2ap  11650  tanval3ap  11651  resinval  11652  recosval  11653  efi4p  11654  resin4p  11655  recos4p  11656  resincl  11657  recoscl  11658  sinneg  11663  cosneg  11664  efival  11669  efmival  11670  efeul  11671  sinadd  11673  cosadd  11674  ef01bndlem  11693  sin01bnd  11694  cos01bnd  11695  absef  11706  absefib  11707  efieq1re  11708  demoivre  11709  demoivreALT  11710  igz  12300  cnrehmeocntop  13193  sincn  13290  coscn  13291  efhalfpi  13320  ef2kpi  13327  efper  13328  sinperlem  13329  efimpi  13340  2sqlem2  13551  qdencn  13866