Axiom ax-icn 8238

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

This axiom is referenced by:  0cn  8282  mulrid  8287  cnegexlem2  8465  cnegex  8467  0cnALT  8479  negicn  8490  ine0  8684  ixi  8874  rimul  8876  rereim  8877  apreap  8878  cru  8893  apreim  8894  mulreim  8895  apadd1  8899  apneg  8902  aprcl  8937  aptap  8941  recextlem1  8942  recexaplem2  8943  recexap  8944  crap0  9249  cju  9252  it0e0  9476  2mulicn  9477  iap0  9478  2muliap0  9479  cnref1o  10001  irec  11025  i2  11026  i3  11027  i4  11028  iexpcyc  11030  imval  11560  imre  11561  reim  11562  crre  11567  crim  11568  remim  11570  mulreap  11574  cjreb  11576  recj  11577  reneg  11578  readd  11579  remullem  11581  imcj  11585  imneg  11586  imadd  11587  cjadd  11594  cjneg  11600  imval2  11604  rei  11609  imi  11610  cji  11612  cjreim  11613  cjreim2  11614  cjap  11616  cnrecnv  11620  rennim  11712  absi  11769  absreimsq  11777  absreim  11778  absimle  11794  climcvg1nlem  12059  sinval  12413  cosval  12414  sinf  12415  cosf  12416  tanval2ap  12424  tanval3ap  12425  resinval  12426  recosval  12427  efi4p  12428  resin4p  12429  recos4p  12430  resincl  12431  recoscl  12432  sinneg  12437  cosneg  12438  efival  12443  efmival  12444  efeul  12445  sinadd  12447  cosadd  12448  ef01bndlem  12467  sin01bnd  12468  cos01bnd  12469  absef  12481  absefib  12482  efieq1re  12483  demoivre  12484  demoivreALT  12485  igz  13097  4sqlem17  13130  cnrehmeocntop  15601  sincn  15760  coscn  15761  efhalfpi  15790  ef2kpi  15797  efper  15798  sinperlem  15799  efimpi  15810  2sqlem2  16114  qdencn  16933