Axiom ax-icn 8275

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

This axiom is used by:  0cn  8319  mulrid  8324  cnegexlem2  8504  cnegex  8506  0cnALT  8518  negicn  8529  ine0  8723  ixi  8914  rimul  8916  rereim  8917  apreap  8918  cru  8933  apreim  8934  mulreim  8935  apadd1  8939  apneg  8942  aprcl  8977  aptap  8981  recextlem1  8982  recexaplem2  8983  recexap  8984  crap0  9291  cju  9294  it0e0  9531  2mulicn  9532  iap0  9533  2muliap0  9534  cnref1o  10062  irec  11091  i2  11092  i3  11093  i4  11094  iexpcyc  11096  imval  11631  imre  11632  reim  11633  crre  11638  crim  11639  remim  11641  mulreap  11645  cjreb  11647  recj  11648  reneg  11649  readd  11650  remullem  11652  imcj  11656  imneg  11657  imadd  11658  cjadd  11665  cjneg  11671  imval2  11675  sq01  11676  rei  11681  imi  11682  cji  11684  cjreim  11685  cjreim2  11686  cjap  11688  cnrecnv  11692  rennim  11784  absi  11841  absreimsq  11849  absreim  11850  absimle  11867  climcvg1nlem  12134  sinval  12488  cosval  12489  sinf  12490  cosf  12491  tanval2ap  12499  tanval3ap  12500  resinval  12501  recosval  12502  efi4p  12503  resin4p  12504  recos4p  12505  resincl  12506  recoscl  12507  sinneg  12512  cosneg  12513  efival  12518  efmival  12519  efeul  12520  sinadd  12522  cosadd  12523  ef01bndlem  12542  sin01bnd  12543  cos01bnd  12544  absef  12556  absefib  12557  efieq1re  12558  demoivre  12559  demoivreALT  12560  igz  13176  4sqlem17  13209  cnrehmeocntop  15802  sincn  15961  coscn  15962  efhalfpi  15992  ef2kpi  15999  efper  16000  sinperlem  16001  efimpi  16012  2sqlem2  16400  qdencn  17238