Axiom ax-icn 8127

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

This axiom is referenced by:  0cn  8171  mulrid  8176  cnegexlem2  8355  cnegex  8357  0cnALT  8369  negicn  8380  ine0  8573  ixi  8763  rimul  8765  rereim  8766  apreap  8767  cru  8782  apreim  8783  mulreim  8784  apadd1  8788  apneg  8791  aprcl  8826  aptap  8830  recextlem1  8831  recexaplem2  8832  recexap  8833  crap0  9138  cju  9141  it0e0  9365  2mulicn  9366  iap0  9367  2muliap0  9368  cnref1o  9885  irec  10901  i2  10902  i3  10903  i4  10904  iexpcyc  10906  imval  11411  imre  11412  reim  11413  crre  11418  crim  11419  remim  11421  mulreap  11425  cjreb  11427  recj  11428  reneg  11429  readd  11430  remullem  11432  imcj  11436  imneg  11437  imadd  11438  cjadd  11445  cjneg  11451  imval2  11455  rei  11460  imi  11461  cji  11463  cjreim  11464  cjreim2  11465  cjap  11467  cnrecnv  11471  rennim  11563  absi  11620  absreimsq  11628  absreim  11629  absimle  11645  climcvg1nlem  11910  sinval  12264  cosval  12265  sinf  12266  cosf  12267  tanval2ap  12275  tanval3ap  12276  resinval  12277  recosval  12278  efi4p  12279  resin4p  12280  recos4p  12281  resincl  12282  recoscl  12283  sinneg  12288  cosneg  12289  efival  12294  efmival  12295  efeul  12296  sinadd  12298  cosadd  12299  ef01bndlem  12318  sin01bnd  12319  cos01bnd  12320  absef  12332  absefib  12333  efieq1re  12334  demoivre  12335  demoivreALT  12336  igz  12948  4sqlem17  12981  cnrehmeocntop  15336  sincn  15495  coscn  15496  efhalfpi  15525  ef2kpi  15532  efper  15533  sinperlem  15534  efimpi  15545  2sqlem2  15846  qdencn  16634